Tóm tắt luận án Tiến sĩ Toán học: Một số cải tiến về ràng buộc xâu trong sinh dữ liệu kiểm thử tự động cho thực thi tượng trưng

BỘ GIÁO DỤC VÀ ĐÀO TẠO

VIỆN HÀN LÂM KHOA HỌC VÀ CÔNG NGHỆ VIỆT NAM

HỌC VIỆN KHOA HỌC VÀ CÔNG NGHỆ

----------------------------

Tô Hữu Nguyên

MỘT SỐ CẢI TIẾN VỀ RÀNG BUỘC XÂU TRONG SINH DỮ LIỆU KIỂM THỬ TỰ ĐỘNG CHO THỰC THI TƢỢNG TRƢNG

Chuyên ngành : Cơ sở toán học cho tin học Mã số: 9 46 01 10

TÓM TẮT LUẬN ÁN TIẾN SĨ TOÁN HỌC

Hà Nội - 2020

Công trình được hoàn thành tại: Học viện Khoa học và Công nghệ - Viện Hàn lâm Khoa học và Công nghệ Việt

Nam

Người hướng dẫn khoa học 1: TS. Nguyễn Trường Thắng

Người hướng dẫn khoa học 2: PGS.TS. Đặng Văn Đức

Phản biện 1:…………………………

Phản biện 2:…………………………

Phản biện 3:…………………………

Luận án sẽ được bảo vệ trước Hội đồng đánh giá luận án tiến sĩ cấp Học viện, họp tại Học viện Khoa học và

Công nghệ - Viện Hàn lâm Khoa học và Công nghệ Việt Nam vào hồi …..giờ…‟, ngày…..tháng

…… năm 201…

Có thể tìm hiểu luận án tại:

- Thư viện Học viện Khoa học và Công nghệ - Thư viện Quốc gia Việt Nam

1

MỞ ĐẦU

1. Tính cấp thiết của luận án

Một cách tổng quát, với mỗi kỹ thuật được dùng trong một giai đoạn kiểm thử động (dynamic run-

time testing) thì bất cứ phần mềm nào cũng có thể được phân ra làm hai công đoạn con: chuẩn bị các ca kiểm

thử (test case) cho việc kiểm tra phần mềm và thực hiện chạy chương trình cần kiểm thử trên một nền tảng

hỗ trợ các nghiệp vụ kiểm thử (testing framework) với các ca kiểm thử đã có.

Một trong các hoạt động quan trọng để giảm chi phí kiểm thử phần mềm là sinh các ca kiểm thử một

cách tự động và có tính đầy đủ. Các tổ chức phát triển phần mềm thường phải chi phí một lượng lớn về tài

chính cho các hoạt động liên quan đến kiểm thử phần mềm. Tính hiệu quả của tiến trình xác minh và thẩm

định phụ thuộc nhiều vào số lỗi được tìm ra và được sửa chữa trước khi sản phẩm được chuyển giao. Điều

này đồng nghĩa với quan điểm chất lượng của phần mềm phụ thuộc chặt chẽ vào chất lượng các ca kiểm thử

được sinh ra.

Trong những năm qua, nhiều nghiên cứu của các nhà khoa học trên thế giới nhằm “sinh dữ liệu kiểm

thử một cách tự động” [3, 4] để giảm thiểu chi phí cho phần mềm. Có hai cách tiếp cận căn bản để sinh dữ

liệu kiểm thử đó là dựa vào mã nguồn (code) và dựa vào mô hình (model). Đối với phương pháp dựa vào mã

nguồn là phương pháp cho khả năng bao phủ cao, có khả năng loại bỏ các dòng lệnh không cần thiết chứa

các tiềm ẩn gây lỗi nhưng cần thiết phải có khả năng tối ưu tính toán của các phần mềm phân tích kiểm thử,

do vậy gần đây có nhiều nghiên cứu tập trung vào phương pháp này [5, 6, 7].

Trong những năm qua, nhiều nghiên cứu về việc sinh các ca kiểm thử một cách tự động như: sinh

các ca kiểm thử dựa vào đặc tả, sinh các ca kiểm thử dựa vào mô hình, sinh ca kiểm thử hướng đường dẫn và

kỹ thuật thông minh. Tuy nhiên, kiểm thử dựa vào thực thi biểu trưng đã và đang là hướng nghiên cứu được

nhiều người quan tâm. Các kỹ thuật cơ bản sinh dữ liệu kiểm thử tự động mà các nhà nghiên cứu đã đề xuất

đó là: Dựa vào chứng minh định lý (test case generation by theorem proving) [8, 9]; Dựa vào thực thi biểu

trưng (test case generation by symbolic execution [5, 7,10,11,12]); Dựa vào kiểm chứng mô hình (test case

generation by model checking) [13]; Dựa vào một mô hình luồng sự kiện (test case generation by an event-

flow model [14]); Dựa vào việc sử dụng mô hình xích Markov (test case generation by using a Markov

chains model) [15]. Trong đó kỹ thuật thực thi biểu trưng (symbolic execution) đang là vấn đề được nhiều

nhà khoa học trên thế giới tìm hiểu, phát triển và xây dựng các ứng dụng [5, 6, 7]. Hiện nay kỹ thuật này đã

và đang được phát triển trên nhiều công cụ, nhiều ngôn ngữ như: C/C++, JavaScrip, .Net, java, HTML vv...

Trong phạm vi giới hạn nghiên cứu, nội dung của luận án tập trung nghiên cứu về một số cải tiến trong bộ

giải ràng buộc xâu áp dụng sinh các ca kiểm thử. Các cài đặt thực nghiệm và đánh giá được thực hiện bằng

ngôn ngữ Java do Java là ngôn ngữ mạnh mẽ, hiện đại. Hơn nữa, Java đang được sử dụng rộng rãi với các

thư viện trên kiểu dữ liệu xâu đa dạng, phong phú và được sử dụng trong nhiều dự án lớn trong hiện tại và

tương lai.

2. Mục tiêu nghiên cứu của luận án

Nghiên cứu các phương pháp mô hình hóa ràng buộc giải ràng buộc từ dó cải tiến khả năng giải

ràng buộc và áp dụng kỹ thuật thực thi biểu trưng trong tự động sinh các ca kiểm thử. Cài đặt thử nghiệm các

phương pháp đề xuất trong sinh tự động các ca kiểm thử trên kiểu dữ liệu xâu và kiểu dữ liệu hỗn hợp. Phân

tích, đánh giá kết quả sau khi thử nghiệm.

2

Tổng quan về các phương pháp tự động sinh các ca kiểm thử phần mềm, kỹ thuật thực thi biểu trưng

và ứng dụng trong sinh tự động các ca kiểm thử. Các kỹ thuật mô hình hóa ràng buộc, giải ràng buộc trên các

kiểu dữ liệu dựa trên hai phương pháp Otomata và Bitvector, Nghiên cứu, phân tích đánh giá các phương

pháp hiện có sinh ca kiểm thử trên các kiểu dữ liệu khác nhau. Đánh giá hiệu quả, chất lượng của các ca

kiểm thử được tạo ra so với thực tế chương trình.

Các kỹ thuật sinh tự động các ca kiểm thử, các vấn đề liên quan mô hình hóa ràng buộc trên các kiểu

dữ liệu. Nghiên cứu cải tiến mô hình hóa và giải ràng buộc trên kiểu dữ liệu xâu kí tự, từ đó ứng dụng trong

kỹ thuật thực thi biểu trưng thực hiện sinh các ca kiểm thử tự động trên kiểu xâu kí tự cho các chương trình

kiểm thử.

Nghiên cứu, phân tích, tổng hợp các liệu liên quan đến thực thi biểu trưng, vai trò của giải ràng buộc

cũng như giải ràng buộc trên kiểu dữ liệu xâu trong thực thi biểu trưng trong sinh tự động các ca kiểm thử

(các bài báo, tạp chí, trên mạng Internet...). Cải tiến mô hình hóa ràng buộc và nâng cao khả năng giải ràng

buộc trên kiểu dữ liệu xâu và ràng buộc hỗn hợp, phân tích, đánh giá các kết quả đã công bố.

3. Các nội dung nghiên cứu chính của luận án

Xây dựng mô hình hóa ràng buộc trên kiểu dữ liệu xâu và ràng buộc hỗn hợp, cải tiến khả năng giải

ràng buộc trong phương pháp thực thi biểu trưng. Cài đặt kỹ thuật mô hình hóa và giải ràng buộc dựa trên

Otomat và Bitvector trong giải ràng buộc xâu, đánh giá so sánh các kết quả thu được với các các kết quả đã

công bố, luận án có bố cục cụ thể như sau:

Chương 1 của luận án trình bày tổng quan về kiểm thử phần mềm và kỹ thuật thực thi biểu trưng ứng

dụng trong tự động sinh các ca kiểm thử. Đồng thời trình bày các lý thuyết cơ sở sử dụng trong luận án nhằm

đưa ra cái nhìn tổng quan về bài toán nghiên cứu, về sử dụng kỹ thuật thực thi biểu trưng ứng dụng trong

sinh tự động các ca kiểm thử và hướng nghiên cứu cụ thể của luận án.

Chương 2 của luận án trình bày kết quả nghiên cứu về các phương pháp mô hình hóa ràng buộc, giải

ràng buộc trong thực thi biểu trưng. Áp dụng các công cụ này vào các trường hợp cụ thể cùng với các đánh

giá tính hiệu quả của các phương pháp này trên kiểu dữ liệu cụ thể.

