7 - Свойства живучести в SPIN. Спецификация и верификация свойств при помощи автоматов Бюхи (1161371), страница 2

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

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

целевое состояние перехода однозначноопределяется исходным состоянием и меткой– в противном случае автомат называетсянедетерминированнымdenyМодель серверазапросов, работающегов бесконечном циклеs0approves2trues1requests3trueОпределение прохода• Проходом конечного автомата S , s0 , L, F , Tназывается такое упорядоченное и, возможно,бесконечное множество переходов из T:  ( s0 , l0 , s1 ), ( s1 , l1 , s2 ), ( s2 , l2 , s3 ),...что i, i  0 : ( si , li , si 1 )  T .• Проход соответствует последовательности состояний из Sи слову в алфавите L.idlestartПоследовательность состояний:{idle, ready, {execute, waiting}*}readypre-emptrunstopexecuteendblockunblockwaitingСоответствующее слово в L:{start, run, {block, unblock}*}Допускающий проход• Допускающим проходом конечногоавтомата A называется конечный проход σ,финальный переход которого (sn-1,ln-1,sn)ведёт в терминальное состояниеidlestartreadypre-emptrunПоследовательность состоянийдля допускающего прохода:{idle, ready, execute, waiting, execute, end}stopexecuteendblockunblockwaitingСоответствующее слово в L:{start, run, block, unblock, stop}Язык автомата• Языком автомата А называется множествослов в алфавите L, соответствующихдопускающим проходам автомата АЯзык автомата:{idlestartstart,run,{{pre-empt,run}+{block,unblock}*}*,stopreadypre-emptrunstopexecuteendblockunblock}waitingСамое короткое слово языка:{start, run, stop}Описание свойств при помощиавтоматаПример свойства:если сначала p=T,а позже q=T,!qто впоследствии r=F!ppq!rЕсли мы попали втерминальное состояние, тосвойство нарушаетсяrerrorИногда нужно рассуждать опотенциально бесконечной задержкеКлассическое свойство живучести:«если p, тогда впоследствии q»!pТакое свойство может быть нарушено толькобесконечным проходомКлассическое определение описывает лишьконечные проходыНужно описать, что автомат не можетнаходиться в терминальном состояниибесконечно долго.!qperrorqНемного обозначений• Для любого бесконечного прохода σ конечногоавтомата можно выделить два множества:– множество σ+ состояний, встречающихся конечноечисло раз,– множество σω состояний, встречающихся бесконечноечисло раз.σ+σσωДопускающий проход по Бюхи(ω-допускание)• Допускающим ω-проходом конечного автомата Аназывается такой бесконечный проход σ, чтоi  0, ( si 1 , li 1 , si )   : si  F  si  т.е.

по крайней мере одно терминальное состояниевстречается бесконечно часто.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 s 0!p∧!qps1 s 0p = truestops2 s 0ps2 s 1stopq = truestops2 s 2stopstops2 s 0!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 s 0Модельне циклична!!p∧!qps1 s 0p = truestops2 s 0stopq = truestops2 s 2stopstops2 s 0!ps0 s0!p∧!qp1!qсинхронно- s0p1 s2 s1q = truestop- -p = truestopДля проверки свойствживучести необходиморассматриватьбесконечные вычисленияstopq = truestopp1 s2 s2stopstopp1 s2 -- s0pp- s1- s2s1 s0s2 s0pps2 s 1p0- s1 p1q = true- s2 p1stop- - p1εСпасибо за внимание!Вопросы?.

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

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