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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 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))• Выполнимость выражений определяется естественнымобразомСпасибо за внимание.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций