2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 86
Текст из файла (страница 86)
Последовательность Репюнов прн проверке выомиинвя формулы нС зл вгрефеоегнонов й(Атфл,ре(зюО)) Для проверки выполнения формулы ЕУмя Ся, н в автомате Ат преобразуем брмАСягл=И~((я<1)лдСз~н))=И <гЯ~--Ер((зе1) лДз). Поскольку формула уз =АСпн выполняется в состоянии Оз =(зг,(хнО)) графе регионов й(Ат) то онв выполняется и в ммзояниях зз зт зз графа Регионов й(Лт 9 з, Ое (з.= О)) (рис.
12.! 8), отличаошдхгя от Оз только значением вспомогательных вформульных" часов. По графу регионов й(Ат 9 з, Ое (з — 0)) последовательно имеем: Ь 'ьСягл1 МУз) (зз зт зз) ' за=(зс1); 3а3(1е) (ве, яг, зз,гз); Л нии Оз графа регионов й(Аз) временного автомата Ат. На рнс. 12.20 показан начальный фрагмент графа регионов, нз которого видно, что формула ДСх, л не выпслнаетса в состоании Ое.
Подобные постРоенма показывают, по зтв ф~р~у~а аыполнзетса юлько а состоянии Оз ~Рафа Рммоюю вре~енного автомата Ат. Равен Тг Л-.уз уь' МЛ)-(а)! УвмЕ%! йп(А)м(зе Э! ЭЗ). Поскольку формула ЕР,(АО (л выполняется в начальном соспжнин графа регионов й(А)(гз,дс(зжО)). построенного нз начального состояния се (рафа регионов й(А)), то зтв формула выполняется для автомата Ат .
Приведем алгоритм пю()е! с))ес)()пй проверки выполнимости формулы Ф логики ТСТВ для графа регионов й(А) временного автомата А с множеством состояний з, множеством атомарных предикатов АР, множеством локальных часов Х н мжнкеством (нраннчеинй на часы Г. Он состоит в разметке состояний й(А) теми подформулами формулы Ф, которые выполняются в этих соспмннях: Яен аьь 0< 1 5 (Е! Со яог а11 ч'е зоые) нгть (ч'! 1 ео /' зсз поннчэсгкм ч' маннонися ангорнтэкм сннтзкснчаского анализа Фщмулн в */ ° «Ьтсь (Ч'1: кю39: ватт .
'31 Р !' Заеч.- ( Зав! Э-< 1СС)(Ч)), РВЬ(1ОС! )Г т: Заст: ( эаЩ з ( 1ос1(ч)) (ч)! т !) Р: ваег . ( Эаз! Э (1ССУ(Ч)), РаЫ1) Рк(: Яакч: ( Заз! РаЫЗ) Ч Чаыэ)' ): В(рргч): ' 'Зьзт: затон(ВП(рчс, (ЗЕЩ Д г! ! ь В(РЦК)): Зае„: Зато„(ВП(РМЬ (ЗЕ/Л Л Ч ! ) ) ° па мммь /* звоним э вр нонна атсэагрньп прекикат рт и состояние гРаФа Регионов из Засг помечаем им */ яок а)з эе закт ео ь(э) ~ ыэ)гг(рт) оа оп ое Отметим еще раз: алгоритм пки(е! сйес)()нй может быль использован только в том случае, если вп временном автомате нет вычислений Зенона.
Зтн вычисления включают бесконечное число действий в конечном интервале времени. Поскольку действий у временного автомата конечное число, то вычисление Зенона в графе рагионов автомата включает цикл, прмводящий к той же самой локации без приращения значения локальных часов на! илн более.
Существует простой способ выяснить наличие таких вычислений: для того Лег Суп в кс иын зтоЕ ний где ввщ фор за на„ Вп лы ~ тнч~ опе! "фо уюк фор выр )0т етс) чтобы во временном автомате отсутствовали вычксленнв Зенона, достаточно, чтобм дяя всех состояний автомата выполнвмсь формула ТСП.; АР, зри. е и. яс го Логика ТСП» Существует аарнюгг временной темпорвльной логики ветвящегося времени, в которой, в отличие от ТСП., ограниченив реального времени задмогся явным введением "формульнык" часов, "щмороженных" в рамках формулы этой логики. Грамматика формул логики ТСП опредсвяег формулы состояний ф, которые строятсл по следующим правилам: фсир)у~ Ц~фчф)згпф(Е(050))А(фбф), где р — атомарный предиквт, а у — условия, ивникенные на значения локальных часов. Оператор " з гв " называется оператором "заноралсиеалия", он вводит новые "формульные" часы з и ограничивает область их действия формулой ф, к «огород он применяется.
Формула з!а ф истинна в состоянии з временного автомата л, если в состоянии з(зжй) истинна формула ф в автомате ЛЭз. Например, очевидно, что формула з'ги(з О) всегда истинна,аформула з!и(г=З) всегдалаюм. В отличие ог логики ТСП„в которой явно укюываются временные ингсрмглы в темпоральном операторе Улгй, конструкция я йз ф логики ТСТАВ фагь тически, отвязывает введенные "формульные" часы от этих темпораяьных операторов, позволяя использовать условия, включмощие единственные "формульные" часы в качества атомарных предикатов любых формул ф, упманных в качестве аргумента оператора "замораживания". Например, формула: Фг = з !а ~Ер(ф~ и (з <1О)» ЕО(з < 20 ю - фз)) ) вырмкаст следующее свойство: из текущего состояния з эа время г, меньшее ! 0 единиц времени, можно достичь такого состояния з', в котором выполняется формула фг и из когорого существует путь, нв котором в течение по меньшей мере 20 единиц времени нс будет выполюпься свойспю фз.
Лспо, что формула Ф, отлична от следующей формулы ТСП.: Фз = Ейме(фг »ЕС»ю фз), а шпорой временнме ограниченна евювны С резянчнмми "формульными" часами. Главе гз Оквзывастсв, формула Ф, не может быть выражена в логике ТСП.. Следова- тельно, логика ТСП. мююе выразительна, чем лопаю ТСП . Однако алго- ритм пюре! спссЫпб для формул ТСП„не отличаеюя от подобного юггорит- ма двя формул ТСТ1.. На ма < яств кой вых 12.12. Сложность алгоритмов пюре! спесйпц для логики ТСТАВ. 12 вр Алгоритмы проверки свойств, вырюкенных формулами ТСТ1., весьма слож- ны.
Например, известно, что ниже сформулнрованнвв проблема являегся ХР- трудной, но она формализусгсл как задача проверки свойства достюкимости лля простого временнпо автомата. Рао ны. Да Приыир ! 2.16 Проблема ВсЬзсг-Вшп состоит в нвхвкденнн тавого псдмновмства заданного конечного множества Я нюУРальных чисел, Я = (мг,мз, ...юз1, сУмма элементов которого равна заданному числу М (зта проблема рассматривалась в примере 9.7). Дяя ее решения построим временной автомат с Ь+ ! состоянием (рис.
!2.2!), переходм (зги я,) которого могут выполняться либо при точных значениях локальных часов х = т„либо мгновенно. Очевидно, что алгоритм проверки выполннмостм формулы ЕР мзз лля этого временного автомата решает проблему ВеЬюьбшв. Ою тго рьн звн Рис. 12.21. Прсдсювясвие проблемы ВеЬяы-Вмп временным авгоматом Вр А Слшкность алгоритма юоде1 сйесЫпй для ТСП формулы Ф во временном автомате А линейна отюювтеяьно числа подформул в формуле Ф, а также относительно числа состояний н переходов в графе регионов автомата А.
Число состояний графа регионов линейно зависит от числа локаций автомата А и числа регионов, В свою очередь, число регионов временного автомата огромно: оно экспененциапьно зависит от числа локальных часов и потолков этих часов. На практике аернфикаторы систем реального времени мог)гг проаерюь мог ма ограниченный диапазон свойств. Например, система Нррмб ммлизирует сети взаимодействукнцих временных автоматов, но ограничивается проверкой лдя них свойств достнашмости, а также проверкой простых одноуровне. вых формул логики ТСП.. 12.13.
Другие проблемы верификации временных автоматов Рассмотрим, какие проблемы, встающие при аарификации, могут быть репы. ны для временных автоматов с использованием модели графа регионов. Допускаемый язык Одна из проблем верификации временного автомата А = (ь', (осе, Е, Х, 1лг, Е)— зю анализ его языка, т. е. возможных цепочек действий из влфавша Е, которые может выполнпгь автомат. Временным действием автомата А была названа пара (г,а), где а н Š— действие, которое выполняется автоматом по. гле временного июераала 1 и К, прошедшим с момента старта автомата Временная траектория — зто (жжможно, бесконечнаа) последователыксзь временных действий (ге,ае)(гнс))(гглзг)(гз,аз)...(гоа„)..., где г, ьгнг днз всех 1 не 12.9 Траекторией временного автомата А нвд временной трамгюрней ч =(го,ае)(гна,)(гг,аг)( з аз) ...
назовем вычисление А: (1 Мге)-Ас-ь(1 'гг)- с- (~ ' )-4- (1 ' 'г)- ((осг гг)-Аг +((асг г'з) аг -+- удовлстаоряюшлй условию г, =г, г + А, . Значение ннюрввла аремснм г в паре (г„а,) назовем временным штемпелем дейошня а,. Временный язык временного автомата А (обозначим его ь'(А)) — зто множество всех временных траакпгрий,Д, для каюрых сушествуст вычислрние А надь. Прммвр 12.11 Лля автомата А, рис.
12, ! временными траекториями будут', (1, а)(1Х а)(1.5, Ь)(42, а)(52, с)(162, а) ...„ (1.34,а)(1 42,а)(1.5,Ь)(4,а)(4.5,а)... Окюываеюя, что проблема включения временных языков (следовательно, и проблема эквивалентности таких языков) для временных автоматов в общем случае алгоритмически иерюрешнма. Если абстрагироваться ог временных штемпелей в цепочках азыка, то мы получим цепочки так называемого "невременнбго" язмка. НевременнЬй язык автомата А, обозначаемый ( „м„г(А),— это множество возмомных цепочек а!азат ... действий А, для которых в А существусг каках-либо временная траектория ч=(г!,аг)(гз,аз)(гз,ст).... чит сив~ Пус фаа сос ЛЕММА 123 (включение языков) Проблема проверки включения (Е .
~ (А) С (ь г(В)) невремениых языков для двух временных автоматов А и В разрешима, Она мшкст быть решена с помощью графов регионов этих автоматов. Пример 12.1$ По графу регионов автомата Аз (см. рис. 12.! 3) видно, что егд иевременными траекториями будут: аЬаЬсссс, асссс и лр. По этому графу молшо закеючигь. что в автомате Аз не могут выполниться цепочки действий аЬсаЬ, ассЬа и подобные им.
Под возлейсшием вкодной цепочки ассЬ временной автомат Аз не машет вернуться в свое начальное состояние, как зто махно было бы предположить по его виду. Граф регионов гз(Аз) показывает, что в этом автомате тмшя посяедоввзеяьноюш действий вообще невозмомиа. Бисимуляция Один из подходов к проверке шюйств временных автоматов заключается в том, что для проверммого автомата А строится контрольный временной автомат В, выращмощий требуемое свойство, и проверяется эквивалентность поведений автоматов А н В.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
