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

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

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

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

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

Тип файла PDF

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

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

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