Лекция 7. Логика линейного времени (LTL). Использование LTL в Spin (К. Савенков - Верификация программ на моделях (2012)), страница 2

 Свойства,  инвариантные  к  прореживанию  •  Пусть  φ  –  трасса  некоторого  вычисления  над  пропозициональными  формулами  P,  –  по  трассе  можно  определить,  выполняется  ли  на  ней  темпоральная  формула,  n1 n 2 n 3ϕ=ϕ–  трассу  можно  записать  в  виде                                1      ϕ        2      ϕ        3        ...        ,    где  значения  пропозициональных  формул  на  каждом  интервале  совпадают.  •  Обозначим  E(φ)  набор  всех  трасс,  отличающихся  лишь  значениями  n1,  n2,  n3  (т.е.  длиной  интервалов)  –  E(φ)  называется  расширением  прореживания  φ.

 Расширение  прореживания  x  =  1  p: (x == mutex)q: (x != y)(y==0)   mutex++   prin‘   mutex-­‐-­‐  x  =  0  x==1  x==1  x==1  x==1  x==1  x==0  x==0  bit x,y;y==0  y==0  y==0  y==0  y==0  y==0  byte mutex;y==0  active proctype A()mutex==0   mutex==0   mutex==0   mutex==1   mutex==1   mutex==0   mutex==0  {x = 1;(y == 0) ->mutex++;printf(“%d\n”, _pid);mutex--;x = 0}трасса  φ  трасса  φ1∈E(φ)  p  !p  !p  p  p  !p  p  !q  q  q  q  q  q  !q  p  !p  p  !p  p  !q  q  q  q  !q  Свойства,  инвариантные  к  прореживанию  •  Свойство  φ,  инвариантное  к  прореживанию,  либо  истинно  для  всех  трасс  из  E(φ),  либо  ни  для  одной  из  них:  ϕf → ∀v ∈ E (ϕ ), vf•  истинность  такого  свойства  зависит  от  порядка,  в  котором  пропозициональные  формулы  меняют  свои  значения,  и  не  зависит  от  длины  трассы;  •  Теорема:  все  формулы  LTL  без  оператора  X  инвариантны  к  прореживанию.

 •  Более  того,  в  рамках  LTL  без  X  можно  описать  все  свойства,  инвариантные  к  прореживанию.  Связь  между  LTL    и    автоматами  Бюхи  (конструкциями  never)  Связь  LTL  с  автоматами  Бюхи  •  Удобно  проверять  допустимость  трасс  для  некоторого  автомата  Бюхи;  •  Удобно  описывать  свойства  правильности  при  помощи  темпоральных  формул;  •  Что  дальше?  •  Теорема:  Для  всякой  формулы  LTL  f  существует  автомат  Бюхи,  который  допускает  те  и  только  те  прогоны,  которым  соответствуют  трассы,  на  которых  выполнима  f.  •  Пример:  формуле  <>[]p соответствует  автомат  true  s0  p  s1  p  Переход  от  LTL  к  автоматам  •  Привести  свойство  правильности  LTL  к  форме  never  языка  Promela  достаточно  просто:  нужно  построить  отрицание  формулы  LTL  f  и  поместить  его  в  тело  never:  –  f  выполняется  на  всех  вычислениях   ⇔–  !f  не  выполняется  ни  на  одном  вычислении   ⇔–  автомат  {!f}  не  допускает  ни  одного  прохода,  полученного  в  результате  синхронного  выполнения  с  системой.

   ! 〈〉 [] p ≡ []![] p ≡ []〈〉! ptrue  s0  !p  true  s1  Примеры  !p||q  •  p -> qtrue  !p||q  •  []p -> qtrue  true  !p  true  •  [](p -> q)!p||q  Примеры  true  •  [](p -> <>q)!p||q  !p  •  [](p -> X<>q)!p&&q  q  q  true  !p&&p  true  q  true  true  И,  наконец…  •  [](p -> X<>q)&&(<>p)true  true  !p&&q  p  p&&q  true  true  q   !p&&q !p    p  true  true  !p  true  •  &&(<>p)!p  p  true  p  true  !p  !q  Отрицания  формул  LTL  Формулу  LTL  всегда  можно  переписать  в  таком  виде,  что  отрицания  будут  появляться  только  перед  пропозициональными  символами  •  •   –  по  определению  логической  импликации  •  <>!(!p || <>q)  –  ![]p  эквивалентно  <>!p  •  <>(p && !<>q) –  По  правилу  ДеМоргана  •  <>(p && []!q) –  !<>q  эквивалентно  []!q  И,  наконец…  •  !([](p -> X<>q)&&(<>p))–  )||!<>p!p  –  <>!(!p || (X<>q))||[]!pp  true  –  <>(p && !(X<>q))||[]!p–  <>(p &&true  (X[]!q))||[]!p!p  p  !q  Используем  Spin  для  трансформации  формул  LTL  > ./spin -f '<>[]p'never {/* <>[]p */T0_init:if:: ((p)) -> goto accept_S4:: (1) -> goto T0_initfi;accept_S4:if:: ((p)) -> goto accept_S4fi;}> ./spin -f `!<>[]p'never {/* !<>[]p */T0_init:if:: (! ((p))) -> gotoaccept_S9:: (1) -> goto T0_initfi;accept_S9:if:: (1) -> goto T0_initfi;}true   T0_init  true   T0_init  p  !p  true  s4  s9  p  Правила  синтаксиса  > ./spin -f `([]p -> <> (a+b <= c) )'#define q (a+b <= c)Вводим  строчные  макроопределения  для  всех  булевых  подформул    > ./spin -f `[] (p -> <> q)'never {/* [] (p -> <> q) */T0_init:if:: (((! ((p))) || ((q)))) -> goto accept_S20:: (1) -> goto T0_S27fi;accept_S20:if:: (((! ((p))) || ((q)))) -> goto T0_init:: (1) -> goto T0_S27fi;accept_S27:if:: ((q)) -> goto T0_init:: (1) -> goto T0_S27fi;T0_S27:if:: ((q)) -> goto accept_S20:: (1) -> goto T0_S27:: ((q)) -> goto accept_S27fi;}Следим  за  приоритетом  операторов  LTL  для  проверки  правильности  при  помощи  Spin  int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}Ограничено  ли  значение  x?  > ./spin -f `[] (x > 0 && x <= 100)'tl_spin: expected ')', saw '>'tl_spin: [] (x > 0 && x <= 100)----------------^>Синтаксическая  ошибка!  LTL  для  проверки  правильности  при  помощи  Spin  int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}#define p (x > 0 && x <= 100)> ./spin -f `[] p'never {/* []p */accept_init:T0_init:if:: ((p)) -> goto T0_initfi;}p  Формула  синтаксически  корректна,  но  мы  же  будем  проверять  её  невыполнимость!  LTL  для  проверки  правильности  при  помощи  Spin  int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}#define p (x > 0 && x <= 100)> ./spin -f `![] p'never {/* ![]p */T0_init:if:: (! ((p))) -> gotoaccept_all:: (1) -> goto T0_initfi;accept_all:skip}true  !p  true  То,  что  ![]p не  может  быть  выполнено,  означает,  что  []p  не  может  быть  нарушено  (нет  ни  одного  контрпримера)  LTL  для  проверки  правильности  при  помощи  Spin  int x = 100;#define p (x > 0 && x <= 100)active proctype A(){do:: x%2 -> x = 3*x + 1od> ./spin -a ltl1.pml}> gcc -o pan pan.cactive proctype B()> ./pan -a(Spin Version 5.1.4 -- 27 January 2008){+ Partial Order ReductiondoFull statespace search for::: !x%2 -> x = x/2never claim+odassertion violations+ (if within scope of claim)}acceptancecycles+ (fairness disabled)never {/* ![]p */invalid end states- (disabled by never claim)T0_init:...if:: (! ((p))) -> goto accept_all:: (1) -> goto T0_initfi;accept_all:skip}Ещё  один  пример  int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}Пусть    #define p (x == 1)Выполнимо  ли  свойство  []<>p?  Даже  в  таком  простом  случае  метод  пристального  взгляда  перестаёт  работать  Для  проверки  неизбежности  []<>pпроверяем  невозможность    ![]<>p<>!(<>p)<>[]!pLTL  для  проверки  правильности  при  помощи  Spin  int x = 100;#define p (x == 1)> ./spin -t -c ltl2.pmlactive proctype A()proc 0 = Aproc 1 = B{Never claim moves to line 18[(!((x==1)))]do[(!((x==1)))]:: x%2 -> x = 3*x + 1 Never claim moves to line 23<<<<<START OF CYCLE>>>>>odspin: trail ends after 3 steps}------------active proctype B()final state:{------------#processes: 2dox = 100:: !x%2 -> x = x/23:proc 1 (B) line 11 "ltl2.pml" (state 3)od3:proc 0 (A) line5 "ltl2.pml" (state 3)}3:proc - (:never:) line 22 "ltl2.pml" (state 9)never {/* ![]<>p */ 2 processes createdT0_init:>if:: (! ((p))) -> goto accept_S4:: (1) -> goto T0_initfi;> ./spin -a ltl1.pml> gcc -a pan pan.caccept_S4:> ./pan -aifpan: acceptance cycle (at depth 2):: (! ((p))) -> goto accept_S4pan: wrote ltl2.pml.trailfi;Практические  приёмы  описания  свойств  на  LTL  Практические  приёмы  описания  свойств  на  LTL  •  Выполнимость  формулы  LTL  проверяется  только  для  первого  состояния  в  трассе  •  Темпоральные  операторы  управляют  проверкой  выполнимости  своих  аргументов  •  Сложное  свойство  можно  (и  нужно!)  строить  как  суперпозицию  простых  •  Суперпозиция  темпоральных  операторов  не  ограничивает  диапазон  действия  «вложенного»  оператора.

 Выполнимость  формул  LTL  •  Выполнимость  формулы  LTL  определена  и  проверяется  для  одного  (первого)  состояния  трассы  •  Распространение  свойств  на  другие  состояния  управляется  темпоральными  операторами  •  Единственный  оператор,  который  может  ограничить  сверху  проверку  выполнимости  формулы  –  Un†l  Суперпозиция  формул  LTL  •  Составлять  сложные  формулы  LTL  нужно  методом  суперпозиции  простых  формул  •  Внешняя  формула  задаёт,  на  каких  участках  вычислений  будет  проверятся  подформула  •  Подформула  задаёт  свойства,  проверяемые  для  участков  вычислений  •  Суперпозиция  темпоральных  операторов  не  ограничивает  диапазон  действия  «вложенного»  оператора.  Пример  •  В  ходе  одного  вызова  функции  F()  x  всегда  не  превышает  3.

                   где  проверяем  (g)    что  проверяем(f)  •  φ  =  g(f)  •  Что  проверяем?  –  f = x <= 3  –  в  синтаксисе  LTL  нет  таких  символов!  –  определяем  пропозициональный  символ–  f = []a –  вроде  бы  точно  описывает  свойство  f  –  #define a x <= 3Пример  •  В  ходе  одного  вызова  функции  F()  x  всегда  не  превышает  3.                    где  проверяем  (g)    что  проверяем(f)  •  φ  =  g(f)  •  Где  проверяем?  –  #define lab_f P@f_call  –  поставим  метку  на  вызов    f  –  не  то,  проверяем  для  всего  участка  пути  за  первым  вызовом  F  –  g = [](lab_f -> f)f_call  f_entry   f_return  f_call  f_entry   f_return  –  нужно  проверять  свойство    #define f_e P@f_return      внутри  тела  функции  –  g = [](f_b -> (f U f_e)) –  похоже  на  правду,  проверяем  от  входа  в  функцию  до  выхода  из  неё  –  #define f_b P@f_entryПример  •  В  ходе  одного  вызова  функции  F()  x  всегда  не  превышает  3.                    где  проверяем  (g)    что  проверяем(f)  •  φ  =  g(f)  •  Подставляем  одно  в  другое  –  φ = [](f_b -> ([]a U f_e))f_b  Проверяем    выполнимость  φ  Проверка    выполнимости  U  f_e  Проверка    выполнимости  []a  Проверка    выполнимости  a  –  зона  действия  []  по  определению  не  ограничивается  Until!  –  φ = [](f_b -> (a U f_e))–  правильная  формула  Помощь  в  формулировке  свойств  База  шаблонов  темпоральной  логики  hŸp://paŸerns.

 projects.cis.ksu.edu  Логические  паттерны  (LTL/CTL/GIL)  встречаемость  (occurence)  отсутствие  (absense)  порядок  (order,  sequence)  универсальность  (universality)  существование  (existence)  bounded  existence  приоритет  (precedence)  chain  precedence  отклик  (response)  База  шаблонов  темпоральной  логики  hŸp://paŸerns.  projects.cis.ksu.edu  •  Для  каждого  шаблона  –  пять  вариантов  формул:          имя      пример  для  “absense”  и  LTL            всегда      [](!p)          перед  r    <>r -> (!p U r)В  чём  разница?            после  q    [](q -> [](!p))          между  r  и  q    []((r && !q && <>q) -> (!p U q))          после  r  до  q                          []((r && !q) -> ((!p U q) || []!p))База  шаблонов  темпоральной  логики  hŸp://paŸerns.

 projects.cis.ksu.edu  •  Для  каждого  шаблона  –  пять  вариантов  формул:          имя              всегда              перед  r            после  q            между  r  и  q            после  r  до  q  пример  для  “absense”  и  LTL      r  r  q  q  q    r  r  q  r  r  r  q  r    r  Спасибо за внимание!Вопросы?.