Инструкция по работе со средством SPIN

Математические методыверификации схем и программИнструкция по использованию средства SPINдля верификации LTL-требованийЗахаров В.А.Подымов В.В.Все вопросы писать на почтуvaldus@yandex.ruWindows vs. LinuxSpin – мультиплатформенное средствоИ в Windows, и в Linux доступны как консольная утилита, так и GUI SpinДанная инструкция ориентирована на пользователей LinuxВроде бы в Windows всё делается аналогично,однако детали запуска средства, само собой, могут отличатьсяОбщая схема работы SPINРабота средства SPIN для проверки LTL-свойств в общем виде выглядит так:Файл .pml с описанием моделиКомпилятор SPINИсходный файл на языке CКомпилятор CИсполняемый файлЗапуск исполняемого файлаОтчёт о проверке свойств в выводе файлаКонсоль + LinuxФайл .pml с описанием моделиКонсоль + LinuxФайл .pml с описанием моделиКомпилятор SPINИсходный файл на языке C“-a” - создать файл “pan.c” с исходным кодомверификатора данной конкретной моделиПо умолчанию создаётся верификатор врежиме проверки свойств живостиЕсли уверены, что режима проверки свойствбезопасности будет достаточно, то флаг “DSAFETY”переключает верификатор на этот режим(свойства безопасностипроверяются быстрее с DSAFETY)Консоль + LinuxИсходный файл на языке CКомпилятор CИсполняемый файлКонсоль + LinuxИсполняемый файлЗапуск исполняемого файла“-N <имя>” - проверить свойство,описанное как “ltl <имя>”Без флага “-a” рассматриваютсятолько конечные трассыСвойство не выполненоПроверяем свойство fПро дополнительные опциичитайте в документацииСтатистикаОтчёт о проверке свойствв выводе файлаКонсоль + LinuxИсполняемый файлЗапуск исполняемого файлаПопробуем проверить такое свойствоЕго можно опровергнуть только бесконечной трассойОтчёт о проверке свойствв выводе файлаКонсоль + LinuxИсполняемый файлЗапуск исполняемого файлаОтчёт о проверке свойствв выводе файлаПросмотрев все конечные трассы, верификатор не нашёл противоречий со свойствомКонсоль + LinuxИсполняемый файлПри верификации смотрими на бесконечные трассы“acceptance cycle” =“свойство нарушено”И здесь в подтверждениеговорится “была ошибка”Запуск исполняемого файлаОтчёт о проверке свойствв выводе файлаКонсоль + LinuxРезюмеДля полной уверенности в результате верификации делаем так:spin -a <имя файла с моделью>(без флага -DSAFETY, чтобыиметь всевозможные трассы)gcc -o pan pan.c./pan -a -N <имя свойства>(с флагом -a, чтобы учитыватьбесконечные трассы при проверке)GUI + LinuxЕсть как минимум две популярных графических оболочки для SPINispinЭто оболочка от разработчиков spin, она идёт в комплекте со средствомОболочка основана на tclОна выглядит старомодно, но в ней есть всё, что нужноО ней будут следующие слайдыjspinhttp://spinroot.com/spin/Man/README.html#S3Это оболочка не от разработчиков spinОболочка основана на javaОна выглядит более современно, и вроде бы в ней тоже есть всё, что нужноВ ней всё делается примерно так же, как в ispin, так что о ней слайдов не будетispin + LinuxЧтобы оболочка ispin работала, необходимо сделать так,чтобы терминал понимал команду “spin”:●поставить spin в стандартные системные папки, или●прописать в нужную переменную окружения путь к spinОболочка запускается исполняемым файлом ispin.tclispinВсё довольно user-friendlyРедакторСимуляцияВерификацияispinРежим свойств безопасностиПроверить ltl-свойствоРекомендованный режим свойств живостиИмя свойстваЗапустить проверкуОтчёт.