Главная » Все файлы » Просмотр файлов из архивов » PDF-файлы » Семинар 6. Средство SPIN. Синтаксис_ трансляция базовых конструкций в модели Крипке

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

PDF-файл Семинар 6. Средство SPIN. Синтаксис_ трансляция базовых конструкций в модели Крипке Математические методы верификации схем и программ (63276): Семинары - 10 семестр (2 семестр магистратуры)Семинар 6. Средство SPIN. Синтаксис_ трансляция базовых конструкций в модели Крипке: Математические методы верификации схем и программ - PDF (63276) 2020-08-25СтудИзба

Описание файла

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.

Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5076
Авторов
на СтудИзбе
455
Средний доход
с одного платного файла
Обучение Подробнее