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