Лекция 9. Временные автоматы. Timed CTL

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016Лекция 9Системы реального времениВременные автоматыНеправдоподобные вычисленияСети временных автоматовTimed CTLВступлениеПример(птица и рой комаров, как было много раз на семинарах)fedfarhungryfarfednearhungrynearЭта модель Крипке содержит, например, такую трассу:hungryhungryfedfednearnearfarfar......Недостаток такой модели (возможно) в том, что и птица, и ройкомаров живут в реальном времени, а в трассе отраженоразвитие системы в дискретном времениВступлениеПри описании системы с учётом реального времени изменениесостояний компонентов системы происходит в какие-то (необязательно целочисленные) моменты времениголод fed hungry?положение far0neareπ?времяУспеет ли птица съесть комара из роя?Или же рой комаров успеет заметить птицу и улететь?Это зависит от того, какими временными свойствамиобладают компоненты системы:Iесли птица успеет схватить комара до поднятия роемтревоги, то исход будет одинIесли рой комаров оказывается быстрее птицы, то исходбудет другойСистемы реального времениСистема реального времени (СРВ) — это система, поведениекоторой существенно зависит не только от того, в какомпорядке изменяются состояния компонентов системы, но и оттого, за какое время происходит изменение состоянийДля верификации СРВ необходимо иметь1.

