I. Tổng quan về đề tài
Luận văn tập trung vào kiểm tra mô hình dựa trên đặc tả cho các chương trình chưa hoàn chỉnh, một vấn đề quan trọng trong khoa học máy tính. Các phương pháp kiểm tra hình thức như model checking và theorem proving được sử dụng rộng rãi nhưng gặp phải vấn đề bùng nổ trạng thái. Để khắc phục, luận văn đề xuất sử dụng kỹ thuật concolic testing để sinh test-case hiệu quả. Chương trình chưa hoàn chỉnh là những chương trình thiếu mã nguồn của các hàm hoặc thủ tục, gây khó khăn cho việc kiểm tra. Luận văn nghiên cứu cách biến đổi chương trình này thành chương trình tự hoàn chỉnh để kiểm tra.
1.1. Mục tiêu nghiên cứu
Mục tiêu chính của luận văn là nghiên cứu và đề xuất phương pháp kiểm tra các chương trình chưa hoàn chỉnh. Cụ thể, luận văn tập trung vào việc rút trích ngữ nghĩa từ ngôn ngữ ACSL, sinh test-case dựa trên luồng thực thi, và biến đổi chương trình thành chương trình tự hoàn chỉnh. Ngoài ra, luận văn cũng nghiên cứu abstract interpretation để chứng minh tính đúng đắn của phương pháp đề xuất.
1.2. Đóng góp chính
Luận văn đóng góp bằng cách đề xuất framework kiểm tra chương trình chưa hoàn chỉnh. Cụ thể, luận văn kết hợp đặc tả hàm với luồng thực thi để tạo test-case và biến đổi chương trình thành chương trình tự hoàn chỉnh. Về lý thuyết, luận văn chứng minh phương pháp này tương đương với consistent abstract interpretation, đảm bảo tính chính xác khi kiểm tra.
II. Kiểm tra mô hình và kỹ thuật concolic testing
Model checking là phương pháp kiểm tra hình thức hiệu quả, giúp xác định lỗi trong chương trình bằng cách vét cạn các trạng thái. Tuy nhiên, phương pháp này gặp phải vấn đề bùng nổ trạng thái. Kỹ thuật concolic testing kết hợp thực thi cụ thể và thực thi ký hiệu để sinh test-case hiệu quả, giảm thiểu số lượng trạng thái cần kiểm tra. Luận văn áp dụng kỹ thuật này để giải quyết vấn đề kiểm tra chương trình chưa hoàn chỉnh.
2.1. Model checking
Model checking là phương pháp kiểm tra hình thức dựa trên việc vét cạn các trạng thái của chương trình. Phương pháp này hiệu quả trong việc tìm lỗi nhưng gặp phải vấn đề bùng nổ trạng thái khi số lượng trạng thái quá lớn. Luận văn đề xuất sử dụng kỹ thuật concolic testing để giảm thiểu số lượng trạng thái cần kiểm tra.
2.2. Concolic testing
Concolic testing là kỹ thuật kết hợp thực thi cụ thể và thực thi ký hiệu để sinh test-case hiệu quả. Kỹ thuật này giúp giảm thiểu số lượng trạng thái cần kiểm tra, giải quyết vấn đề bùng nổ trạng thái trong model checking. Luận văn áp dụng kỹ thuật này để kiểm tra chương trình chưa hoàn chỉnh.
III. Giải pháp kiểm tra chương trình chưa hoàn chỉnh
Luận văn đề xuất giải pháp kiểm tra chương trình chưa hoàn chỉnh bằng cách biến đổi chương trình thành chương trình tự hoàn chỉnh. Giải pháp này kết hợp đặc tả hàm với luồng thực thi để tạo test-case và biến đổi chương trình. Luận văn cũng chứng minh rằng phương pháp này tương đương với consistent abstract interpretation, đảm bảo tính chính xác khi kiểm tra.
3.1. Chương trình chưa hoàn chỉnh
Chương trình chưa hoàn chỉnh là những chương trình thiếu mã nguồn của các hàm hoặc thủ tục, gây khó khăn cho việc kiểm tra. Luận văn đề xuất phương pháp biến đổi chương trình này thành chương trình tự hoàn chỉnh để kiểm tra bằng model checking.
3.2. Biến đổi chương trình
Luận văn đề xuất phương pháp biến đổi chương trình chưa hoàn chỉnh thành chương trình tự hoàn chỉnh bằng cách kết hợp đặc tả hàm với luồng thực thi để tạo test-case. Phương pháp này đảm bảo tính chính xác khi kiểm tra bằng model checking.
IV. Ứng dụng và đánh giá
Luận văn xây dựng ứng dụng minh họa cho phương pháp kiểm tra chương trình chưa hoàn chỉnh. Ứng dụng này hỗ trợ sinh test-case và biến đổi chương trình để kiểm tra bằng model checking. Kết quả thực nghiệm cho thấy phương pháp đề xuất hiệu quả trong việc kiểm tra các chương trình này.
4.1. Ứng dụng minh họa
Luận văn xây dựng ứng dụng minh họa cho phương pháp kiểm tra chương trình chưa hoàn chỉnh. Ứng dụng này hỗ trợ sinh test-case và biến đổi chương trình để kiểm tra bằng model checking.
4.2. Kết quả thực nghiệm
Kết quả thực nghiệm cho thấy phương pháp đề xuất hiệu quả trong việc kiểm tra chương trình chưa hoàn chỉnh. Phương pháp này giúp giảm thiểu số lượng trạng thái cần kiểm tra và đảm bảo tính chính xác khi kiểm tra.
