Лекция 6. Логика TCTL. Средство верификации UPPAAL (Лекции)

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 6:Логика TCTLСредство верификации UPPAALВМиК МГУ им. М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.1План лекции• Логики CTL, CTL* и TCTL• Общее описание средства UPPAAL• Модуль описания– Пример системы реального времени– Описание сети автоматов– Синтаксис выражений• Модуль симуляции• Модуль верификации– Общее описание– Язык запросовСравнение LTL с другими логиками• LTL‐формула описывает свойство, которое должно выполнятьсяна всех вычислениях, начинающихся из исходного состояниясистемыграмматика:Операторы:логическое отрицание!логическое И&&логическое ИЛИ||в следующемXсостоянии сильный unilUслабый unilUрано или поздно<>всегда[]Серым отмечены операторы,которые можно вывести издругих:!(! φ 1 && ! φ 2)φ1 || φ 2 ==<> φ==true U φ[] φ==!<> !φφ 1 U fi2 ==[] φ 1 || (φ 1 U φ 2)пропозициональные формулы:p!f(f)f && ff || fтемпоральные формулы:f!φ(φ)φ && φφ || φXφφUφ<> φ[] φp – некоторый пропозициональный символf – некоторая пропозициональная формулаφ – некоторая темпоральная формула•ЛогикаСTL*Логика ветвящегося времени:– использует кванторы  и ,– использует F вместо <> и G вместо [].Операторылогическое отрицание:!&&логическое Илогическое ИЛИ||существует путьEдля всех путейАв следующемXсостоянии unilU(сильный)Fрано или поздно всегдаGСерым отмечены операторы,которые можно вывести из других:φ 1 || φ 2==Aφ==!(! φ 1 && ! φ 2)!E ! φtrue U φ!F! φформулы состояния: p!f(f)f && ff || fAφEφформулы пути:f!Φ(φ)φ && φφ || φXφφUφFφGφp – некоторый пропозициональный символf – некоторая формула состоянияφ – некоторая формула путиЛогика СTL• Логика CTL – фрагмент логики CTL*, в котором подуправлением квантора пути (E или A) может находиться неболее одного оператора X или U.Корректная CTL формула:p!φφ && φφ || φEXφE (φ U φ)A (φ U φ)p – некоторый пропозициональный символf – некоторая формула состоянияφ – некоторая формула путиМожно вывести:EFAFEGAGAXfffff==========E(true U f)A(true U f)!AF !f!EF !f!EX !fПримерВ LTL <>p означает:A<>pдля всех вычислений, начинающихсяв исходном состоянии s0, выполняется <>pВ CTL можновыразить:EF(p)существует вычисление, длякоторого выполняется <>pAF(p)для всех вычислений выполняется <>pAG(p)для всех вычислений p – инвариантEG(p)существует вычисление, для котороговыполняется p – инвариантитд.Выразительные возможности CTL* и• CTL* и CTL описывают подмножестваω‐регулярныхCTLавтоматов над деревьями• автоматы над деревьями более выразительны, чемавтоматы над словами (CTL‐формула выполнима надереве трасс, а не на одной трассе);• CTL и LTL являются подмножествами CTL*;• CTL и LTL не сравнимы по выразительной мощности(пересекаются, но не включают);• на LTL можно описать свойства, не выразимые на CTL:• CTL не позволяет описать свойства вида []<>(p),• при помощи []<>(p) в LTL задаются ограничениясправедливости;CTLLTL– на CTL можно описать свойства, не выразимые на LTL:• на LTL нельзя описать свойства вида AGEF(p),• AGEF(p) используется для описания свойства reset: излюбого состояния система может перейти в нормальное.ВыразительнаямощностьМодальное µ‐исчисление,Автоматы над ω‐деревьямиАвтоматы над ω‐словами,автоматы Бюхи,конструкции never,LTLCTL*CTLLTLLTL без XПримеры формализацийвысказыванийДжейн вышла замуж и родила ребенкаP( Джейн_выходит_замуж /\ F Джейн_рожает_ребенка)Джейн родила ребенка и вышла замужP(Джейн_рожает_ребенка /\ F Джейн_выходит_замуж)Джон умер и его похоронилиP(Джон_умирает /\ XF Джона_хоронят)Если я видел ее раньше, то я ее узнаю при встречеG( Р Увидел  G(Встретил  X Узнал))Ленин – жил, Ленин – жив, Ленин – будет жить (В.В.Маяковский)PG Ленин_живЛюбое посланное сообщение будет полученоG( Послано(m) F Получено(m) )Вчера он сказал, что придет завтра, значит, он придет сегодняХ-1Х Приходит  Приходит(истинно)LTL и CTL – подклассы CTL*Алгоритмы проверки выполнения формул CTL* сложны  нужны подклассыВ LTL - формулы пути, которые должны выполняться для всех вычисленийпредваряются квантором пути АВ CTL каждый темпоральный оператор предваряется квантором пути А или ЕФормулы LTL:Формулы СTL:Формулы СTL*:AG( p F q )AG( p&EF(qr) )Е(p & X A F q)А ( а\/ Gb & (aU c))EF( а & E(aU c))ЕX (а & AX(bUc) ]А ( a U b)A (a U  b )А (a U  (F b) )СTL*LTLСTLСравнение логик LTL и CTL CTL*LTLФормулы этих двух логик характеризуют свойства разных объектовLTL – формулы пути, СTL – формулы состоянийВыражают свойства вычислений, которые представлены по-разномуCTLLTL – множество поведений, CTL – деревья поведенийИнтерпретируются по-разномуформулы LTL - на бесконечном множестве поведенийформулы CTL – на конечном множестве состоянийМетоды анализа - алгоритмы model checking - совершенно разныеВыразительная мощь несравнима: есть формулы CTL, невыразимые в LTL, инаоборотнапример, FG не может быть выражена в CTL (с некоторого времени вбудущем  будет все время истинным) AFAGp сильнее, AFEGp – слабеенапример, AGEF в CTL не может быть выражена в LTLПример формализации вСTL*М::“Летят за днями дни, и каждый час уноситЧастичку бытия, а мы с тобой вдвоемПредполагаем жить, и глядь — как раз - умрем”br = A [( G life)  (GEX death)]lifeА.С.ПушкинM |= brРазвертка М1:M1::lifedeathРазвертка М:.........life...death......M1 | br...............На развёртке М1 формула br не выполняется: ее развертка имеет траектории“вечной жизни” без возможного ответвления на состояния, помеченные deathРазличия LTL и CTL*Эти две модели не различаются LTL, но различаются CTL*:AG(pEFq).

