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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Математические методыверификации схем и программИнструкция по использованию средства 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-свойствоРекомендованный режим свойств живостиИмя свойстваЗапустить проверкуОтчёт.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций