Надёжность ПО (All in one) (2014), страница 6

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

М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.2План лекции• Статический анализ– Модели программ– Алгоритмы статического анализа– Обнаружение дефектов• Другие статические методы• Заключение2Литература• Карпов Ю.Г. Model Checking.Верификация параллельных ираспределенных программныхсистем, БХВ-Петербург, 2010.• Кларк, Грумберг, Пелед.Верификация моделей программ:Model checking, МЦНМО, 2002.• Peled. Software Reliability Methods,Springer, 2001.3О чём этот курс• Концепции и связи• Аналитические модели и средстваподдержки• Методы для увеличения надёжности ПО:––––––ВерификацияСтатический анализТестированиеРасчёт надёжностиАнализ статистики ошибокБезопасность4Статические методыобеспечения качества5• Формальные инспекции, аудит• Формальная верификация– Дедуктивная верификация– Model checking• Статический анализ• Трансформации– Рефакторинги– Модификации56Статический анализ• Использует исходный код ПО для анализа• Применяется для–––––––––Форматирования программВычисления программных метрикОптимизации программРаспараллеливания программПреобразования программОбфускации программДеобфускации программОбнаружения дефектов…6Статический анализ дляобнаружения дефектов7• Использует исходный код ПО ВС дляанализа• Позволяет проанализировать всевозможные трассы исполнения• Позволяет проанализировать все наборывходных данных• Может быть полностью автоматизирован• Позволяет обнаружить нефункциональныедефектыx=1 y=2 z=9 x=2z = 13y=5 z=07Нефункциональные дефекты• Ошибки этапа кодирования• Не являются явным нарушениемспецификации• Являются следствием– сложности языков программирования– сложности библиотек– сложности алгоритмов и структурданных88Нефункциональные дефекты• Выход за границу массива• Переполнение буфера• Использование неинициализированныхобъектов• Работа с некорректным указателем• Арифметические ошибки• Утечки ресурсов• Ошибки форматных строк• Ошибки работы с ресурсами• и т.д.9910Проявление дефектов••••••Без проявленияЗависанияСбоиПаденияДеградация производительности…1011Опасные конструкции• Язык С–––––––МакроопределенияУказателиМассивыАдресная арифметикаУказатели на функцииПриведения типовОбъединения (union)1112Характеристики анализа• Полнота – доля найденных дефектовпо отношению ко всем дефектампрограммы• Точность – доля найденныхистинных дефектов по отношению ковсем найденным• Ресурсоемкость12Общая схема обнаружениядефектов1313Модели программ.Требования14• Полнота представления объектовпрограммы• Восстанавливаемость– Идеально: возможность полноговосстановления исходного кода– Желательно: связь с исходным кодом• Эффективность поиска объектов1415Модели программ.