Перевірка моделей

Перевірка моделі або перевірка властивості полягає у вичерпній і автоматичній перевірці чи задана модель певної системи відповідає заданій специфікації. Зазвичай, йдеться про апаратну або програмну систему, а специфікація містить вимоги безпеки як-от відсутність взаємних блокувань та інших подібних критичних станів, що можуть призвести до креша. Перевірка моделі — це техніка для автоматичної перевірки правильності властивостей системи зі скінченною кількістю станів.

Для того, що розв'язати таку задачу алгоритмічно, модель системи й специфікація формулюються якоюсь точною математичною мовою. Для цього проблему записують як задачу в логіці, — перевірити чи задана структура задовольняє заданій логічній формулі. Ця загальна концепція застосовна для багатьох видів логік і підхожих структур. Простим прикладом може бути перевірка чи задана формула в численні висловлень задовільнена заданою структурою.

Див. також

• Допасованість (статистика)
• Перехресне затверджування
• ^[en]