lect07 (1158548)

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

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

Верификация программна моделяхЛекция №7Практические приёмы абстракции.Спецификация и верификация свойств припомощи автоматов Бюхи.Константин Савенков (лектор)План лекции••••Практические приёмы абстракцииПроверка свойств правильностиАвтоматы БюхиПроверка свойств при помощи автоматовБюхиПрактические приёмы абстракцииОбщая схемаПрограмма на СМодель наPromela• Неправильный подход!– Если строить модель без оглядки на проверяемыесвойства, то она получится слишком детальной.– Скорее всего, не хватит ресурсов на верификацию.Общая схемаПрограмма на СМодель наPromelaПроверяемыесвойства• Модель должна моделировать только то,что влияет на выполнимость проверяемыхсвойств.Примерvoid f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}• Модель точная, но у неёслишком многодостижимых состояний.• Давайте посмотрим назаданные свойства.proctype f(int x){do:: x < 3 ->printf(“Case 1\n”);x = x + 1:: x >= 10 ->break;:: else ->printf(“Case 2\n”);x = x + 1od}init {int x;do:: x++;:: x--;:: break;od;run f(x)}Примерvoid f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}«Проверить, что передпечатью “Case 2”всегда была выполненапечать “Case 1”.»proctype f(int x){do:: x < 3 ->printf(“Case 1\n”);x = x + 1:: x >= 10 ->break;:: else ->printf(“Case 2\n”);x = x + 1od}init {int x;do:: x++;:: x--;:: break;od;run f(x)}Примерvoid f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}«Проверить, что передпечатью “Case 2”всегда была выполненапечать “Case 1”.»mtype {X1, X2, X3};proctype f(mtype x){do:: x == X1 ->printf(“Case 1\n”);incr(x);:: x == X3 ->break;:: x == X2 ->printf(“Case 2\n”);incr(x);inline incr(x){odif}:: x += 1;init{:: skipmtype x;fiif}:: x = X1:: x = X2:: x = X3fi;run f(x)}Не загромождаеммодельПриёмы абстракции•••••Абстракция предикатовАбстракция типов данныхАбстракция наблюдаемых переменныхАбстракция от «лишнего» кодаАбстракция от функций и системныхвызововАбстракция предикатовif(x < 0){printf (“Case 1”);}else{printf (“Case 2”);}…if:: printf (“Case 1”);:: printf (“Case 2”);fi• В модели увеличивается количество возможныхвычислений– если формула не нарушается ни на одном вычислении модели,то на исходной программе она также будет выполнима,– если формула нарушается на одном из «добавленных»вычислений, необходимо увеличить уровень детализациимоделиАбстракция типов данныхint x;…if(x < 0) {…}else {if(x < 3) {…}else {…}…}mtype { X1, /*x < 0*/X2, /*0 <= x < 3*/X3 /*x >= 3*/};if:: x == X1 -> …:: x == X2 -> …:: x == X3 -> …fi• Диапазон типа данных разбивается на классыэквивалентности относительно конструкций организациипотока управления и проверяемых свойств.• Необходимо корректно моделировать:– предикаты в операторах ветвления,– операторы, изменяющие значения переменных этого типа.Абстракция наблюдаемыхпеременных• Из модели удаляется переменные, значениякоторых не влияют на выполнимость заданныхсвойств:– не используются при формулировке свойства,– не влияют на поток управления модели.• Операторы модели могут быть связаныдостаточно сложными зависимостями поданным и управлению, поэтому в ходе удаленияпеременных допускается только расширениемножества возможных вычислений моделиАбстракция наблюдаемыхпеременныхint x;…while (x != 0){x = get_value();}…printf (“Something\n”);printf (“Something\n”);do:: skip:: breakod;printf(“Something\n”)• Свойство – операция печати будет выполнена один раз,• Если абстрагируемся от цикла – теряем возможностьбесконечного зацикливания (сужаем множествовозможных вычислений).Абстракция «лишнего» кода…some_func();printf(“Func called!\n”)……some_func: skip;…• Свойство – some_func() будет вызвана.• Можно абстрагироваться от:– кода, не влияющего на проверяемое свойство (printf),– реального выполнения операторов, если нас интересует лишьфакт его выполнения («функция была вызвана»).• Здесь также необходимо следить за допустимымивычислениями.…int x;x = some_func();if (x)……int x;some_func: skip;if:: x -> ……Абстракция от функций и системныхвызововff(){sys_call();}sys_callcallres• Выполнение реальной функции заменяется наобмен сообщениями с процессом-«заглушкой»,• Обмен сообщениями должен корректномоделировать вызов функции:– синхронное взаимодействие, гарантированный отклик.От чего не стоит абстрагироваться• Поток управления:– ветвление, циклы;• Можно добавлять новые ветви и пути выполнения:– см.

«абстракция предикатов»,– если на добавленных путях будет нарушаться свойство,то эта ошибка будет обнаружена при анализеконтрпримера.• Нельзя убирать пути выполнения на основе «методапристального взгляда»– можно случайно убрать путь выполнения программы,на котором происходит нарушение свойстваправильности программы.Пример поэтапной абстракции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 , (a, 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  т.е.

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

Тип файла PDF

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

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

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