Chương 3 của luận án trình bày các kết quả nghiên cứu của các cải tiến mô hình hóa ràng buộc trên

kiểu xâu và ràng buộc hỗn hợp, giải ràng buộc trong thực thi biểu trưng trên kiểu dữ liệu xâu và dữ liệu hỗn

hợp. Đồng thời trình bày việc mở rộng kỹ thuật thực thi biểu trưng, cách thực hiện giải ràng buộc xâu dựa

trên phương pháp Otomat.

Phần kết luận nêu những đóng góp, hướng phát triển, những vấn đề quan tâm; danh mục các công

trình đã được công bố của luận án và danh sách các tài liệu tham khảo được sử dụng trong luận án cũng được

trình bày.

CHƢƠNG 1. TỔNG QUAN VỀ KIỂM THỬ PHẦN MỀM VÀ THỰC THI BIỂU TRƢNG

Chương này trình bày lý thuyết tổng quan về kiểm thử và sinh dữ liệu kiểm thử, thực thi biểu trưng

và ứng dụng của thực thi biểu trưng trong sinh các ca kiểm thử. Trong đó, trình bày các khái niệm cơ bản và

các phân tích liên quan đến kỹ thuật thực thi biểu trưng. Đồng thời, một vài thách thức và hướng phát triển

của luận án cũng được trình bày trong chương này.

1.1. Kiểm thử phần mềm

Để đảm bảo một hệ thống phần mềm hoặc các thành phần của phần mềm làm việc như mong muốn là

một thách thức lớn trong ngành công nghiệp phần mềm. Các phần mềm lỗi gây ra những tổn thất về kinh tế

cũng như những hậu quả nghiêm trọng khác tùy thuộc vào lĩnh vực mà phần mềm được sử dụng.

3

1.1.2 Các kỹ thuật kiểm thử [24]:

Kiểm thử hộp đen (Black box testing)

Kiểm thử hộp trắng (White box testing)

Kiểm thử đơn vị (Unit test)

1.2. Kỹ thuật kiểm thử hộp trắng dòng điều khiển

Kiểm thử hộp trắng dòng điều khiển chia ra gồm kiểm thử hướng tĩnh và kiểm thử hướng động. Đầu

vào của hai kĩ thuật này đều là mã nguồn và tiêu chí phủ kiểm thử. Sau một loạt quá trình phân tích, đầu ra

tương ứng là tập ca kiểm thử. Mỗi một kĩ thuật đều có những ưu điểm và hạn chế riêng. Mục tiêu của kiểm

thử hộp trắng dòng điều khiển là tìm tập ca kiểm thử tối thiểu nhưng đạt được độ phủ tối đa.

1.3. So sánh kiểm thử hộp trắng dòng điều khiển theo hƣớng tĩnh và động

Mỗi một kĩ thuật kiểm thử đều có những ưu điểm và hạn chế riêng. Để có cái nhìn tổng quan về hai

kĩ thuật, luận án đưa ra sự so sánh về số ca kiểm thử, thời gian sinh ca kiểm thử, khả năng kiểm thử vòng lặp,

ảnh hưởng bởi phức tạp mã nguồn đối với hai kĩ thuật.

1.4. Thách thức trong kiểm thử phần mềm

Tồn tại các ý tưởng không đúng về kiểm thử như: Ca kiểm thử tốt luôn là ca kiểm thử có độ phức

tạp cao; Tự động kiểm thử có thể thay thế kỹ sư kiểm thử để kiểm thử phần mềm một cách tốt đẹp; Kiểm thử

phần mềm thì đơn giản và dễ dàng. Ai cũng có thể làm, không cần phải qua huấn luyện.

Ngoài ra, việc kiểm thử còn gặp nhiều hạn chế bao gồm: Không thể chắc là các đặc tả phần mềm

đều đúng 100%; Không thể chắc rằng hệ thống hay công cụ kiểm thử là đúng; Không có công cụ kiểm thử

nào thích hợp cho mọi phần mềm; Kỹ sư kiểm thử không chắc rằng họ hiểu đầy đủ về sản phẩm phần mềm;

Không bao giờ có đủ tài nguyên để thực hiện kiểm thử đầy đủ phần mềm; Không bao giờ chắc rằng ta đạt đủ

100% hoạt động kiểm thử phần mềm.

1.5. Thực thi biểu trƣng

1.5.1. Tổng quan về thực thi biểu trưng

Trong khoa học máy tính, thực thi biểu trưng là một phương tiện để phân tích một chương trình để xác

định đầu vào nào gây ra mỗi phần của chương trình để thực thi. Một bộ biên dịch theo chương trình, giả sử

nhận các giá trị biểu trưng cho các đầu vào thay vì nhận các đầu vào thực tế như thực thi bình thường của

chương trình.

1.5.2. Thực thi biểu trưng tĩnh

Ý tưởng chính của thực thi biểu trưng [31] là thực thi chương trình với các giá trị biểu trưng thay vì

các giá trị cụ thể của các tham số đầu vào.

Giá trị biểu trưng của biến x có thể được biểu thị bởi:

(a). Một ký hiệu đầu vào.

(b). Một biểu thức kết hợp giữa các giá trị biểu trưng bởi các toán tử,

(c). Một biểu thức kết hợp giữa giá trị biểu trưng và giá trị cụ thể bởi toán tử.

1.5.3. Thực thi biểu trưng động

Thực thi biểu trưng động [32, 33] là kỹ thuật thực thi tượng trưng dựa trên phân tích chương trình

động. Thực thi biểu trưng động chính là sự kết hợp giữa thực thi cụ thể và thực thi biểu trưng. Trong thực thi

biểu trưng động, chương trình được thực thi nhiều lần với những giá trị khác nhau của tham số đầu vào.

4

Bảng 1.1. Ví dụ về thực thi biểu trưng động

Ràng buộc C’(i) Input i Ràng buộc đƣợc ghi nhớ C(i)

null a = = null

{} a!=null a!=null && !(a.length>0)

a!=null && a.length>0 {0} a!=null&& a.length>0 && a[0]!=123456789

a!=null && a.length>0 && a!=null && a.length>0 {123456789} a[0]!=123456789 && a[0]!=123456789

1.5.4 Thực thi Concolic

Thực thi Concolic là một mô hình thực hiện cụ thể và là một biến thể của thực thi biểu trưng. Nó được

tiên phong bởi các công cụ DART [36] và CUTE [35].

Bảng 1.2. So sánh thực thi Concolic với thực thi biểu trưng

Thực thi biểu trƣng cổ điển Thực thi Concolic

- Sử dụng một đầu vào biểu trưng, thu tập và -Sử dụng một đầu vào cụ thể và chạy chương

giải ràng buộc với đầu vào biểu trưng. trình trong khi thu thập các ràng buộc đường dẫn

Thực thi biểu trƣng cổ điển đối với đầu vào đó

Thực thi Concolic

- Gọi bộ giải trên mọi điểm nhánh nên việc tiếp - Chạy chương trình trong khi thu thập các ràng

cận các phần sâu của mã chậm hơn. buộc đường dẫn. Không can thiệp vào việc chạy

chương trình nhiều – Nhanh

- Biểu trưng cổ điển sẽ sử dụng ít tài nguyên hơn - Các phần sâu hơn của mã được thực thi trong

khi muốn khám phá đầy đủ tất cả các đường mỗi lần lặp

dẫn. – tiếp cận các phần sâu của mã nhanh hơn.

- Thực hiện lại các bit bắt đầu của chương trình

nhiều lần - không cần thiết

- Thực thi đồng thời có thể tốt hơn nếu bạn chỉ

muốn tìm lỗi vì sẽ tiếp cận các phần sâu hơn của

chương trình nhanh hơn.

1.6.6. Ràng buộc xâu và vai trò của giải ràng buộc xâu

Mấu chốt của thực thi biểu trưng đó là khả năng giải ràng buộc và xâu dữ liệu là một kiểu dữ liệu cơ

bản nó có trong tất cả các ngôn ngữ lập trình hiện đại và việc sử dụng các phép toán trên xâu là thường

xuyên được thực hiện. Trong các lĩnh vực khác nhau như phân tích phần mềm, kiểm chứng mô hình, cơ sở

dữ liệu, bảo mật web, tin sinh học [47 - 52]. Vì lý do trên việc giải các ràng buộc phức tạp trên xâu là cần

hiết và có rất nhiều ứng dụng.

Các quan hệ được định nghĩa trên biến xâu kí tự bao gồm: Độ dài xâu, so sánh xâu, các phép nối,

kiểm tra xâu con, cắt xâu, so sánh biểu thức chính quy vv..

Thuật ngữ giải ràng buộc xâu (String Constraint Solving)trong luận án đề cập đến việc mô hình hóa,

và giải quyết các biểu thức kết hợp liên quan đến ràng buộc xâu, ta có thể xem như giải ràng buộc xâu như là

phần giao giữa giải ràng buộc và tổ hợp các từ, trong đó người dùng sẽ đưa ra một vấn đề với các biến xâu và

5

một bộ giải ràng buộc xâu sẽ tìm ra một giải pháp phù hợp cho vấn đề đó. Từ những năm 2010 việc giải ràng

buộc xâu đã có một số các nghiên cứu quan tâm có kết quả nhất định [51, 52] do nó có vai trò chủ đạo trong

các lĩnh vực sinh dữ liệu kiểm thử, kiểm chứng mô hình, và bảo mật web.

Trong những năm qua có nhiều hướng tiếp cận khác nhau đã được đưa ra, nhưng có ba loại chính:

