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ừ 108 đến 1010 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.
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
