Семинар 8. SPIN практика
Описание файла
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)Ещё немного синтаксиса и семантикиРанее на слайдах факт “процесс завершил работу”отождествлялся с фактом “процесс находится у меткисостояния после всех его инструкций”В общем случае всё работает сложнее: в некоторых случаяхпроцесс по завершении работы полностью исчезает изсистемы, и тогда он не будет находиться у метки состоянияпосле всех его инструкцийЕсли нет уверенности в том, удалился ли процесс, то следуетвыбрать другой способ выяснения того, завершился ли он(например, использовать булевы переменные как флагизавершения).