Лекция 6. Свойства живучести в Promela. Спецификация и верификация свойств при помощи автоматов Бюхи (1158559)

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

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

Верификация программ на моделях Лекция №6 Свойства живучести в SPIN. Спецификация и верификация свойств при помощи автоматов Бюхи. Константин Савенков (лектор) План лекции •  Проверка свойств живучести в Spin. Конструкции never •  Проверка свойств правильности •  Автоматы Бюхи •  Проверка свойств при помощи автоматов Бюхи Способы описания свойств правильности (напоминание) •  Свойства правильности могут задаваться как: –  свойства достижимых состояний (свойства безопасности), –  свойства последовательностей состояний (свойства живучести); •  В языке Promela –  ассерты: •  локальные ассерты процессов, •  инварианты системы процессов; –  метки терминальных состояний: •  задаём допустимые точки останова процессов; –  метки прогресса (поиск циклов бездействия); –  утверждения о невозможности (never claims) •  например, определяются LTL-­‐формулами; –  трассовые ассерты.

свойства состояний свойства последова-­‐ тельностей состояний Конструкции never (отрицание свойств) Never say never (народная пословица) Рассуждения о вычислениях программы •  Существует несколько вариантов формализации вычислений распределённой системы: –  последовательность состояний, –  последовательность событий (переходов), –  последовательность значений высказываний в состояниях (свойства состояний) – трассы. bit x,y;byte mutex;x = 1 (y==0) mutex++ prinl mutex-­‐-­‐ x = 0 active proctype A(){x = 1;x==1 x==1 x==1 x==1 x==1 x==0 x==0 (y == 0) ->y==0 y==0 y==0 y==0 y==0 y==0 y==0 mutex++;mutex==0 mutex==0 mutex==0 mutex==1 mutex==1 mutex==0 mutex==0 printf(“%d\n”, _pid);mutex--;x = 0p !p !p p p !p p }p: (x == mutex)q: (x != y)!q q q q q q !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 (отрицание свойств) Проверка инварианта системы при помощи конструкции never never{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 ¬φ) Пример •  Одновременное выполнение ¬ ( M ϕ ) и ¬ ( M ¬ϕ )byte x = 0;init {do:: x = 0:: x = 2od}never {do:: assert(x == 0)od}Нарушается выполнением x = 2 never {do:: assert(x != 0)od}Нарушается выполнением x = 0 Автоматы и логика •  Проще проверять нарушение свойства, чем его выполнение •  Нарушение свойства описывается при помощи конструкции never – автомата, распознающего неправильное поведение •  Свойства на последовательностях состояний удобно описывать при помощи темпоральной логики Конечные автоматы •  Конечный автомат A задаётся сигнатурой S , s0 , L, F , Tгде –  S – множество состояний, –  s 0 ∈ S – начальное состояние, –  L – конечное множество меток (символов), –  F ⊆ S – множество терминальных символов, – T ⊆ S × L × S – отношение перехода на состояниях.

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

Тип файла PDF

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

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

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