Лекция 9. Выразительная мощность LTL. Корректная абстракция графов программ. Отношение моделирования (симуляции) (К. Савенков - Верификация программ на моделях (2012))

Верификация  программ  на  моделях  Лекция  №9  Выразительная  мощность  LTL.  Корректная  абстракция  графов  программ.  Отношение  моделирования  (симуляции).  Константин  Савенков  (лектор)  План  лекции  •  Выразительная  мощность  LTL:  –  сравнение  с  автоматами  Бюхи,  –  сравнение  с  CTL*,  CTL,  –  Общая  картина.  •  Корректная  абстракция  графов  программ:  –  Отношение  слабого  моделирования,  –  Сильное  моделирование.  Выразительная  мощность  LTL  по  сравнению  с  конструкциями  never  •  Автомат  Бюхи  описывает  ω-­‐регулярный  язык:  –  Aω,  где  А  –  регулярный  язык,  –  AB,  где  А  –  регулярный,  а  В  –  ω-­‐регулярный  язык,  –  АUB,  где  A  и  B  –  ω-­‐регулярные  языки;  •  при  помощи  never  можно  описать  любой  ω-­‐регулярный  автомат  над  словами.  Выразительная  мощность  LTL  по  сравнению  с  конструкциями  never  •  LTL  описывает  подмножество  этого  языка:  –  всё,  выразимое  в  LTL,  может  быть  описано  при  помощи  never,  –  при  помощи  never  можно  описать  свойства,  невыразимые  на  LTL.

 •  Теорема:  Добавление  одного  квантора  существования  над  одним  пропозициональным  символом  расширяет  выразительные  способности  LTL  до  всех  ω-­‐регулярных  автоматов  над  словами.  Пример  свойства,  не  выразимого  на  LTL  •  (p)  может  быть  истинным  после  выполнения  системой  чётного  числа  шагов,  но  никогда  не  истинно  после  нечётного.  •  []X(p) не  подходит  true  p  •  p && [](p -> X!p) && [](!p -> Xp) –  также  не  подходит  (здесь  p  всегда  истинно  после  чётных  шагов)  p  !p  •  ∃t.t&&[](t->X!t)&&[](!t->Xt)&&[](!t->!p) –  то,  что  надо:  true  !p  Сравнение  LTL  с  другими  логиками  •  LTL-­‐формула  описывает  свойство,  которое  должно  выполняться  на  всех  вычислениях,  начинающихся  из  исходного  состояния  системы  грамматика:  Операторы:  !  логическое  отрицание  &&  логическое  И  ||  логическое  ИЛИ  X  в  следующем  состоянии  U  сильный  unil  U  слабый  unil  <>    рано  или  поздно  []  всегда  Серым  отмечены  операторы,  которые  можно  вывести  из  других:    φ1  ||  φ  2  ==  !(!  φ  1  &&  !  φ  2)  <>  φ    ==    true  U  φ  []  φ    ==    !<>  !φ  φ  1  U  fi2  ==    []  φ  1  ||  (φ  1  U  φ  2)  пропозициональные  формулы:    p    !f    (f)    f  &&  f    f  ||  f  темпоральные  формулы:    f    !  φ    (φ)      φ  &&  φ      φ  ||  φ    X  φ      φ  U  φ    <>  φ    []  φ  p  –  некоторый  пропозициональный  символ  f  –  некоторая  пропозициональная  формула  φ  –  некоторая  темпоральная  формула  Логика  СTL*  •  Логика  ветвящегося  времени:  –  использует  кванторы  ∀  и  ∃,  –  использует  F  вместо  <>  и  G  вместо  [].

 Операторы:  !  логическое  отрицание  &&  логическое  И  ||  логическое  ИЛИ  E  существует  путь  А  для  всех  путей  X  в  следующем  состоянии  U  unil  (сильный)  F    рано  или  поздно  G  всегда  Серым  отмечены  операторы,  которые  можно  вывести  из  других:    φ  1  ||  φ  2  ==  !(!  φ  1  &&  !  φ  2)  A  φ    ==    !E  !  φ  F  φ    ==  true  U  φ  G  φ    ==    !F!  φ  формулы  состояния:  p      !f      (f)      f  &&  f      f  ||  f      A  φ          E  φ  формулы  пути:  f      !  φ      (φ)        φ  &&  φ        φ  ||  φ      X  φ        φ  U  φ      F  φ      G  φ  p  –  некоторый  пропозициональный  символ  f  –  некоторая  формула  состояния  φ  –  некоторая  формула  пути  Логика  СTL  •  Логика  CTL  –  фрагмент  логики  CTL*,  в  котором  под  управлением  квантора  пути  (E  или  A)  может  находиться  не  более  одного  оператора  X  или  U.

 Корректная  CTL  формула:      p      !  φ        φ  &&  φ        φ  ||  φ      E  X  φ      E  (φ  U  φ)      A  (φ  U  φ)    p  –  некоторый  пропозициональный  символ  f  –  некоторая  формула  состояния  φ  –  некоторая  формула  пути  Можно  вывести:    EF  f  ==AF  f  ==EG  f  ==AG  f  ==AX  f  ==  E(true  U  f)    A(true  U  f)    !AF  !f    !EF  !f    !EX  !f  Пример  В  LTL  <>p  означает:  A<>p      для  всех  вычислений,  начинающихся      в  исходном  состоянии  s0,  выполняется  <>p  В  CTL  можно  выразить:    EF(p)      существует  вычисление,  для  которого          выполняется  <>p    AF(p)    для  всех  вычислений  выполняется  <>p    AG(p)    для  всех  вычислений  p  –  инвариант    EG(p)      существует  вычисление,  для  которого        выполняется  p  –  инвариант  итд.  Выразительные  возможности  CTL*  и  CTL  •  CTL*  и  CTL  описывают  подмножества  ω-­‐регулярных  автоматов  над  деревьями  –  автоматы  над  деревьями  более  выразительны,  чем  автоматы  над  словами  (CTL-­‐формула  выполнима  на  дереве  трасс,  а  не  на  одной  трассе);  –  CTL  и  LTL  являются  подмножествами  CTL*;  –  CTL  и  LTL  не  сравнимы  по  выразительной  мощности  (пересекаются,  но  не  включают);  –  на  LTL  можно  описать  свойства,  не  выразимые  на  CTL:  •  CTL  не  позволяет  описать  свойства  вида  []<>(p),  •  при  помощи  []<>(p)  в  LTL  задаются  ограничения  справедливости;  CTL  LTL  –  на  CTL  можно  описать  свойства,  не  выразимые  на  LTL:  •  на  LTL  нельзя  описать  свойства  вида  AGEF(p),  •  AGEF(p)  используется  для  описания  свойства  reset:  из  любого  состояния  система  может  перейти  в  нормальное.

 Выразительная  мощность  Модальное  µ-­‐исчисление,  Автоматы  над  ω-­‐деревьями    Автоматы  над  ω-­‐словами,  автоматы  Бюхи,  конструкции  never,  ∃LTL  CTL*  CTL  LTL  LTL  без  X  Корректность  абстракции  графов  программ  Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Корректность  моделирования  графов  программ  PG  абстракция  развёртка  развёртка  TS(PG)  PG’  абстракция    (корректная)  TS(PG’)  •  Необходимое  и  достаточное  условие:  –  Программа  PG’  корректно  моделирует  программу  PG  тогда  и  только  тогда,  когда  система  переходов  TS(PG’)  корректно  моделирует  систему  переходов  TS(PG).

 Абстракция  графов  программ  Пример  корректной  абстракции  Программа:  PG:  PG’:  00T:x = 2;int x,y;0: x = 2;1: y = 3;2: while (x > 0) x <= 0:τ{3:y += 1;4:x -= 1;}5:T:x = 2;1T:y = 3;x <= 0:τ22x > 0:τx > 0:τ3T:y += 1;45T:x -= 1;45T:x -= 1;Абстракция  графов  программ  Пример  некорректной  абстракции  TS(PG):  PG:  PG’:  TS(PG’):  0,0,0  000,0,0  x = 2;T:x = 2;1,2,0  x = 2;T:x = 2;1y = 3;2,2,3  2,1,4  x>0 x<=0:τ 2x > 0:τx-=1;x > 0T:y = 3;3,1,4  3,2,3  y+=1;1x > 0:τ2T:y += 1;x -= 1;43T:x-=1;y+=1;T:x-=1;4,1,2  x -= 1;2,0,2  !(x > 0)!(x > 0)5,0,5  x>03,1,1  3,2,0  4,1,5  2,0,5  2,1,1  x-=1;x > 0y+=1;T:y += 1;4,2,1  y+=1;4,2,4  3x<=0:τ2,2,0  545,0,2  Абстракция  графов  программ  Пример  корректной  абстракции  TS(PG):  PG:  PG’:  TS(PG’):  0,0,0  000,0,0  x = 2;T:x = 2;1,2,0  x = 2;T:x = 2;11,2,0  1y = 3;y = 3;2,2,3  2,1,4  x>0 x<=0:τ 2x > 0:τx-=1;x > 0T:y = 3;3,1,4  3,2,3  T:τ2T:τ4,1,5  T:y += 1;T:y += 1;x -= 1;442,0,5  55x-=1;x>03,1,4  y+=1;y+=1;4,2,4  4,1,5  T:x-=1;x -= 1;2,0,5  !(x > 0)5,0,5  2,1,4  3,2,3  3T:x-=1;2,2,3  x > 03y+=1;y+=1;4,2,4  T:y = 3;5,2,3  !(x > 0)5,1,4  5,0,5  Абстракция  графов  программ  Пример  корректной  абстракции  TS(PG):  PG:  PG’:  TS(PG’):  0,0,0  000,0  x = 2;T:x = 2;1,2,0  1y = 3;T:y = 3;y = 3;2,2,3  2,1,4  x>0 x<=0:τ 2x > 0:τx-=1;x > 0T:y = 3;3,1,4  3,2,3  y+=1;y+=1;4,2,4  11,4  y+=1;y+=1;T:τ34,1,5  T:y += 1;x -= 1;42,0,5  T:τ1,3  T:x-=1;2,4  22,5  T:y+=1;1,5  !(x > 0)5,0,5  533,3  3,4  3,5  Неформальное  определение  PG = Loc, Act, Effect, →, Loc0 , g0PG ' = Loc' , Act' , Effect' , →' , Loc0 ' , g0 'Будем  говорить,  что  PG’  моделирует  PG,  если  1.  В  PG’  присутствуют  переменные,  соответствующие  наблюдаемым  переменным  PG,  2.  Все  действия  PG,  влияющие  на  наблюдаемые  переменные,  отражены  в  модели,  3.  Модель  корректно  воспроизводит  возможные  последовательности  изменения  значений  наблюдаемых  переменных  PG.

 Отношение  (слабого)  моделирования  (слабой  симуляции)  •  Будем  говорить,  что  точки  l0  и  l’0  связаны  отношением  слабого  моделирования  S  (  (l0,l0’)∈S  )  тогда  и  только  тогда:  g:ag:a∀l0 ⎯⎯→l1 : ((a ≠ τ ) ⇒ (∃l1 ' , l0 ' ⎯⎯→l1 ' )) ∧ (l1 , l1 ' )∈ SСлабая  симуляция!  a  a  b  b  a  τ  b  Достаточное  условие  корректности  •  Будем  говорить,  что  PG’  моделирует  PG,  если  ∃α Loc : Loc → Loc' , Loc0 ' = α ( Loc0 )g0 ' = g0 |VarPG '∃α Act : Act → Act '∪{τ }∃αVar : VarPG → VarPG ' ∪ {ε }∀a ∈ Act, v ∈Var PG , (α Act ( a ) = τ ∧ αVar ( v ) ≠ ε ) ⇒ Effect ( a, v ) = v∀a ∈ Act, v ∈Var PG , (α Act ( a ) ≠ τ ∧ αVar ( v ) ≠ ε ) ⇒⇒ Effect ' (α Act ( a ),αVar ( v )) = Effect ( a, v )∀a ∈ Act '\ Act, v ∈VarPG ∩ VarPG ' , (Effect ' ( a, v ) = v )  а  точки  Loc0  и  α(Loc0’)  связаны  отношением  слабой  симуляции  S:  g:ag:a∀l0 ⎯⎯→l1 : ((α Act (a ) ≠ τ ) ⇒ (∃l1 ' , l0 ' ⎯⎯→l1 ' )) ∧ (l1 , α Loc (l ' ) )∈ SСлабое  моделирование  •  Отношение  слабого  моделирования  не  сохраняет  количество  шагов  между  состояниями:  00T:x = 2;1T:y = 3;T:y = 3;21•  Не  сохраняются  свойства,  не  инвариантные  к  прореживанию  Сильное  моделирование  •  Для  сохранения  отношения  сильного  моделирования  необходимо  сохранять  количество  шагов  программы  между  изменением  состояния  0T:x = 2;0T:τ11T:y = 3;T:y = 3;22Сильное  моделирование  •  С  добавлением  переменных  и  операторов  в  модели  тоже  не  всё  просто:  0T:y = 3;10T:count += 1;Сильное  моделирование  нарушается  2T:y = 3;01T:atomic{y = 3;count += 1;}1Сильное  моделирование  сохраняется  Практикум  •  …  Спасибо за внимание!Вопросы?.