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

 Пример  конечного  автомата  A = S , s0 , L, F , Ts0  α0  S = {s0 , s1 , s2 , s3 , s4 }s1  α2  α4  L = {α 0 , α1 , α 2 , α 3 , α 4 , α5 }α1  s2   α s4  5  α3  s3  F = {s4 }T = {( s0 , α 0 , s1 ), ( s1 , α1 , s2 ),...}Вариант  интерпретации  (планировщик  процессов)  idle  s0  α0  α4  α1  s2   α s4  5  α3  s3  ready  pre-­‐empt  s1  α2  start  run  execute  unblock  stop  block  wai•ng  end  Записываем  в  виде  never  idle  start  ready  pre-­‐empt  never {idle:(start) ->ready:(run) ->execute: if:: (pre-empt) -> goto ready:: (block) -> goto waiting:: (stop) -> goto endfi;waiting: (unblock) -> goto execute;end:skipexecute  unblock  }run  stop  block  wai•ng  end  Детерминизм  и  недетерминизм  •  Конечный  автомат      A      =            S    ,    s  0    ,    L    ,    F      , Tназывается  детерминированным,  только  если    ∀s, ∀l, ((( s, l, s' ) ∈ T ∧ ( s, l, s' ' ) ∈ T ) → s' ≡ s' ')–  т.е.

 целевое  состояние  перехода  однозначно  определяется  исходным  состоянием  и  меткой  –  в  противном  случае  автомат  называется  недетерминированным  deny  Модель  сервера  запросов,  работающего  в  бесконечном  цикле  s0  approve  s2  true  s1  request  s3  true  Определение  прохода  •  Проходом  конечного  автомата          S      ,      s    0    ,    L      ,    F        ,  T            называется  такое  упорядоченное  и,  возможно,  бесконечное  множество  переходов  из  T:  σ = ( s0 , l0 , s1 ), ( s1, l1, s2 ), ( s2 , l2 , s3 ),...  что    ∀        i  ,    i      ≥        0        :    (    s    i  ,    l    i  ,    s    i  +    1    )    ∈        T        .

 •  Проход  соответствует  последовательности  состояний  из  S  и  слову  в  алфавите  L.  idle  start  Последовательность  состояний:  {idle,  ready,  {execute,  wai•ng}*}  ready  pre-­‐empt  execute  unblock  wai•ng  run  stop  block  end  Соответствующее  слово  в  L:    {start,  run,  {block,  unblock}*}  Допускающий  проход  •  Допускающим  проходом  конечного  автомата  A  называется  конечный  проход  σ,  финальный  переход  которого  (sn-­‐1,ln-­‐1,sn)  ведёт  в  терминальное  состояние  idle  start  ready  pre-­‐empt  execute  unblock  wai•ng  run  stop  block  Последовательность  состояний  для  допускающего  прохода:    {idle,  ready,  execute,  wai•ng,  execute,  end}  end  Соответствующее  слово  в  L:    {start,  run,  block,  unblock,  stop}  Язык  автомата  •  Языком  автомата  А  называется  множество  слов  в  алфавите  L,  соответствующих  допускающим  проходам  автомата  А  Язык  автомата:  {idle  start  start,run,{{pre-empt,run}+{block,unblock}*}*,stopready  pre-­‐empt  execute  unblock  wai•ng  run  stop  block  end  }Самое  короткое  слово  языка:    {start,  run,  stop}  Описание  свойств  при  помощи  автомата  Пример  свойства:  если  сначала  p=T,    а  позже  q=T,    !q  то  впоследствии  r=F  !p  p  q  !r  Если  мы  попали  в  терминальное  состояние,  то  свойство  нарушается  r  error  Иногда  нужно  рассуждать  о  потенциально  бесконечной  задержке  Классическое  свойство  живучести:  «если  p,  тогда  впоследствии  q»  Такое  свойство  может  быть  нарушено  только  бесконечным  проходом    Классическое  определение  описывает  лишь  конечные  проходы    Нужно  описать,  что  автомат  не  может  находиться  в  терминальном  состоянии  бесконечно  долго.

 !q  !p  p  error  q  Немного  обозначений  •  Для  любого  бесконечного  прохода  σ  конечного  автомата  можно  выделить  два  множества:  –  множество  σ+  состояний,  встречающихся  конечное  число  раз,  –  множество  σω  состояний,  встречающихся  бесконечное  число  раз.  σ+  σ  σω  Допускающий  проход  по  Бюхи  (ω-­‐допускание)  •  Допускающим  ω-­‐проходом  конечного  автомата  А  называется  такой  бесконечный  проход  σ,  что  ∃i ≥ 0, ( si −1 , li −1 , si ) ∈ σ : si ∈ F ∧ si ∈ σωт.е.  по  крайней  мере  одно  терминальное  состояние  встречается  бесконечно  часто.

 idle  start  Допускающий  ω-­‐проход:  {idle,  ready,  {execute,  ready}*}  ready  pre-­‐empt  execute  unblock  wai•ng  run  stop  block  end  Соответствующее  ω-­‐слово:    {start,  run,  {pre-­‐empt,  run}*}  Множество  допускаемых  автоматом  ω-­‐слов  называется  его  ω-­‐языком  Расширение  автоматов  Бюхи  (конечные  проходы  как  частный  случай  бесконечных)  •  Расширяем  алфавит  автомата  меткой  ε  (пустой  переход),  •  Дополняем  все  конечные  проходы  бесконечным  повторением  перехода  по  метке  ε.  idle  start  Допускающий  ω-­‐проход:  {idle,  ready,  execute,  wai•ng,  execute,  [end,]*}  ready  pre-­‐empt  execute  unblock  wai•ng  run  stop  block  end  ε  Соответствующее  ω-­‐слово:    {start,  run,  block,  unblock,  stop,  ε*}  Проверка  свойств  при  помощи  автоматов  Бюхи  •  При  помощи  автомата  Бюхи  можно  описать  наблюдаемое  поведение  программы  и  требования  к  нему,  •  Проход  автомата  соответствует  наблюдаемому  вычислению  (трассе)  программы,  •  Определение  допускаемости  прохода  позволяет  рассуждать  о  выполнении  или  нарушении  требований  (свойств  правильности).

 Безопасность  и  живучесть  •  Безопасность  –  Любое  свойство  безопасности  можно  проверить,  исследуя  свойства  отдельных  состояний  модели;  –  если  свойство  безопасности  нарушено,  всегда  можно  определить  достижимое  состояние  системы,  в  котором  оно  нарушается;  –  для  проверки  свойств  безопасности  требуется  генерировать  состояния  системы  и  для  каждого  из  них  проверять  свойство;  –  при  проверке  таких  свойств  можно  обойтись  без  темпоральных  логик  и  автоматов  Бюхи.  •  Живучесть  –  Для  проверки  свойств  живучести  необходимо  рассматривать  последовательности  состояний  (конечные  и  бесконечные  проходы  соотв.

 автомата  Бюхи);  –  для  проверки  свойств  используются  другие,  более  сложные  алгоритмы;  –  свойства  удобно  описывать  при  помощи  формул  темпоральной  логики,  а  проверять  –  при  помощи  автоматов  Бюхи.  Пример  свойства  безопасности  Как  только  p  впервые  стало  истинно,    q  больше  не  может  быть  истинно.  never{do:: !p:: p -> breakoddo:: assert(!q)od}!p  p  assert(!q)  Как  только  достигнуто  состояние,  удовлетворяющее  условию,  будет  зафиксировано  нарушение  свойства.  Рассуждать  о  бесконечных  вычислениях  здесь  не  требуется.  Пример  поведения  системы  bool p,q;A  B  active proctype A(){(!p && !q) -> p = true}s0  s0  active proctype B(){(p) -> q = true}!p∧  !q  s1  s1  p  =  true  s2  stop  !p  p  assert(!q)  p  q  =  true  s2  stop  A∥B  s0  s0  !p∧!q  s1  s0  p  =  true  stop  s2  s0  p  -­‐  s0  p  s2  s1   stop   -­‐  s1  q  =  true  stop  q  =  true  -­‐  s2  асинхронно   s2  s2  stop  stop  синхронно  s2  s0   stop   -­‐    -­‐  Проверка  свойства    безопасности    A∥B  A∥B  p0  s0  s0  !p∧!q  p  s1  s0  p  =  true  stop  s2  s0  p  s2  s1   stop  q  =  true  stop  s2  s2  stop  stop  s2  s0  p1  !p  s0  s0  !p∧!q  assert(!q)  синхронно  -­‐  s0  Свойства  безопасности  всегда  можно  проверить  p  путём  анализа  -­‐  s1  достижимости  состояний  q  =  true   либо  асинхронной  параллельной  композиции  -­‐  s2  процессов  А∥В,  либо  её  stop   синхронной  композиции  с  процессом,  описывающим  -­‐    -­‐  свойство  –  (A∥B)∣P  s1  s0  p  =  true  stop  s2  s0  p  -­‐  s0  p  stop  s  s-­‐  s1   p1  p1   2 1  q  =  true   q  =  true  stop  pp1   s2  s2  stop  stop  p1   s2  -­‐  -­‐  s2  1  stop  -­‐    -­‐   p1  Пример  свойства  живучести  Как  только  p  впервые  стало  истинно,  в  течение  конечного  числа  шагов  q  также  станет  истинным.

   Нарушение  свойства:  p  становится  истинным,  а  затем  q  может  навсегда  остаться  ложным.    !p  p  !q  Мы  можем  заключить  о  нарушении  свойства,  только  если  обнаружим  удовлетворяющую  условию    потенциально  бесконечную  последовательность  состояний  Пример  поведения  системы  bool p,q;A  B  active proctype A(){(!p && !q) -> p = true}s0  s0  active proctype B(){(p) -> q = false}Модель    не  циклична!  !p  p  !q  !p∧  !q  s1  s1  p  =  true  s2  p  stop  q  =  false  s2  stop  A∥B  s0  s0  !p∧!q  s1  s0  p  =  true  stop  s2  s0  p  -­‐  s0  p  s2  s1   stop   -­‐  s1  q  =  false   q  =  false  stop  -­‐  s2  асинхронно   s2  s2  stop  stop  синхронно  s2  -­‐   stop   -­‐    -­‐  Проверка  свойства    живучести    A∥B  A∥B  Модель    s0  s0   не  циклична!  !p∧!q  p0  p  s1  s0  p  =  true  stop  s2  s0  p1  !p  s0  s0  !q  синхронно  p  q  =  false  stop  q  =  false  stop  stop  s2  s0  stop  -­‐    -­‐  p  =  true  stop  p  s2  s1   stop   -­‐  s1  -­‐  s2  s1  s0  s2  s0  -­‐  s0  p  s2  s2  !p∧!q  -­‐  s0  p  stop  s  s-­‐  s1   p1  p1   2 1  Для  проверки  свойств  живучести  необходимо  рассматривать  бесконечные  вычисления  q  =  false   q  =  false  stop  pp1   s2  s2  stop  stop  p1   s2  -­‐  -­‐  s2  1  stop  -­‐    -­‐   p1  ε  Спасибо за внимание!Вопросы?.