Лекция 6. Свойства живучести в Promela. Спецификация и верификация свойств при помощи автоматов Бюхи (К. Савенков - Верификация программ на моделях (2012))

Верификация  программ  на  моделях  Лекция  №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      –  отношение  перехода  на  состояниях.