NuSMV

В компьютерной науке NuSMV является переопределением и расширением символического средства проверки моделей SMV , первого инструмента проверки моделей, основанного на диаграммах бинарных решений (BDD). ^[1] Инструмент был разработан как открытая архитектура для проверки моделей. Он нацелен на надежную проверку проектов промышленного масштаба, для использования в качестве бэкэнда для других инструментов проверки и в качестве исследовательского инструмента для формальных методов проверки.

NuSMV был разработан как совместный проект ITC-IRST (Istituto Trentino di cultura  [it] в Тренто ), Университета Карнеги-Меллона , Университета Генуи и Университета Тренто .

NuSMV 2 , версия 2 NuSMV, наследует все функциональные возможности NuSMV. Кроме того, он объединяет проверку моделей на основе BDD с проверкой моделей на основе SAT . ^[2] Он поддерживается Fondazione Bruno Kessler, организацией-правопреемницей ITC-IRST.

NuSMV поддерживает анализ спецификаций, выраженных в CTL и LTL . Он может быть запущен в пакетном режиме или интерактивно с текстовым пользовательским интерфейсом.

Оболочка взаимодействия NuSMV активируется из системного приглашения следующим образом:

[system_prompt]$ NuSMV  -int NuSMV> перейти NuSMV>

NuSMV сначала пытается прочитать и выполнить команды из файла инициализации, если такой файл существует и доступен для чтения, если только он не -sбыл передан в командной строке. Файл master.nusmvrcищется в каталогах, определенных в переменной среды NUSMV_LIBRARY_PATH, или в пути к библиотеке по умолчанию, если такая переменная не определена. Если такого файла не существует, также будут проверены домашний каталог пользователя и текущий каталог. Команды в файле инициализации выполняются последовательно. После завершения фазы инициализации отображается приглашение оболочки NuSMV, и теперь система готова выполнять команды пользователя.

Команда NuSMV обычно состоит из имени команды и аргументов вызываемой команды. Можно заставить NuSMV читать и выполнять последовательность команд из файла с помощью параметра командной строки -source:

[system_prompt]$ NuSMV  -source  cmd_file

Если опция -int не указана, NuSMV запускается как пакетная программа, которая имеет следующий вид:

[system_prompt]$ NuSMV [ параметры командной строки ] входной_файл    

NuSMV можно использовать для проверки того, выполняются ли заданные ограничения LTL или CTL для заданной модели. Например, у нас есть спецификация CTL, которую мы хотим проверить:

CTLSPEC EF ( proc5 . state = critical );   

Эта спецификация верна, если существует путь выполнения, такой, что компонент stateпроцесса proc5имеет значение criticalв какой-то момент. Пользователь может проверить, соответствует ли его модель этой спецификации, используя следующие команды.

[system_prompt]$ NuSMV [ параметры командной строки ] входной_файл NuSMV> перейти NuSMV> check_ctlspec    

Если спецификация верна, NuSMV сообщит вам об этом

-- спецификация EF proc5.state = critical is true > NuSMV

Если какая-либо спецификация не выполняется, NuSMV вернет полную трассировку выполнения, показывающую, как она не выполняется, если это возможно.

• Spin Model Checker — универсальный инструмент проверки моделей для асинхронных программных систем.
• CADP (Построение и анализ распределенных процессов), набор инструментов для формального проектирования асинхронных параллельных систем

• веб-сайт NuSMV
• Сайт Nuseen: набор инструментов на основе Eclipse для проверки моделей NuSMV.
• nuXmv: расширяет NuSMV с помощью проверки на основе SMT и обновленных методов решения SAT