Лекция 6. Свойства живучести в Promela. Спецификация и верификация свойств при помощи автоматов Бюхи (1158559), страница 2
Текст из файла (страница 2)
Пример конечного автомата A = S , s0 , L, F , Ts0 α0 S = {s0 , s1 , s2 , s3 , s4 }s1 α2 α4 L = {α 0 , α1 , α 2 , α 3 , α 4 , α5 }α1 s2 α s4 5 α3 s3 F = {s4 }T = {( s0 , α 0 , s1 ), ( s1 , α1 , s2 ),...}Вариант интерпретации (планировщик процессов) idle s0 α0 α4 α1 s2 α s4 5 α3 s3 ready pre-‐empt s1 α2 start run execute unblock stop block wai•ng end Записываем в виде never idle start ready pre-‐empt never {idle:(start) ->ready:(run) ->execute: if:: (pre-empt) -> goto ready:: (block) -> goto waiting:: (stop) -> goto endfi;waiting: (unblock) -> goto execute;end:skipexecute unblock }run stop block wai•ng end Детерминизм и недетерминизм • Конечный автомат A = S , s 0 , L , F , Tназывается детерминированным, только если ∀s, ∀l, ((( s, l, s' ) ∈ T ∧ ( s, l, s' ' ) ∈ T ) → s' ≡ s' ')– т.е.
целевое состояние перехода однозначно определяется исходным состоянием и меткой – в противном случае автомат называется недетерминированным deny Модель сервера запросов, работающего в бесконечном цикле s0 approve s2 true s1 request s3 true Определение прохода • Проходом конечного автомата S , s 0 , L , F , T называется такое упорядоченное и, возможно, бесконечное множество переходов из T: σ = ( s0 , l0 , s1 ), ( s1, l1, s2 ), ( s2 , l2 , s3 ),... что ∀ i , i ≥ 0 : ( s i , l i , s i + 1 ) ∈ T .
• Проход соответствует последовательности состояний из S и слову в алфавите L. idle start Последовательность состояний: {idle, ready, {execute, wai•ng}*} ready pre-‐empt execute unblock wai•ng run stop block end Соответствующее слово в L: {start, run, {block, unblock}*} Допускающий проход • Допускающим проходом конечного автомата A называется конечный проход σ, финальный переход которого (sn-‐1,ln-‐1,sn) ведёт в терминальное состояние idle start ready pre-‐empt execute unblock wai•ng run stop block Последовательность состояний для допускающего прохода: {idle, ready, execute, wai•ng, execute, end} end Соответствующее слово в L: {start, run, block, unblock, stop} Язык автомата • Языком автомата А называется множество слов в алфавите L, соответствующих допускающим проходам автомата А Язык автомата: {idle start start,run,{{pre-empt,run}+{block,unblock}*}*,stopready pre-‐empt execute unblock wai•ng run stop block end }Самое короткое слово языка: {start, run, stop} Описание свойств при помощи автомата Пример свойства: если сначала p=T, а позже q=T, !q то впоследствии r=F !p p q !r Если мы попали в терминальное состояние, то свойство нарушается r error Иногда нужно рассуждать о потенциально бесконечной задержке Классическое свойство живучести: «если p, тогда впоследствии q» Такое свойство может быть нарушено только бесконечным проходом Классическое определение описывает лишь конечные проходы Нужно описать, что автомат не может находиться в терминальном состоянии бесконечно долго.
!q !p p error q Немного обозначений • Для любого бесконечного прохода σ конечного автомата можно выделить два множества: – множество σ+ состояний, встречающихся конечное число раз, – множество σω состояний, встречающихся бесконечное число раз. σ+ σ σω Допускающий проход по Бюхи (ω-‐допускание) • Допускающим ω-‐проходом конечного автомата А называется такой бесконечный проход σ, что ∃i ≥ 0, ( si −1 , li −1 , si ) ∈ σ : si ∈ F ∧ si ∈ σωт.е. по крайней мере одно терминальное состояние встречается бесконечно часто.
idle start Допускающий ω-‐проход: {idle, ready, {execute, ready}*} ready pre-‐empt execute unblock wai•ng run stop block end Соответствующее ω-‐слово: {start, run, {pre-‐empt, run}*} Множество допускаемых автоматом ω-‐слов называется его ω-‐языком Расширение автоматов Бюхи (конечные проходы как частный случай бесконечных) • Расширяем алфавит автомата меткой ε (пустой переход), • Дополняем все конечные проходы бесконечным повторением перехода по метке ε. idle start Допускающий ω-‐проход: {idle, ready, execute, wai•ng, execute, [end,]*} ready pre-‐empt execute unblock wai•ng run stop block end ε Соответствующее ω-‐слово: {start, run, block, unblock, stop, ε*} Проверка свойств при помощи автоматов Бюхи • При помощи автомата Бюхи можно описать наблюдаемое поведение программы и требования к нему, • Проход автомата соответствует наблюдаемому вычислению (трассе) программы, • Определение допускаемости прохода позволяет рассуждать о выполнении или нарушении требований (свойств правильности).
Безопасность и живучесть • Безопасность – Любое свойство безопасности можно проверить, исследуя свойства отдельных состояний модели; – если свойство безопасности нарушено, всегда можно определить достижимое состояние системы, в котором оно нарушается; – для проверки свойств безопасности требуется генерировать состояния системы и для каждого из них проверять свойство; – при проверке таких свойств можно обойтись без темпоральных логик и автоматов Бюхи. • Живучесть – Для проверки свойств живучести необходимо рассматривать последовательности состояний (конечные и бесконечные проходы соотв.
автомата Бюхи); – для проверки свойств используются другие, более сложные алгоритмы; – свойства удобно описывать при помощи формул темпоральной логики, а проверять – при помощи автоматов Бюхи. Пример свойства безопасности Как только p впервые стало истинно, q больше не может быть истинно. never{do:: !p:: p -> breakoddo:: assert(!q)od}!p p assert(!q) Как только достигнуто состояние, удовлетворяющее условию, будет зафиксировано нарушение свойства. Рассуждать о бесконечных вычислениях здесь не требуется. Пример поведения системы bool p,q;A B active proctype A(){(!p && !q) -> p = true}s0 s0 active proctype B(){(p) -> q = true}!p∧ !q s1 s1 p = true s2 stop !p p assert(!q) p q = true s2 stop A∥B s0 s0 !p∧!q s1 s0 p = true stop s2 s0 p -‐ s0 p s2 s1 stop -‐ s1 q = true stop q = true -‐ s2 асинхронно s2 s2 stop stop синхронно s2 s0 stop -‐ -‐ Проверка свойства безопасности A∥B A∥B p0 s0 s0 !p∧!q p s1 s0 p = true stop s2 s0 p s2 s1 stop q = true stop s2 s2 stop stop s2 s0 p1 !p s0 s0 !p∧!q assert(!q) синхронно -‐ s0 Свойства безопасности всегда можно проверить p путём анализа -‐ s1 достижимости состояний q = true либо асинхронной параллельной композиции -‐ s2 процессов А∥В, либо её stop синхронной композиции с процессом, описывающим -‐ -‐ свойство – (A∥B)∣P s1 s0 p = true stop s2 s0 p -‐ s0 p stop s s-‐ s1 p1 p1 2 1 q = true q = true stop pp1 s2 s2 stop stop p1 s2 -‐ -‐ s2 1 stop -‐ -‐ p1 Пример свойства живучести Как только p впервые стало истинно, в течение конечного числа шагов q также станет истинным.
Нарушение свойства: p становится истинным, а затем q может навсегда остаться ложным. !p p !q Мы можем заключить о нарушении свойства, только если обнаружим удовлетворяющую условию потенциально бесконечную последовательность состояний Пример поведения системы bool p,q;A B active proctype A(){(!p && !q) -> p = true}s0 s0 active proctype B(){(p) -> q = false}Модель не циклична! !p p !q !p∧ !q s1 s1 p = true s2 p stop q = false s2 stop A∥B s0 s0 !p∧!q s1 s0 p = true stop s2 s0 p -‐ s0 p s2 s1 stop -‐ s1 q = false q = false stop -‐ s2 асинхронно s2 s2 stop stop синхронно s2 -‐ stop -‐ -‐ Проверка свойства живучести A∥B A∥B Модель s0 s0 не циклична! !p∧!q p0 p s1 s0 p = true stop s2 s0 p1 !p s0 s0 !q синхронно p q = false stop q = false stop stop s2 s0 stop -‐ -‐ p = true stop p s2 s1 stop -‐ s1 -‐ s2 s1 s0 s2 s0 -‐ s0 p s2 s2 !p∧!q -‐ s0 p stop s s-‐ s1 p1 p1 2 1 Для проверки свойств живучести необходимо рассматривать бесконечные вычисления q = false q = false stop pp1 s2 s2 stop stop p1 s2 -‐ -‐ s2 1 stop -‐ -‐ p1 ε Спасибо за внимание!Вопросы?.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
