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

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

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

Верификация программна моделяхЛекция №7Свойства живучести в SPIN.Спецификация и верификация свойств припомощи автоматов Бюхи.Константин Савенков (лектор)План лекции• Проверка свойств живучести в Spin.Конструкции never• Проверка свойств правильности• Автоматы Бюхи• Проверка свойств при помощи автоматовБюхиСпособы описания свойствправильности (напоминание)• Свойства правильности могут задаваться как:– свойства достижимых состояний (свойствабезопасности),– свойства последовательностей состояний (свойстваживучести);• В языке Promela– ассерты:• локальные ассерты процессов,• инварианты системы процессов;– метки терминальных состояний:свойствасостояний• задаём допустимые точки останова процессов;– метки прогресса (поиск циклов бездействия);– утверждения о невозможности (never claims)• например, определяются LTL-формулами;– трассовые ассерты.свойствапоследовательностейсостоянийКонструкции never(отрицание свойств)Never say never(народная пословица)Рассуждения о вычисленияхпрограммы• Существует несколько вариантов формализациивычислений распределённой системы:– последовательность состояний,– последовательность событий (переходов),– последовательность значений высказываний всостояниях (свойства состояний) – трассы.bit x,y;byte mutex;x = 1 (y==0) mutex++ printf mutex-- x = 0active proctype A(){x = 1;x==1x==1x==1x==1x==1x==0x==0(y == 0) ->y==0y==0y==0y==0y==0y==0y==0mutex++;printf(“%d\n”, _pid); mutex==0 mutex==0 mutex==0 mutex==1 mutex==1 mutex==0 mutex==0mutex--;x = 0p!p!ppp!pp}p: (x == mutex)q: (x != y)!qqqqqq!qПример• «не существует вычисления, в котором за pследует q»active proctype invariant(){assert(!p || !q);}НЕПРАВИЛЬНО!Свойства только дляодного состоянияactive proctype invariant(){p;do::assert(!q);od}НЕПРАВИЛЬНО!Асинхронноевыполнениеnever claims(утверждения о невозможности)• выполняются синхронно с моделью,• если достигнут конец, то – ошибка,• состоят из выражений и конструкцийзадания потока управления,• фактически, описывают распознающийавтомат.Пример• «не существует вычисления, в котором за pследует q»never{p;q}never{do:: p -> breakoddo:: q -> breakod}НЕПРАВИЛЬНО!Синхронное выполнение– будет работать только дляпервых двух состоянийПРАВИЛЬНО!Конструкция never• может быть как детерминированной, так и нет;• содержит только выражения без побочных эффектов(соотв.

булевым высказываниям на состояниях);• используются для описания неправильного поведениясистемы;• прерывается при блокировании:– блокируется => наблюдаемое поведение не соответствуетописанному,– паузы в выполнении тела never должны быть явно заданыкак бесконечные циклы;• never нарушается, если:– достигнута закрывающая скобка,– завершена конструкция accept (допускающий цикл);• бездействие может быть описано как конструкция neverили её часть (для обнаружения циклов бездействия естьтело never «по умолчанию»).Пересечение множеств трасс(языков)Описаниеповедения наPromelaКОНТРПРИМЕРЫОграничениясправедливостиСпецификация припомощи never(отрицание свойств)Проверка инварианта системы припомощи конструкции nevernever{do:: invariant:: else -> breakod}never{do:: assert(invariant)od}never{do:: atomic{ !invariant ->assert(invariant)}od}Ссылки на точки процессовиз тела never• из тела never можно сослаться на точку (состояниеуправления) любого активного процесса;• синтаксис такой ссылки:– proctypename[pidnr]@labelname• это выражение истинно только если процесс с номеромpidnr находится в точке описания типа процессаproctypename, размеченной меткой labelname;имя типа процессаuser[1]@critномер экземпляра процессаимя метки• если существует только один процесс типа user, то можноопустить часть *pidnr]:user@critСсылки на точки процессов(пример)never{do:: user[1]@crit && user[2]@crit -> break:: elseod}Используемметкиуправлениявместосчётчикапроцессовmtype = {p, v};chan sem = [0] of { mtype };active proctype semaphore(){do sem!p ; sem?v od}active [2] proctype user(){ assert(_pid == 1 || _pid == 2);do:: sem?p ->crit:/*критическая секция*/sem!vod}Проверяем, что процесс завершилсяactive proctype runner(){do:: ...

...:: else -> breakod;L:(false)}active proctype runner(){do:: ... ...:: else -> breakod}runner@LКонструкции never:• могут содержать любые конструкции потока управления:– if, do, unless, atomic, d_step, goto;• должны содержать только выражения:– т.е. q?[ack] или nfull(q), но не q?ack или q!ack;• не должны содержать меток progress и end;• нужно аккуратно использовать never вместе с метками progress;• могут использоваться для фильтрации интересующего насповедения:never{do:: atomic {(p || q) -> assert(r)}od}Проверяем assert(r) накаждом шаге, но лишь длятех вычислений, гдевыполняются p или q.Видимость• все конструкции never – глобальны;• тем самым, в них можно ссылаться на– глобальные переменные,– каналы сообщений,– точки описания процессов (метки),– предопределённые глобальные переменные,– но не локальные переменные процессов;• нельзя ссылаться на события (действия),только на состояния.