Tiếp cận dựa trên lý thuyết về Otomat: phương pháp này sử dụng một Otomat hữu hạn để biểu diễn

giá trị của một biến xâu, nó được dùng để lưu trữ, xử lý các phép toán trên xâu.

Tiếp cận dựa trên từ: Phương pháp này sử dụng hệ thống của so sánh từ với nhau, chúng sử dụng chủ

yếu lý thuyết thỏa mãn (SMT)[53] để giải các ràng buộc xâu.

Tiếp cận dựa trên phân tách xâu: Nguyên lý là thực hiện phân tách xâu thành các phần tử liền kề

tương đương là các kí tự của xâu. Xâu có thể phân rã thành các số nguyên hoặc bitvector

Bảng chữ cái hữu hạn là một tập hữu hạn Σ ={a1,a2 . . . , an} với n>1 các kí hiệu cũng được gọi là kí tự. Một xâu w hay một tự là một dãy hữu hãn các kí tự thuộc bảng chữ cái Σ, kí hiệu |w| biểu diễn cho độ dại

của xâu w( trong luận án này không đề cập đến xâu có độ dài vô hạn). Một xâu rỗng được biểu diễn bởi ký tự

ɛ, gọi tập hữu hạn Σ*là tập tất cả các xâu của bảng chữ cái Σ được định nghĩa đệ quy như sau:

Xâu rỗng: ɛ ∈ Σ* Nếu kí tự a∈ Σ và w∈ Σ* thì thì wa∈ Σ* Ngoài ra không có gì thuộc Σ*

Bảng 1.4. Mô tả ràng buộc xâu

Ràng buộc xâu Mô tả

x = y, x ≠ y So sánh bằng, so sánh khác

x < y, x≤y, x≥y, x > y So sánh thứ tự logic của hai xâu

So sánh độ dài xâu với một số nguyên n

Phép nối xâu, phép lặp của phép nối xâu

Phép đảo ngược xâu

n=|x| z=x.y, y=xn y=x-1 y=x[i..j] Lấy về xâu con của xâu x

n=find(x,y) n là chỉ số đầu tiên xuất hiện của xâu x trong xâu

y

y = replace(x, q, q′ ) y có được bằng cách thay thế lần xuất hiện đầu

tiên của q bằng q‟ trong x.

y = replaceAll(x, q, q′ ) y có được bằng cách thay thế tất cả q bằng q‟

trong x

n = count(a, x) n là số lần xuất hiện của kí tự a trong x

x thuộc ngôn ngữ chính quy được biểu diễn bởi x ∈ L(R)

R

x thuộc ngôn ngữ phi ngữ cảnh được biểu diễn x ∈ L(G)

bởi G

Ví dụ như ràng buộc substring(x,y) có nghĩa là xâu x phải là xâu con của xâu y có thể được định

nghĩa tương đương với ràng buộc find(x,y) được định nghĩa trong[54] cũng có thể tham chiếu tương đương

với ràng buộc indexOf(y,x). Thứ tự của các kí tự trong xâu cũng tùy biến, trong một cách tiếp cận giải ràng

buộc xâu thứ tự đầu tiên trong xâu được bắt đầu là 0 nhưng với một số cách tiếp cận thì nó là 1 khi đó kí tự

6

đầu tiên của xâu lại là x[1] thay vì x[0]. Nói tóm lại mục tiêu của giải ràng buộc xâu nhằm xác định xem có

tồn tại các giá trị của các biến xâu có thỏa mãn một biểu thức ràng buộc đã cho hay không và nhiệm vụ này

có thể được giải quyết bởi hai phương pháp là lập trình ràng buộc và lý thuyết thỏa mãn.

1.6. Kết luận chƣơng 1

Chương 1 của luận án đã trình bày các khái niệm nền tảng của nghiên cứu bao gồm các kỹ thuật kiểm thử

phần mềm, các kỹ thuật cơ bản sinh dữ liệu kiểm thử tự động từ mô hình đang quan tâm. Đồng thời cũng đã

đánh giá so sánh các kỹ thuật kiểm thử hộp trắng theo hướng động và tĩnh, chỉ ra các thách thức về kiểm thử

phần mềm chưa được giải quyết. Trong đó kỹ thuật thực thi biểu trưng đang là vấn đề có triển vọng nghiên

cứu. Các kiến thức nền tảng và tổng quan về kỹ thuật thực thi biểu trưng cũng như các thách thức, các vấn đề

chưa được giải quyết cũng được trình bày trong chương này.

Các nội dung liên quan đến giải ràng buộc xâu ứng dụng trong sinh tự động các ca kiểm thử sẽ được trình

bày trong các chương tiếp theo của luận án.

CHƢƠNG 2. THỰC THI BIỂU TRƢNG VÀ MÔ HÌNH HÓA RÀNG BUỘC

Trong chương này, các khó khăn của kỹ thực thực biểu trưng sẽ được phân tích đánh giá. Đồng thời,

các công cụ mở rộng, cài đặt kỹ thuật thực thi biểu trưng mà nó sẽ được dùng để thực hiện cải tiến kỹ thuật

mô hình hóa ràng buộc kiểu xâu cũng được giới thiệu. Ngoài ra, phương pháp mô hình hóa phục vụ cho cài

đặt, đánh giá giải ràng buộc xâu và ràng buộc hỗn hợp cũng được trình bày trong chương này.

Nội dung chương này được thể hiện trong các kết quả công bố [CT1], [CT2], [CT3] của tác giả.

2.1. Những khó khăn và một vài giải pháp

Trong phần này, những khó khăn trong quá trình áp dụng thực thi biểu trưng được thảo luận và một vài giải

pháp cho việc giải quyết các thách thức đặt ra được trình bày.

2.1.1. Bùng nổ đường đi

Một trong những thách thức quan trọng của thực thi biểu trưng là nó sẽ sinh ra một số lượng lớn các

đường thực thi mặc dù chương trình là nhỏ và thường là hàm mũ trong số các câu lệnh rẽ nhánh tĩnh của mã

nguồn. Kết quả là trong một khoảng thời gian định trước nó sẽ quyết định khám phá con đường đầu tiên sao

cho phù hợp nhất.

2.1.2. Mô hình hóa bộ nhớ

Độ chính xác của các câu lệnh của chương trình khi chuyển sang các ràng buộc biểu trưng có ảnh

hưởng đáng kể đến độ bao phủ khi thực hiện thực thi biểu trưng cũng như khả năng giải các ràng buộc. Ví dụ

khi sử dụng mô hình hóa bộ nhớ mà xấp xỉ để thiết lập độ rộng cho tham biến kiểu Interger có thể có hiệu

quả hơn trong thực tế nhưng mặt khác kết quả lại thiếu chính xác trong phân tích mã nguồn. Nó phụ thuộc

vào khoảng lựa chọn giá trị tương ứng như lỗi tràn bộ nhớ toán học, cũng có thể gây ra thiếu đường dẫn

trong thực thi biểu trưng, hoặc khai phá những đường đi không khả thi vv..

2 .2. Thực thi biểu trƣng và công cụ mở rộng

2.2.1. Thực thi biểu trưng và kiểm thử phần mềm

Kỹ thuật sinh dữ liệu kiểm thử sử dụng thực thi biểu trưng được cài đặt trên ngôn ngữ Java để sinh

dữ liệu kiểm thử cho các chương trình. Tuy nhiên, hiệu năng công cụ hiện có còn hạn chế: thời gian thực thi

khá lớn. Việc áp dụng thuật toán tối ưu các ràng buộc - biểu diễn các lộ trình thực thi mã nguồn - nhằm giảm

thời gian thực thi, nhưng vẫn đảm bảo hiệu quả bao phủ. Giải pháp cải tiến được thử nghiệm trên tập các

chương trình Java khác nhau và cho kết quả rất khả quan. Nội dung phần này trình bày về JPF như khả năng

kiểm tra của JPF, kiến trúc mức cao của JPF và khả năng mở rộng của JPF.

7

2.2.2. Thực thi biểu trưng trên ngôn ngữ Java

Giới thiệu về Java PathFinder (JPF)

Ngày nay kỹ thuật thực thi biểu trưng cho phép thực hiện trên nhiều công cụ và ngôn ngữ khác nhau

như là DART[36], CUTE[35] là các công cụ cho ngôn ngữ C/C++, hay PEX[36,37] cho các mã nguồn .NET tuy nhiên trong luận án này lựa chọn sử dụng Path Finder cho ngôn ngữ Java. Lý do là Java là ngôn ngữ độc

lập với môi trường và có nhiều ứng dụng quan trọng được xây dựng trên nền tảng java, một lý do khác là

công cụ JPF là một công cụ mạnh mẽ hỗ trợ cho kỹ thuật thực thi biểu trưng nó cho khả năng mở rộng và có

một cộng đồng phát triển rộng rãi.

JPF là một bộ kiểm chứng mô hình phần mềm trạng thái tường minh cho Java [68]. Hiểu một cách

cơ bản JPF là một máy ảo thực thi chương trình Java không chỉ một lần (giống như các máy ảo thông

thường), mà thực thi trong tất cả các nhánh, các đường đi có thể. JPF sẽ kiểm tra các vi phạm thuộc tính như

khóa chết hoặc các ngoại lệ không thể bắt được xuyên suốt các đường thực thi tiềm năng. Hình 2.1 mô tả mô

hình hoạt động của JPF.

Hình 2.1. Mô hình hoạt động của JPF

Khả năng kiểm tra của JPF

JPF có thể kiểm tra tất cả các chương trình Java. JPF có thể tìm ra các khóa chết hoặc ngoại lệ.

