Семинар 6. Средство SPIN. Синтаксис_ трансляция базовых конструкций в модели Крипке
Описание файла
PDF-файл из архива "Семинар 6. Средство SPIN. Синтаксис_ трансляция базовых конструкций в модели Крипке", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016НапоминаниеКакая глобальная цель перед нами стоит?ДаныIнеформальное описание системыIсодержательное описание требований к системеТребуется проверить,удовлетворяет ли система набору требованийСистемаТребованияЗадача model checking для LTLТребованияСистемаСистема — это модель Крипке MТребование — это LTL-формула ϕПроверка требования — это проверка соотношения M |= ϕмодель Крипке MLTL-формула ϕалгоритм проверки LTL-формул?M |= ϕСредства верификацииВот список программных средств, способных проверятьвыполнимость LTL-формул в каких-то моделях:(на случай если захотите их использовать)BANDERACADENCE SMVLTSALTSminNuSMVPATProBSALSATMCSPINSpot...Disclaimer: список скорее всего неполный, и я не знаю большинства этихсредств; информация взята из соответствующей страницы в википедииНекоторые из этих средств работают и с CTLВ курсе сосредоточим внимание на средстве SPIN:Iоно открытое и бесплатноеIоно довольно популярноIего язык достаточно прост для понимания(и более “последователен”, чем язык NuSMV )SPIN: вступлениемодель Крипке MLTL-формула ϕалгоритм проверки LTL-формул?M |= ϕВсё ли так просто с этой схемой?SPIN: вступлениемодель для SPINмодель Крипке MLTL-формула ϕалгоритм проверки LTL-формул?M |= ϕВсё ли так просто с этой схемой?Каждое средство верификации имеет свой входной языкЭтот язык может быть довольно близок к входным данным“чистой” задачи model checking для LTL(как было в NuSMV для CTL)Язык, обрабатываемый средством SPIN, далёк от такого“чистого” описанияSPIN: вступлениеТребованияСистемаформализациямодель для SPINмодель Крипке MLTL-формула ϕалгоритм проверки LTL-формул?M |= ϕВходной язык средства SPIN — PROMELA(PROcess MEta LAnguage)“SPIN” = Simple Promela INterpreterSPIN: вступлениеЧтобы язык PROMELA понимался проще, будем проводитьаналогии между его конструкциями и конструкциями C++При этом надо иметь в виду, что если программа на языкеC++ работает последовательно, то модель, описанная наязыке PROMELA, работает параллельно-последовательно(более точно: это параллельная композиция последовательныхпроцессов)Таким цветом будут выделяться названия аналогичныхконструкций в C++PROMELA: типы переменныхIbit или boolIII(short)минимальный диапазон значений: [−215 , 215 )(int)intII(uchar)значения: целые числа от 0 до 255shortIIположительное значение: 1, trueотрицательное значение: 0, falsebyteII(bool)3131минимальный диапазон значений: [−2 , 2 )беззнаковые числа заданной шириныIсинтаксис: unsigned ...
: <число бит >;PROMELA: типы переменныхIструктуры typedefI(struct)синтаксис:typedef <имя типа > {<тип > <имя поля >;...<тип > <имя поля >;}Iодномерные массивы любого типа, кроме массивовIIIв том числе можно объявить массив структур, содержащихполя-массивысинтаксис — как в C++: после имени переменной пишется[<константа >]индексация элементов массива производится с ноляPROMELA: типы переменныхIперечисление mtypeIIII(enum)mtype — это один типсинтаксис объявления этого типа:mtype = {id1 , id2 , .
. . , idk };объявление типа mtype можно делать несколько раз: всеидентификаторы будут внесены в этот типс каждым идентификатором в mtype можно работать как сцелочисленной константойТрансляция значений mtype в целочисленные константы напримере:mtype = {a, b, c, d};mtype = {e, f, g};mtype = {h, i, j};Отождествление идентификаторов с константами происходиттак:a = 4b = 3 c = 2 d = 1e = 7f = 6 g = 5h = 10 i = 9 j = 8PROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;PROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Попробуем это прочитать:Тип mtype содержит значения A, B, C, D, E, FPROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Попробуем это прочитать:Имеется тип T с единственным полем — одномерным булевыммассивом a из пяти элементовPROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Попробуем это прочитать:Имеется переменная a булевого типаPROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Попробуем это прочитать:Имеются переменные b и c: беззнаковое целые числа ширины 3и 4 соответственноPROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Попробуем это прочитать:Имеется массив twodim из трёх элементов типа TТак можно объявлять многомерные массивыPROMELA: объявления переменныхОбъявления переменных и полей выглядят так же, как и вC++, единственное отличие: объявление типа должно бытьотделено от объявления переменнойПримерbool a;unsigned b : 3, c : 4;mtype = {A, B, C};typedef T {bool a[5];};mtype = {D, E, F};T twodim[3];mtype symvar;Попробуем это прочитать:Имеется переменная symvar типа mtypePROMELA: инициализация переменныхКаждая переменная имеет однозначно определённое начальноезначение:Iвсе переменные и поля типов bit, bool, short, int,unsigned инициализируются значением 0Iпеременные типа mtype также инициализируютсязначением 0, не совпадающим ни с одним из значенийтипа mtypeТак же, как и для переменных в C++ (как минимум стандарта11 ), можно явно задавать начальные значения переменных иполей:unsigned a : 3 = 4;bool b[3] = {true, false};typedef T {int a = 6;};PROMELA: типы процессовТип процесса — это нечто среднее между описанием функциии описанием класса:proctype <имя типа процесса >(<аргументы >) {<тело процесса >}Более точно, это описание устройства последовательноработающей сущности, преобразующей в числе прочегоглобальные переменныеВо время выполнения системы могут параллельно запускатьсяпроцессы — экземпляры типа процесса (объекты класса)Самый простой способ запуска процесса выглядит так:active proctype P() {...}В этом случае в начале работы системы запускается одинпроцесс типа PPROMELA: тело процесса: присваивание<тело процесса > ::= <последовательность ><последовательность > ::=<инструкция > [; <инструкция >]∗ [;]В теле процесса можно писать много разных инструкцийБудем их описывать постепенно, от простых к сложнымПрисваивания похожи по написанию и значению на то, чтопишется в C++:<имя переменной > = <выражение ><имя переменной >++<имя переменной >-В выражениях могут использоваться многие операции,имеющие те же значения и приоритеты, что и в C++,например: +, -, *, /, %, <<, >>, <, <=, >, >=, ==, !=, !, ~,&, ^, |, &&, ||, ->: (это аналог ?:), индексирование ([]),обращение к полям структур (.), константыАрифметические операции работают с переполнениемPROMELA: примерТеперь можно привести какой-нибудь простой полноценноработающий пример, чтобы хоть что-нибудь стало понятно:bool a;active proctype P() {a = true;}Как работает эта система:Iв начале работы переменная a имеет значение false,запущен один процесс типа P, и процесс готовитсявыполнить единственную инструкцию своего телаIна следующем шаге работы переменная a имеет значениеtrue, и запущенный процесс завершил своё выполнениеА что произойдёт с системой дальше?Этот вопрос разъяснится позжеPROMELA: метки состоянийКак и в C++, в PROMELA можно помечать состоянияуправления:<имя метки >: <инструкция >Будем использовать запись P@L для обозначения факта“процесс типа P готовится выполнить инструкцию с меткой L”Забегая немного вперёд: запись P@L можно будет писать вспецификацияхPROMELA: примерbool a;active proctype P() {L1: a = true;L2:}Теперь можно строго описать семантику написанной модели:состояния и переходы модели Крипке (или нечто похожее нанеё)!aP@L1aP@L2?SPIN: безопасность и живость!aP@L1aP@L2?В SPIN имеется (как минимум) два режима верификации:Iверификация свойств безопасностиIверификация свойств живостиSPIN: безопасность и живость!aP@L1aP@L2В SPIN имеется (как минимум) два режима верификации:Iверификация свойств безопасностиIверификация свойств живостиСвойство безопасности: достижимо ли “плохое” состояние?В этом режиме в модели могут быть состояния блокировки, изкоторых не исходит ни одной дуги, и проверяется достижимостьплохого состояния в имеющейся системе — не совсем моделиКрипкеSPIN: безопасность и живость!aP@L1aP@L2В SPIN имеется (как минимум) два режима верификации:Iверификация свойств безопасностиIверификация свойств живостиСвойство живости: верно ли, что как бы ни работала система,всегда можно получить “хорошую” бесконечную трассу?В этом режиме в каждое состояние блокировки добавляется петляPROMELA: бесконечный циклПроцесс, работающий бесконечно долго, как правило имеет втеле бесконечный цикл:do:: <последовательность >...:: <последовательность >odШаг работы цикла выглядит так:1.
если цикл собирается выполниться, тонедетерминированно выбирается одна изпоследовательностей, в которой может быть выполненапервая инструкция, и эта инструкция выполняется2. если на предыдущем шаге выполнилась непоследняяинструкция последовательности, то выполняетсяследующая по порядку инструкция3. после выполнения последней инструкции происходитпереход к пункту 1PROMELA: примерbool a;active proctype P() {L1: do:: L2: a = !a; L3: a = !a;:: L4: a = !a;odL5:}!aL1aL3aL1!aL3PROMELA: бесконечный циклdo:: <последовательность >...:: <последовательность >odВ выполняемой последовательности может встретитьсяинструкция breakВыполнение этой инструкции приводит к выходу из цикла ипереходу к следующей после цикла инструкцииPROMELA: примерbool a;active proctype P() {L1: do:: L2: a = !a; L3: a = !a;:: L4: break;odL5:}!aL1!aL5aL3PROMELA: оператор ветвленияif:: <последовательность >...:: <последовательность >fiШаг работы оператора ветвления выглядит так:1. если оператор собирается выполниться, тонедетерминированно выбирается одна изпоследовательностей, в которой может быть выполненапервая инструкция, и эта инструкция выполняется2.