2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 79
Текст из файла (страница 79)
Кыкдое состояние— это пара (1ос; «), где ДюиЕос — локащи. в «гХ-+И интерпре. Анализ свойств поведенна временного автомата нежжможно выполнить непосредственно по его спецификации, Определение временного автомата— зто просто синтаксические правила, конечное описание, определжощее возможные действия и ограничения на выполнение этих действий. В таком определении некоторые ограничения могут быль противоречивы, некоторые состояния и дюкс локации могут быль вообще недостижимымн.
Интерпрепь цией этих синтаксических правил описания временного автомата является его поведение, его возможные вычисления. Каждое возможное вычисление временного автомата определяепз последовательностью состояний, которые проходит автомат в вычислении, и переходами между этими состояниями. Поведение временного автомата А определяеюв его операционной семантикой, которую можно представить графом переходов Т(А) .
Определим граф переходов временного автомата формально. Введем понатие нлтгрнргтаяин часов «квк присваивания юокдым локальным часан временного автомата неотрицатсньнсго дайстщпельного значения, «:Х-«Кк~. Обозначим «+А увеличение показаний часов хиХ с Главе ГЗ Граф ~ денна тацнн всех локальных часов денного автомата, удовлетворяющие инаврианту локации 1сс г т'г= глг(1сс); Ое — югчвльное состоанне, Ое =(!осе,'те), пш те — начальнал ннтарпреташш всех часов, такая, что дая любых х в Х, те(х) = О; ° Š— мно.'кесшо действий (совпадает с мншкеспюм действий автомата А); ° К вЂ” множество переходов двух видов: задержка в локации автомюи А на временйой шпервал А>О (переход по времени): (1сс; т) — Н -+ (1сс; т+ л) — выполняется' прн условии удовлетво- рения инварнаитов, т, е, в случае, если ннааршпгг 1лг(!сс) исти- нен для т+г прилюбом г в интервале Оп!яд; переход авь с изменением локации автомата А (переход по действию й (!ос; т) — а -+ (1ос", т') — выполнясюя прн условии истинности запштм на этом перекопе, т.
е. если (!ос, 7, а, 2, 1сс') в Е, то т уяовлетворяет зашите 7 и Г(Х): т! 7; т' — новые значения часов после перехода таковы: показания сбрасываемых часов из множества 2 становятся раанымн О, показания оспшьных часов не изменяются, и показания часов после выполнения перехода улоапсгаоряют инварнагпу новойлакацни !се .
т ) 1лт(!сс ). Будем обозначать з+И для любого состояния з (1ос;з) сисюмыпереходов временного автомата и неотрицательного А такое сосюянне (1сс;т+А), в которое система переходов моямт перейти после задержки А . Примпр 12.6 На рис. 12.7 схематически представлен граф переходоа Т(Аз) временного автомата Аз (см. рнс. ! 2.5). У авгомюи Аз аозмшкны слелукицне переходы, которые предссшлены в Т1Аз): (г '(г (г След (з (я ш~ (я !>О ТЩх ! по т эв мн ов ) Р 12.т. Гр фщ...р, Е Л, Граф переходов временного автомата представллст все мимсмнме его паве. денна. Любое поведение временного автомата начн!метов с начвлыкн'о со- (щ х 03)-03-+(щ к=04) (переход по закерагм); (щ к = О, 1)-022! 1-+(щ л 0321!) (переход по задерхске); (щ к=!,3)-а-ь(щ л=0) (переход по действию).
Слслукннне переходы невозмомнм в автомате А г (щ к =О 1)-2 5-ь(щ х 2 6) — нарушение ннвзриюпа в локаллн щ (щ к=13)-а-+(щ л=!.0) — часы т на переходе должны быть сбро. (щ л 0 3)-л -г (щ т 0) — нарушение змцнтм перехода. Гавел гд Абст пред вычи где и (зе! х = 0) -0.5 -+ (яе,' т = 0.5) — 6.! -ь(зе! х = 6.6) -л -+ (я,; я = 0) — 0.5 -+ (збх=05)-02-+(яб» 07)-а-ь(~;х 07)-02-ь(зз,'.х=Ъ9)-Ь-ь (гс'я=09) 03-+(те!к=! 2)-+- Ли произвольного вычисления к=Ос -св-+9! -<~-+ Чг -пз-+ Уз -лз-+- где а, — либо действие, либо щаержкв, обозначим д(к, 1) время, промедлив с момента стаРта автомата из начального состоанив рв до момента, котла автомат окажеюя в состоянии 9,, Формально: Д(к.й) О; д(я,1+!) 0(к,1)+4,еслипереход а, — зтозадержка Н; = б(к,1) — если переход а, — зтп переход по действжо. Лля приведенного выше вычисления о автомата А',: Д(п, 2) 6.6 Д(а, 4) = 7.
! Д(п, 5) 7.3 й(п, 6) = 7.3 Вмчнслення временного автомата можно рассматривать по-рщному в зази. симости от целей внаямзх Например, абстрагируясь от действий, вычисление можно продолжить как последовательность состояний и переходов — временных задерхмк, например: По в "врез дейа лись: (1, Така можа вие с по уч "еркь вычи каны состо начал (з; х стоян ляет ! числе стояния с начальной локвцией 1осс н всеми вокальными часами, установленными в О.
Затем автомат альтернативно выбирает либо задержку по времени, синхронно увеличивая значения всех локальных часов, если удовлетворяется инвариант текущей локации, либо переход по действию, если значения лоющьных часов удовлепюряют защите з юю перехода. Переход по действию мгновенный: значения локальных часов при его выполнении не меняются за исключением тех, которые сбрасываотся на переходе в О. Все допустимые последовательности состовний графа переходов представ. лают возмоягиые вычисление соответствующего временного автомата. Например, во временном автомате А, рис. !23 возможно следующее вычис ление: ш г2 ленами, егся ло|я за эгда вви.'ние аре- о (зе;х = 0) — 0.5 -+ (зе;х 0.5) - 62 -+(зс,х = 6.6) -0 -+ (збх О) — 0.5 -ч (збх = О 5) — О 2-+ (збх = 07) -0-+ (зз, х = 07) - О 2 -+ (збх = 03) ...
Абстрагируясь от переходов (и задержек, и действий), вычисление можно представить просто как последовательность сосгояний. Приведенное выше вычисление с этой точки зрения мохшо предсташпь так: о = Че 01 Оз ЧЗ 04 " где Чс =(зе'""0) ' рз = (зс, хи 0.5) Оз = (зе'* х = 6.6) ... По вычислению времянного автомата можно тркжв пЖтроню допурзнмое "временное слово" автомата — последовательность выполненных аиюматом действий и моментм реального времени, в "шнорых жн действия вмиошшлись: (ге,ое)(г$ о!)(гз,оз).. Такая послсяовательносш интерпретируется следующим образом: временной автомат А после запуска ш его начального состояния в момент времени ге молит выполнить действие ас, потом в момент врвмени г, выполнить действие а,, затем в момент времени гз вьиюлншь действие аз и т.
д. Например, по указанному выше иычисленшо о автомата А, может быль построено "временное свжо" (6.6, а)(7.3, а)(7.5, Ь) .... Состояние (Ьзс; г) достижимо во времанном автомате А, если существует вычисление графа лерехсаов А, начинакилееся в состоянии (гесс, ге) и заканчивающееся в состоянии (Ыс;т). Например, в автомате А~ достюкимо состояние (зз, х= 0.7), поскольку существует вычисление, начинающееся в начальном состоянии (зе, х=О) автомата А| н заканчивающееся в состоянии (зз, «= 0.7) . Непосредственно по временному аатоыату о достнхшмости состояний судить трудно. Таким обраюм, система переходов Т(А) представляет реальное поведение временнбго автомата А, т.
е. все его возможные вычисления. Поскольку часы мшуг принимать бесконечно много гконгинуум) Главе эг значений, система переходов любого временного автомата бесконечщь а сам временной автомат — лишь удобная конечнав модель дяя задания поведения систем реального времени. Существует важный результат относительно семантики нвраллельной жэмпозиции временных автоматов: ТЕОРЕМА 12.1 Графы переходов Т(А) !1Т(В) и Т(4!! З) щоморфны. Смысл этой норемы в том, что вычисления совместно функционирующих взаимодействующих систем реального времени пшено получить как асаф переходов параллельной композиции моделей этих систем — временных автоматов.
12.4. Нереалистичные поведения временного автомата Для того чтобы вычисления графа переходов временного автомага огрмкали реальное поведение системы, онн должны удовлетворять некоторым ограничениям, свезенным со свойствами реального времени. В частности, для любых состояний з, з', з' и неотрищпсяьных чисел Ы,Н'ей~ вычисления графа переходов временного автомата должны удовлетворять следующим требованиям: 1. з-И-+з'л з-гг-ьз" ~ з'из' !детерминизм времени) 2.
з-0-ьз (нулещя эаэшржвл); 3. з-И-ьз' л з'-Н'-ез" ~з-г)+И'-ьз" (влднтмвиощь времени); 4. з-з)ьг)'-ьз' =>(Зз"):з-г1-ьз" л з"-гр-ез' (непрерывнастьвремгии) Но дике при выпоянеини этих требований не все вычисления, допустимые в еоотвеюэвин с описанием временного автомата, являются реалистичными. Рассмотрим юг. Кенвергвнтвые и днвергевтиые иычишыиии. Во-первых, рассмотрим следующую пеночку переходов по задержке времени в автомащ А,, представ. ленном на рис. 12.1; (з~",.т 03)-0,1-+(зб я=031)-001-ь(зб я=0311)-0001-+ (зб я=03!11)-е з она г ся пг ние з при: чисж бескг Подо ззргз нятщ возрг чисж Форл )н При; Взют автол Вычп кото) прон Таки по д у ввв (я (я (л Это г же рг добн~ выла зрели В мо мыс ~ вател вычи ле мь ыа <г в сам мнив <х ав- жали рани< лю.
ыния ицим зннй ений <анну <ые в ыми. < спев<ив- Эту цепочку с уменьшением шага по времени можно продолншть бесмнючно: она представляет вычисление, которве синтаксически возможно, Оио строке ся по правилам дробления задержан на произвольно малые части. Вычисление это проходит бесконечное число состояний и шагов по времени, но время лри этом остается меньше некоторой границы. Нереалистичность таких вычислений состоит в том, что они не мшуг выпслниться: здесь время делится бесконечно, фактически, останавливаясь на этих бесконечных вычислениях. Подобные бесконечные вычисления с остановкой времени называются "колверггнтными", Конвергентные вычисления противоречат интуитивному понятию времени: при бесконечном числе временных шагов время в природе возрастает неограниченно (время не делится бесконечноцй Бесконечные вычисления, в которых время растет бесконечно.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