Ngoài ra chúng ta có thể tự phát triển mở rộng để kiểm tra các thuộc tính khác.

Kiến trúc mức cao của JPF

JPF được thiết kế (như Hình 2.3) thành 2 thành phần chính đó là: JVM, và Search. Trong đó, JVM là một bộ

sinh trạng thái cụ thể Java. Bằng việc thực hiện các chỉ thị Java bytecode. Search chịu trách nhiệm lựa chọn

trạng thái mà JVM nên xử lý, hoặc hướng JVM sinh trạng thái tiếp theo, hoặc yêu cầu JVM quay trở lại một

trạng thái trước đó.

8

Hình 2.3. Biểu diễn sơ đồ kiến trúc mức cao của JPF.

Các cài đặt chính của Search bao gồm tìm kiếm theo độ sâu (DFSearch) và HeuristicSearch.

Trừu tượng hoá: Là quá trình loại bỏ các chi tiết không liên quan đến thuộc tính để có được các mô

hình hữu hạn đơn giản đủ để xác minh thuộc tính

Trừu tượng hoá dữ liệu: Hàm trừu tượng hoá h biến đổi từ S thành S‟ (Hình 2.4, 2.5)

Hình 2.4. Ví dụ về trừu tượng hoá dữ liệu.

9

Hình 2.5. Một ví dụ khác về trừu tượng hoá dữ liệu.

Quy trình trừu tượng – sàng lọc dữ liệu (Hình 2.6):

Các bước thực hiện:

i. Xây đựng mô hình trừu tượng hoá mới

ii. Kiểm tra mô hình:

+ Nếu đạt yêu cầu thì không có lỗi,

+ Nếu không đạt yêu cầu, kiểm tra các ví dụ truy cập (Các truy cập hợp lệ sẽ có lỗi, các truy cập

không hợp lệ sẽ có các gợi ý sàng lọc.)

Hình 2.6. Quy trình sàng lọc dữ liệu.

Dựa trên các gợi ý sàng lọc, mô hình trừu tượng hoá mới sẽ được xây dựng.

Quy trình này dừng trong các trường hợp không có lỗi hoặc có lỗi.

Nhược điểm: Mất độ chính xác

Khả năng mở rộng của JPF

JPF có thể được coi như là một Framework mà tại đó bất kỳ nhà phát triển nào đều có thể mở rộng

để phục vụ cho một mục đích cụ thể. JPF cung cấp một cơ chế mở rộng để cho phép thêm vào các chức năng

mới mà không phải thay đổi trực tiếp cài đặt của Search hoặc JVM.

Với kiến trúc mở rộng linh hoạt, hiện nay đã có một số mở rộng được phát triển cho JPF

10

2.3. Giải các ràng buộc và thực thi biểu trƣng

Liên quan đến sinh các ca kiểm thử, hướng tiếp cận dựa trên giải thuật di truyền đã được tìm hiểu

trong công trình nghiên cứu CT[1] của nghiên cứu sinh. Tuy nhiên, cách tiếp cận này thể hiện nhiều hạn chế.

Mặc dù đã có những tiến bộ đáng kể trong kỹ thuật thực hiện giải các ràng buộc trong những năm

gần đây, giúp cho thực thi biểu trưng trở nên thực tế hơn, nhưng việc giải các ràng buộc vẫn là cản trở đáng

kể của thực thi biểu trưng. Nó thường chiếm nhiều thời gian trong quá trình thực hiện và là một trong những

lý do chính khiến thực thi tượng trưng không mở rộng được với một số loại chương trình mà mã nguồn của

nó sinh ra với yêu cầu rất lớn trong việc giải các ràng buộc.

Kết quả là cần thiết phải thực hiện tối ưu khi giải các ràng buộc được sinh ra trong quá trình thực thi

biểu trưng trong những chương trình thực tế. Hai phương pháp tối ưu được sử dụng bởi các công cụ hiện tại

bao gồm:

Loại bỏ ràng buộc không liên quan

Giải ràng buộc theo phương pháp gia tăng (Increamental Solving) [71]

Một trong những tính chất quan trọng của tập các ràng buộc được tạo ra trong quá trình thực thi biểu

trưng là nó mô tả biểu diễn cho một tập các nhánh tĩnh từ mã nguồn của chương trình.

Trong KLEE tất cả các kết quả truy vấn được lưu vào vùng nhớ đệm ánh xạ tập các ràng buộc và các

giá trị cụ thể tìm được tương ứng với ràng buộc đó (trong trường hợp đặc biệt không có lời giải hoặc không

thỏa mãn tương ứng với một kí hiệu đặc biệt).

2.4. Ràng buộc hỗn hợp và cải tiến trong giải ràng buộc xâu

Trên thực tế, kiểu dữ liệu xâu xuất hiện trong hầu hết các chương trình, đặc biệt là trong những đoạn

chương trình hoặc phương thức nhằm “làm sạch” xâu dùng cho dữ liệu đầu vào của các chương trình nhằm

kiểm tra tính hợp lệ cũng như phát hiện và loại bỏ các nội dung độc hại. Với một thư viện rộng lớn, kiểu dữ

liệu xâu trong ngôn ngữ Java còn ẩn chứa nhiều lỗi.

Với mong muốn hoàn thiện khả năng kiểm thử và phát hiện lỗi trên những chương trình Java có sử

dụng kiểu dữ liệu xâu, nội dung luận án quan tâm đến việc xác định lỗi để có những phần mềm hoàn thiện

hơn. Áp dụng kiểm thử phần mềm sử dụng kiểu dữ liệu xâu nhằm tăng khả năng bao phủ hướng tới nâng cao

chất lượng phần mềm.

Tại sao thực thi biểu trưng trên kiểu dữ liệu xâu lại khó khăn?

Các phép toán xâu là sự trộn lẫn giữa hai miền giá trị, cụ thể là xâu và số nguyên. Ví dụ phép toán

lấy kí tự thứ n của xâu. Hiện tại những giải pháp được đưa ra để thực thi biểu trưng cho kiểu dữ liệu xâu

nhưng nó mới chỉ dừng lại ở việc chỉ hỗ trợ một tập con các phép toán đó hoặc thường là không có gì đáng

kể. Ta thực hiện cách tiếp cận lặp đi lặp lại, trong đó đầu tiên ta thực hiện giải các ràng buộc trên kiểu dữ liệu

số nguyên, sau đó sử dụng kết quả đó để giải ràng buộc xâu và nếu nó được thỏa mãn thì công việc được

hoàn thành. Mặt khác các ràng buộc kiểu nguyên được thêm vào bổ sung và quá trình này được lặp đi lặp lại.

Ý tưởng cốt lõi cho việc mở rộng kỹ thuật thực thi biểu trưng mà nghiên cứu này đề xuất được chỉ ra

trong Hình 2.7 dưới đây.

11

Hình 2.7. Đồ thị xâu

Tiếp theo, quá trình lặp được thực hiện với hai bước như sau:

- Bước 1: Bộ giải ràng buộc hiện thời của JPF được gọi để xử lý các ràng buộc kiểu nguyên, kiểu

thực, kiểu logic…và nếu nó giải được chuyển qua bước 2

- Bước 2: Các giá trị cụ thể thu được từ bước 1 được truyền tới cho đồ thị xâu và khi đó bộ giải ràng

buộc xâu được gọi để giải chúng. Trong trường hợp này, “bộ giải ràng buộc xâu” có thể là AutomataSolve

hay là BitVectorSolve và có thể ràng buộc của đồ thị xâu không thỏa mãn với các giá trị nhận được và nếu

thời gian giới hạn còn thỏa mãn ta thực hiện quay lại bước 1 và ràng buộc xâu sẽ được thêm các ràng buộc

mới.

Solve(PathCondition pc){

1:

StringGraph sg; sg=BuilStringGraph(pc); 2:

boolean sat=false; 3:

4:

While(!sat and !timeout){ sat=CurrentSolver(pc,sg); 5:

if(sat) 6:

7:

sat=StringSolver(pc,sg); return sat; } 8:

}

buildStringGraph(PathCondition pc) {

1: StringGraph sg ;

2: for string or mixed constraint c 2 pc:

3: sg= sg hyperedge(c)

4: return preprocess(pc; sg)

}

Hình 2.8. Thuật toán giải ràng buộc hỗn hợp

Giá trị giới hạn thời gian “timeout” được đưa vào để đảm bảo trong trường hợp sự kết hợp giữa hai

bộ giải ràng buộc kiểu xâu và ràng buộc kiểu nguyên vẫn không thể đưa ra được kết luận cuối cùng trong

một thời gian cho phép. Khi đó thuật toán vẫn dừng với kết luận ràng buộc trên là không thỏa mãn.

2.4.1. Đồ thị xâu

Các loại ràng buộc có thể được phân loại thành ràng buộc kiểu xâu, ràng buộc kiểu nguyên, ràng

buộc hỗn hợp kiểu xâu và kiểu nguyên. Trong quá trình cài đặt, ràng buộc kiểu xâu và ràng buộc hỗn hợp

được biểu diễn bởi một đồ thị đặc biệt gọi là đồ thị xâu.

12

Định nghĩa: Đồ thì xâu là một loại đồ thị có hướng H=(X, E, Ʊ). Trong đó, tập đỉnh được xác định

bởi X=I S với I và S là lai tập rời nhau (I là tập biểu diễn cho các biến kiểu nguyên và S là tập biểu diễn cho

các biến kiểu xâu). Tập Ʊ thể hiện cho phép toán trên xâu. Đồng thời, nó cũng thể hiện tập các cạnh gán nhãn có hướng (E = E1 E2 E3 E4) sao cho En= Ʊ Xn.

