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

Chia sẻ: _ _ | Ngày: | Loại File: PDF | Số trang:27

Thêm vào BST

Báo xấu

21
lượt xem 4
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Đề tài 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.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: 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 a!=null&& a.length>0 {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 n=|x| So sánh độ dài xâu với một số nguyên n z=x.y, y=x n Phép nối xâu, phép lặp của phép nối xâu y=x-1 Phép đảo ngược xâu 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 ∈ L(R) x thuộc ngôn ngữ chính quy được biểu diễn bởi R x ∈ L(G) x thuộc ngôn ngữ phi ngữ cảnh được biểu diễn 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; 2: sg=BuilStringGraph(pc); 3: boolean sat=false; 4: While(!sat and !timeout){ 5: sat=CurrentSolver(pc,sg); if(sat) 6: 7: sat=StringSolver(pc,sg); 8: return sat; } } 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, s 3, 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 s 1 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 li>0 Sa.charAt(n) charAt,Sa,n,c la≥n Sa.concat(Sb) concat, Sa , Sb, Sx lx=la+lb Sa.indexOf(Sb) indexOf, Sa, Sb,x (x=-1)˅(la≥lb+x) Sa.lastIndexOf(Sb) lastIndexOf, Sa, Sb,x (x=-1)˅(la≥lb+x) Sa.subString(n,k) subString,Sa,n,k,Sx la=n+lx Sa.contains(Sb) contains,Sa,Sb 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 (charAt,sa,n,x) Ma= Ma [n] {x} [*] Sa[n]=x (concat,sa,sb,sx) Ma= Ma substring(Mx,0,la) (sa=sx[la:0]) (sb=sx[lx:la]) Mb=Mb subString(Mx,lb, ) Mx=Mx (Ma Mb) (indexOf, sa,sb,x) Ma= Ma ([x] Mb) Mb [*] (sa[x+lb:x]=sb) sa[i+lb:i] sb, i,0 i
16 trim(sa,sx) Ma= Ma [„˽‟,*] Mx [„˽‟,*] (sx[0] ˽) sx[lx-1] „˽‟) (sa[j]= Mx= Mx trim(Ma) „˽‟ (sa[i+lx:i]=sx) (sa[k]= „˽‟), i,j,k |(0 i la-lx) (0 j i) (i+lx k
17 CheckNegativeEdges(pathcondition pc, StringGraph sg, (M1,M2..)) 1: i=1; M‟1=M1; M‟2=M2;… M‟k=Mk; 2: while(1≤i
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: 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