Семинар 6. Средство SPIN. Синтаксис_ трансляция базовых конструкций в модели Крипке (1185518)

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

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

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевич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.

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

Тип файла PDF

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

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

Список файлов семинаров