средство описания моделей, учитывающее поведениемодели в реальном времени2. формальный язык описания требований, учитывающийреальное время3. алгоритм проверки требований для составленной моделиСистемы реального времениПример системы, учитывающей временныехарактеристикиI птица переваривает комара ровно 3 минутыI поголодав 5 минут, птица умираетI голодная птица не более чем за 1 минуту подлетает к роюкомаровI птице требуется не более 2 минут, чтобы поймать комара,когда она подлетела к роюI рой замечает птицу не менее чем за 3 минутыI заметив птицу, рой немедленно улетаетТогда развитие системы птица-рой во времени может выглядетьтак:...голод fed hungryfedположение far0near33.5far5.59...времяСистемы реального времениПример системы, учитывающей временныехарактеристикиI птица переваривает комара ровно 3 минутыI поголодав 5 минут, птица умираетI голодная птица не более чем за 1 минуту подлетает к роюкомаровI птице требуется не более 2 минут, чтобы поймать комара,когда она подлетела к роюI рой замечает птицу не менее чем за 3 минутыI заметив птицу, рой немедленно улетаетТогда развитие системы птица-рой во времени может выглядетьтак:...голод fed hungryfedположение far0near34far69...времяСистемы реального времениПример системы, учитывающей временныехарактеристикиI птица переваривает комара ровно 3 минутыI поголодав 5 минут, птица умираетI голодная птица не более чем за 1 минуту подлетает к роюкомаровI птице требуется не более 2 минут, чтобы поймать комара,когда она подлетела к роюI рой замечает птицу не менее чем за 1 минутуI заметив птицу, рой немедленно улетаетТогда развитие системы птица-рой во времени может выглядетьтак:голод fed hungryfeddeadположение far03nearfarnearfarnear45678времяСистемы реального времениПример системы, учитывающей временныехарактеристикиI птица переваривает комара ровно 3 минутыI поголодав 5 минут, птица умираетI голодная птица не более чем за 1 минуту подлетает к роюкомаровI птице требуется не более 2 минут, чтобы поймать комара,когда она подлетела к роюI рой замечает птицу не менее чем за 1 минутуI заметив птицу, рой немедленно улетаетВ зависимости от того, насколько быстро будут действовать птица и рой, птица может как накормиться, так и умеретьСистемы реального времениИ как же учесть реальное время в модели Крипке?Давайте попробуем явно добавить время в состояние:hungrynear2’53”?Реальное время континуально, а число элементов трассысчётно, поэтому “по-честному” добавить в трассу реальноевремя непростоНо как правило, система изменяет своё состояние неконтинуально часто, а в худшем случае счётноЧтобы анализировать СРВ, достаточно обозревать те моментывремени, в которые система изменяет своё состояниеСистемы реального времениА почему бы не абстрагироваться от времени и нерассматривать только такие системы и свойства, как былираньше в лекциях?В СРВ, как правило, существуют директивные срокивыполнения задач, и для таких систем требуются гарантиивыполнения этих сроков:Iптица не поела вовремя — умерлаIпарашют не раскрылся в срок — тоже не очень хорошоIподушка безопасности раскрылась на долю секунды позже— и опять всё плохоУпомянутые здесь системы — это жёсткие СРВ: для такихсистем требуется обязательное соблюдение директивных сроковСистемы реального времениЕсть двойственное понятие: мягкие СРВСрыв директивных сроков в таких системах возможен, но какправило ведёт к ухудшению качества работы системыНапример, обычная операционная система на высоком уровнеабстракции — это мягкая СРВ: если процесс освободил памятьна секунду позже запланированного, то система продолжитработать, но некоторое время будет работать медленнее, чеммогла быДля анализа жёстких и мягких СРВ используются совершенноразные подходы и моделиМы будем рассматривать только жёсткие СРВВременные автоматы— это самый популярный формализм, используемый приверификации жёстких СРВПрежде чем вводить формальные определения, рассмотримтакой пример:`2`1`3Это автомат, с помощью которого мы попытаемсяпромоделировать щелчок и двойной щелчок мышки:I`1 : никаких щелчков не поступалоI`2 : поступил щелчокI`3 : после щелчка поступил второй щелчокВременные автоматы`2`1clickclick`3Что нужно добавить в автомат, чтобы он адекватно описывалдвойной щелчок мышкой?Автомат взаимодействует с окружением: нужно уметь различать, когда пришёл щелчок мыши, и адекватно на него реагироватьТак в автомате на переходах появляются события; здесь — событие clickВременные автоматы`2`1clickclick`3Чтобы два нажатия на кнопку мышки трактовались как двойнойщелчок, между первым и вторым нажатиями должно пройтидостаточно мало времени — скажем, меньше секундыЧтобы уметь отслеживать, сколько времени прошло после первого щелчка, заведём таймер x: переменную, значение которойпринимает действительные значения и увеличивается с той жескоростью, с которой течёт времяВременные автоматы`2`1click, xclickclick, x < 1`3Как только в системе возникло событие click, эта переменнаядолжна быть сброшена в 0: начинаем отслеживать, сколько времени прошло с первого щелчкаЕсли второе событие click произошло меньше чем через секунду после первого, то следует перейти в состояние двойногощелчкаЭто ограничение на возможность срабатывания самого правогоперехода: предусловие x < 1Временные автоматы`2click, x`1doubleclick, x < 1, x`3x ≤ 0Из состояния “был двойной щелчок” следует немедленно перейти в состояние “ожидаем первый щелчок” и проинформироватьокружение о том, что произошёл двойной щелчокДля этогоIсбросим x при переходе в `3Iзапретим в `3 течь времени: пометим инвариантом x ≤0 (при нахождении в этом состоянии значение переменнойx не может быть больше 0)Iпри переходе в `1 произведём событие doubleВременные автоматыsingle, x = 1x ≤ 1`2click, x`1doubleclick, x < 1, x`3x ≤ 0Если мы прождали в состоянии одинарного щелчка секунду исобытие click не произошло, то следует немедленно сделатьзаключение, что произошёл одинарный щелчок мышьюДля этого добавим инвариант x ≤ 1 в состояние одинарногощелчка, разрешим перейти из этого состояния в исходное тольков том случае, если x = 1, и при переходе в исходное состояниепроизведём событие singleВ результате получен временной автомат, распознающий одинарный и двойной щелчки мышиВременные автоматыА какой спектр действительных констант можно использовать вописании автомата?Если цель — описать алгоритм верификации временныхавтоматов, то использование континуума различных константпомешает достигнуть этой цели: входные данные алгоритмадолжны быть конечными, а конечного способа описанияпроизвольных действительных чисел не существуетВременные автоматыЧтобы ограничиться счётным набором констант, не снизиввыразительные возможности модели, обычно предлагаютсятакие рассуждения:Iвремя наступления событий в СРВ всегда измеряется спогрешностьюIзначит, вместо действительного числа во временныхограничениях можно использовать достаточно близкоерациональное числоIкогда модель составлена и образовалось множествоиспользуемых в модели рациональных чисел, можнопривести эти числа к общему знаменателю и“масштабировать” время модели, убрав знаменательIв конечном итоге можно без снижения выразительныхвозможностей использовать в модели только целыенеотрицательные числаВременные автоматыВременной автомат — это система (L, `0 , Σ, C , I , T ), гдеIL — конечное множество состояний автоматаI`0 ∈ L — начальное состояниеIΣ — конечное множество событийIC — конечное множество таймеровII : L → inv (C ) — разметка состояниий инвариантамиT ⊆ L × (Σ ∪ {λ}) × guard(C ) × 2C × L — отношениепереходовIIIIλ — особое событие, означающее отсутствие событийтретья компонента перехода — предусловиечетвёртая компонента перехода — множествосбрасываемых таймеровВременные автоматыЕсли разрешить в качестве предусловий и инвариантов писатьочень выразительные формулы, то задача анализа поведениявременного автомата окажется неоправданно сложнойЧтобы упростить эту задачу, оставив достаточно широкийспектр описательных возможностей, в модели временныхавтоматов предлагаются такие множества inv (C ), guard(C ):I элементарные ограничения ATC (C ) — это выраженияtrue, false и всевозможные выражения вида x ./ k иx − y ./ k, гдеIIIx, y — таймерыk — целая неотрицательная константа./∈ {<, ≤, >, ≥, =, 6=}(то есть k ∈ N0 )Iв множество guard(C ) входят всевозможные формулы,составленные из элементарных ограничений и логическихсвязок &, ∨, ¬, →Iв множество inv (C ) входят всевозможные конъюнкцииэлементаных ограничений true, c < k, c ≤ kСемантика временных автоматовСодержательное описаниеТекущее состояние вычисления (конфигурация) временного автомата определяется тем, в каком состоянии находится автомати какие значения имеют его таймеры.Изменение состояния компонента СРВ занимает некоторое время, и в течение этого времени компонент находится в “промежуточном” состоянии: одно состояние уже покинуто, а другое ещёне достигнутоСемантика временных автоматовСодержательное описаниеВ семантике временного автомата такое поведение компонентовсистемы невозможно, вместо это автомату разрешается выполнение одного из двух действий:Iнекоторое время находиться в некотором состоянии, неизменяя его, если это позволяет инвариант состоянияIмгновенно изменить состояние согласно переходу систинным предусловием, сбросив таймеры, указанные напереходе и перейдя в состояние с истинным инвариантомПри моделировании СРВ следует учитывать такое расхождение“реальной” и “модельной” семантикСемантика временных автоматовБолее строгое описаниеКонфигурация временного автомата (L, `0 , Σ, C , I , T ) — это пара(`, d), где ` ∈ L и d : C → R≥0(R≥0 — множество всех неотрицательных действительных чисел)Для простоты иногда будем полагать, что таймеры автоматаупорядочены: C = (x1 , .