Luận án cải tiến ràng buộc xâu trong sinh dữ liệu kiểm thử tự động bằng thực thi tượng trưng

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.

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- 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. 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ừ đó 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. Đối tƣợng và phạm vi nghiên cứu: 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 3 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.

Nội dung nghiên cứu: Các phƣơng pháp kỹ thuật sinh tự động 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ử. Phƣơng pháp nghiên cứu: 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 triê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ố.

Các đóng góp 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ố. Bố cục của luận án: Cấu trúc luận án bao gồm phần mở đầu, ba chƣơng nội dung, phần kết luận, danh mục công trình công bố và danh mục các tài liệu tham khảo. Nội dung chính của các chƣơng trong luận án 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ể. 4 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. 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. Kiểm thử phần mềm 1. Các khái niệm cơ bản Để đả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.

Do đó cần phải phát hiện và khắc phục các lỗi của phần mềm trƣớc khi sử dụng. Có các phƣơng pháp khác nhau để phát hiện lỗi của phần mềm bao gồm kiểm chứng mô hình (model checking) [16], các kỹ thuật phân tích tĩnh (static analysis) [17] và kiểm thử (software testing) [18 - 23]. Trong kiểm chứng mô hình, một mô hình của hệ thống đƣợc tạo ra để hỗ trợ phân tích mọi sự thực thi có thể trong mô hình. Kiểm chứng mô hình có thể kiểm chứng đƣợc rằng mô hình của hệ thống hoạt động chính xác trong tất cả trƣờng hợp có thể.

Hạn chế của kiểm chứng mô hình đó là không gian trạng thái của mô hình thƣờng quá lớn do đó việc khám phá tất cả các trạng thái không phải lúc nào cũng thực hiện đƣợc. Trong khi đó, các kỹ thuật phân tích chƣơng trình tĩnh thƣờng đƣa ra nhiều cảnh báo (warnings) không tƣơng ứng với các lỗi thực sự. Các kỹ thuật kiểm thử phát hiện ra các lỗi thực sự nhƣng thƣờng không phát hiện ra đƣợc tất cả các lỗi do chỉ phân tích một số sự thực thi trong chƣơng trình. Kiểm thử phần mềm là quá trình thực thi một chƣơng trình với mục đích tìm ra lỗi.

Kiểm thử phần mềm đảm bảo sản phẩm phần mềm đáp ứng chính xác, đầy đủ và đúng theo yêu cầu của khách hàng, yêu cầu của sản phẩm đã đặt ra.