2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 77
Текст из файла (страница 77)
Требования недопустимости нарушения установленной временной границы назывыотса "жесткнмн" (Ьвгб) требоеанивмн реального времени. В отличие от "жестких" требований реального времени, в некоторых системах нарушения временной границы возможны, но они не должны быть слишком частыми (например, доставка почтового сообщения). Такие требования называют "мягкими" требованиами реального времени. Проверка свойств "мягкого" реального времени связана с оценкой вероятности нарушения временных границ, алгоритмы проверки таких свойств рассматривались в гх П. Свойства "жесткого" реального времени рассматривыотся в данной главе.
Дяя распространения на такие системы методов верификации, объединенных под названием «юде) сйесязлб. необходимо: (У разработать модель систем реального времени, операционная семантика которых адекватно отршюыт их поведение во вренени; П расширить темпоральную логику так, чтобы можно быяо бы формулиро- вать свойспш поведения, вкяючшощие временные ограничшпш1 гневе ш чение стоян менел не 12Л (сислнмгы внове Для т произ звень рых е рис.
! ни. В ную < среде Твкое труди (з ршрвбоппь влгорппяы люде! сйш)плй — влгорнтмы проверки формул рвсширенной твмпорвльиой логики нв модели систем реального времени. Именно этим вопросам посввщенв двннвя глене. 12.1. Модель систем реального времени. Временной автомат и его поведение Сисгемы реального времени — это такие системы, которые доюкны выполнять свои задачи в пределвх строгих временных огрвниченнй. К классу систем рояльного времени относпся прогреммные и аппаратные системы, применяющиеся в совершенно разных сблвстях.
Это протоколы связи, системы управления роботов, бортовые системм легвтельнмх вппврвтов, встроенные системы медицинской техники и т, л. Кяк и для других систем, верификация систем ревльного времени требует формального зядвння нх функционировеиия и формвльной специфнквцнн нх свойств. И то н другое лоюкно включать уквзвнне нв интервалы рмшьного времени между событиям н. Одна из неибшме респрострененных формвльных моделей для опнсения систем этого типа называстсл временным автоматом (Тшшд Аншпшнщ). В этой мщшлн используется простое решение — в модель конечного автомата введены вещественные переменные спецнвльного виде — таймеры, илн локальные часы.
Прцыпр 12,1 Рвссмотрим пример простой прогрвммы, рвэличмощей одинврный н двойной щелчок мыши. Очевидно, что для того, гюбы различить их, программа полжил оценшь временной нншереае между последоипельными нажатиями нв кнопку мыши, и сглн этот нигерввл меньше некоторой границы, то считать дев последовятельных ншквтия нв кеввншу одним двойным щелчком. Нв рис. )2.1 прелсшвлене автоматная модель такой пршреммы.
В автомате А, переменим х — это переменнвя, которая по умолчанию непрерывно измешмтся со временем, онв моделирует поведение часов (нвпример, аппаратного твймерв) и незыввстся локальными чвсвмн. С помощью таких переменных можно отсчнтыввть интервалы времени, прошедшие с момента прихода сишчмы в некоторые состояния.
В печальном состоянии гс автомат ожидвег ок окружения события "нвжвтне кнопки мыши" (дейстием а ). Когда это собмтне наступает, автомат А, нереходнт в сосювние з!, н при перышке зне- вяз! прихг перел миру~ щел н инфо! я<1 !рмул ени. яжны 3. квз;с ! сисэтой ~ вве- каль- Оной амма няни счи- >ызтФ о ю- арвт- КОЛЙ о со- зна- пиые зсжы паре; сисругое юбы- чение локальных часов х сбрасмвастся в О. Когда автомат находмюя в со. стоянии з,, переменная х непрерывно изменяется — увеличивается со временем в одном темпе с реальным временем. Условие х <1 на переходе из з, в зз говорит, что сели менее чем через одну единицу времени после момента прихода в состояние з, произойдет следующее нмкатне шишки, то автомат перейдет в состояние зз н затем прн переходе в зе вываст сигнал Ь, информируя окружение (например, операционную систему) о событии "двойной щелчок".
Если щюшла в точности одна единица времени после первого нажатия ююпки, то автомат переходит нз состояния з, в зс с выдачей енгнам с, информируя окружение о событии "одинарный щелчок". Неравенства х > О, к <1 и хи! на переходах назмваются "зпшимамн" переходов. Рнс, 12Л. Временной автомат, рвзлнчвюжий овннарный н двойнон щелчок мыши Дпя того чтобы указать. что автомат не макет находиться в сосзоянии з, произвольно долго, это соспжнне помечено неравенством х К! — так назмеаеммм "нляарналмом ссслиншня". Инвариант определяет условия, прн которых автомат может находиться в лаином состоянии. Автомат, показанный нв рис. 12.1, не может находнтьса в состоянии з! дольше, чем 1 единицу времени. В состоянии зз автомат выдаст сигнал Ь, информирующий операционную систему о том, что произошло событие "двойной щелчок кнопки".
не позже, чем часы х примут значение!. Таким об1изом, инвариант — это средспю "заставизь" врмненной автомат покинуть состояние. Такое расширение модели конечного автомата удобно, но возникает одна трудносп Первменная х — это переменная апециаиивео тзинк воторая по умолчанию непрерывно изменяется со временем, поэтому состояния такого автомата уже ие явлшотся сосюяниами в строгом смысле этого слова.
Состояние системы — это набор значений всех ее переменных, спнозначно определающий дальнейшее поведение системы. Локальные часы временного автомата являются его переменными, от их значений зависит будущее поведение автомата. Но локальные часы .т ышуг принимать бесконечное число значений (континуумЕ поэтому у любого временного автомата будет бесконечное число состояний. Назовем зе, г,, и зз на рнс. 12.1 локациаыи. Состош~мем временного автомата будет шнппъся нмя локации пикк значения всех его переменных, в том числе его локальных часов. Например, состояниями автомата на рис. 12.! могут быть: (зсг х=б!), (зс,' я=2011), (г~', я=04), (гз,' я=0345), ио не могут быть (з!! я = 5. 1), поскольку здесь нарушен инвариант а локации г!, или (эсг х = -2.бб) — часы не могут принимать пгрицательнью значения. Определим формально модель временного автомата — конечного автомата, расширенного введением локальных часов, отсчитывающих иитервшты реального времени.
о Определенна 12.2 ! Вреыенндй автомат — это шссшрвв л (Еос. йые, Е, Х, йгг, л), где: ° Еас — конечное множесшо локаций, содеряшщее начальную локапдго !гюс'* ° Х вЂ” конечное множество наряженных специального типа, называемых локальпыын часами, Значениа локальных часов непрерывно изменяются — они непрерывно возрастают синхронно с реальным временен. Часы могут прнниматыпобые ващественные значения из Вз", они могут только читаться 1испольынатьгл в ограничениях) и сбрасываться в 0 на переходах; Š— конечное ыншкество действий; будем считать, чго пуспю дейспше входит в Е; е глг: Есс -+ у — инвариант. определенный в некоторых локацнях.
Здесь у — это предикат, ограничение на возмшкные значения часов, опрвлеляеиое квк логнчеепш формула, построенная из зяенензврных ограннченнй л-с юпг к у-с, где с — рывюшшьное число, вием торы рис. мы г! при: Пере пере. иа зт Как ! х, у — локвльмые чваы, а отношение — принвдлмкмг мнолмству (ь. <) (т.е. - в (~ <)). Будем обозначен далее Г(Х) множаство возмакных ограничений на значения локальных часов из множества Х.
Если значение 1лэ()ас) не определено, то инвариант в локации (ас естысие. Инварианты определмот про~расс системы; онн ограничивают сверху те значения, которые чаем ма~уз принимать в локации. Если инвариант определен в локации (аа, то нз этой локации должен быть выполнен переход до того, квк мог инвариант спнвт ложным. Ситуация нарушения инварнанта в локации останавливает прогресс времени и является ошибочной; ° Š— множество переходов автомата, Е с Хас х Г х Е х 2» х Хос; если ((ас, у, а, Л, (ас') е Е, то мы будем пнешь: (ас-(у,а, Л)-ь(ас'.
Кшкдый переход во временнОм автомате — зто переход мшкку двумя локвциями, помеченный защитой перехода у е Г(Х) (возмшкно, пустой), действием ю множсспш Е (возмшкно. пустмм), а также множествам Л часгж, кеторые на данном переходе сбрвсывматся вб (рис.12.2). Квк показано на рис. 12.2, далее в этой паве опермшю сброса локальных часов на переходе мы иногда будем обозначать явно, т.е, вмесю Л (х,у) будем писатьх: О; ужб. Например, переход автомата рнс. 12.1 нз локации гэ в локвшво гз молва записать таю з,-(х<1,а,о)-+зз. Автомат переходит из локации г, в локацию гз с'выполненицч собьпъш а, прн этом значение времени, нмгопленного часами х, должно быль меньше 1. Переход всегда счичается мгновенным; в данном примере после выполнения перехода значение часов к сохраняаюя: мноямство сбрасываемых в О часов на этом переходе пусто.
Как н состовння структуры Кринке. локации временного автомата могут быть помечены атомарными преднкатвмн из конечного мнохмства АР. Пусть ܄— эта функция пометок: Е,: Хос -+ 2"Г. В дальнейшем будам считать, что имена локации таске яшшются атомармммн преднкатами. :эйэ Рнс. 12.2. Переход яременеого автомата Таким образом, временной автомат — зто такое расширение конечного авто.
мата, у которого существует конечное мноэмство локальных часов (непрерывнмх переменных специального типа). Локальные часы отличаются от переменных других типов: они принимают талька неотрицательные вещественные значения, с часами мелик выполнять операций, их можно только сбрасывать в ноль на переходах н их можно указывать в ограничениях. Часы исполиукпся дяя точной фиксации иншрвалов времени между событиями в системе и для ограничения времени нахождения системы в той или другой локации. Все локальные часы идут синхронно, а одной и той же скоростью 1 — синхронно с реальным временем. В каждый момент функционирования временного автомата юокдые локальные часы показывыот интервал рвшьного времени, прошедший после их последнего сброса.
Такая модель позволяет выразить неопределенность временных ннтервшюв мюкэу двумя событиями. Длительность интерышов может находиться от 1 (ншкнэя граница временного ингервала, )ем Ьошн1) до к (верхняя гранина, вррег Ьоош1). Например, можно предстаыпь так называемые "неточные" временные переходы э,-[1, н]-+эх, моделирующие протяженные во времени дейешня. Такие переходы можно выразить установвением инварианта в локации и установлением подходящей зашиты перехода. Две возможности определить. что после события эгагг. событие у)лпй наегупит в произвольный момент во временном интервале [2„8), показаны на рис.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
