Luận án Tiến sĩ: Cải tiến 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 LUẬN ÁN TIẾN SĨ TOÁN HỌC Hà Nội - 2020 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 LUẬN ÁN TIẾN SĨ TOÁN HỌC Chuyên ngành : Cơ sở toán học cho tin học Mã số: 9 46 01 10 Ngƣời hƣớng dẫn khoa học: 1. Nguyễn Trƣờng Thắng 2. Đặng Văn Đức Hà Nội - 2020 i MỤC LỤC MỤC LỤC .i LỜI CAM ĐOAN. iii LỜI CẢM ƠN .iv DANH MỤC THUẬT NGỮ VÀ TỪ VIẾT TẮT .v DANH MỤC BẢNG BIỂU .vi DANH MỤC HÌNH VẼ.

vii MỞ ĐẦU. TỔNG QUAN VỀ KIỂM THỬ PHẦN MỀM VÀ THỰC THI BIỂU TRƢNG. Kiểm thử phần mềm. Các khái niệm cơ bản.2 Các phƣơng pháp kiểm thử.

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 theo hƣớng động .2 Kiểm thử hộp trắng dòng điều khiển theo hƣớng tĩnh. Các tiêu chí phủ kiểm thử. Đồ thị dòng điều khiển.

Đƣờng kiểm thử. So sánh kiểm thử hộp trắng dòng điều khiển theo hƣớng tĩnh và động. Thách thức trong kiểm thử phần mềm. Thực thi biểu trƣng.

Tổng quan về thực thi biểu trƣng. Thực thi biểu trƣng tĩnh. Thực thi biểu trƣng động .4 Thực thi Concolic. Thực thi biểu trƣng với các lời gọi phƣơng thức.

Ràng buộc xâu và vai trò của giải ràng buộc xâu. Kết luận chƣơng 1. THỰC THI BIỂU TRƢNG VÀ MÔ HÌNH HÓA RÀNG BUỘC. Bùng nổ đƣờng đi.

Mô hình hóa bộ nhớ. Thực thi biểu trƣng và công cụ mở rộng. Thực thi biểu trƣng và kiểm thử phần mềm. Thực thi biểu trƣng trên ngôn ngữ Java.

Giải các ràng buộc và thực thi biểu trƣng. Ràng buộc hỗn hợp và cải tiến trong giải ràng buộc xâu. Xây dựng lại ràng buộc. Quá trình tiền xử lý.

Sinh các ràng buộc xâu và kết quả thực hiện. Giải ràng buộc sử dụng Otomat. Kết luận chƣơng 2. GIẢI RÀNG BUỘC XÂU.

Các vấn đề liên quan đến Bitvector và bộ thỏa mãn SMT (satisfiability modulo theories). Lý thuyết thỏa mãn SMT. Giải ràng buộc xâu dựa trên phƣơng pháp BitVector. Giải ràng buộc xâu dựa trên phƣơng pháp sử dụng OTOMAT.

Đề xuất giải ràng buộc xâu trong thực thi biểu trƣng .1 Mô hình hoá ràng buộc xâu sử dụng đồ thị .2 Phát hiện thêm ràng buộc kiểu nguyên trên dữ liệu xâu. Thực nghiệm và đánh giá kết quả. Kết luận chƣơng 3. 85 KẾT LUẬN VÀ KIẾN NGHỊ.86 DANH MỤC CÔNG TRÌNH CỦA TÁC GIẢ .87 TÀI LIỆU THAM KHẢO .88 iii LỜI CAM ĐOAN Tôi xin cam đoan đây là công trình nghiên cứu của riêng tôi đƣợc hoàn thành dƣới sự hƣớng dẫn tận tình của tập thể hƣớng dẫn gồm.

Các kết quả đƣợc viết chung với các tác giả khác đã đƣợc sự nhất trí của đồng tác giả khi đƣa vào luận án. Các kết quả nêu trong luận án là trung thực và chƣa từng đƣợc công bố trong bất kỳ công trình nào trƣớc thời gian công trình của tôi và cộng sự đƣợc công bố. Hà Nội, ngày….năm … Tác giả luận án iv LỜI CẢM ƠN Trƣớc hết, tác giả xin bày tỏ lòng biết ơn chân thành và sâu sắc tới các thầy giáo hƣớng dẫn, TS. Nguyễn Trƣờng Thắng và PGS.

Sự tận tình giúp đỡ, chỉ bảo, động viện tận tình và quí báu mà các thầy đã dành cho tác giả trong suốt quá trình thực hiện luận án là không thể nào kể hết đƣợc. Xin chân thành cảm ơn các thầy các cô, các nhà khoa học thuộc Viện Công nghệ thông tin và Học viện khoa học và Công nghệ đã tận tình giúp đỡ và tạo một môi trƣờng làm việc hết sức thuận lợi giúp tác giả thực hiện tốt công việc nghiên cứu của mình. Xin chân thành cảm ơn Ban Giám Hiệu Trƣờng đại học Công nghệ thông tin và Truyền thông – Đại học Thái Nguyên đã hết sức tạo điều kiện về thời gian và công việc để tác giả có thể tập trung hoàn thành quá trình học tập, nghiên cứu của mình. Đặc biệt xin gửi lời cảm ơn đến các thầy cô, các bạn đồng nghiệp trong Khoa Công nghệ thông tin đã động viên, giúp đỡ tác giả trong suốt quá trình nghiên cứu.

