НуСМВ

НуСМВ
Разработчик(и)	FBK-первый (Тренто, Италия), CMU (Питтсбург, Пенсильвания), Университет Генуи (Италия), Университет Тренто (Италия)
Стабильная версия	2.6.0 / 14 октября 2015 г .; 8 лет назад
Написано в	АНСИ С
Операционная система	Linux , Mac OS X , Microsoft Windows
Тип	Проверка модели
Лицензия	LGPL v2.1
Веб-сайт	nusmv.fbk.eu

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

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

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

Функциональные возможности

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

Интерактивный запуск NuSMV

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

[system_prompt]$ NuSMV -int
NuSMV> go
NuSMV>

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

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

[system_prompt]$ NuSMV -source cmd_file

Запуск пакета NuSMV

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

[system_prompt]$ NuSMV [command line options] input_file

Проверка спецификации LTL или спецификации CTL

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

CTLSPEC EF(proc5.state = critical);

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

[system_prompt]$ NuSMV [command line options] input_file
NuSMV> go
NuSMV> check_ctlspec

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

-- specification EF proc5.state = critical  is true
>NuSMV

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

См. также

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

Ссылки

^ К.Л. Макмиллан. Символическая проверка модели. В Академическом издании Клювера, 1993.
^ А. Бьер, А. Чиматти, Э. Кларк и Ю. Чжу. Символьная проверка модели без BDD. В «Инструментах и алгоритмах построения и анализа систем», TACAS'99, март 1999 г.

Внешние ссылки

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

[McM93-1] К.Л. Макмиллан. Символическая проверка модели. В Академическом издании Клювера, 1993.

[BCCZ99-2] А. Бьер, А. Чиматти, Э. Кларк и Ю. Чжу. Символьная проверка модели без BDD. В «Инструментах и алгоритмах построения и анализа систем», TACAS'99, март 1999 г.

[1]

[2]