✨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ử. 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 đó. 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 đó. Ý 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 cũng như Jean-Pierre Queille và Joseph Sifakis Jean-Pierre. 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 và Explicite State Model Checking.