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

Проверка моделей (проверка на модели, англ. model checking) — метод автоматической формальной верификации параллельных систем с конечным числом состояний, позволяет проверить, удовлетворяет ли заданная модель системы формальным спецификациям.

В качестве модели обычно используется так называемая модель Крипке, которая формально задаётся следующим образом: ${\displaystyle M=\left(S,S_{0},R,L\right)}$ , где ${\displaystyle S}$ — множество состояний, ${\displaystyle S_{0}}$ — множество начальных состояний, ${\displaystyle R\subseteq S\times S}$ — отношение переходов, ${\displaystyle L:S\rightarrow 2^{AP}}$ — функция разметки.

Обычно спецификации задаются на языке формальной логики. Для спецификации аппаратного и программного обеспечения, как правило, применяют темпоральную логику — специальный язык, позволяющий описывать поведение системы во времени.

Важным вопросом спецификации является полнота. Метод проверки на модели позволяет убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которым должна удовлетворять система, невозможно.

Основная трудность, которую приходится преодолевать в ходе проверки на модели, связана с эффектом комбинаторного взрыва в пространстве состояний. Эта проблема возникает в системах, состоящих из многих компонентов, взаимодействующих друг с другом, а также в системах, обладающих структурами данных, способных принимать большое число значений.

• BLAST — статический анализатор Си-программ
• CADP (Construction and Analysis of Distributed Processes) — инструмент проектирования протоколов и распределенных систем
• CHESS — инструмент для тестирования многопоточных программ для .Net (управляемых) и Win32, 64
• ISP — верификатор кода MPI-программ
• Java Pathfinder — свободный инструмент для проверки многопоточных Java-программ
• MoonWalker — свободный инструмент для проверки .Net-программ
• MRMC (Markov Reward Model Checker)
• NuSMV — символьный верификатор
• PRISM — вероятностный символьный верификатор
• Rabbit — верификатор для систем реального времени
• SPIN — верификатор общего назначения для проверки корректности распределенных программ и протоколов
• Vereofy — верификатор программ компонентных систем
• μCRL2 — свободный инструмент, основан на ACP
• UPPAAL — инструментарий для моделирования, верификации и валидации систем реального времени моделируемых как сети временных автоматов
• Zing^[1] — инструментарий от Microsoft, используемый для разработки драйверов, позволяет проверять модели состояний параллельного программного обеспечения.

• Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. — М.: МЦНМО, 2002. — 416 с. — ISBN 5940570542.
• Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. — СПб.: БХВ-Петербург, 2009. — 460 с. — ISBN 9785977504041.
• Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. — СПбГУ ИТМО, 2011. — 242 с.

• Верификация программ с помощью моделей // «Открытые системы», № 12, 2003
• Robert B. France Modeling and Analyzing Concurrent Systems
• Миронов А. М. Верификация программ методом Model Checking.