ĐA TRỪU TƯỢNG KẾT HỢP TINH LỌC TRONG KIỂM TRA MÔ HÌNH HƯỚNG KÝ HIỆU

Abstract

In model checking, the state space explosion prevents verifying the large systems because exhaustive search fails to find errors. The problem becomes much more serious recently when the size and the complexity of the system-under-check are constantly growing up. Abstraction is the most effective method to overcome this problem. It is an approach used to reduce the size (of the state space) of the model in the reality. However, how to use abstraction effectively in reducing model checking efforts is still a question. This work proposes a multiple abstraction refinement technique in symbolic model checking that allows to verify large state space systems. The proposed technique employs the abstraction refinement algorithm CEGAR proposed by Clarke et al. in 2000 combining with the multiple abstraction method of Qian and Nymeyer. Instead of checking on concrete model, an abstract model is verified first. If a counter-example is found, the searching scope will be widen on the next abstract model and so on, even on the original model. This process can be called refinement. The experimental results show that the new approach improves the performance of the model checking process.

Tóm tắt

Trong kiểm tra mô hình, bùng nổ không gian trạng thái gây trở ngại đến việc kiểm chứng các hệ thống lớn vì quá trình tìm kiếm lỗi có thể không hoàn thành. Vấn đề càng trở nên nghiêm trọng hơn khi kích thước và sự phức tạp của hệ thống cần kiểm tra đang liên tục lớn dần lên. Trừu tượng là phương pháp hiệu quả nhất để giải quyết vấn đề này. Đây là một cách tiếp cận để giảm kích thước (của không gian trạng thái) của mô hình trong thực tế. Tuy nhiên, làm thế nào để sử dụng trừu tượng một cách hiệu quả trong việc giảm chi phí kiểm tra mô hình vẫn còn là câu hỏi. Công trình này đề xuất kỹ thuật tinh lọc đa trừu tượng trong kiểm tra mô hình cho phép kiểm chứng các hệ thống có không gian trạng thái lớn. Phương pháp đề xuất là sự tận dụng giải thuật CEGAR được Clarke đề xuất vào năm 2000 kết hợp với phương pháp đa trừu tượng của Qian & Nymeyer. Thay vì kiểm tra trên mô hình thực, mô hình trừu tượng được kiểm chứng đầu tiên. Nếu tìm thấy counter-example, phạm vi tìm kiếm được mở rộng trên các mô hình trừu tượng tiếp theo và cứ thế, thậm chí là trên mô hình gốc. Quá trình này được gọi là tinh lọc. Kết quả thực nghiệm cho thấy rằng phương pháp mới cải thiện hiệu suất của quá trình kiểm tra mô hình.