Sử dụng đồ thị là phương pháp phổ biến trong lập trình thỏa mãn ràng buộc. Hình 3.1 mô tả ví dụ

cho đồ thị xâu tương ứng với ràng buộc:

s1.trim().equals(s2)^s1.equals(s3.concat(s2))

2.4.2. Xây dựng lại ràng buộc

Phục vụ cho giai đoạn tiền xử lý, với mỗi ràng buộc xâu hoặc ràng buộc hỗn hợp của điều kiện ràng

buộc đường đi, đóng góp vào một cạnh của đồ thị xâu, nó xây dựng lại ràng buộc bởi ràng buộc và giá trị trả

về của phép toán được ánh xạ trực tiếp vào các cạnh của đồ thị xâu. Ví dụ: ràng buộc s1.equals(s2) thêm vào cạnh (equals, s1,s2) với những toán tử khác.

Giá trị trả về có thể là là kiểu kí tự, kiểu nguyên hoặc kiểu xâu. Một biến phụ được sinh ra và đại

diện cho kết quả của phép toán. Biến phụ này được thêm vào như là một đỉnh của đồ thị xâu. Nó cho phép

cạnh được thêm vào như là một trường hợp của giá trị trả về.

Trong ví dụ được trình bày ở Hình 2.9 dưới đây, vòng tròn mô tả cho đỉnh, dấu chấm và đường

thẳng mô tả cho cạnh. Mỗi cạnh được gắn nhãn biểu diễn cho phép toán tương ứng và con số chỉ ra thứ tự

của đỉnh đồ thị xâu tương ứng với một ràng buộc. Các biến xâu s1, s2 và s3 xuất hiện như là đỉnh của S với đồ thị này thì Ʊ = {trim, equals, concat}. Phép toán trim sẽ sinh ra một biến phụ s‟ được thêm vào S. Tự bản thân phép toán chính là cạnh (trim, s1, s‟) được gắn nhãn là phần tử trim của Ʊ và nối đỉnh s1 với s‟. Tương tự phép toán concat là ràng buộc thứ hai sinh ra biến phụ s” và cạnh (concat, s3, s2, s”). Cuối cùng hai phép toán equals sẽ tương ứng với hai cạnh còn lại.

Khi một đồ thị xâu được xây dựng xong, nó sẽ được tiền xử lý theo hai cách:

1. Xác định một cách đơn giản các ràng buộc nào là không có giá trị thỏa mãn

2. Thêm vào các giá trị được sinh ra bởi bộ giải ràng buộc nguyên vào biểu thức ràng buộc đường

đi.

2.4.3. Quá trình tiền xử lý

Khi phát hiện những ràng buộc không có giá trị thỏa mãn, quá trình thực thi sẽ tránh được việc mất

thời gian cho bộ giải ràng buộc xâu. Một trong những đề xuất là loại bỏ cạnh equals khỏi đồ thị xâu. Với ví

dụ như trên, đồ thị xâu được chuyển thành đồ thị xâu được đưa ra ở Hình 2.9 dưới đây.

Hình 2.9. Đồ thị sau khi loại bỏ phép toán equals.

Và điều này cũng giúp nhanh chóng xác định tập các ràng buộc được biểu diễn trong đồ thị xâu là

không có giá trị thỏa mãn. Ví dụ (xem Hình 2.10) sau khi loại bỏ cạnh trong Hình 2.10.(a) đỉnh s1 tự nối với

13

nó bằng cạnh notEquals được chỉ ra trong Hình 2.10.(b) và rõ ràng rằng không tồn tại xâu nào thỏa mãn ràng

buộc này.

Hầu hết những đề xuất để giải quyết với những trường hợp phép toán là hằng số. Ví dụ: ràng buộc là

s1.concat(“xyz”) = ”vwxyz” sẽ dẫn đến việc loại bỏ các cạnh phức tạp và thay thế đỉnh s1 bằng xâu vw. Một ví dụ khác cho ràng buộc s1.startsWith(“abc”).chatAt(0) ≠ „a‟ là không phù hợp và dễ dàng phát hiện. Nếu tình huống này phát sinh trong giai đoạn tiền xử lý, sẽ tránh được khi gọi bộ giải ràng buộc xâu và nhanh

chóng trả về giá trị false cho lời gọi.

Hình 2.10. Các ràng buộc không thỏa mãn sau khi loại bỏ phép toán equals

2.4.4. Sinh các ràng buộc xâu và kết quả thực hiện

Trước khi các ràng buộc được tạo ra, các đỉnh mới được thêm vào đồ thị xâu. Đối với các đỉnh

không phải là hằng xâu SiS một biến kiểu nguyên liI được thêm vào để đại diện cho độ dài xâu Si. Hình 3.4 chỉ ra rằng đỉnh mới của đồ thị xâu trong Hình 3.2 được nối với các đỉnh xâu tương ứng bằng các nét đứt.

Hình 2.11. Các đỉnh mới đại diện cho độ dài xâu được bổ sung

Các ràng buộc khác dựa trên các cạnh được chỉ ra tại bảng 2.1.

14

Bảng 2.1. Xây dựng các ràng buộc cho các phép toán trên xâu.

Phép toán Java Heper-edge Ràng buộc mới

Với mỗi ràng buộc cho đỉnh không là hằng xâu Si S Sa.charAt(n) Sa.concat(Sb) Sa.indexOf(Sb) Sa.lastIndexOf(Sb) Sa.subString(n,k) Sa.contains(Sb) charAt,Sa,n,c concat, Sa , Sb, Sx indexOf, Sa, Sb,x lastIndexOf, Sa, Sb,x subString,Sa,n,k,Sx contains,Sa,Sb li>0 la≥n lx=la+lb (x=-1)˅(la≥lb+x) (x=-1)˅(la≥lb+x) la=n+lx la≥lb

2.4.5. Giải ràng buộc sử dụng Otomat

Các bộ giải ràng buộc là những công cụ nổi tiếng để giải quyết nhiều vấn đề trong thế giới thực như

chứng minh định lý và lập lịch thời gian thực. Thực thi biểu trưng để tạo dữ liệu kiểm thử tự động đã được

sử dụng trong các công trình CT[2], CT[3]. Nhiều nhà nghiên cứu đã giảm bớt những thiếu sót của các bộ

giải ràng buộc có sẵn để cải thiện các ứng dụng trong thực thi biểu tượng nhằm tạo dữ liệu kiểm thử. Dù đã

có nhiều cải tiến nhưng các bộ giải ràng buộc vẫn không xử lý hiệu quả với một số loại ràng buộc nhất định.

Trong các chương trình máy tính, dữ liệu xâu xuất hiện thường xuyên, đặc biệt là trong phần chương

trình hoặc phương thức. Ngôn ngữ Java cung cấp một thư viện lớn các kiểu dữ liệu chuỗi nhưng vẫn còn

nhiều lỗi. Trong kiểm thử phần mềm, chúng tôi quan tâm đến việc xác định lỗi. Trong thực thi biểu tượng,

các ràng buộc xâu cũng được xem xét trong hầu hết các trường hợp. Otomat hữu hạn đơn định (Deterministic

Finite Automaton – DFA) được sử dụng để giải ràng buộc xâu dựa trên các thuật toán cụ thể CT[5].

2.5. Kết luận chƣơng 2

Chương 2 của luận án đã trình bày các vấn đề liên quan đến thực thi biểu trưng và công cụ mở rộng

với vai trò hiệu quả trong sinh tự động các ca kiểm thử. Nội dung chủ yếu liên quan đến thực thi biểu trưng

bao gồm các kỹ thuật thực thi biểu trưng khác nhau; ưu, nhược điểm của các kỹ thuật này cùng những xử lý

cần thiết để áp dụng thực thi biểu trưng trong quá trình kiểm thử phần mềm. Đồng thời, chương 2 còn nêu

những khó khăn khi áp dụng thực thi biểu trưng và một vài giải pháp được nêu ra trong chương này. Các

cách tiếp cận mô hình hóa ràng buộc sử dụng đồ thị xâu, xây dựng các ràng buộc trên đồ thị xâu, quy trình

tiền xử lý phát hiện các ràng buộc không thỏa mãn cũng được đưa ra trong chương này. Các nội dung trình

bày trong chương 2 là các kết quả nghiên cứu từ các công trình CT[1], CT[2], CT[3], CT[5].

CHƢƠNG 3. GIẢI RÀNG BUỘC XÂU

Trong chương này, luận án trình bày một đề xuất cải tiến giải ràng buộc xâu trong thực thi biểu trưng

dựa trên lý thuyết Otomat và áp dụng trên kiểu dữ liệu xâu kí tự. Kết quả đặt thực nghiệm, đánh giá về xử lý

dữ liệu văn bản của mô hình cải tiến với một số mô hình đã có cũng được trình bày trong chương này. Nội

dung chương này được thể hiện trong các kết quả công bố [CT4], [CT5], [CT6] của tác giả.

15

3.1. Giải ràng buộc xâu

Nhiều ứng dụng phụ thuộc vào việc xử lý kiểu dữ liệu văn bản (text). Do việc sử dụng Internet đã trở

nên phổ biến với sự gia tăng của các ứng dụng tương tác (mạng xã hội, chat, quản lý các thông tin nhạy cảm,

quan trọng, các thông tin cá nhân) đã khiến cho vấn đề này trở nên quan trọng hơn. Dữ liệu đầu vào của các