Cuối cùng, xin gửi lời cảm ơn sâu sắc nhất tới gia đình, bạn bè và ngƣời thân, những ngƣời đã luôn là nguồn động viên để tác giả có thể học tập và nghiên cứu, luôn sẻ chia những khó khăn vất vả trong quá trình nghiên cứu và hoàn thiện đề tài. Hà Nội, ngày…. Tác giả luận án v DANH MỤC THUẬT NGỮ VÀ TỪ VIẾT TẮT Từ viết tắt Từ đầy đủ JPF Java Path Finder MJI Model Java Interface DFA Deterministic Finite Automaton PC Điều kiện đƣờng dẫn (path condition) QTKT Quy trình kiểm thử SAT Boolean satisfiability problem SDLC Software Development Life Cycle SE Thực thi biểu trƣng (Symbolic Execution) SET Cây thực thi biểu trƣng (Symbolic Execution Tree) SMT Satisfiability Modulo Theories SQA Software quality assurance STLC Software Test Life Cycle TPPM Thành phần phần mềm UT Kiểm thử đơn vị - Unit Testing VSUnit Visual Studio Unit Testing vi DANH MỤC BẢNG BIỂU Bảng 1. Ví dụ về thực thi biểu trƣng động.

So sánh thực thi Concolic với thực thi biểu trƣng. Minh họa việc chuyển đổi từ mã nguồn Java sang mã Jimple. Mô tả ràng buộc xâu. Xây dựng các ràng buộc cho các phép toán trên xâu.

Xây dựng ràng buộc tƣơng ứng với các phép toán trên xâu. Kết quả đánh giá mô hình cải tiến trên bộ dữ liệu. 79 vii DANH MỤC HÌNH VẼ Hình 1. Mối quan hệ giữa phát triển phần mềm và kiểm thử phần mềm.

Quy trình chung của kiểm thử hộp trắng theo hƣớng động. Ví dụ về chèn mã nguồn trong DMS/SRT. Mã nguồn hàm triangle sau khi thêm mã nguồn. Quy trình chung của kiểm thử hộp trắng theo hƣớng tĩnh.

Các cấu trúc điều khiển phổ biến. Ví dụ về ý tƣởng thực hiện cụ thể của thực thi biểu trƣng. Cây thực thi biểu trƣng. Thực thi biểu trƣng với phƣơng thức nhận đầu vào là đối tƣợng.

Cây thực thi biểu trƣng đƣợc quản lý riêng. Thực thi biểu trƣng trên lời gọi phƣơng thức. Mô hình hoạt động của JPF. Sơ đồ trạng thái trong quá trình kiểm thử.

Biểu diễn sơ đồ kiến trúc mức cao của JPF. Ví dụ về trừu tƣợng hoá dữ liệu. Một ví dụ khác về trừu tƣợng hoá dữ liệu. Quy trình sàng lọc dữ liệu.

Thuật toán giải ràng buộc hỗn hợp. Đồ thị sau khi loại bỏ phép toán equals. Các ràng buộc không thỏa mãn sau khi loại bỏ phép toán equals. Các đỉnh mới đại diện cho độ dài xâu đƣợc bổ sung.

Giải ràng buộc xâu dựa trên Otomat. Phƣơng thức giải ràng buộc phủ định. Sơ đồ mô hình hoá ràng buộc xâu sử dụng đồ thị .4: Thuật toán giải ràng buộc xâu. Chƣơng trình Java kiểm thử.

Kết quả sinh dữ liệu biểu trƣng trên một số phép toán trên xâu. Code kiểm thử. Kết quả đánh giá mô hình cải tiến trên bộ dữ liệu. Chƣơng trình Java.

83 1 MỞ ĐẦU Kiểm thử phần mềm (testing) là một trong những hoạt động quan trọng nhất trong chu trình phát triển phần mềm. Theo số liệu thống kê thực tế, kiểm thử phần mềm chiếm tới 50-60% tổng chi phí toàn bộ quy trình phát triển phần mềm. Để giảm chi phí kiểm thử và tăng mức độ tin cậy của phần mềm, các nhà nghiên cứu đang cố gắng tự động hoá các hoạt động phục vụ công việc kiểm thử phần mềm [1, 2]. 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ó.

Công việc đầu tiên và hết sức quan trọng đó là chuẩn bị bộ dữ liệu kiểm thử. Việc này thƣờng đƣợc làm thủ công nên cần rất nhiều nhân lực để tạo ra bộ dữ liệu đầy đủ, có tính bao phủ cao (coverage criteria) trên toàn bộ các đƣờng tính toán (computation paths) của chƣơng trình. Các ca kiểm thử bao gồm dữ liệu kiểm thử và các giá trị đầu ra mong muốn. 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]. 2 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.