Luận á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

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 (charAt,sa,n,x) Ma= Ma [n] {x} [*] Sa[n]=x (concat,sa,sb,sx) Ma= Ma substring(Mx,0,la) Mb=Mb subString(Mx,lb, ) Mx=Mx (Ma Mb) (sa=sx[la:0]) (sb=sx[lx:la]) (indexOf, sa,sb,x) Ma= Ma ([x] Mb) Mb [*] Mb=Mb substrings(Ma,x,x+lb (sa[x+lb:x]=sb) sa[i+lb:i ] sb, i,0 i<x) 67 ) (lastIndexOf, sa,sb,x) Ma= Ma [*] Mb ([x+lb] ] ([*] Mb [*])) Mb= Mb substrings(Ma,x,x+lb) (sa[x+lb:x]=sb) (sa[i+lb:i] s b, , i x<i la-lb) substring(sa,n,sx) Ma= Ma [n] Mx Mx= Mx substring(Ma,n,∞) sa[n+lx:n]=sx substring(sa,n,k,sx) Ma= Ma [n] Mx [*] Mx= Mx substring(Ma,n,k) Sa[n+lx:n]=sx trim(sa,sx) Ma= Ma [„˽‟,*] Mx [„˽‟,*] Mx= Mx trim(Ma) (sx[0] ˽) sx[lx-1] „˽‟) (sa[j]= „˽‟ (sa[i+lx:i]=sx) (sa[k]= „˽‟), i,j,k |(0 i la- lx) (0 j i) (i+lx k<la)) (contains, sa,sb) Ma= Ma [*] Mb [*] Mb= Mb substring(Ma,0,∞) 0 i<la-lb sa[i+lb:i]=sb (endsWith, sa,sb) Ma= Ma [*] Mb Mb=suffises(Ma) sa[la:la-lb]=sb (startsWith, sa,sb) Ma:= Ma Mb [*] Mb:=prefixes(Ma) sa[lb:0]=sb 3.3. Giải ràng buộc xâu dựa trên phƣơng pháp sử dụng OTOMAT Định nghĩa 3.2: Một otomat hữu hạn đơn định (Deterministic Finite Automata- DFA) là một bộ năm: A = , trong đó: + Q là một tập hữu hạn khác rỗng, đƣợc gọi là tập các trạng thái. + Σ là một bảng chữ cái, đƣợc gọi là bảng chữ vào. + δ: D →Q, là một ánh xạ từ D vào Q, trong đó D ⊆Q × Σ, đƣợc gọi là hàm chuyển trạng thái (hay hàm chuyển); + q0 ∈Q, đƣợc gọi là trạng thái khởi đầu. + F ⊆Q đƣợc gọi là tập các trạng thái kết thúc. 68 Trong trƣờng hợp D = Q × Σ, ta nói A là otomat đầy đủ. Sau này ta sẽ thấy rằng mọi otomat hữu hạn đều đƣa về đƣợc otomat hữu hạn đầy đủ tƣơng đƣơng. Hoạt động của otomat hữu hạn đơn định A = khi cho xâu vào ω= a1a2 an có thể đƣợc mô tả nhƣ sau: Khi bắt đầu làm việc, otomat ở trạng thái khởi đầu q0 và đầu đọc đang nhìn vào ô có ký hiệu a1. Tiếp theo otomat chuyển từ trạng thái q0 dƣới tác động của ký hiệu vào a1về trạng thái mới δ(q0, a1) = q1∈Q và đầu đọc chuyển sang phải một ô, tức là nhìn vào ô có ký hiệu a2. Sau đó otomat A có thể lại tiếp tục chuyển từ trạng thái q1 nhờ hàm chuyển δ về trạng thái mới q2 = δ(q1, a2) ∈Q. Quá trình đó sẽ tiếp tục cho tới khi gặp một trong các tình huống sau:  Otomat A đọc hết xâu vào ωvà δ(qn-1,an) = qn ∈F, ta nói rằng A đoán nhận xâu ω.  Hoặc otomat A đọc hết xâu vào ωvà δ(qn-1,an) = qn ∉F, ta nói A không đoán nhận xâu ω.  Hoặc khi otomat A đọc đến aj ,(j ≤n) và hàm δ(qj-1, aj) không xác định, ta cũng nói không đoán nhận xâu ω. Định nghĩa 1.2. Cho otomat hữu hạn không đơn định A = , ω ∈ Σ* và L là một ngôn ngữ trên Σ. Ta nói: − ω đƣợc đoán nhận bởi A nếu δ(q0, ω) ∩F ≠ ∅; −L đƣợc đoán nhận bởi A nếu L = {ω∈Σ* | δ(q0, ω) ∩F ≠ ∅} và ký hiệu L là T(A). Otomat hữu hạn là lựa chọn tự nhiên phù hợp dùng cho biểu diễn xâu. Ngôn ngữ của Otomat là một tập các từ mà Otomat có thể đoán nhận tƣơng đƣơng với tập các biến xâu có thể thỏa mãn thỏa mãn một ràng buộc. Các ràng buộc tự chúng tƣơng đƣơng với các toán tử Otomat. Giải ràng buộc dựa trên Otomat đƣợc chỉ ra tại Hình 3.5. Trong đó, Otomat Mi đƣợc xây dựng cho mỗi đỉnh si của đồ thị xâu. Với các biến li đƣợc khởi tạo giá trị bởi bộ giải ràng buộc kiểu nguyên và do đó mỗi các ngôn ngữ đoán nhận bởi Otomat đƣợc xây dựng ở dòng 2 phải có độ dài cố định và các Otomat khác nhau có thể đoán nhận đƣợc các từ có độ dài khác nhau. 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 69 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13 StringGraph sg=(I S,E, Ʊ)) for( các đỉnh si S) Automaton Mi=[li]; W=E while W≠∅ W=W\e 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); 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 Giả sử rằng Ma,Mb là hai Otomat đại diện cho các đỉnh sa,sb tƣơng ứng, ta sẽ cập nhật lại cho hai Otomat trên nhƣ sau: Ma=Ma ([ ].Mb.[ ]); Mb=Mb substring(Ma,i,j) (i<j≤la) Hay nói một cách khác với bất kỳ một tập từ nào mà Ma đang đoán nhận, nó sẽ đƣợc giới hạn lại cho những từ mà nó bao gồm sb nhƣ là một xâu con. Tƣơng tự nhƣ vậy, với bất kỳ tập từ nào mà Mb đang đoán nhận, nó sẽ giới hạn lại cho những từ là xâu con con của Ma. Tƣơng tự đối với các phép toán khác. Đố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. CheckNegativeEdges(pathcondition pc, StringGraph sg, (M1,M2..)) 1: i=1; M‟1=M1; M‟2=M2; M‟k=Mk; 2: while(1≤i<k) 70 3: if(Mi=∅) 4: Mi=M‟I; 5: i=i-1; 6: else 7: vi=a Mi; 8: Mi=Mi\{a}; 9: for( với mỗi ei E và last(e)=si) 10: if(e là vi phạm với vi) 11: Break;\\ quay lại dòng 2 12: i=i++; 13 return; Hình 3.2. Phương thức giải ràng buộc phủ định Khởi tạo W bao gồm tất cả các cạnh của đồ thì xâu, sau đó các cạnh đƣợc lần lƣợt gỡ bỏ và đƣa vào xử lý. Bất cứ thay đổi nào của Mi sẽ làm cho những cạnh kết nối với Si đƣợc đƣa vào W một lần nữa. Cuối cùng mặc dù thuật toán phải kết thúc và tất cả các Otomat thay đổi theo kiểu Mi=Mi X. Nói ngắn gọn ngôn ngữ của mỗi Otomat sẽ đƣợc giữ nguyên không thay đổi hoặc bị rút gọn trong mỗi câu lệnh gán, khi thuật toán kết thúc mỗi Otomat sẽ bao gồm chính xác những từ mà nó sẽ thỏa mãn ràng buộc. 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. 71 3.4.1 Mô hình hoá ràng buộc xâu sử dụng đồ thị Mô hình hoá 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 đã đƣợc trình bày và công bố trong công trình CT[4] của nghiên cứu sinh. 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: 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: Với mỗi chƣơng trình máy tính, mô hình tiến hành thu thập các đỉnh, các cạnh để tạo thành đồ thị luồng. Trong đó, một đỉnh trong đồ thị luồng có thể chứa phƣơng thức hoặc tên biến. Một đỉnh cũng chứa một giá trị cụ thể và một ID duy nhất. Đồ thị luồng này sẽ đƣợc đƣa qua một bộ xử lý. Mục đích của bộ xử lý này nhằm duyệt đồ thị luồng để tạo ra các ràng buộc đƣờng dẫn. Các ràng buộc đƣờng dẫn này đƣợc gửi đến bộ giải ràng buộc. Đồ thị ràng buộc đƣợc xử lý bằng một thuật toán duyệt đồ thị 72 cụ thể (duyệt đồ thị theo chiều rộng, duyệt theo chiều sâu hoặc phƣơng pháp Heuristic). Hai trƣờng hợp sau đƣợc thực hiện: - Đầu vào là các giá trị rời rạc đƣợc xác định, chƣơng trình đƣợc kiểm thử bằng công cụ kiểm thử thông thƣờng. - Với đầu vào là biểu trƣng, các ràng buộc đƣờng dẫn đƣợc xác định. Áp dụng bộ giải ràng buộc xâu để tiến hành kiểm thử theo phƣơng pháp thực thi biểu trƣng. 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 10 với RAM 8 GB, sử dụng công cụ mã nguồn mở JavaPathFinder đƣợc tải tại: và phần mềm Eclipse Java EE IDE Cài đặt thực nghiệm Thuật toán giải ràng buộc đƣờng dẫn đƣợc trình bày cụ thể trong Hình 3.4 dòng 2 tạo ra một hình thức trung gian của biểu thức ràng buộc đƣờng dẫn và gọi hình thức trung gian này là đồ thị xâu. Dòng 4 chỉ ra rằng thuật toán sẽ đƣợc lặp lại cho đến khi tìm đƣợc giá trị thỏa mãn hoặc đã vƣợt quá thời gian giới hạn. Dòng 5 cung cấp bộ giá trị số nguyên phỏng đoán tốt nhất. Dòng 6 chuyển đổi ràng buộc sang đồ thị xâu (đƣợc chuyền kèm theo các giá trị cụ thể là các giá trị phỏng đoán tốt nhất) sang các phép toán của Otomat hoặc Bitvectors. SOLVE(PathCondition pc) 1: StringGraph sg 73 2: (pc,sg)←BuildStringGraph(pc); 3: boolean sat←false; 4: 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 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. Các số nguyên cụ thể phỏng đoán tốt nhất thực ra là các giái trị nguyên thỏa mãn tất cả các ràng buộc kiểu nguyên và có thể là tất cả các ràng buộc hỗn hợp. Chỉ khi các ràng buộc xâu đƣợc xem xét trong giai đoạn chuyển đổi tại bƣớc 4 thì mới có thể xác định đƣợc số nguyên phỏng đoán có thỏa mãn tất cả các ràng buộc hỗn hợp hay không. Phần khởi tạo của thuật toán quan tâm đến xây dựng đồ thị xâu biểu diễn cho ràng buộc xâu và chuẩn bị bộ giải ràng buộc cho kiểu số nguyên để cung cấp giá trị phỏng đoán tốt nhất đầu tiên. Theo nhƣ quy trình lặp gồm hai bƣớc. 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ể và 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. Trong trƣờng hợp này, bộ giải ràng buộc xâu là Otomat hoặc Bitvector và có thể ràng buộc của đồ thị xâu không tồn tại giá trị thỏa mãn để nhận đƣợc các giá trị mong muốn. Khi đó, bộ giải ràng buộc xâu sẽ thêm vào các ràng buộc mới cho điều kiện đƣờng dẫn và quá trình đƣợc lặp lại. Ngay cả khi vấn đề xâu đƣợc quyết định và có sự kết hợp của bộ giải số nguyên và bộ giải xâu không đƣa ra đƣợc giải pháp cho sự thỏa mãn ràng buộc hỗn 74 hợp. Để đảm bảo thuật toán đƣợc kết thúc một giới hạn trên đƣợc đƣa ra và áp dụng cho độ dài xâu biểu trƣng. 1. Đối với bất kỳ ràng buộc dƣờng dẫn thỏa mãn nào yêu cầu một xâu mà có độ dài lớn khi đó định nghĩa về giới hạn sẽ không thực hiện giải và thuật toán sẽ kết luận rằng ràng buộc đƣờng dẫn là không thỏa mãn. 2. Thời gian cũng cần phải đƣợc chỉ định để ngăn bộ giải dùng quá nhiều thời gian cho các điều kiện ràng buộc của những đƣờng đi phức tạp không cần thiết, và nếu vƣợt quá thời gian điều kiện đƣỡng dẫn đƣợc phân loại là không tồn tại giá trị thỏa mãn. Các phần phụ thuộc, theo nhƣ miêu tả của đồ thị xâu, là cấu trúc và tiền xử lý. Một mô tả về cách tiếp cận đƣợc sử dụng để chuyển đổi từ đồ thị xâu sang các phép toán Otomat hoặc ràng buộc Bitvector đƣợc đƣa ra. Cuối cùng, một ràng buộc mới đƣợc sinh ra khi ràng buộc xâu không tồn tại giá trị thỏa mãn và thông tin này đƣợc đƣa trở lại cho bộ giải ràng buộc số nguyên. Để đánh giá kết quả cài đặt, luận án này thực nghiệm sinh các ca kiểm thử trên một chƣơng trình Java (Hình 3.8) cho các phép toán điển hình của java.lang.String. nhƣ:.lastIndexOf(“s”), contains(String s),.substring (int k),.substring(int i, int j), startsWith(String st). Đồng thời, việc đánh giá có sử dụng phƣơng pháp tiếp cận Otomat thực hiện kiểm tra trên một số phép toán xâu và sinh test case dựa trên thực thi thực biểu trƣng trên các phép toán này. 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: public static String s = ""; private static boolean IsBigWebQuery(String str) { // (1) Kiểm tra xem xâu sau dấu „/‟ cuối cùng có // chứa "BigWeb" hay không int lastSlash = str.lastIndexOf('/'); if (lastSlash < 0) { return false; } String rest = str.substring(lastSlash + 1); if (!rest.contains("BigWeb")) { return false; } // (2) Kiểm tra xem xâu s có bắt đầu bằng //"http://" if (!str.startsWith("http://")) { 75 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: 36: 37: 38: 39: 40: 41: 42: 43: 44: 45: return false; } // (3) lấy về xâu giữa của xâu "http://" và ký // tự //cuối cùng của kí tự "/" và nếu nó bắt đầu bằng // “www”. Tiến hành loại bỏ chúng String t = str.substring("http://".length(), lastSlash); if (t.startsWith("www.")) { t = t.substring("www.".length()); } // (4) Kiểm tra sau khi loại bỏ “www” chúng có // chứa " other.com " hoặc "google.com" if (!(t.equals("other.com")) && !(t.equals("google.com"))) { return false; } // Xâu s đã thỏa mãn tất cả các kiểm tra //throw new RuntimeException("Xâu đã cho thỏa //mãn các điều kiện kiểm tra");*/ return true; } public static void doTest() { IsBigWebQuery(s); } Hình 3.5. Chương trình Java kiểm thử Chƣơng trình sinh test-case chạy trên Java PathFinder Eclipse (Hình 3.6) đƣợc trình bày kết hợp với công cụ Junit đƣợc trình bày nhƣ dƣới đây: 76 Hình 3.6. Kết quả sinh dữ liệu biểu trưng trên một số phép toán trên xâu Một cải tiến của JPF (ShadowJPF) áp dụng ý tƣởng thực thi biểu trƣng [75] trên mã byte Java và do đó, thực thi biểu trƣng shadow có sẵn cho một loạt các chƣơng trình Java. Luận án đã thực hiện các thử nghiệm sơ bộ trên 51 đột biến đƣợc tạo và so sánh kết quả với Symbolic Path Downloader và ShadowKLEE thực hiện ban đầu. Chúng cho thấy ShadowJPF có thể giảm đáng kể số lƣợng trƣờng hợp thử nghiệm so với SPF và nó hoạt động giống nhƣ cách triển khai ban đầu trong ShadowKLEE. Mặc dù những kết quả này rất hứa hẹn, các đối tƣợng đƣợc phân tích là tƣơng đối nhỏ, và do đó, chúng ta không thể khái quát kết quả cho các ví dụ lớn hơn và trong thế giới thực. Trong tƣơng lai, Nghiên cứu này có kế hoạch mở rộng triển khai và xây dựng trên ShadowJPF một công cụ mạnh hơn để tạo ra các trƣờng hợp kiểm tra hồi 77 quy. Điều này bao gồm tự động hóa hoàn toàn ghi chú thay đổi, hiện đang đƣợc thực hiện thủ công. Ngoài ra, luận án này muốn mở rộng đánh giá bằng cách thêm nhiều lớp tƣơng thích JPF và lỗi hồi quy trong thế giới thực vào phân tích của nghiên cứu này. Thuật toán 1: Thực thi biểu trƣng shadow của IADD trên dữ liệu Bytecode 1: op_v1 ← Đối tượng thuộc tính của toán hạng thứ nhất; 2: op_v2 ← Đối tượng thuộc tính của toán hạng thứ hai; 3: if then 4: return super.execute(); 5: else 6: stack.pop(); 7: stack.pop(); 8: stack.push(0); 9: if op_vi (i ∈ 1, 2) instanceof DiffExpression then 10: sym_vi ← op_vi.getSymbc(); 11: shadow_vi ← op_vi.getShadow(); 12: else 13: sym_vi ← op_vi; 14: shadow_vi ← op_vi; 15: sym_r ← sym_v1 + sym_v2; 16: shadow_r ← shadow_v1 + shadow_v2; 17: if op_v1 or op_v2 instanceof DiffExpression then 18: result ← new DiffExpression(shadow_r,sym_r); 19: else 20: result ← sym_r; 21: setAttributeObject(result); 22: return nextInstruction(); Chƣơng trình: 78 Hình 3.7. Code kiểm thử Kết quả trong Bảng 3.2 cho thấy kết quả chi tiết của các thí nghiệm đƣợc thực hiện. Cột đầu tiên đặt tên cho lớp và phƣơng thức tƣơng ứng đã đƣợc thử nghiệm, cùng với một id chỉ định từng biến thể. Cột Type chứa toán tử đột biến đƣợc điều chỉnh bởi việc thay thế toán tử quan hệ (ROR), Thay thế toán tử số học (AOR) và Xóa câu lệnh (STD). Vì Major chỉ tạo các đột biến đơn cho mỗi lớp, luận án cũng kết hợp chúng theo cách thủ công để có nhiều thay đổi cho mỗi lớp. Trong những trƣờng hợp nhƣ vậy, các số ở cuối mỗi tên đối tƣợng biểu thị các đột biến kết hợp (luận án này đặt tên loại là MUL cho nhiều thay đổi). Các cột sau mô tả thời gian thực hiện (tính bằng giây), số trạng thái đƣợc truy cập trong quá trình khám phá biểu trƣng, bộ nhớ đƣợc sử dụng tối đa (tính bằng MB) và số PC kết quả. Số trong ngoặc cho SPF biểu thị số lƣợng đƣờng dẫn là diff cho thực thi biểu trƣng thông thƣờng (SPF), cho thực thi biểu trƣng shadow với phần mở rộng SPF ShadowJPF (SWPF) của luận án và cho công cụ ban đầu ShadowKLEE (SW). Hàng đầu tiên của bảng hiển thị kết quả thực hiện chi tiết cho phƣơng thức foo (). 79 Bảng 3.2. Kết quả đánh giá mô hình cải tiến trên bộ dữ liệu SPF SWPF SPF SWPF SPF SWPF SPF SWPF SW Foo - 2 2 16 17 434 690 4(2) 2 2 BankAccount deposit_1 ROR <1 <1 4 19 245 245 2(0) 1 1 BankAccount deposit_2 ROR <1 <1 4 16 245 245 2(0) 1 1 BankAccount deposit_3 ROR <1 <1 2 10 245 245 1(0) 1 1 BankAccount deposit_4 STD <1 <1 4 7 245 245 2(0) 1 1 BankAccount deposit_5 AOR <1 <1 4 5 245 245 2(0) 0 0 BankAccount deposit_6 AOR <1 <1 4 5 245 245 2(0) 0 0 BankAccount deposit_7 AOR <1 <1 8 9 245 245 3(1) 1 1 BankAccount deposit_8 STD 1 1 4 5 245 245 2(0) 0 0 BankAccount deposit_1 ROR <1 <1 6 19 245 245 3(0) 1 1 BankAccount deposit_2 ROR <1 <1 6 19 245 245 3(0) 1 1 BankAccount deposit_3 ROR <1 <1 4 9 245 245 2(0) 2 2 BankAccount deposit_4 STD <1 <1 8 9 245 245 4(2) 2 2 BankAccount deposit_5 ROR <1 <1 6 22 245 245 3(0) 1 1 BankAccount deposit_6 ROR <1 <1 6 22 245 245 3(0) 1 1 BankAccount deposit_7 ROR <1 <1 4 10 245 245 2(0) 1 1 BankAccount deposit_8 STD <1 <1 6 8 245 245 3(0) 0 0 BankAccount deposit_9 AOR <1 <1 6 8 245 245 3(0) 0 0 BankAccount deposit_10 AOR <1 <1 6 8 245 245 3(0) 0 0 BankAccount deposit_11 AOR <1 <1 8 12 245 245 4(2) 1 0 BankAccount deposit_12 STD <1 <1 6 8 245 245 3(0) 0 0 BankAccount deposit_1 ROR 2 <1 24 52 433 245 4(0) 1 1 BankAccount deposit_2 ROR 2 <1 24 52 690 245 4(0) 1 1 BankAccount deposit_3 ROR 2 <1 16 26 434 245 3(0) 1 1 BankAccount deposit_4 STD 3 <1 24 17 690 245 4(1) 1 1 BankAccount deposit_5 AOR 3 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_6 AOR 3 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_7 AOR 3 <1 32 22 690 245 5(0) 0 0 BankAccount deposit_8 STD 3 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_9 ROR 2 <1 24 58 434 245 4(0) 1 1 BankAccount deposit_10 ROR 3 <1 24 58 690 245 4(0) 1 1 BankAccount deposit_11 ROR 1 <1 16 26 434 245 3(0) 1 1 BankAccount deposit_12 STD 3 <1 24 17 690 245 4(0) 1 1 BankAccount deposit_13 ROR 3 <1 24 20 690 245 4(1) 0 0 BankAccount deposit_14 ROR 3 <1 24 20 690 245 4(0) 0 0 BankAccount deposit_15 ROR 3 <1 20 11 434 245 4(1) 1 1 BankAccount deposit_16 STD 3 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_17 AOR 2 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_18 AOR 2 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_19 AOR 3 <1 28 22 690 245 5(0) 1 0 BankAccount deposit_20 STD 2 <1 24 14 690 245 4(0) 0 0 BankAccount deposit_21 STD 3 <1 24 17 690 245 4(0) 0 0 BankAccount deposit_22 ROR 1 <1 8 15 309 245 2(2) 2 2 BankAccount deposit_23 ROR 1 <1 8 15 309 245 2(2) 2 2 time[s] #State Memory[MB] #Path(difs] Subject type Mô hình kiểm thử đột biến trên các chương trình C#: Trong thời gian gần đây, ngôn ngữ C# là một trong những ngôn ngữ đƣợc sử dụng rộng rãi để phát triển các ứng dụng, C# là phiên bản cao của C. Trong phần này, quy trình áp dụng kỹ thuật kiểm thử đột biến cho các ứng dụng đƣợc phát triển dùng C# đƣợc trình bày. Quy trình ứng dụng kiểm thử đột biến để kiểm thử các chƣơng trình C-Sharp áp dụng kỹ thuật kiểm thử đột biến lựa chọn và sử dụng công cụ Nester, dùng để phân tích và tạo đột biến, và công cụ NUnit dùng để kiểm thử đơn vị. Quy trình này đƣợc minh họa trong Hình 3.8. 80 Hình 3.8. Kết quả đánh giá mô hình cải tiến trên bộ dữ liệu Các hệ thống kiểm thử đột biến truyền thống tạo ra số lƣợng lớn các chƣơng trình đột biến. Ví dụ, có 385 đột biến đƣợc tạo ra cho thủ tục tìm nghiệm theo phƣơng pháp Newton gồm 18 dòng lệnh. Phân tích cho thấy rằng số lƣợng các đột biến tạo ra xấp xỉ bằng tích của số các tham chiếu dữ liệu và số các đối tƣợng dữ liệu. Do đó, số lƣợng đột biến sẽ làm tăng tính phức tạp của chƣơng trình. Điều này làm tăng chi phí thực thi do mỗi đột biến phải thực thi với ít nhất một ca kiểm thử. Nhƣ vậy, chi phí là chấp nhận đƣợc cho nghiên cứu ở các trƣờng (đại học, học viện, ) với các ràng buộc về thời gian có thể linh hoạt, nhƣng trong công nghiệp sự lãng phí này là không thể. Mặt khác, các hệ thống truyền thống phải thông dịch các chƣơng trình đột biến nên thực tế thời gian chạy sẽ lâu hơn. Điều này gây ra nhiều bất tiện, nó làm cho các hệ thống thực hiện chậm và rất khó để mô phỏng môi trƣờng hoạt động. Để khắc phục những chi phí liên quan với đột biến, các nghiên cứu hầu hết đã tập trung vào một số phƣơng pháp làm ít hơn, làm nhanh hơn mà không làm giảm khả năng phát hiện lỗi. 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 sáng 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‟}. 81 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 và 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à khi 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‖ mặt khác nếu hai tham số không bằng nhau. Cuối cùng nhánh cuối cùng nằm trên dòng 9 nếu kí tự thứ năm của biến xâu đầu tiên bằng kí tự ‗a‟. 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 và 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 và cuối cùng là 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(' ') (startsWith, s1,‟˽‟) s1.equals(s2 ) (equals, s1, s2) news1.endsWith('ab') (notEndsWith, s3,”ab”) s1.equals(s2) (notEquals, s1, s2) 82 s1.indexOf (5) == ('a') (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. Giả sử điều kiện đƣờng dẫn tiếp theo là trƣờng hợp dòng 1, 3, 9 hay s1 là 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(' ') (startsWith, s1,‟˽‟) s1.equals(s2 ) (equals, s1, s2) news1.endsWith('ab') (endsWith, s3,”ab”) s1.indexOf (5) == ('a') (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: 83 Hình 3.11. Đồ thị xâu 2 Áp dụng tiền xử lý và đồ 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 2 l1 l3 l1 1 l1>5 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 và kết quả đƣợc gán cho M1 là: ˽.. ii. trim(s1,s3) M1 sẽ giao với ngôn ngữ của M3 trong dó M3 là ngôn ngữ 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] 84 iii. 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‖. Theo cách tiếp cận của nghiên cứu này lặp lại trên mỗi cạnh lần thứ hai vì mỗi cạnh gây ra sự thay đổi cho một hoặc nhiều autoata do đó đã đƣợc đặt lại trong danh sách công việc dòng 12 trong hình 3.11 vì lợi ích của mối quan tâm duy nhất là các cạnh là đầu tiên, một lần nữa đi qua cạnh (trim,s1,s3) trong đó M1= ˽.a và M3=‖ab‖ ta sẽ thấy rằng giao của hai ngôn ngữ là rỗng. do M1 kết thúc bằng kí tự a và M3 kết thúc bằng kí tự b điều này dẫn đến bộ giải xâu trả về UNSAT và ràng buộc số nguyên mới đƣợc thêm vào với các ràng buộc số nguyên chuẩn bị đƣợc giải là: l1 6 l3 2 sẽ cho kết quả là l1=7 l2=7, l3=2. 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. Cạnh (trim,s1,s3) sẽ không làm cho kết quả của phép giao M1 và M3 bằng rỗng nhƣng sẽ làm thay đổi lại M1= ˽.ab và chọn giải pháp ngắn nhất có thể cho từng Otomat 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 ii. 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<b.length-1, ngoài ra b3[0] ‘˽‘ và b3[1] ‘˽‘ iii. indexOf(s1,‘a‘,5) ràng buộc b1[5]=‘a‘ đƣợc thêm vào để đảm bảo kí tự ‗a‘ ít nhất phải đƣợc ở vị trị thứ 5 của xâu s1 các ràng buộc sau đƣợc thêm vào b1[0] ‘a‘ b1[1] ‘a‘ b1[2] ‘a‘ b1[3] ‘a‘ b1[4] ‘a‘. iv. endsWith(s3,‖ab‖) khi đó các ràng buộc sau đƣợc thêm vào b3[0] ‘a‘ b3[1] ‘b‘ 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 đã 85 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 và thực tế là b1 biến này sẽ kết thúc là kí tự b và bộ giải Bitvector sẽ báo là SAT và trả lại 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‖. Ngoài ra, các bộ giải ràng buộc trong thực thi biểu trƣng còn sử dụng otomat đa rãnh CT[6]. Mô hình đƣợc xây dựng nhằm giải quyết các ràng buộc phức tạp (dƣới dạng một công thức đa biến). Trƣớc hết, các ràng buộc đầu vào phức tạp này đƣợc tách thành các công thức nhỏ hơn và tập các giải pháp hiện tại đƣợc khởi tạo là rỗng. Sau khi phân tách, mỗi công thức nhỏ đƣợc biểu diễn bởi một otomat đa rãnh. Mỗi rãnh trong otomat tƣơng ứng với một biến đầu vào. Sau đó, các dữ liệu tự động có cùng rãnh sẽ đƣợc kết hợp lại. Sau bƣớc kết hợp theo cùng biến đầu vào, tính tƣơng thích của các rãnh đã thay đổi đƣợc kiểm tra. Đồng thời, tập các giải pháp hiện tại đƣợc cập nhật. Mô hình đã đƣợc thực nghiệm trên các bộ dữ liệu xâu phức tạp, đồng thời, các kết quả cũng đƣợc tổng hợp. 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 phƣơng pháp giải ràng buộc xâu dựa trên Otomat cùng với sự kết hợp của các bộ giải số nguyên sẵn có và phân tích đánh giá kết quả cũng đƣợc trình bày trong chƣơng này. Nội dung chƣơng 3 là kết quả của các công trình nghiên cứu CT[4], CT[6] đã đƣợc công bố của nghiên cứu sinh. 86 KẾT LUẬN VÀ KIẾN NGHỊ Những kết quả chính của luận án: 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. Sau quá trình nghiên cứu, các đóng góp chính của luận án bao gồm: 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. Hƣớng phát triển của luận án: 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ế. 87 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 88 TÀI LIỆU THAM KHẢO [1]. Dibia, V., & Demiralp, Ç. (2019). Data2vis: Automatic generation of data visualizations using sequence-to-sequence recurrent neural networks. IEEE computer graphics and applications, 39(5), 33-46. [2]. Ed-Douibi, H., Izquierdo, J. L. C., & Cabot, J. (2018, October). Automatic generation of test cases for REST APIs: a specification-based approach. In 2018 IEEE 22nd International Enterprise Distributed Object Computing Conference (EDOC) (pp. 181-190). IEEE. [3]. Arcuri, A. (2019). RESTful API automated test case generation with EvoMaster. ACM Transactions on Software Engineering and Methodology (TOSEM), 28(1), 1-37. [4]. Nogueira, S., Araujo, H., Araujo, R., Iyoda, J., & Sampaio, A. (2019). Test case generation, selection and coverage from natural language. Science of Computer Programming, 181, 84-110. [5]. Amadini, R., Andrlon, M., Gange, G., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2019, June). Constraint Programming for Dynamic Symbolic Execution of JavaScript. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (pp. 1-19). Springer, Cham. [6]. Haijiang, Z., & Junhua, W. (2016). On Test Case Generation Based on Symbolic Execution and Hybrid Constraint Solving. Computer Applications and Software, 33(6), 23-26. [7]. Yoshida, H., Li, G., Kamiya, T., Ghosh, I., Rajan, S., Tokumoto, S., ... & Uehara, T. (2017). KLOVER: Automatic test generation for C and C++ programs, using symbolic execution. IEEE Software, 34(5), 30-37. [8]. Cashin, P., Martinez, C., Weimer, W., & Forrest, S. (2019, November). Understanding automatically-generated patches through symbolic invariant differences. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE) (pp. 411-414). IEEE. [9]. Liu, S. (2016, July). Testing-based formal verification for theorems and its application in software specification verification. In International Conference on Tests and Proofs (pp. 112-129). Springer, Cham. 89 [10]. Nötzli, A., Khan, J., Fingerhut, A., Barrett, C., & Athanas, P. (2018, March). P4pktgen: Automated test case generation for p4 programs. In Proceedings of the Symposium on SDN Research (pp. 1-7). [11]. Turpie, J., Reisner, E., Foster, J. S., & Hicks, M. (2011). Multiotter: Multiprocess symbolic execution. [12]. Uehara, T. (2016). Exhaustive Test-case Generation using Symbolic Execution. FUJITSU Sci. Tech. J, 52(1), 3440. [13]. Enoiu, E. P., Čaušević, A., Ostrand, T. J., Weyuker, E. J., Sundmark, D., & Pettersson, P. (2016). Automated test generation using model checking: an industrial evaluation. International Journal on Software Tools for Technology Transfer, 18(3), 335-353. [14]. Saddler, J. A., & Cohen, M. B. (2017, October). Eventflowslicer: A tool for generating realistic goal-driven gui tests. In 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (pp. 955- 960). IEEE. [15]. Gebizli, C. S., & Sözer, H. (2016, August). Model-based software product line testing by coupling feature models with hierarchical markov chain usage models. In 2016 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C) (pp. 278-283). IEEE. [16]. Clarke E. M., Grumberg O., & Peled D. (1999), Model checking, MIT press, pp. 209- 224. [17]. Cadar C., & Engler D. (2005, August), ―Execution generated test cases: How to make systems code crash itself‖, International SPIN Workshop on Model Checking of Software, Springer Berlin Heidelberg, pp. 2-23. [18]. Arcaini, P., Gargantini, A., & Riccobene, E. (2019). Fault‐based test generation for regular expressions by mutation. Software Testing, Verification and Reliability, 29(1-2), e1664. [19]. Chowdhury, S., Borle, S., Romansky, S., & Hindle, A. (2019). Greenscaler: training software energy models with automatic test generation. Empirical Software Engineering, 24(4), 1649-1692. [20]. Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2019). Model-based, mutation-driven test-case generation via heuristic-guided 90 branching search. ACM Transactions on Embedded Computing Systems (TECS), 18(1), 1-28. [21]. Luo, L. (2001), ―Software testing techniques‖, Institute for software research international Carnegie mellon university Pittsburgh, PA, 15232, pp. 1-19. [22]. Smaragdakis, Y., & Balatsouras, G. (2015). Pointer analysis. Foundations and Trends® in Programming Languages, 2(1), 1-69. [23]. Wang, F., & Gupta, S. (2019, April). Automatic test pattern generation for timing verification and delay testing of rsfq circuits. In 2019 IEEE 37th VLSI Test Symposium (VTS) (pp. 1-6). IEEE. [24]. Trần, T. L., & Bùi, T. D. (2012). Nghiên cứu và đề xuất các phương pháp kiểm thử giao diện phần mềm (Doctoral dissertation, Trƣờng Đại học Công nghệ. Đại học Quốc gia Hà Nội). [25]. Anand, S., Godefroid, P., & Tillmann, N. (2008, March). Demand-driven compositional symbolic execution. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 367-381). Springer, Berlin, Heidelberg. [26]. Ma, K. K., Phang, K. Y., Foster, J. S., & Hicks, M. (2011, September). Directed symbolic execution. In International Static Analysis Symposium (pp. 95-111). Springer, Berlin, Heidelberg. [27]. Staats, M., & Pǎsǎreanu, C. (2010, July). Parallel symbolic execution for structural test generation. In Proceedings of the 19th international symposium on Software testing and analysis (pp. 183-194). ACM. [28]. Kuznetsov, V., Kinder, J., Bucur, S., & Candea, G. (2012, June). Efficient state merging in symbolic execution. In Acm Sigplan Notices (Vol. 47, No. 6, pp. 193-204). ACM. [29]. DeMilli, R. A., & Offutt, A. J. (1991). Constraint-based automatic test data generation. IEEE Transactions on Software Engineering, (9), 900-910. [30]. Cadar C., Dunbar D., & Engler D. R. (2008), ―KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs‖, OSDI Vol. 8, pp. 209-224. [31]. King, J. C. (1976), ―Symbolic execution and program testing‖, Communications of the ACM, 19(7), pp. 385-394. 91 [32]. Godefroid, P., Klarlund, N., & Sen, K. (2005), ―DART: directed automated random testing‖, ACM Sigplan Notices, Vol. 40, No. 6, pp. 213-223. [33]. Xie, T., Tillmann, N., de Halleux, J., & Schulte, W. (2009), ―Fitness-guided path exploration in dynamic symbolic execution‖, 2009 IEEE/IFIP International Conference on Dependable Systems & Networks, IEEE, pp. 359- 368. [34]. Zhu, H., Hall, P. A., & May, J. H. (1997), ―Software unit test coverage and adequacy‖, ACM computing surveys (csur), 29(4), pp. 366-427. [35]. Sen, K., & Agha, G. (2006), Automated systematic testing of open distributed programs, In International Conference on Fundamental Approaches to Software Engineering, Springer Berlin Heidelberg, pp. 339-356. [36]. Godefroid, P., Levin, M. Y., & Molnar, D. A. (2008, February). Automated Whitebox Fuzz Testing. In NDSS, Vol. 8, pp. 151-166. [37]. Microsoft (2008), [38]. Microsoft (2008), 2008. [39]. Sen, K. (2006), Scalable automated methods for dynamic program analysis. [40]. Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., & Sundaresan, V. (1999, November), ―Soot-a Java bytecode optimization framework‖, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, IBM Press, pp. 13-20. [41]. Anand S., Orso A., & Harrold M. J. (2007), ―Type-dependence analysis and program transformation for symbolic execution‖, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp. 117-133. [42]. Sun Microsystems(2014), [43]. Andersen, L. O. (1994). Program analysis and specialization for the C programming language (Doctoral dissertation, University of Cophenhagen). [44]. Aquino, A., Braione, P., Denaro, G., & Salza, P. (2019). Facilitating program performance profiling via evolutionary symbolic execution. Software Testing, Verification and Reliability. 92 [45]. Hind, M. (2001, June). Pointer analysis: Haven't we solved this problem yet? In Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (pp. 54-61). ACM. [46]. Smaragdakis, Y., & Balatsouras, G. (2015). Pointer analysis. Foundations and Trends® in Programming Languages, 2(1), 1-69. [47]. Hossein Hojjat, Philipp Rümmer, and Ali Shamakhi. 2019. On Strings in Software Model Checking. In Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings (Lecture Notes in Computer Science), Anthony Widjaja Lin (Ed.), Vol. 11893. Springer, 19–30. [48]. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. 2014. String Constraints for Verification. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem (Eds.), Vol. 8559. Springer, 150–166. [49]. Pedro Barahona and Ludwig Krippahl. 2008. Constraint Programming in Structural Bioinformatics. Constraints 13, 1-2 (2008), 3–20 [50]. Prithvi Bisht, Timothy L. Hinrichs, Nazari Skrupsky, and V. N. Venkatakrishnan. 2011. WAPTEC: Whitebox analysis of web applications for parameter tampering exploit construction. In Proceedings of ACM Conference on Computer and Communications Security. ACM, 575–586. [51]. Roberto Amadini, Alexander Jordan, Graeme Gange, François Gauthier, Peter Schachte, Harald Søndergaard, Peter J. Stuckey, and Chenyi Zhang. 2017. Combining String Abstract Domains for JavaScript Analysis: An Evaluation. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. 41–57 [52]. Roberto Amadini, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2019. Constraint Programming for Dynamic 93 Symbolic Execution of JavaScript. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4-7, 2019, Proceedings (Lecture Notes in Computer Science), Louis-Martin Rousseau and Kostas Stergiou (Eds.), Vol. 11494. Springer [53]. Harris, A. (2019). Suitability of Finite State Automata to Model String Constraints in Probablistic Symbolic Execution. [54]. Roberto Amadini, Graeme Gange, and Peter J. Stuckey. 2018. Propagating Lex, Find and Replace with Dashed Strings. In Proc. 15th Int. Conf. Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (LNCS), W.-J. van Hoeve (Ed.), Vol. 10848. Springer [55]. Burnim J., & Sen K. (2008), ―Heuristics for scalable dynamic test generation‖, Proceedings of the 2008 23rd IEEE/ACM international conference on automated software engineering, IEEE Computer Society, pp. 443-446. [56]. Collingbourne, P., Cadar, C., & Kelly, P. H. (2011), ―Symbolic crosschecking of floating-point and SIMD code‖, Proceedings of the sixth conference on Computer systems. ACM, pp. 315-328. [57]. Ganesh, V., & Dill, D. L. (2007), ―A decision procedure for bit-vectors and arrays‖, International Conference on Computer Aided Verification, Springer Berlin Heidelberg, pp. 519-531. [58]. Godefroid, P., Levin, M. Y., & Molnar, D. A. (2008), ―Automated Whitebox Fuzz Testing‖, NDSS Vol. 8, pp. 151-166. [59]. Godefroid, P. (2007), ―Compositional dynamic test generation‖, Acm Sigplan Notices, Vol. 42, No. 1, pp. 47-54. [60]. Sen, K., & Agha, G. (2006), ―CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools‖, International Conference on Computer Aided Verification, Springer Berlin Heidelberg, pp. 419-423. [61]. Sen, K., Marinov, D., & Agha, G. (2005), ―CUTE: a concolic unit testing engine for C‖, ACM SIGSOFT Software Engineering Notes,Vol. 30, No. 5, pp. 263-272. [62]. Majumdar, R., & Sen, K. (2007), Latest: Lazy dynamic test input generation, EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS- 2007-36, pp. 297-306. 94 [63]. Lakhotia, K., McMinn, P., & Harman, M. (2010), ―An empirical investigation into branch coverage for C programs using CUTE and AUSTIN‖, Journal of Systems and Software, 83(12), pp. 2379-2391. [64]. Inkumsah, K., & Xie, T. (2008), ―Improving structural testing of object- oriented programs via integrating evolutionary testing and symbolic execution‖, Automated Software Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on , IEEE, pp. 297-306. [65]. Cadar, C., Ganesh, V., Pawlowski, P. M., Dill, D. L., & Engler, D. R. (2008). EXE: automatically generating inputs of death. ACM Transactions on Information and System Security (TISSEC), 12(2), 10. [66]. Boonstoppel, P., Cadar, C., & Engler, D. (2008, March). RWset: Attacking path explosion in constraint-based test generation. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 351-366). Springer, Berlin, Heidelberg. [67]. Bugrara, S., & Engler, D. (2013). Redundant state detection for dynamic symbolic execution. In Presented as part of the 2013 {USENIX} Annual Technical Conference ({USENIX}{ATC} 13) (pp. 199-211). [68]. Sun Microsystems(2014), [69]. Artzi, S., Kiezun, A., Dolby, J., Tip, F., Dig, D., Paradkar, A., & Ernst, M. D. (2008, July). Finding bugs in dynamic web applications. In Proceedings of the 2008 international symposium on Software testing and analysis (pp. 261-272). [70]. Boyer R. S., Elspas B., & Levitt K. N. (1975), ―SELECT—a formal system for testing and debugging programs by symbolic execution‖, ACM SigPlan Notices, 10(6), pp. 234-245. [71]. Lin, Y., Miller, T., & Søndergaard, H. (2016, December). Compositional Symbolic Execution: Incremental Solving Revisited. In 2016 23rd Asia-Pacific Software Engineering Conference (APSEC) (pp. 273-280). IEEE. [72]. Abbassi, A., Day, N. A., & Rayside, D. (2019). Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB. arXiv preprint arXiv:1906.05881. [73]. Gauthier, F., & Steinhauser, A. (2019). Static detection of context-sensitive cross-site scripting vulnerabilities, U.S. Patent No. 10,325,097. Washington, DC: U.S. Patent and Trademark Office. 95 [74]. Hekmatnejad, M., & Fainekos, G. (2019). Model Checking Clinical Decision Support Systems Using SMT. arXiv preprint arXiv:1901.04545. [75]. Palikareva, H., Kuchta, T., & Cadar, C. (2016, May). Shadow of a doubt: testing for divergences between software versions. In 2016 IEEE/ACM 38th International Conference on Software Engineering (ICSE) (pp. 1181-1192). IEEE.