В М1 эта формула выполняется, в М2 она не выполняетсяВ LTL обе модели представляются одним и тем же множеством из двухвычислений, поэтому LTL их не различаетTCTLTCTL – Timed CTL – естественное расширение операторов U, F, ... логики CTLколичественной информацией.Грамматика ТCTL (= CTL + Time):::= p    z in  E [ U ]  A [ U ]р – атомарный предикат - ограничение на таймеры и формульные часы z – формульные часыz in  - введение новых часов в формулу E [ U ], A [ U ] – как в CTLОбозначение: E [ U]  z in E [ ( &  )U ] Выводимыеоператоры EF  E [ True U   ] и т.д.Формулы TCTL включают E [ U~ k], A [ U~ k], EF~ k, EG~ k, AF~k , AG~ kгде ~ - любой символ из {<,,=, , >}иk – рациональноечислоПримеры свойств реальноговремениModel checking временных автоматов относительно выполнения заданнойформулы TCTL сводится к model checking его регионального графа относительновыполнения формулы CTL1.[ p U<2 q ] – р истинно непрерывно до тех пор, пока не станет истинно q, иистинность q наступит не позднее, чем через 2 единицы времени2.AG(problem  AG5 alarm) – как только проблема возникла, сигнал alarm зазвучитсразу и будет звучать не менее 53.AG(far  AF< 7 far) – поезд покинет область контроля не позже, чем через 74.AG [ send(m)  AF<5 receive(rm) ] – подтверждение приходит в пределах 55.EG [ send(m)  AF> 4 receive(rm) ] - подтверждение может быть получено более, чем за46.AG [ AF= 15 tick ] – тики следуют периодически точно через 15 е.в.