chương trình được sử dụng trong các câu lệnh truy vấn SQL và được lưu trữ trên các hệ quản trị cơ sở dữ

liệu. Điều này cho phép người dùng truy cập trực tiếp vào cơ sở dữ liệu. Lý do là các dữ liệu đầu vào là mở

và công khai và nó cũng là mở cho các đối tượng khác. Một số đối tượng có ý định xấu nên việc “làm sạch”

đầu vào dưới dạng văn bản là yêu cầu xuất hiện hầu hết trong các dịch vụ web.

Phương pháp hiện tại để thực thi biểu trưng mã xâu được chia thành hai nhóm: nhóm thứ nhất dựa

trên Otomat [5, 53] và nhóm thứ hai dựa trên Bitvector [7].

3.2. Bitvector và bộ thỏa mãn SMT (satisfiability modulo theories)

3.2.1. Lý thuyết thỏa mãn SMT

Nghiên cứu của luận án này dùng bộ giải ràng buộc SMT Z3 [70] được xây dựng bởi Microsoft.

Nghiên cứu này cũng đã xem xét sử dụng CVC[25] nhưng nhận ra rằng nó chậm hơn Z3 bởi vì luận án này

sử dụng chuẩn SMT-lib2 cho ràng buộc bitvector. Luận án cũng đã xem xét sử dụng các ký hiệu thay thế cho

cách đánh địa chỉ theo byte thay cho bit. Ví dụ a[0:7]=01100010 sẽ được thay là a[0]=‟b‟. Việc giải quyết

các ràng buộc bằng bitvector nằm ngoài phạm vi của nghiên cứu này.

3.2.2. Giải ràng buộc xâu dựa trên phương pháp BitVector

Xem xét ví dụ với cạnh (contains,Sa,Sb) tương ứng với ràng buộc Sa.contains(Sb), ta giải sử ước

lượng hiện tại cho độ dài của Sa và Sb tương ứng là 5,3 kết quả ràng buộc cho cạnh này là:

