Model checking

Một vài năm trở lại đây, trong khoa học máy tính, kiểm định mô hình (Model Checking) bắt đầu được sử dụng rộng rãi trong kiểm định các hệ thống phần mềm và các hệ thống điều khiển điện tử.^[1] Model Checking là một nhóm các kỹ thuật kiểm định tự động một cách hình thức một mô hình với một đặc tả các tính năng của mô hình đó.^[2] Mô hình của một hệ thống bao gồm tập hợp có giới hạn các trạng thái và tập hợp các chuyển tiếp giữa trạng thái đó. Thông thường, một đặc tả hoặc một tính năng của hệ thống được viết dưới dạng công thức lô-gic và thường được diễn tả bằng một ngôn ngữ lo-gic thời gian (temporal logic) nào đó.^[3][4][5][6] Ý tưởng cơ bản là chứng minh xem một mô hình có thỏa mãn các tính năng đã mô tả trước đó về nó hay không bằng cách duyệt toàn bộ không gian trạng thái của hệ thống đó. Nếu mô hình đó không thỏa mãn một tính năng nào đó, thuật toán cần phải đưa ra một phản ví dụ (counterexample). Phản ví dụ là một tập hợp các giá trị của biến đầu vào để chỉ ra rằng với một đầu vào như thế thì mô hình sẽ chạy không đúng như tính năng đã được mô tả.

Các nghiên cứu đầu tiên về Model Checking được thực hiện bởi Edmund Melson Clarke và Ernest Allen Emerson^[7] cũng như Jean-Pierre Queille và Joseph Sifakis Jean-Pierre^[5]. Clarke, Emerson và Sifakis đã được nhận giải thưởng Turing năm 2007 cho các đóng góp của họ về Model Checking.

Model Checking không được dùng cho các hệ thống có số trạng thái không giới hạn vì lý do giới hạn của bộ nhớ và số nhân xử lý của hệ thống máy tính. Hiệu suất của việc kiểm định thường phụ thuộc vào không gian trạng thái của hệ thống. Các hệ thống Model Checking gần đây có thể xử lý các không gian trạng thái lên đến từ 10⁸ đến 10¹⁰ phần tử^[8]. Tuy nhiên, vấn đề lớn nhất của Model Checking vẫn là bùng nổ tổ hợp không gian trạng thái của hệ thống. Không gian trạng thái của một chương trình phần mềm thường tăng theo hàm số mũ so với số dòng mã và phụ thuộc vào nhiều yếu tố như: số lượng biến, kích thước của biến tính theo số bit, và cấu trúc của chương trình. Các phương thức biểu diễn trạng thái của hệ thống được chia thành hai nhóm: Symbolic Model Checking^[9] và Explicite State Model Checking.

Tham khảo

1. Edmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1): 7-34 (2001)
2. Edmund M. Clarke, Bernd-Holger Schlingloff: Model Checking. Handbook of Automated Reasoning 2001: 1635-1790.
3. Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 8(2): 244-263 (1986)
4. Orna Lichtenstein, Amir Pnueli: Checking That Finite State Concurrent Programs Satisfy Their Linear Specification. POPL 1985: 97-107.
5. ^ Jean-Pierre Queille, Joseph Sifakis: A Temporal Logic to Deal with Fairness in Transition Systems FOCS 1982: 217-225.
6. Moshe Y. Vardi, and Pierre Wolper: An automata-theoretic approach to automatic program verification. Proc. 1st Symp. on Logic in Computer Science Cambridge: (June 1986), tr.332--344.
7. Edmund M. Clarke, E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs 1981: 52-71.
8. Gerard J. Holzmann: The SPIN Model Checker - primer and reference manual. Addison-Wesley 2004: I-XII, 1-596.
9. Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen: Symbolic Model Checking. CAV 1996: 419-427.