Семинар 8. SPIN практика

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

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

PDF-файл из архива "Семинар 8. SPIN практика", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст из PDF

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016Семинар 8SPIN: практикаУпражнение 1: реализация модели КрипкеПроверить выполнимость свойств в модели Крипкеba, cIG(a → b ∨ c)IGFaIFGaIGF¬c → F(a ∧ b)IGF¬c → G(¬bUa ∧ b)∅a, bЕщё немного синтаксиса и семантикиУ модели на языке PROMELA есть строгая семантикапошаговой работы, и к ней нужно привыкнутьОднако если в требовании не встречается оператора X,некоторые детали семантики можно не принимать во внимание:...a, b . .

.∅...∅∅a, b...(потратили шаг работы на проверку условия)...aa, b . . .∅(изменяли a и b на разных шагах)Iесли состояния трассы дублируются, то свойстваисходной и полученной трасс одинаковы, если запрещеноиспользовать оператор XIесли в трассу добавляются существенно новыесостояния, то свойства исходной и полученной трассмогут отличатьсяЕщё немного синтаксиса и семантикиВ моделях, подаваемых на вход SPIN, можно использовать рядне упомянутых ранее возможностей языка C/C++Например:#define N 3#define good (a == 1) // внимание: скобки!#define bad (a == 2)...active [N] proctype P() { ...:: good -> a = 2;...}ltl f {[]!bad}Упражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Процесс может сколь угодно долго находиться в критическойи некритической секциях (CRITICAL и NONCRITICAL соответственно)Переменная free не изменяется процессом, находящимся в этихсекцияхУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Инструкция в каждой отдельной строке выполняется атомарноИнструкция block(free) блокирует процесс, пока не станет истинным условие freeУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Выяснить,Iмогут ли процессы одновременно находиться в своихкритических секцияхIвозможна ли блокировка обоих процессов сразу,Iверно ли, что, выйдя из некритической секции, процессрано или поздно достигнет критическойУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Добавить в модель справедливость: процесс не может бесконечно долго находиться в критической секцииИзменить модель так, чтобы пара инструкций block(free);free = false; выполнялась атомарно: если block(free) неблокирует процесс, то немедленно выполнить free = falseУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Внимательно посмотреть на флаг “слабая справедливость” в настройках верификацииЕщё немного синтаксиса и семантикиНаряду с обычными булевыми выражениями вLTL-требованиях языка PROMELA можно использовать такиебулевы выражения:P[i]@labelЗдесьIP — имя типа процессаIi — идентификатор процессаIlabel — метка состояния процессаЕщё немного синтаксиса и семантикиНаряду с обычными булевыми выражениями вLTL-требованиях языка PROMELA можно использовать такиебулевы выражения:P[i]@labelУ каждого процесса есть свой идентификатор — неотрицательное целое число:Iпервому процессу, появившемуся в системе, присваиваетсяидентификатор 0Ещё немного синтаксиса и семантикиНаряду с обычными булевыми выражениями вLTL-требованиях языка PROMELA можно использовать такиебулевы выражения:P[i]@labelУ каждого процесса есть свой идентификатор — неотрицательное целое число:I каждому следующему процессу, появившемуся в системе, вбольшинстве случаев присваивается идентификатор —число, следующее за последним присвоеннымидентификаторомIIменьшинство случаев — это только те случаи, в которыхпроцесс завершаетсяпро эти случаи читайте в документацииЕщё немного синтаксиса и семантикиНаряду с обычными булевыми выражениями вLTL-требованиях языка PROMELA можно использовать такиебулевы выражения:P[i]@labelУ каждого процесса есть свой идентификатор — неотрицательное целое число:Iпроцессы, запущенные с помощью active, появляются всистеме в том порядке, в котором встречается словоactive в тексте моделиЕщё немного синтаксиса и семантикиСистемы с goto — это плохо, но не всегда, и в синтаксисеPROMELA есть инструкция безусловного переходаЭта инструкция работает точно так же, как и в C/C++:...LAB: a = b;...goto LAB;...В частности, если выполнение процесса — это зацикленноеповторение какой-либо последовательности действий, тодостаточно написать в теле процесса эту последовательность ив конце тела перейти в началоУпражнение 3: передача сообщенийСистема состоит из одного клиента, одного сервера идвунаправленного канала связи между нимиКлиент и сервер описываются левым и правым автоматамисоответственно:request!request?response?response!Запись m! означает, что при выполнении перехода сообщение mпосылается в канал, запись m? — что сообщение m принимаетсяиз каналаУпражнение 3: передача сообщенийСистема состоит из одного клиента, одного сервера идвунаправленного канала связи между нимиКлиент и сервер описываются левым и правым автоматамисоответственно:request!request?response?response!Выяснить,Iверно ли, что если клиент посылает сообщение request,то он обязательно примет сообщение responseIвозможна ли ситуация, в которой и клиент, и серверожидают приёма сообщенийРассмотреть два варианта устройства канала:IсинхронныйIасинхронный ёмкости 1Упражнение 4: синхронные системыПо комнате летает два комараВ начальный момент времени оба комара не жужжатЕсли комар не жужжит, в следующий момент времени онначинает жужжатьЕсли комар жужжит, в следующий момент времени онперестаёт жужжатьЖужжание комара описывается булевой переменнойОписать систему жужжания двух комаров с такимтребованием: в каждый момент времени либо оба комаражужжат, либо оба комара не жужжатПодсказка: в теле требований можно использовать меткисостоянийУпражнение 5: переправаВолк, коза, капуста и лодочник с лодкой стоят на левом берегуреки и хотят переправиться на правыйТолько лодочник может грестиЛодка вмещает только двоих, включая лодочникаНельзя оставлять волка с козой, а также козу с капустой наодном берегу без присмотра лодочникаМогут ли все переправиться на правый берег?Упражнение 6: распределённые алгоритмыТри процесса соединены друг с другом в кольцооднонаправленными асинхронными каналами связи ёмкости 1:P2P1P3Каждый процесс имеет булеву переменную b, имеющую произвольное значение в начале работы системы, и ровно два разаделает следующее:Iпосылает в канал значение bIпринимает из канала значение, и если принято true, тозаписывает true в переменную bУпражнение 6: распределённые алгоритмыТри процесса соединены друг с другом в кольцооднонаправленными асинхронными каналами связи ёмкости 1:P2P1P3Убедиться, чтоIкаждый процесс рано или поздно выполнит всю своюпоследовательность действийI(каждый процесс в конце работы хранит значение true) ⇔(хотя бы один процесс в начале работы хранил значениеtrue)I(каждый процесс в конце работы хранит значение false)⇔ (ни один процесс в начале работы не хранил значениеtrue)Ещё немного синтаксиса и семантикиРанее на слайдах факт “процесс завершил работу”отождествлялся с фактом “процесс находится у меткисостояния после всех его инструкций”В общем случае всё работает сложнее: в некоторых случаяхпроцесс по завершении работы полностью исчезает изсистемы, и тогда он не будет находиться у метки состоянияпосле всех его инструкцийЕсли нет уверенности в том, удалился ли процесс, то следуетвыбрать другой способ выяснения того, завершился ли он(например, использовать булевы переменные как флагизавершения).

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