2. Модели Крипке. LTL. Безопасность, живость. (1185949)

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

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

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 2Модели КрипкеLTLБезопасность и живостьУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказыванийСистема:cobeginx := 1; y := 2||y := 1; x := 2coend(начальное состояние данных:Высказывания:x = i иy = ix = 0, y = 0),i ∈ZУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказыванийСистема:cobegin x := x + x || x := x + x coend(начальное состояние данных:Высказывания:x = i,i ∈Zx = 1)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказыванийСистема:cobegin x := x + x || x := x + x coend(начальное состояние данных:Высказывания:x = ix = 1),i ∈ZУсложнение: инструкция присваивания суммы реализованакак 4 атомарных действия:1.

прочитать значение первого слагаемого2. прочитать значение второго слагаемого3. вычислить результат — сумму прочитанных значений4. записать результат в целевую переменнуюУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказыванийСистема: схема из функциональных элементов с задержкойxВысказывания:&⊕yÿ(i ∈ {0, 1})Ixi : на вход x подано значение iIyi : на выходе y получено значение iУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказыванийСистема: волк, коза, капуста и лодочник в задаче о переправеВариации:1.

Все события (обед, посадка в лодку, переправа, высадка излодки, . . . ) мгновенны, и при необходимых условиях могуткак происходить, так и не происходить2. Все события, кроме переправы, мгновенны; обедпроисходит немедленно при соблюдении необходимыхусловий3. Все события, проме переправы, мгновенны; обед можеткак произойти, так и не произойти при соблюдениинеобходимых условийВысказывания:Iwr , gr , cr : волк/коза/капуста находятся на правом берегуIwa, ga, ca: волк/коза/капуста живыУпражнение 2Описать множество всех трасс заданной модели Крипкеaaa, bS— состояние, помеченное множеством высказываний {S}Переходы модели изображаются дугами— начальное состояниеУпражнение 3Является ли заданное множество трасс над непустыммножеством атомарных высказываний AP свойствома) безопасности?б) живости?1.

(2AP )ω2. ∅3. {a, b}ω(2AP = {a, b, c, d})4. {a}∗ · {b} · {a}ω(2AP = {a, b})5. {a, b}∗ · {a}ω∗6. {a, b, c} · {d} · {a}7. {ab}ω(2AP = {a, b})ω(2AP = {a, b, c, d})(2AP = {a, b})X ω = {w1 w2 w3 · · · | wi ∈ X }X ∗ = {w1 w2 . . . wk | wi ∈ X , k ∈ N0 }X · Y = {wx wy | wx ∈ X , wy ∈ Y }Упражнение 4Всегда ли верны следующие утверждения?1. Если P1 и P2 — свойства безопасности,то P1 ∩ P2 — свойство безопасности2.

Если P1 и P2 — свойства безопасности,то P1 ∪ P2 — свойство безопасности3. Если P1 и P2 — свойства живости,то P1 ∩ P2 — свойство живости4. Если P1 и P2 — свойства живости,то P1 ∪ P2 — свойство живостиУпражнение 5Записать LTL-формулу, адекватно формализующую следующеевысказывание:1. Кто много тренируется, тот обязательно достигнетсовершенства2. Если лифт отправился, то он обязательно остановится, иво время движения двери не откроются3. Два процесса никогда не займут критическую секциюодновременно4. Сообщение может быть потеряно в канале связи лишьконечное число раз5.

Приём и обработка сообщения обязательно чередуются6. Операция выполняется процессором ровно 4 такта7. Как только система сломалась, она начнёт бесконечночасто сигнализировать о неисправности, пока её питаниене отключатУпражнение 6В каких состояниях приведённой ниже модели выполняетсязаданная LTL-формула?baIAXaIAXXXaIAGaIAGFaIAFGaIAG(bUa)IAF(aUb)a, bУпражнение 6В каких состояниях приведённой ниже модели выполняетсязаданная LTL-формула?Ip, qqpp, qAF(XpUG¬q)p.

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

Тип файла PDF

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

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

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