Подходы modelchecking

Можно выделить несколько подходов к применению проверки моделей для верификации программ:

• построение моделей для существующих верификаторов (Modex/Feaver, Java2spin/JCAT, Java PathFinder 1, Bandera)


• анализатор кода и верификатор в одном средстве.

Достоинство первого подхода в том, что не нужно реализовывать верификатор. Недостаток в том, что сложно автоматически построить консистентную и адекватную модель поскольку многие возможности языков программирования не выразимы на языках моделирования напрямую (указатели, числа с плавающей запятой, динамическое выделение памяти, вызов функций, вызов через указатель, объединения, исключения, виртуальные функции, неявный вызов конструкторов), что приводит к необходимости моделировать эти конструкции имеющимися в языке верификатора средствами, а также использовать статический анализ. Кроме того, при построении модели необходимо учитывать возможности верификатора по проверке свойств (для SPIN в формулах можно использовать только глобальные переменные).

Второй подход более легко адаптируем к конструкциям языка программирования, однако более сложно реализуем. Большинство средств, использующих подход CEGAR (Counter-Example Guided Abstraction Refinement), реализованы с использование такого подхода.

Входные данные для верификации могут быть представлены:

• исходным кодом на языке программирования (Blast, YASM)


• моделью на специализированном языке (Promela, входной язык SMV)


• байт-кодом для платформ общего назначения (Java байт-код для Java Path Finder 2)


• байт-кодом виртуальной машины для генерации пространства состояний (NIPS VM-байт код для CMC)