lect07 (1158548), страница 2

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

Текст из файла (страница 2)

по крайней мере одно терминальное состояниевстречается бесконечно часто.idlestartДопускающий ω-проход:{idle, ready, {execute, ready}*}readypre-emptrunstopexecuteendblockunblockwaitingСоответствующее ω-слово:{start, run, {pre-empt, run}*}Множество допускаемых автоматомω-слов называется его ω-языкомРасширение автоматов Бюхи(конечные проходы как частный случай бесконечных)• Расширяем алфавит автомата меткой ε (пустойпереход),• Дополняем все конечные проходы бесконечнымповторением перехода по метке ε.idlestartДопускающий ω-проход:{idle, ready, execute, waiting, execute, [end,]*}readypre-emptrunstopexecuteendblockunblockwaitingСоответствующее ω-слово:{start, run, block, unblock, stop, ε*}Проверка свойств при помощиавтоматов Бюхи• При помощи автомата Бюхи можно описатьнаблюдаемое поведение программы итребования к нему,• Проход автомата соответствуетнаблюдаемому вычислению (трассе)программы,• Определение допускаемости проходапозволяет рассуждать о выполнении илинарушении требований (свойствправильности).Безопасность и живучесть• Безопасность– Любое свойство безопасности можно проверить, исследуясвойства отдельных состояний модели;– если свойство безопасности нарушено, всегда можноопределить достижимое состояние системы, в котором ононарушается;– для проверки свойств безопасности требуется генерироватьсостояния системы и для каждого из них проверять свойство;– при проверки таких свойств можно обойтись безтемпоральных логик и автоматов Бюхи.• Живучесть– Для проверки свойств живучести необходимо рассматриватьпоследовательности состояний (конечные и бесконечныепроходы соотв.

автомата Бюхи);– для проверки свойств используются другие, более сложныеалгоритмы;– свойства удобно описывать при помощи формултемпоральной логики, а проверять – при помощи автоматовБюхи.Пример свойства безопасностиКак только p впервые стало истинно,q больше не может быть истинно.never{do:: !p:: p -> breakoddo:: assert(!q)od}!ppassert(!q)Как только достигнуто состояние, удовлетворяющее условию,будет зафиксировано нарушение свойства. Рассуждать обесконечных вычислениях здесь не требуется.Пример поведения системыbool p,q;ABactive proctype A(){(!p && !q) -> p = true}s0s0active proctype B(){(p) -> q = true}!p∧ !qs1ps1p = trues2q = trues2stopstop!ppA∥Bs0 s0!p∧!qs1 s0p = truestops2 s0pps2 s1stopq = truestopасинхронно s2 s2assert(!q)синхронноstopstops2 s0- s0- s1q = true- s2stop- -Проверка свойствабезопасностиA∥BA∥Bp0s0 s0!p∧!qps1 s0p = truestops2 s0ps2 s1stopq = truestops2 s2stopstops2 s0!ps0 s0!p∧!qp1assert(!q)синхронно- s0Свойства безопасностивсегда можно проверитьpпутём анализа- s1достижимости состоянийq = true либо асинхроннойпараллельной композиции- s2процессов А∥В, либо еёсинхронной композиции сstopпроцессом, описывающим- свойство – (A∥B)∣Ps1 s0p = truestops2 s0ppp1 s2 s1stopq = truestopp1 s2 s2stopstopp1 s2 -- s0- s1 p1q = true- s2 p1stop- - p1Пример свойства живучестиКак только p впервые стало истинно, в течение конечногочисла шагов q также станет истинным.Нарушение свойства: p становится истинным, а затем qможет навсегда остаться ложным.!pp!qМы можем заключить о нарушении свойства, только еслиобнаружим удовлетворяющую условиюпотенциально бесконечную последовательность состоянийПример поведения системыbool p,q;ABactive proctype A(){(!p && !q) -> p = true}s0s0active proctype B(){(p) -> q = false}Модельне циклична!!p∧ !qs1ps1p = trues2q = falses2stopstop!pp!qA∥Bs0 s0!p∧!qs1 s0p = truestops2 s0pps2 s1stop- s1q = falsestopq = falsestopstopstopасинхронно s2 s2синхронно- s0s2 -- s2- -Проверка свойстваживучестиA∥BA∥Bs0 s0Модельне циклична!!p∧!qps1 s0p = truestops2 s0stopq = truestops2 s2stopstops2 s0!ps0 s0!p∧!qp1!qсинхронноp1 s2 s1q = truestop- -p = truestopДля проверки свойствживучести необходиморассматриватьбесконечные вычисленияstopq = truestopp1 s2 s2stopstopp1 s2 -- s0pp- s1- s2s1 s0s2 s0- s0pps2 s1p0- s1 p1q = true- s2 p1stop- - p1εСпасибо за внимание!Вопросы?.

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

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