Семинар 2. Модели Крипке. CTL_ LTL. Безопасность_ живость_ справедливость (1185513)

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

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

Математические методыверификации схем и программСеминар 2Модели Крипке, CTL, LTL,Безопасность, живость,справедливостьУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система:cobegin p1 | | p2 coend , гдеp1:p2:x := 1 ;y := 2y := 1 ;x := 2Начальное состояние данных: x = 0, y = 0Атомарные высказывания:x = i,y =i(i ∈ Z)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система:cobegin x := x + x | | x := x + x coendНачальное состояние данных: x = 1Атомарные высказывания: x = i(i ∈ Z)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система:cobegin x := x + x | | x := x + x coendНачальное состояние данных: x = 1Атомарные высказывания: x = i(i ∈ Z)А если операция сложения не атомарна?Построить модель в предположении, что присваивание x := y + zреализуется как четыре неделимые команды работы с локальнымстеком программы: положить в стек значение y ; положить в стекзначение z; выбрать из стека два верхних значения, сложить иположить результат в стек; выбрать значение из стека и загрузитьв переменнуюУпражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система — схема из функциональных элементов с задержкой:x⊕∨¬ÿyАтомарные предикаты: x0 , x1 , y0 , y1 , ÿ0 , ÿ1(индекс — текущее значение переменной/задержки)Упражнение 1Построить модель Крипке для заданной системы и заданногонабора атомарных высказываний.Система: волк, коза, капуста и лодочник в задаче о переправе1.

Лодочник переправляет мгновенно и может отдыхать наберегу сколько угодно, поедание не мгновенно2. Лодочник переправляет дольше, чем происходит поедание,и не отдыхает на берегу3. Лодочник переправляет дольше, чем происходит поедание,и может отдыхать на берегуАтомарные предикаты: волк переправлен (wr ), коза переправлена (gr ), капуста переправлена (cr ), коза жива (ga), капуста несъедена (ca)Упражнение 2Описать множество всех трасс заданной модели Крипке.aa∅a, bУпражнение 3Является ли множество P свойствома) безопасностиб) живоститрасс над непустым множеством атомарных высказываний AP?1.2.3.4.5.6.7.P = AP ωP =∅AP = {a, b, c},AP = {a, b}, PAP = {a, b}, PAP = {a, b, c},AP = {a, b}, PP = {a, b}ω= {a}∗ · {b} · {a}ω= {a, b}∗ · {a}ωP = {a, b}∗ · {c} · {a}ω= {ab}ω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-формула?baIIIIIIIAXaAXXXaAGaAGFaAFGaAG(bUa)AF(aUb)∅a, bУпражнение 6В каких состояниях приведённой ниже модели выполняетсязаданная LTL-формула?p, qqpp, q∅IAF(XpUG¬q)p∅Упражнение 7Записать формулу логики CTL, адекватно формализующуюследующее высказывание:1. Если постоянно запрашивать вход в критическую секцию,то когда-нибудь доступ в неё будет получен2.

Между приёмом и обработкой сообщения оно никогда неудаляется3. Когда компьютер запущен, всегда есть возможность еговыключить4. Если компьютер сломался, то это навсегда5. Если когда-нибудь я захочу всё бросить, то всегда смогуэто сделать на следующий день6. Если когда-нибудь обнаружится, что я не сдал сессию, томеня обязательно вышвырнут на следующий деньУпражнение 8В каких состояниях приведённой ниже модели выполняетсязаданная CTL-формула?dac1.2.3.4.5.AGAFaEFbAFbEGbEG¬bbУпражнение 8В каких состояниях приведённой ниже модели выполняетсязаданная CTL-формула?dac1.2.3.4.5.EXdAXdE(cU¬c)A(¬cUEFc)A(bUA(aUd))bУпражнение 9Будет ли верным для любых модели M и состояния sследующее утверждение:если M, s |= ϕ, то M, s |= ψ ?1.2.3.4.5.6.7.8.ϕ = AFAGp, ψ = AFGpϕ = AFGp, ψ = AFAGpϕ = AFEGp, ψ = AFGpϕ = AFGp, ψ = AFEGpϕ = AGAFp, ψ = AGFpϕ = AGFp, ψ = AGAFpϕ = AGEFp, ψ = AGFpϕ = AGFp, ψ = AGEFpУпражнение 10Какие пути приведённой ниже модели M не входят в множествоTr (M, Fair ) для ограничений справедливостиFair = (WeakFair , StrongFair )?αγβα1.2.3.4.5.6.WeakFairWeakFairWeakFairWeakFairWeakFairWeakFair= ∅, StrongFair = ∅;= {α}, StrongFair = ∅;= {α, β}, StrongFair = ∅;= {α}, StrongFair = {β};= ∅, StrongFair = {α, β};= ∅, StrongFair = {α, β, γ};Упражнение 11Описать всевозможные условия справедливостиFair = (WeakFair , StrongFair ), для которых будет верносоотношение M, Fair |= AGFa?γ∅∅γγδγM:a∅αβ.

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

Тип файла PDF

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

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

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