8-9. SPIN - практические задания по проверке LTL-спецификаций (1185954)

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

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

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 8–9Spin(практика)Упражнение 1: реализация модели КрипкеПроверить выполнимость свойств в модели Крипкеba, cIG(a → b ∨ c)IGFaIFGaIGF¬c → F(a ∧ b)IGF¬c → G(¬bUa ∧ b)∅a, bУпражнение 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;}Внимательно посмотреть на флаг “слабая справедливость” в настройках верификацииУпражнение 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-файл и есть ли нужная программа для его просмотра.

Список файлов лекций