lect_all (1161275), страница 10

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

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

«абстракция предикатов»,– если на добавленных путях будет нарушаться свойство,то эта ошибка будет обнаружена при анализеконтрпримера.• Нельзя убирать пути выполнения на основе «методапристального взгляда»– можно случайно убрать путь выполнения программы,на котором происходит нарушение свойстваправильности программы.Пример поэтапной абстракцииint x = 0;…while (x < 5){x++;}…printf (“Something\n”);1cycle: do:: inc: skip:: breakod;printf(“Something\n”)2//finite cycle removedprintf (“Something\n”);• Свойство – «Рано или поздно “Something” будетнапечатано».• При полной предикатной абстракции модель корректна, ноне адекватна свойству.• Если мы докажем, что в цикле – конечное число итераций,от него можно абстрагироваться.• Для этого нужно показать, что между двумя проверкамиусловия цикла всегда происходит инкремент х.Типичные ошибки и «странности»bit b;...if:: b ==:: b ==:: b ==:: b ==fi«Я хочу повыситьвероятность b == 1»1110->->->->AAABНедетерминизм связанне с понятием вероятности, ас понятием возможностиТипичные ошибки и «странности»bit b;active proctype A(){do:: b == 1 -> A:: else -> skipod}bit b;active proctype A(){(b == 1) -> A}«Я жду, пока невыполнится условие!»Используйте нативныеконструкции Promela!Типичные ошибки и «странности»bit b;...if:: b = 1:: b = 0fi;if:: b == 1 -> A:: b == 0 -> Bfiif:: A:: Bfi«Переменная можетпринимать разныезначения»От неё вообще нужноабстрагироваться!Типичные ошибки и «странности»chan f1 = [0] of bit;chan f2 = [0] of bit;active proctype caller(){do:: if::f1!m;:: else -> breakfi;...od}active proctype callee(){msg m;do:: f1?m -> f2!mod}«Но я же долженучесть, что каналможет быть занят!»Некорректное моделированиевызова функции: вызов«сбрасывается», если процесс«заглушка» занятТипичные ошибки и «странности»«Я сначала построюмодель, а потомуберу всё лишнее»Сначала прочитайтеспецификацию!!!Автоматы Бюхи.Проверка свойств линейноговремени.Проверяемые свойства(напоминание)• Свойства моделей– Tr(M) – множество всех трасс модели,– φ – свойство правильности.• Свойство выполняется на модели:M   ,   Tr( M )     • Свойство нарушается на модели, еслинарушается хотя бы на одной из трасс:M    ,   Tr( M )     Отрицание свойств(вспоминаем про двойственность)• Доказательство нарушения свойства φM    ,   Tr( M )     • Отличается от доказательства выполнения¬φM    ,   Tr( M )    • ПОЧЕМУ?M    ,   Tr( M )     MM    ,   Tr( M )        ,   Tr( M )    Более наглядноM φM ¬φφ ¬φМММ¬ (M φ)¬ (M ¬φ)Пример• Одновременное выполнение Mbyte x = 0;init {do:: x = 0:: x = 2od}  и M never {do:: assert(x == 0)od}Нарушаетсявыполнениемx=2never {do:: assert(x != 0)od}Нарушаетсявыполнениемx=0Автоматы и логика• Проще проверять нарушение свойства, чемего выполнение• Нарушение свойства описывается припомощи конструкции never – автомата,распознающего неправильное поведение• Свойства на последовательностяхсостояний удобно описывать при помощитемпоральной логикиКонечные автоматы• Конечный автомат A задаётся сигнатуройS , s0 , L, F , Tгде– S – множество состояний,– s0  S – начальное состояние,– L – конечное множество меток (символов),– F  S – множество терминальных символов,– T  S  L  S – отношение перехода насостояниях.Пример конечного автоматаA  S , s0 , L, F , Ts0α0S  s0 , s1 , s2 , s3 , s4 α2α4L  0 , 1 ,  2 ,  3 ,  4 , 5 s1α1s2 α s45α3s3F  {s4 }T  {( s0 , 0 , s1 ), ( s1 , 1 , s2 ),...}Вариант интерпретации(планировщик процессов)idles0α0α4α1s2 α s45α3s3readypre-empts1α2startexecuteunblockwaitingrunstopblockendЗаписываем в виде neveridlestartreadypre-emptnever {idle:(start) ->ready:(run) ->execute: if:: (pre-empt) -> goto ready:: (block) -> goto waiting:: (stop) -> goto endfi;waiting: (unblock) -> goto execute;end:skipexecuteunblock}waitingrunstopblockendДетерминизм и недетерминизм• Конечный автомат A  S , s0 , L, F , Tназывается детерминированным, только еслиs, l , ( s, l , s' )  T  ( s, l , s' ' )  T   s'  s' ' – т.е.

целевое состояние перехода однозначноопределяется исходным состоянием и меткой– в противном случае автомат называетсянедетерминированным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»Такое свойство может быть нарушено толькобесконечным проходомКлассическое определение описывает лишьконечные проходыНужно описать, что автомат не можетнаходиться в терминальном состояниибесконечно долго.!q!pperrorqНемного обозначений• Для любого бесконечного прохода σ конечногоавтомата можно выделить два множества:– множество σ+ состояний, встречающихся конечноечисло раз,– множество σω состояний, встречающихся бесконечноечисло раз.σ+σσωДопускающий проход по Бюхи(ω-допускание)• Допускающим ω-проходом конечного автомата Аназывается такой бесконечный проход σ, что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 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εСпасибо за внимание!Вопросы?Верификация программна моделяхЛекция №8Логика линейного времени (LTL).Константин Савенков (лектор)План лекции• Логика линейного времени (LTL)• Свойства, инвариантные к прореживанию• Связь между LTL и автоматами Бюхи/ конструкциями never• Применение LTL в системе Spin• Практические приёмы формулированиясвойств на LTLПроверка свойств при помощиавтоматов Бюхи(напоминание)• При помощи автомата Бюхи можно описатьнаблюдаемое поведение программы итребования к нему,• Проход автомата соответствует наблюдаемомувычислению (трассе) программы,• Определение допускаемости проходапозволяет рассуждать о выполнении илинарушении требований (свойствправильности).• Задавать свойства правильности при помощиавтоматов неудобно.Безопасность и живучесть• Безопасность(напоминание)– Любое свойство безопасности можно проверить, исследуясвойства отдельных состояний модели;– если свойство безопасности нарушено, всегда можноопределить достижимое состояние системы, в котором ононарушается;– для проверки свойств безопасности требуется генерироватьсостояния системы и для каждого из них проверять свойство;– при проверки таких свойств можно обойтись безтемпоральных логик и автоматов Бюхи.• Живучесть– Для проверки свойств живучести необходимо рассматриватьпоследовательности состояний (конечные и бесконечныепроходы соотв.

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

Список файлов лабораторной работы