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

Верификация  программ  на  моделях  Лекция  №7  Логика  линейного  времени  (LTL).  Константин  Савенков  (лектор)  План  лекции  •  Логика  линейного  времени  (LTL)  •  Свойства,  инвариантные  к  прореживанию  •  Связь  между  LTL  и  автоматами  Бюхи      /  конструкциями  never    •  Применение  LTL  в  системе  Spin  •  Практические  приёмы  формулирования  свойств  на  LTL  Проверка  свойств  при  помощи  автоматов  Бюхи  (напоминание)  •  При  помощи  автомата  Бюхи  можно  описать  наблюдаемое  поведение  программы  и  требования  к  нему,  •  Проход  автомата  соответствует  наблюдаемому  вычислению  (трассе)  программы,  •  Определение  допускаемости  прохода  позволяет  рассуждать  о  выполнении  или  нарушении  требований  (свойств  правильности).

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

 автомата  Бюхи);  –  для  проверки  свойств  используются  другие,  более  сложные  алгоритмы;  –  свойства  удобно  описывать  при  помощи  формул  темпоральной  логики,  а  проверять  –  при  помощи  автоматов  Бюхи.  Примеры  темпоральных  свойств  •  p  всегда  истинно;  •  p  рано  или  поздно  станет  всегда  ложным;  •  p  всегда  рано  или  поздно  станет  ложным  хотя  бы  ещё  один  раз;  •  p  всегда  ведёт  к  ¬q;  •  p  всегда  ведёт  к  тому,  что  рано  или  поздно  станет  истинным  q.  Почему  бы  не  описывать  темпоральные  свойства  на  естественном  языке?  •  нет  строгой  семантики  =>  возможно  множество  трактовок  –  в  части  области  проверки:  «индикатор  не  горит»  -­‐  в  начальном  состоянии?  или  это  инвариант?  –  в  темпоральной  части:    •  попробуйте  объяснить  разницу:  «от  события  А  до  события  Б»  и  «между  событиями  А  и  Б»  •  «деньги  выплачиваются,  как  только  работа  будет  выполнена»  -­‐-­‐  требуется  ли  выполнение  работы?  •  значение  зависит  от  контекста:  –  если  нажата  кнопка,  рано  или  поздно  будет  выпущено  шасси  –  от  взлёта  и  до  посадки,  если  нажата  кнопка,  то  рано  или  поздно  будет  выпущено  шасси  (область  проверки  вложенного  свойства  изменилась)  –  после  взлёта,  если  была  нажата  кнопка,  то  до  посадки  будет  выпущено  шасси  (более  строгая  формулировка)  •  зависит  от  знания  и  понимания  естественного  языка,  который  сложнее  LTL.

 Темпоральная  логика  LTL  •  Ясный,  лаконичный  и  непротиворечивый  способ  описания  требований  к  программам;  •  В  явном  виде  время  не  присутствует,  однако  рассуждения  ведутся  в  терминах  «никогда»,  «всегда»,  «рано  или  поздно»,  которые  представлены  в  виде  темпоральных  операторов.  •  Мы  рассматриваем  темпоральную  логику  линейного  времени  –  LTL.  С  её  помощью  можно  описывать  свойства,  которым  должны  удовлетворять  линейные  последовательности  наблюдаемых  состояний  –  трассы.  •  LTL  предложена  Амиром  Пнуэли  (Amir  Pnueli)  в  конце  70-­‐х.

 Темпоральная  логика  LTL  •  Семантика  LTL  определена  на  бесконечных  проходах  автомата  Бюхи.  •  Пример:  –  ☐ ((a  ≠  b)  →  ♢ (a  =  b))  Синтаксис  Spin  –  #define  p  a  !=b    #define  q  a  ==  b    [](p  -­‐>  <>q)  –  всегда,  когда  выполняется  (  a!=b  ),  в  конце  концов  становится  истинным  (a  ==  b).  –  как  правило,  формула  описывает  не  одну  конкретную  трассу,  а  класс  трасс.    Формулы  LTL  •  Могут  использоваться  для  описания  как  свойств  живучести,  так  и  безопасности  •  LTL  =  пропозициональная  логика        +  темпоральные  операторы    •  Формула  LTL    f  ::=  –  p,  q,  …  -­‐  свойства  состояний,  включая  true  и  false,  –  (  f  )  –  группировка  при  помощи  скобок,  –  α  f  –  унарные  операторы,  –  f1  β f2  –  бинарные  операторы.

 Операторы  LTL  •  Унарные:  –  ☐([])  всегда  (в  будущем),  –  ♢(<>)  рано  или  поздно,  –  (Х)  в  следующем  состоянии,  –  ¬  (!)  логическое  отрицание;  •  Бинарные:  ≡(¬p∨q)  –  U  (U)  пока,    –  ∧(&&)  логическое  И,  –  ∨(||)  логическое  ИЛИ,  ≡(p→q)∧(q→p)  –  →(->)  логическая  импликация,  –  ↔(<->)  логическая  эквивалентность.  Выполнимость  формул  •  Последовательность  состояний  прохода  σ  s0 , s1 , s2 , s3 ,...•  Набор  пропозициональных  формул  p,  q:  ∀i, i ≥ 0, и ∀p, определено sip•  Семантика  LTL:  s0  f⇔s0si [] fsi ◊f⇔⇔∀j , j ≥ i : s j∃j , j ≥ i : s jsi⇔si +1σXfsi  si+1  ffffСлабый  и  сильный  un†l  слабый:   si eWf    сильный:   si eUf(Spin)  si⇔f ∨ ( sie ∧ si +1 (eWf ))∃j, j ≥ i : s j⇔f∀k , i ≤ k < j : sksi  e  sj  e  e  e  f  иeПрактически  важные  следствия  σe W false ⇔ σσ true U fσeW f[]e⇔ σ ◊f⇔ σ []e ∨ eUfp  p  p  s0  p  Примеры  p  p  si  si+1  p  q  p  p  p  p  sn-­‐1  sn  q  σ |= [] pσ |= 〈〉 pσ |= []〈〉 pσ |= []qσ |= 〈〉 qσ |= []〈〉 qσ |= pUq σ |= []( pUq ) σ |= []( pWq)σ |= qUp σ |= []( qUp )σ |= qWpσ |= []qWpЦикличность  и  стабильность  •  Свойством  цикличности  называется  любая  темпоральная  формула,  которая  представима  в  виде  ☐♢p,  где  p  –  формула  на  состоянии;  •  Свойством  стабильности  называется  любая  темпоральная  формула,  которая  представима  в  виде  ♢☐p,  где  p  –  формула  на  состоянии.

 Распространённые  LTL-­‐формулы  Формула  Описание        Тип  []  p    всегда  p      инвариант  〈〉   p    рано  или  поздно  p      гарантия              p   → 〈〉   q  если  p,  то  рано  или  поздно  q    отклик  p   → qUr    если  p,  то  q,  затем  r  приоритет  []  〈〉 p    всегда  рано  или  поздно  будет  p            рано  или  поздно  всегда  будет  p            если  рано  или  поздно  p,      то  рано  или  поздно  q      〈〉   [] p        〈〉     p →〈〉 q        цикличность    (прогресс)    стабильность    (бездействие)    корреляция  Эквивалентные  преобразования  ![] p! 〈〉 p! ( pUq )! ( pWq)[]( p ∧ q)〈〉 ( p ∧ q)pW ( q ∨ r )( p ∧ q)WrpU ( q ∨ r )( p ∧ q)Ur[]〈〉 ( p ∨ q)〈〉 []( p ∧ q)⇔⇔⇔⇔⇔⇔⇔⇔⇔⇔⇔⇔〈〉! p[]! p! qW (! p∧! q)! qU (! p∧! q)[]p ∧ []q〈〉 p ∧ 〈〉 q(pWq) ∨ ( pWr)(pWr) ∧ ( qWr)(pUq) ∨ ( pUr)(pUr) ∧ ( qUr)[]〈〉 p ∨ []〈〉 q〈〉 []p ∧ 〈〉 []qПримеры  темпоральных  свойств  []p<>[]!p•  p  всегда  истинно;  •  p  рано  или  поздно  станет  всегда  ложным;  •  p  всегда  рано  или  поздно  станет  ложным  хотя  бы  ещё  один  раз;  []<>!p•  p  всегда  ведёт  к  ¬q;   [](p->!q)•  p  всегда  ведёт  к  тому,  что  рано  или  поздно  станет  истинным  q.

 [](p-> <>q)Правильная  интерпретация    формул  LTL  LTL:      (〈〉 (b1 ∧ (!b2Ub2 ))) → []! a31. 2. 3. 4. Пусть  b1  всегда  ложно,  p→q  означает,  что  !p∨q;  формула  выполняется.  Пусть  b1  стало  истинно,  но  b2  всегда  ложно;  формула  выполняется.  Пусть  b1  стало  истинно,  затем  –  b2,  однако  a3  всегда  ложно;  формула  выполняется.  Пусть  b1  стало  истинно,  затем  –  b2,  затем  –  a3;  формула  не  выполняется.  !b1  время  b1  !b2  b2  b1  время  !b2  !a3  b2  b1  !b2  !a3  время  a3  время  Правильная  интерпретация    формул  LTL  LTL:      (〈〉b1 ) → (〈〉b2 )1.  Пусть  b1  и  b2  всегда  ложно;  формула  выполняется.  2.  Пусть  и  b1,  и  b2  становятся  истинными;  формула  выполняется.

 3.  Пусть  b1  становится  истинным,  но  b2  всегда  ложно;  формула  не  выполняется.  !b1  b2  !b2  время  b1  время  !b1  b1  !b1  !b2  время  Правильная  интерпретация    формул  LTL  LTL:      []((〈〉b1 ) → (〈〉b2 ))1.  Пусть  b1  и  b2  всегда  ложно;  формула  выполняется.  2.  Пусть  и  b1,  и  b2  бесконечно  чередуются;  формула  выполняется.

 3.  Пусть  b2  становится  истинным  только  один  раз;  формула  не  выполняется.  !b1  !b2  b1  b2  !b1  b1  !b2  !b2  b2  !b1  !b2  !b1  !b1  время  !b2  b1  b2  !b1  b1  время  !b1  !b2  время  Описание  требований  при  помощи  LTL  “p  приведёт  к  q”  •  p  -­‐>  q  –  нет  темпоральных  операторов,  т.е.  применяется  только  к  первому  состоянию;  –  выполняется  только  если  !p∨q  в  первом  состоянии,  остальная  трасса  не  рассматривается;  –  не  подходит;  –  нужно  использовать  темпоральные  операторы.  Описание  требований  при  помощи  LTL  “p  приведёт  к  q”  •  []  p  -­‐>  q  –  правила  приоритета!  []  применяется  только  к  p;  –  означает  ([]p)  -­‐>  q;  –  не  подходит;  –  нужно  расставить  скобки.  Описание  требований  при  помощи  LTL  “p  приведёт  к  q”  •  []  (p  -­‐>  q)  –  проверяем  условие  во  всех  состояниях,  но  причинно-­‐следственная  связь  между  p  и  q  отсутствует;  –  выполняется,  только  если    !  p∨q  во  всех  состояниях;  –  не  подходит;  –  нужно  описать,  что  p  является  причиной  q.

 Описание  требований  при  помощи  LTL  “p  приведёт  к  q”  •  []  (p  -­‐>  <>q)  –  уже  лучше;  –  тем  не  менее,  формула  выполнима,  если  q  становится  истинным  в  том  же  состоянии,  что  и  p  –  причинно-­‐следственная  связь  отсутствует;  –  не  подходит;  –  нужно  описать,  что  q  не  может  произойти  раньше  следующего  шага  после  p.  Описание  требований  при  помощи  LTL  “p  приведёт  к  q”  •  []  (p  -­‐>  X(<>q))  –  практически  то,  что  нужно;  –  формула  выполнима,  если  p  всегда  ложно;  –  возможно,  не  подходит;  –  нужно  описать,  что  p  обязательно  произойдёт  и  приведёт  к  q.

 Описание  требований  при  помощи  LTL  “p  приведёт  к  q”  •  []  (p  -­‐>  X(<>q))  &&  (<>p)  –  скорее  всего,  мы  имели  ввиду  именно  это;  –  несколько  отличается  от  первоначального  p-­‐>q;  –  LTL  позволяет  выразить  множество  различных  оттенков  свойства;  –  подойдёт  ли  такое  свойство  для  модели  параллельной  программы?  Оператор  neXt  •  Оператор  X  нужно  использовать  аккуратно:  –  с  его  помощью  делается  утверждение  о  выполнимости  формулы  на  непосредственных  потомках  текущего  состояния;  –  в  распределённых  системах  значение  оператора  Х  неочевидно;  –  поскольку  алгоритм  планирования  процессов  неизвестен,  не  стоит  формулировать  спецификацию  в  предположении  о  том,  какое  состояние  будет  следующим;  –  стоит  ограничиться  предположением  о  справедливости  планирования.