8 - Логика линейного времени (LTL) (К. Савенков - Презентации лекций)

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

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

С её помощью можноописывать свойства, которым должныудовлетворять линейные последовательностинаблюдаемых состояний – трассы.• LTL предложена Амиром Пнуэли (Amir Pnueli) вконце 70-х.Темпоральная логика LTL• Семантика LTL определена на бесконечныхпроходах автомата Бюхи.• Пример:Синтаксис Spin– ((a ≠ b)(a = b))– #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s0sisi[] ffj, j  i : s jj, j  i : s jsiXfsi 1sisi+1ffffСлабый и сильный untilслабый: sieWfсильный: si(Spin)eUfsif  ( sie  si 1 (eWf ))j, j  i : s jfk , i  k  j : sksiesjeeefиeПрактически важные следствияe W false  []etrueU f  feW f  []e  eUfПримерыppps0pppsisi+1pqppppsn-1snq | [] 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 p   qесли рано или поздно 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)Правильная интерпретацияформул LTLLTL: b1  !b2Ub2   []! a31.2.3.4.Пусть b1 всегда ложно, pq означает, что !p∨q;формула выполняется.Пусть b1 стало истинно,но b2 всегда ложно;формула выполняется.Пусть b1 стало истинно,затем – b2, однако a3всегда ложно; формулавыполняется.Пусть b1 стало истинно,затем – b2, затем – a3;формула невыполняется.!b1времяb1!b2b2b1время!b2!a3b2b1времяa3!b2!a3времяПравильная интерпретацияформул LTLb1   b2 LTL:1.Пусть b1 и b2 всегдаложно; формулавыполняется.!b1времяb22.3.Пусть и b1, и b2становятсяистинными; формулавыполняется.Пусть b1 становитсяистинным, но b2всегда ложно;формула невыполняется.b1!b2время!b1b1!b1!b2времяПравильная интерпретацияформул LTL[]b1   b2 LTL:1.Пусть b1 и b2 всегдаложно; формулавыполняется.!b1времяb12.3.Пусть и b1, и b2бесконечночередуются; формулавыполняется.Пусть b2 становитсяистинным толькоодин раз; формула невыполняется.!b2b1b2!b1!b2b2!b1!b2!b1!b1время!b2b1b2!b1b1!b2!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 нужно использовать аккуратно:– с его помощью делается утверждение овыполнимости формулы на непосредственныхпотомках текущего состояния;– в распределённых системах значение оператора Хнеочевидно;– поскольку алгоритм планирования процессовнеизвестен, не стоит формулироватьспецификацию в предположении о том, какоесостояние будет следующим;– стоит ограничиться предположением осправедливости планирования.Свойства, инвариантные кпрореживанию• Пусть φ – трасса некоторого вычисления надпропозициональными формулами P,– по трассе можно определить, выполняется ли наней темпоральная формула,n1 n 2 n 3– трассу можно записать в виде   1  2 3 ...