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

Đề 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.
Nội dung trích xuất từ tài liệu:
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ưngBỘ 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ênMỘ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 - 2020Cô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ệtNam 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Ở ĐẦU1. 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ểmthử (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ảnghỗ 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ộtcá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àichí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ềunà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ểmthử 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ứacá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ư: sinhcá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 đượcnhiề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ểutrưng (test case generation by symbolic execution [5, 7,10,11,12]); Dựa vào kiểm chứng mô hình (test casegeneration 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 Markovchains model) [15]. Trong đó kỹ thuật thực thi biểu trưng (symbolic execution) đang là vấn đề được nhiềunhà 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ằngngô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ácthư 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ảirà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ácphươ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ântích, đánh giá kết quả sau khi thử nghiệ ...