(но, кроме того,могут быть и в промежутках)7.AG (xy) - таймер х всегда не больше таймера упор, поках не будетиметь если светофор выключен,8.A [выключенoff U x  3 ] допо техлюбомупути таймериз начальногосостояниязначението онбудет  3Общие идеи в TLЛогика высказываний строится введениемВ логике линейного времени LTL кромеатомарных утверждений и операций логикивысказываний вводятся темпоральныеоператоры {U, X} (кроме них удобноиспользовать еще F и G)По конкретной цепочке состояний (миров) вкаждом состоянии можем вычислитьистинностные значения любой формулытемпоральной логики LTLВ логике СТL* добавляются кванторы пути,позволяющие различать свойства различныхпутейФормула CTL* определена для конкретнойинтерпретации (структуры Крипке) и всехвозможных ее вычисленийa, b,...c bd,...a,b, ...,Хс, bUd,...b, с, ...,b ...,a,d, ...,СTL является подмножеством CTL* - вформулах CTL каждый темпоральный операторпредваряется квантором пути...16Особенности UPPAALUPPAAL – это весьма популярное средство•••••верификации систем реального времениПростое в использованииБесплатное для научных исследованийИмеет в основе простую, но при этом довольномощную математическую модельМалопригодно для разработки больших системНе поддерживает описание иерархиивложенности компонентов системСтруктура• Модуль описания• входная модель – расширение модели сети временныхавтоматов• возможность описания параметризованных шаблонов• наличие данных различной степени локальности• Модуль симуляции• генерация и визуализации трассы сети• различные типы генерации (случайная, из файла)• Модуль верификации• проверка темпоральных свойств• предоставление трассы-контрпримера• воспроизведение контрпримера в модуле симуляцииПримерTrain Gate• Система обеспечения доступа к критическомуресурсу• Требуется обеспечить проход нескольких поездовпо одному мосту• В наличии устройство управления поездами• Остановка и разгон поезда происходят немгновенноМодуль описанияИмена состоянийИнвариантыПосылка сигналовПрием сигналовПредусловияПрисваиванияПараметрыМодуль описанияДополнительные возможностиГлобальные описанияЛокальные описанияЛокальные описанияОписание системыСинтаксис выражений• Выражение (в стиле языка C)Exp ::= ID | NAT |Exp[Exp] | (Exp) |Exp++ | ++Exp | Exp-- | --Exp |Exp AOp Exp | UOp Exp | Exp BOp Exp |Exp?Exp:Exp | Exp.IDUOp ::= - | ! | notBOp ::= < | <= | == | != | >= | > | + | - |* | / | % | & | | | ^ | << | >> | && ||| | <? | >? | and | or | implyAOp ::= := | += | -= | *= | /= | %= | |= |&= | ^= | <<= | >>=Синтаксис выраженийПредусловие• Булево выражение• Таймеры (t, t’) могут встретиться только вt rel Expt – t’ rel Exp• Указанные выше сравнения должны идти в предусловииподряд через конъюнкциюПрисваивания• Разделенные запятой выражения видаx AOp ExpИнвариант• Булево выражение без отрицаний• Таймеры (t) могут встретиться только в выражениях видаt rel ExpМодуль симуляцииВизуализация активных состоянийВизуализация трассыОкно текущих значений данныхОкно генерации трассыМодуль верификацииОкно результатов проверкиОкно текущего запросаОкно списка запросовПримеры запросовПримеры запросовПримеры запросовЯзык запросов• Допустимая формула языка запросов ::= A[]  | A<>  | E[]  | E<> |  -->  ::= Exp | A.l | deadlock|  or  |  and  | not  | ()• deadlock можно использовать только с A[], E<>• Семантика определяется на основе семантикиформул логики CTL• A.l  автомат A находится в состоянии l• deadlock  вычисление после достижения текущейконфигурации невозможно продолжить• 1 --> 2  AG(1  AF(2))• Выполнимость выражений определяется естественнымобразомСпасибо за внимание.