А если очень хочется?Ассерты на трассы• Используются для описания правильных и неправильныхпоследовательностей выполнения операторов send и receive.mtype = {a, b };chan p = [2] of mtype;chan q = [1] of mtype;trace {do:: p!a; q?bod}Если в ассерте упоминаетсяхотя бы одна операцияотправки сообщения вканал q, ему должнысоответствовать всеподобные операцииЭтот ассерт фиксирует лишь взаимный порядоквыполнения операций посылки сообщенийв канал p и приёма сообщений по каналу q.Он утверждает, что каждая отправкасообщения a в канал p сопровождаетсяполучением сообщения b из канала q.Отклонение от этой схемы приветётк сообщению об ошибке.В ассертах на трассы могу использоваться лишьоператоры отправки и получения сообщений.Не могут использоваться переменные, толькоконстанты, mtype или _q?_ используется для обозначения приёмалюбого сообщенияПримерВерно ли, что в протоколе голосования типы сообщенийone, two и winner приходят в строгом порядке, так чтоникто не увидит сообщение one после сообщения two?trace {do:: q[0]?one,_:: q[0]?two,_ -> breakod;do:: q[0]?two,_:: q[0]?winner,_ -> breakod}Верификация(неправда!)> ./spin -a leader_trace.pml> gcc -o pan pan.c> ./panpan: event_trace error (no matching event) (at depth 64)pan: wrote leader_trace.pml.trail(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completed+ Partial Order ReductionFull statespace search for:trace assertion+never claim- (none specified)assertion violations+acceptancecycles- (not selected)invalid end states+State-vector 200 byte, depth reached 63, errors: 152 states, stored0 states, matched52 transitions (= stored+matched)12 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)pan: elapsed time 0 secondsКак же так?Ассерт нарушен!> ./spin -t -c leader_trace.pmlproc 0 = :init:proc 1 = nodeproc 2 = nodeproc 3 = nodeproc 4 = nodeproc 5 = nodeq\p0123451.....out!one,45....out!one,55.....in?one,51.....out!two,54...out!one,14....in?one,15....out!two,15.....in?two,11.....out!one,53..out!one,23...in?one,24...out!two,24....in?two,22.out!one,32..in?one,33..out!two,33...in?two,31.in?one,42.out!two,42..in?two,41.in?two,51.in?one,5spin: trail ends after 64 stepsАссерты notrace• обратное утверждение: ассерт notraceутверждает, что описанный шаблон поведенияневозможенmtype = {a, b };chan p = [2] of mtype;chan q = [1] of mtype;notrace {do:: p!a; q?b:: q?b; p!aod}Этот ассерт утверждает, что не существуетвычисления, в котором отправкасообщения a в канал p сопровождаетсяполучением сообщения b из q, и наоборот.Сообщение об ошибке генерируется, еслидостигнута закрывающая фигурная скобкаассерта notrace.О невозможном и неизбежном• ассерт формализует утверждение:– указанное выражение не может принимать значение ложь,если достигнут ассерт;• метка end формализует утверждение:– система не может завершить работу без того, чтобы всеактивные процессы либо завершились, либо остановились вточках, помеченных метками end;• метка progress формализует утверждение:– система не может выполняться бесконечно без того, чтобыпроходить через точку, помеченную меткой progressбесконечно часто;• конструкция never формализует утверждение:– система не может демонстрировать поведение (конечноеили бесконечное), полностью совпадающее с описанным втеле never;• ассерт на трассах формализует утверждение:– система не может демонстрировать поведение, отличное отописанного шаблона.Автоматы Бюхи.Проверка свойств линейноговремени.Проверяемые свойства(напоминание)• Свойства моделей– 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' ' – т.е.

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

Тип файла PDF

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

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

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