(Sa[0]=Sb[0])˄(Sa[1]=Sb[1]) ˄ (Sa[2]=Sb[2]) ∨((Sa[1]=Sb[0]) ˄ (Sa[2]=Sb[1]) ˄ (Sa[3]=Sb[2]) ∨((Sa[2]=Sb[0])˄(Sa[3]=Sb[1])˄(Sa[4]=Sb[2]) Nếu như nền tảng của bộ giải ràng buộc hỗ trợ kiểu mảng nó có thể đơn giản hóa thành

(Sa[0:2]=Sb)∨(Sa[1:3]=Sb) ∨(Sa[2:4]=Sb). Quá trình biên dịch các cạnh của đồ thị xâu sang ràng buộc BitVector được chỉ ra tại cột thứ 2 của bảng 3.1

Bảng 3.1. Xây dựng ràng buộc tương ứng với các phép toán trên xâu.

Cạnh Công thức Otomat Ràng buộc bitvector

{x} [*]

(charAt,sa,n,x) (concat,sa,sb,sx) Sa[n]=x (sa=sx[la:0]) (sb=sx[lx:la])

(Ma Mb) ([x] [*] i,0 i

(lastIndexOf, i ([x+lb] (sa[i+lb:i] s b, ,

sa,sb,x) (sa[x+lb:x]=sb) la-lb) x

substring(sa,n,sx) Ma= Ma sa[n+lx:n]=sx

[*] substring(sa,n,k,sx) Ma= Ma Sa[n+lx:n]=sx

Mb=Mb substrings(Ma,x,x+lb) [*] Mb Ma= Ma ] ([*] Mb [*])) Mb= Mb substrings(Ma,x,x+lb) [n] Mx Mx= Mx substring(Ma,n,∞) [n] Mx Mx= Mx substring(Ma,n,k)

16

[„˽‟,*] „˽‟) trim(sa,sx)

(sa[j]= i,j,k Ma= Ma Mx= Mx [„˽‟,*] Mx trim(Ma)

sx[lx-1] (sx[0] ˽) „˽‟ (sa[i+lx:i]=sx) (sa[k]= „˽‟), |(0 i i) (i+lx k

[*] (contains, sa,sb) la-lx) (0 j 0 i

Ma= Ma [*] Mb Mb= Mb substring(Ma,0,∞)

(endsWith, sa,sb) [*] Mb sa[la:la-lb]=sb

Ma= Ma Mb=suffises(Ma)

[*] (startsWith, sa,sb) Ma:= Ma Mb sa[lb:0]=sb

Mb:=prefixes(Ma)

3.3. Giải ràng buộc xâu dựa trên phƣơng pháp sử dụng OTOMAT

Trong thuật toán này, khi các cạnh trong quá trình xử lý các Otomat được sửa đổi lại để phản ánh tác

động của ràng buộc, bản chất của sự sửa đổi phụ thuộc vào ràng buộc. Ví dụ, cạnh (contains, sa,sb) tương ứng với ràng buộc sa.contains(sb).

atomatonSolver(PathCondition pc;StringGraph

StringGraph sg=(I S,E, Ʊ))

1:

2:

for( các đỉnh si S) Automaton Mi=[li]; W=E 3:

4:

while W≠∅ W=W\e 5:

6:

7:

8:

9: for(si kết nối với e) Cập nhật lại Mi dựa vào ràng buộc e; if(Mi=∅) pc=pc freshConstranints(pc:sg);

10:

11:

12:

13

return(false,pc,sg); else if(Mi đã thay đổi) W=W tất cả các cạnh kết nối với si; return checkNegativeEdges(pc;sg;(M1,M2..));

Hình 3.1. Giải ràng buộc xâu dựa trên Otomat

Đối với các ràng buộc phủ định như !equals, !constain, !startsWith và !endsWith giả sử rằng hai M1, M2 là hai Otomat tương ứng với hai biến xâu s1,s2 mà ta phải giải ràng buộc s1.!equals(s2) khi đó sẽ có 3 trường hợp:

TH1: Cả hai Otomat chỉ đoán nhận duy nhất một từ và khi đó ràng buộc này sẽ thỏa mãn khi hai từ

này là không bằng nhau.

TH2: Chỉ có một Otomat đoán nhận duy nhất một từ và khi đó ta chỉ việc gỡ bỏ từ đó ra khỏi Otomat còn

lại. Trong trường hợp này, ràng buộc cũng sẽ được thỏa mãn.

TH3: Trong tất cả các trường hợp khác, ràng buộc được thỏa mãn và không Otomat nào phải thay

đổi. Phần chính của thuật toán trong Hình 3.6 mô tả hình thức các bước thực hiện cho việc tìm lời giải cho

ràng buộc phủ định.

17

1:

2:

3:

4:

CheckNegativeEdges(pathcondition pc, StringGraph sg, (M1,M2..)) i=1; M‟1=M1; M‟2=M2;… M‟k=Mk; while(1≤i

6:

7:

8:

9:

10:

else vi=a Mi; Mi=Mi\{a}; for( với mỗi ei E và last(e)=si) if(e là vi phạm với vi) Break;\\ quay lại dòng 2 11:

i=i++; 12:

return; 13

Hình 3.2. Phương thức giải ràng buộc phủ định

Tạo ra sự cập nhật cho ràng buộc: Nếu những ràng buộc xâu được kết luận là không thỏa mãn, khi đó

ràng buộc nguyên mới sẽ được thêm vào ràng buộc đường đi.

3.4. Đề xuất giải ràng buộc xâu trong thực thi biểu trƣng

Các bước chính thực hiện thực thi biểu trưng bao gồm:

Bước 1: Điều kiện ràng buộc đường dẫn sẽ được chuyển đổi sang một định dạng trung gian.

Bước 2: Giải hoặc đơn giản hóa định dạng trung gian.

Bước 3: Thay thế biến biểu trưng kiểu nguyên bằng các giá trị cụ thể phỏng đoán.

Bước 4: Chuyển đổi định dạng trung gian sang phép toán Otomat hoặc Bitvector.

Bước 5: Nếu việc giải ràng buộc trên Otomat hoặc bitvector thất bại thực hiện lặp lại bước 3 với các giá trị

cụ thể nguyên khác trong tập các giá trị số nguyên tốt nhất.

Bước 6: Quá trình giải ràng buộc kết thúc nếu tìm được giá trị xâu thỏa mãn hoặc trong một khoảng thời gian

giới hạn cho phép không tìm thêm được các giá trị nguyên mới và quá trình giải ràng buộc trên Otomat và

bitvector không có giá trị thỏa mãn.

3.4.1 Mô hình hoá ràng buộc xâu sử dụng đồ thị

Quá trình mô hình hoá ràng buộc xâu sử dụng đồ thị được thể hiện bằng sơ đồ dưới đây:

18

Hình 3.3. Sơ đồ mô hình hoá ràng buộc xâu sử dụng đồ thị

Quá trình thực hiện diễn ra như sau:

Trong cả hai trường hợp trên, các kết quả được đánh giá bằng một bộ đánh giá phù hợp với từng tình

huống trên. Bộ đánh giá được sử dụng để so sánh các bộ giải ràng buộc.

3.4.2 Phát hiện thêm ràng buộc kiểu nguyên trên dữ liệu xâu

Với một mô hình thực thi biểu trưng, ngoài biến kiểu xâu, tất cả các biến gồm biến số nguyên, được

gán các giá trị thời gian chạy được thu thập trong thực thi biểu trưng động. Nghiên cứu này không mô hình

hoá để giải ràng buộc hỗn hợp (giải ràng buộc đối với dữ liệu kiểu xâu và kiểu số nguyên hỗn hợp). Tuy

nhiên, trong mô hình hoá ràng buộc kiểu xâu, quá trình thực thi trích xuất các ràng buộc số nguyên trên độ

dài của chuỗi để tìm một phép gán độ dài thỏa mãn. Do đó phát sinh các ràng buộc kiểu nguyên trên dữ liệu

xâu. Hầu hết các bộ giải ràng buộc hiện đại cho dữ liệu kiểu nguyên đều hiệu quả và chính xác nên việc phát

sinh ràng buộc kiểu nguyên cũng không gây trở ngại cho quá trình thực thi.

3.5. Thực nghiệm và đánh giá kết quả

Tất cả các thử nghiệm được tiến hành trên hệ thống Window 10với RAM 8 GB, sử dụng công cụ

mã nguồn mở JavaPathFinder được tải tại: http://javapathfinder.sourceforge.net/ và phần mềm Eclipse Java

EE IDE

Cài đặt thực nghiệm

SOLVE(PathCondition pc)

1: StringGraph sg

2: (pc,sg)←BuildStringGraph(pc);

3:

4: boolean sat←false; while (!sat˄!timeout)

5: (sat,pc,sg) ←IntegerSolver(pc,sg)

6: if(sat)

7: (sat,pc,sg) ←StringSolver(pc,sg)

8: if( pc unchanged): break;

9: return sat

19

BuildStringGraph(PathCondition pc)

11: StringGraph sg:= ∅ 12: for( String or mixed contraint c pc)

13: sg:=sg Hyperedge(c)

14: return Preprocess(pc,sg)

Hình 3.4: Thuật toán giải ràng buộc xâu.

1. Bộ giải ràng buộc JPF sẽ được sử dụng cho các kiểu ràng buộc trên kiểu số nguyên, số thực,

boolean, v..v..

2. Nếu bước 1 thực hiện thành công nó sẽ cung cấp một số giá trị cụ thể. Các giá trị này sẽ được truyền

cho đồ thị xâu (những giá trị liên quan trong ràng buộc hỗn hợp) và một bộ giải ràng buộc xâu

được gọi để giải quyết chúng.

1: public static String s = "http://www./BigWeb";

2: private static boolean IsBigWebQuery(String str) {

3: // (1) Kiểm tra xem xâu sau dấu „/‟ cuối cùng có

4: // chứa "BigWeb" hay không

5: int lastSlash = str.lastIndexOf('/');

6: if (lastSlash < 0) {

7: return false;

8: }

9: String rest = str.substring(lastSlash + 1);

10: if (!rest.contains("BigWeb")) {

11: return false;

12: }

13: // (2) Kiểm tra xem xâu s có bắt đầu bằng

14: //"http://"

15: if (!str.startsWith("http://")) {

return false;

16: }

17: // (3) lấy về xâu giữa của xâu "http://" và ký

18: // tự

19: //cuối cùng của kí tự "/" và nếu nó bắt đầu bằng

20: // “www”. Tiến hành loại bỏ chúng

21:

22: String t =

23: str.substring("http://".length(), lastSlash);

24: if (t.startsWith("www.")) {

25:

26: t = t.substring("www.".length());

27: }

28: // (4) Kiểm tra sau khi loại bỏ “www” chúng có

20

29:

// chứa " other.com " hoặc "google.com"

30: if (!(t.equals("other.com")) && !(t.equals("google.com"))) {

31: return false;

32: }

33: // Xâu s đã thỏa mãn tất cả các kiểm tra

34: //throw new RuntimeException("Xâu đã cho thỏa

35: //mãn các điều kiện kiểm tra");*/

36: return true;

37: }

38: public static void doTest() {

39: IsBigWebQuery(s);

40: }

41:

42:

43:

44:

45:

Hình 3.5. Chương trình Java kiểm thử

3.5.2 Kết quả thực nghiệm

Sau đây là kết quả cài đặt toàn bộ phương pháp đã được mô tả ở trên. Bắt đầu với một chương trình

Java suy ra từ các điều kiện đường dẫn. Xây dựng và tiền xử lý của đồ thị xâu, chuyển đổi sang các phép

toán Otomat và ràng buộc Bitvector và giải các ràng buộc đó và thực hiện các chuyển đổi giữa các bộ giải

ràng buộc nếu cần thiết với giới hạn các tập kí tự trong {„ ‟,‟a‟,‟b‟}.

Hình 3.9 là một chương trình Java bao gồm một hàm với hai tham số xâu. Trên dòng 1 có một nhánh

có thể tham số xâu đầu tiên được bắt đầu bằng khoảng trắng. Nếu các tham số này bằng nhau, dòng 2 tạo một

biến xâu mới bằng cách loại bỏ các khoảng trắng ở hai đầu (và biến mới này sẽ không bao giờ thỏa mãn các

câu lệnh if trên dòng 1). Dòng 3 nếu biến mới kết thúc là xâu “ab”. Nguợc lại, kiểm tra hai tham số không

bằng nhau ở dòng 7. Cuối cùng nhánh cuối cùng nằm trên dòng 12 kiểm tra nếu kí tự thứ năm của biến xâu

đầu tiên bằng kí tự „a‟.

1: public static String s = "http://www./BigWeb";

2: private static boolean IsBigWebQuery(String str) {

3: // (1) Kiểm tra xem xâu sau dấu „/‟ cuối cùng có

4: // chứa "BigWeb" hay không

5: int lastSlash = str.lastIndexOf('/');

6: if (lastSlash < 0) {

7: return false;

8: }

9: String rest = str.substring(lastSlash + 1);

10: if (!rest.contains("BigWeb")) {

11: return false;

12: }

13: // (2) Kiểm tra xem xâu s có bắt đầu bằng

21

14: //"http://"

15: if (!str.startsWith("http://")) {

return false;

16: }

17: // (3) lấy về xâu giữa của xâu "http://" và ký

18: // tự

19: //cuối cùng của kí tự "/" và nếu nó bắt đầu bằng

20: // “www”. Tiến hành loại bỏ chúng

21:

22: String t =

23: str.substring("http://".length(), lastSlash);

24: if (t.startsWith("www.")) {

25:

26: t = t.substring("www.".length());

27: }

28: // (4) Kiểm tra sau khi loại bỏ “www” chúng có

29: // chứa " other.com " hoặc "google.com"

30: if (!(t.equals("other.com")) &&

31: !(t.equals("google.com"))) {

32: return false;

33: }

34: // Xâu s đã thỏa mãn tất cả các kiểm tra

35: //throw new RuntimeException("Xâu đã cho thỏa

36: //mãn các điều kiện kiểm tra");*/

37: return true;

38: }

39: public static void doTest() {

40: IsBigWebQuery(s);

41: }

Hình 3.5. Chương trình Java kiểm thử.

22

Hình 3.9. Chương trình Java

Trong chương trình này, với hai xâu ngẫu nhiên nó sẽ rất khó thực hiện bất kỳ một trong bốn nhánh

của chương trình. Do đó nghiên cứu đặt ra là phải đưa ra các dữ liệu tốt nhất để thực thi chương trình này với

tất cả các nhánh có thể của nó. Để thực thi các nhánh này đầu tiên chúng ta cần xây dựng tất cả các ràng

buộc đường dẫn có thể có của chương trình. Trong chương trình này, có tất cả 12 điều kiện đường dẫn nhưng

nghiên cứu chỉ chọn hai điều kiện đường dẫn để minh họa cho nghiên cứu này. Điều kiện đầu tiên, nhánh

dòng 1 được lấy, tiếp theo là nhánh trên dòng 5. Nhánh trên dòng 9 để đáp ứng các luồng dữ liệu có thể này

theo các ràng buộc phải thỏa mãn.

Ràng buộc Cạnh

s1.startsWith(' ') s1.equals(s2 ) news1.endsWith('ab') s1.equals(s2) s1.indexOf (5) == ('a')

(startsWith, s1,‟˽‟) (equals, s1, s2) (notEndsWith, s3,”ab”) (notEquals, s1, s2) (indexOf , s1,‟a‟,5) (trim, s1, s3) Việc chọn điều kiện đường dẫn này dẫn đến chúng ta phải xây dựng đồ thị xâu được đưa ra tại hình

3.10 với các cạnh được đưa ra trong bảng trên.

Hình 3.10. Đồ thị xâu 1

Chạy bộ tiền xử lý trên đồ thị đã cho thấy ràng buộc tồn tại giá trị không thỏa mãn cho cặp cạnh

(equals,s1, s2 và notequals(s1,s2) bộ tiền xử lý sẽ kết luận UNSAT và một điều kiện đường dẫn mới sẽ được lựa chọn.

23

Giả sử điều kiện đường dẫn tiếp theo là trường hợp dòng 1, 3, 9 hay s1 phải được bắt đầu bằng kí tự trắng và bằng s2 sau khi đước cắt các khoảng trắng ở hai đầu. phải kết thúc bằng xâu “ab” và có kí tự thứ 5 là kí tự „a‟ do vậy sẽ tạo ra ràng buộc.

Ràng buộc Cạnh

s1.startsWith(' ') s1.equals(s2 ) news1.endsWith('ab') s1.indexOf (5) == ('a') (startsWith, s1,‟˽‟) (equals, s1, s2) (endsWith, s3,”ab”) (indexOf , s1,‟a‟,5) (trim, s1, s3)

Điều kiện đường dẫn này sẽ tương ứng với đồ thị xâu:

Hình 3.11. Đồ thị xâu 2

Áp dụng tiền xử lý trên đồ thị xâu trên sẽ loại bỏ đỉnh s2 khỏi đồ thị xâu và sẽ ghi nhớ giải pháp của

s1 cũng là giải pháp của s2 khi các giải pháp được báo cáo ngược lại cho lời gọi

Các ràng buộc nguyên sau được thêm vào để chuẩn bị cho bộ giải ràng buộc kiểu nguyên và sẽ cho

ra giải pháp đầu tiên của nó. Theo như cách tiếp cận của nghiên cứu này, nó được gọi là dự đoán tốt nhất (li là độ dài của biến biểu trưng si): l1>0 l2>0 l3>0 l1=l2 l3 l3 l1 1 l1>5 2 l1

Trước khi bắt đầu bộ giải xâu, bộ giải ràng buộc trên số nguyên được gọi để đưa ra bộ số nguyên cụ

thể thỏa mãn. Giả sử các giá trị này là l1=6, l2=6, l3=2 Các giá trị này là một giải pháp phù hợp vì chúng là các giá trị nhỏ nhất mà mỗi biến sẽ thỏa mãn ràng buộc.

Hãy xem xét cách tiếp cận Otomat đầu tiên thực hiện ánh xạ từng xâu si biểu trưng cho Otomat Mi.

Mỗi Otomat được khởi tạo để chứa tất cả các từ có độ dài li do đó M1=…… và M3=…

Ta thực hiện duyệt qua từng cạnh của đồ thị.

i.

startsWith(s1,‟˽‟) M1 sẽ giao với ngôn ngữ „˽‟.* và gán lại cho M1. Kết quả được gán cho M1 là: ˽…..

ii.

iii.

trim(s1,s3) M1 sẽ giao với ngôn ngữ của M3 trong đó M3 là các từ có khoảng trắng ở đầu vào cuối M1 ˽.* M3 ˽.* do vậy ngôn ngữ của M1 là: ˽….., M3 sẽ giao với ngôn ngữ của M1 sau khi loại bỏ các khoảng trắng ở hai đầu do đó ngôn ngữ của M3 sẽ là: [a-b],[b-a] indexOf(s1,‟a‟,5) M1 giao với ngôn ngữ ….a.* và kết quả của phép giao được gán cho M1 là: ˽….a

iv. endsWith(s3,”ab”) M3 giao với ngôn ngữ “ab”. Kết quả ngôn ngữ của M3 là “ab”.

Tương tự với các bước đã thực hiện bên trên sau khi thực hiện duyệt qua các cạnh sẽ cho kết quả là

M1= ˽….a. và M3=ab. sẽ cho chúng ta kết quả cuối cùng là

s1,s3 sẽ là “˽ ˽ ˽ ˽ ˽ab” và s3 là “ab”

Chuyển sang cách tiếp cận Bitvector chúng ta sẽ trở lại dự đoán tốt nhất l1=6, l2=6, l3=2 hai biến

Bitvector b1 và b3 được khởi tạo tương ứng với độ dài là 6 và 2, duyệt qua từng cạnh của đồ thị.

i. startsWith(s1,‟˽‟) sẽ sinh ra ràng buộc tương ứng là b1[0]= ‟˽‟ được thêm vào

24

ii.

‟˽‟ ‟˽‟ và b3[1]

iii.

‟a‟ ‟a‟ b1[2] ‟a‟ b1[1]

‟a‟. ‟a‟ b1[4]

iv. ‟b‟ ‟a‟ trim(s1,s3) một vài ràng buộc được thêm vào b1[i]=b3[0] b1[i+1]=b3[1] trong đó i=0,i

Sau mỗi cạnh chúng ta đẩy ràng buộc vào ngăn xếp giải ràng buộc Bitvetor. Nó sẽ có kết quả SAT

hoặc UNSAT. Khi ràng buộc endsWith được đẩy vào nó sẽ cho kết quả là UNSAT do b1 kết thúc bởi kí tự „a‟ và b3 kết thúc bởi kí tự „b‟. Khi UNSAT đã nhận được từ bộ giải bitvector và thêm ràng buộc mới l1 6 l3 2, trạng thái của bộ giải bị xóa và quá trình chuyển đổi sẽ bắt đầu lại từ cạnh đầu tiên. Một số dự đoán tốt nhất có thể được thực hiện. Xem xét trường hợp l1=7 l2=7, l3=2 trong lần này sự chuyển đổi sẽ giống với các lần lặp trước. Thực tế, biến b1 này sẽ kết thúc là kí tự b và bộ giải Bitvector sẽ báo là SAT. Các câu lệnh gán thỏa mãn có thể là s1 và s3 sẽ là “˽ ˽ ˽ ˽ ˽ab” và s3 là “ab” sẽ được trả về. 3.6. Kết luận chƣơng 3

Chương này của luận án đã trình bày đề xuất liên quan đến giải ràng buộc xâu trong thực thi biểu

trưng. Từ các khái niệm đồ thị xâu, giải ràng buộc xâu dựa trên phương pháp Otomat và phương pháp

BitVector. Đồng thời, chương này cũng đề xuất một mô hình giải ràng buộc xâu dựa trên Otomat và phân

tích đánh giá kết quả cũng được trình bày trong chương này.

KẾT LUẬN VÀ KIẾN NGHỊ

Luận án nghiên cứu tổng quan về kỹ thuật thực thi biểu trưng trong sinh tự động các ca kiểm thử, từ đó

lựa chọn bài toán cải tiến bộ giải ràng buộc xâu nhằm tăng khả năng giải ràng buộc, áp dụng trong sinh tự

động các ca kiểm thử trên kiểu dữ liệu xâu.

Nhằm tiếp tục các kết quả của luận án, các nghiên cứu trong thời gian tới có thể được thực hiện theo

các hướng sau:

Tiếp tục nghiên cứu, đề xuất các thuật toán nhằm tăng khả năng giải giải ràng buộc trên kiểu dữ liệu

xâu ứng dụng trong sinh dữ liệu kiểm thử .

Cài đặt ứng dụng trên các ngôn ngữ khác, mở rộng quy mô áp dụng trên các dự án phần mềm cụ thể.

Mặc dù đã tập trung nghiên cứu và trình bày báo cáo, luận án vẫn không tránh khỏi một số hạn chế

như: Chương trình sinh ca kiểm thử dựa trên kỹ thuật thực thi biểu trưng trên ngôn ngữ Java mới chỉ giới hạn

trên số loại chương trình nhất định, chưa có điều kiện áp dụng trên những dự án có quy mô lớn, việc đánh giá

so sánh còn hạn chế.

NHỮNG ĐÓNG GÓP MỚI CỦA LUẬN ÁN

Mô hình hóa ràng buộc dưới dạng đồ thị xâu từ đó thực hiện đơn giản hóa ràng buộc hoặc phát hiện

các ràng buộc không tồn tại giá trị thỏa mãn nhằm giảm bớt thời gian giải ràng xâu và ràng buộc hỗn hợp.

Đề xuất thuật toán giải ràng buộc dựa trên kết quả ở bước tiền xử lý trên hai phương pháp tiếp cận

Otomat và Bitvector từ đó sinh dữ liệu kiểm thử trong trên kiểu dữ liệu xâu.

Thực nghiệm các thuật toán đã đề xuất, luận án đã thực hiện mở rộng Java Path Finder để cài đặt mô

hình hóa ràng buộc sử dụng đồ thị xâu và giải tràng buộc trên ngôn ngữ Java. Kết quả thực nghiệm được

thực hiện trên một số phép toán xâu điển hình đã chỉ ra một số kết quả nhất định.

25

DANH MỤC CÔNG TRÌNH CỦA TÁC GIẢ

[CT1]. Hà Thị Thanh, Tô Hữu Nguyên, Nguyễn Hồng Tân, Nguyễn Văn Việt, Nguyễn Lan Oanh (2013), “Ứng dụng giải thuật di truyền vào sinh testcase hiệu quả”, Tạp chí Khoa học và công nghệ - Đại học Thái Nguyên, Tập 110, số 10, trang 131-135. [CT2]. Tô Hữu Nguyên, Nguyễn Hồng Tân, Hà Thị Thanh, Đỗ Thanh Mai (2016), “Thực thi tượng trưng trong sinh tự động dữ liệu kiểm thử phần mềm”, Tạp chí khoa học đại học Đà Lạt, Tập 6, Số 2, trang 258– 178. [CT3]. To Huu Nguyen, Tran Thi Ngan, Do Thanh Mai, Tran Manh Tuan (2016), “A novel symbolic execution model in automated generation of test cases”, International Research Journal of Engineering and Technology (IRJET), Volume: 03 Issue: 07. Page 1-7. [CT4]. Tô Hữu Nguyên, Đỗ Thanh Mai, Nguyễn Hồng Tân(2016), “Kỹ thuật mô hình hóa ràng buộc hỗn hợp và phương pháp giải ràng buộc xâu trong thực thi tượng trưng”, Tạp chí Khoa học và Công nghệ, Đại học Thái Nguyên, 159(14), tr.141-147 [CT5]. To Huu Nguyen, Tran Thi Ngan (2020), Finding new integer constraints incorporated with string constraints using automata in symbolic execution, International Research Journal of Engineering and Technology (IRJET), Volume 7, Issue 6, pp. 4144 – 4148. [CT6]. To Huu Nguyen, Nguyen Truong Thang, Dang Van Duc (2020), Mixed constraint solvers in symbolic execution using multi-track automata, International Journal of Latest Engineering Science (IJLES), Volume: 03 Issue: 04