2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 82
Текст из файла (страница 82)
Во многих случаях для иас важиы только переходы с учетом иитермша времеии, связанного с переходом, с точиостью до целых, что достаточно и для проверки свойств реаяьиого времени, вырикеииых любым миожеспюм ограничений, коистаиты в которых — целые числа. Если временной автомат с одними локальиыми часами имеет несколько локвпий, то число сасгояиий соответствующего графа регионов макет иметь ло (2С„т 2)ь ! Хос ! состояний, На рис. 12 1! еще ряз приведен временной автомат А„различакиций одинарный и двойной щелчок мыши, и его граф региоиов Й(А!), имеющий 1О состоаиий. Статическим анализом графа регионов можно проверить огсугствие во времеииом автомате вычислеиий Зеиоиа. На графе регионов мошко таске проверить, доспокимы ли состояния с остановкой времеии.
чае с б=[ буде репи проб~ Таки~ иес!к иым 12.8, Временные регионы ДЛЯ НЕььКОЛЬКИХ ЛОКЕЛЬНЫХ ЧЕСОВ Век!с эквив иых а При иескольких локальиых часах во временном автомате опрсделеиие времеииых регионов иссколько усложияетса. Например, два состояиия, г! =(!ос;х 1.1,у=0.4) и зз (!ос;х=!.4,у=0.3), ие будут зквивалеитиы отиосительио всех возмсжиых ограничений иа часы, поскольку при возрастаиии времени в состояиии з, всегда сохраиястся соотиошеиие бг(к) < А (у), а в состояиии гз это соопюшевие будет обратным.
Отиошеиие дробных частей пары локальиых часов определяет порядок достижеиия целых значений (и, следовашлыю, следующего региоиа) различиыми часами, а от этого порядка может зависеть возмвкиое дальиейшее поведение временного автомата. Еслм сисюма реяльиого времеии иаходится в состояиии г, =(!ос; к=1.1,у=04), то через 06 едиииц времени оиа переплет в состояиие г,'=(1ос;т 1.Т,у=1), а из состояиия зз=(1сс;х=1.4,у=03) через Обединиц времеви оиа перейдет в состояние зз'=(!ос;х=2,у=09) (если иивариапг локации !ос оспмтся истиииым). Ииыми словами, в первом слу- ВСС зях ~мн леий.
иы очни, Пс- ио- у), нсшй ого яо- тии лу- чае при сстесиениом течении времени слелуюшим регионом системы будет т! =[к=!.7,у=1]=(1 <к<2, у=1), а во втором случае следующим регионом будет гт =[я=2,у=0,9]=[я=2. 1<у<2) . Позгому определение временных регионов при нескольких часах долмно включать н сохранение отношения дробных частей значений всех пар часов. Таким образом, определение отношения репюнаяьной эквивалентности для нескольких локальных часов дапкно быль уточнено по сравнению с подобным определением для одних часов.
Ф Оп!ТеденВПНВ 12.7 (раапотганьнаи аканаютаншнесщь бия нвслолыих лшшльньа часов) Две интерпретации «и «' конечного множества локальных часов Х иаходатся в отношении региональной эквивалентности и тогда и только тогда, когда: ° для Всех часоВ х е Х: «(х] > С„л «'(х) > С, в обеих иитерпрсшцнях значения всех часов превышмот свой потолок, или ° дяя Всех пар часов (Пх, «е Х), если они нс преВышают свой пото лок [«(я), «'Тх)ьс„) н [«(у),«'(у)псу),тот [«(х)]=[«'(х)]л(ф((«(х))=0 и уг((«(х5)=0) все они имекзт совпадающие в обеих интерпретациях целые значения; и [,й'(«(х))хи(«(у))и,р(«тх)) х)ь(«(у))) двв кало!ой пэры часов отношения меяшу нх дробными часшми в обеих интерпретвьнзх совпалают. Векторы показаний часов.
определяемые этими правилами, образуют юмссы эквивааентности (временные регионы) на мншксстве наборов иеотрнпательных вещественных чисел, характеризуемые слелующнмн опюшаниями: (2 для кислых лошшьиых часов х е Х: ° всеми значениями нелых О, 1, ..., С,; ° всеми открьпымн интервашмн меящу соседними тшлыми [лг, !«'+!) для У<С„; ° етервалом (С„ф Гла ещ (2 для кяящой пари локальиьш часов х, уа Х, значениа которых находятся аиишрзаяах (ш<х<ш+!) и (и<у<и+1): ° отношениями равенства дробных частей нх значений уг(х) и Л(у) нли их отношения < нли >.
Кшкдый репюн определяется набором ограничений на чван (с!оск сопя<пипи). Число временных регионов опредшшсгся следующим саатноше- )Х~(Р П„„(2С, +2). Дейспнпельно, дяя часов х с потолком С, существует 2С„+2 возможных иигервалов, и лля юпкдых часов существует независимая возможность выбора мнтервала.
Кроме того, для всех часов с ненулевыми дробными часами шггеряалы агличвются друг от друга также упоркаоченностью этих дробных часшй. Верхней границей числа таких перестановок валяется величина !Х1! . Третий компонент оценки ограничивает сверху число тех часов, дробные части которых совпадшот. Прмывр 12Л Структура регионов лля пары часов х, у с максимальными значениями С, = 2, С„= ! представлена на рнс. 12.12. Эта струк<ура содержит 28 регионов. Пусть граф регионов для временного автомата с двумя локвльнымн чвсамн х н у (рис.!2.12) находится в состоянии <(ос;(ы<]>. На рисунке интерпретация чшхж ы, находится в регионе (ы<], который хврвкгернзуется следующими временными ограничениями: (1 < х < 2) л (О < у < 1) д (дь(х) < Яу) ) шя<, чта та лм: (! < т < 2) «(О < у < 1) «(х — у < 1 ) .
Этот репюн абьеднияет шперпрепщии часов (х 1.25, у = 0.5б), (х 1.),у=0.72),(х=1.1,у 0.4) ит.п. рассмотрим примеры возможных переходов для этого графа репюнов: (3 переход по действию. Если выполнение перехолв ((ос;(ы<]) -а-+ (1 .[ ]) р д пр м У=О ( Ч' шнм нз ы, на рис, 12.12), то каждая интерпрепшия чшюв нз этого региона п< н< с< з< с ((ы] -.
(2 (< л< нли з!ос(г оше- шмн ~ рн ч! О гных ыбосами шых [х[!. )ные попадает в один н тот же регион [й '[, который определжтся ограннченнамн: (! <к<2)л(у=О). Прнсванванне х-у значений локальных часов на переходе временного автомата нз любой ннтерпрегацнн часов в ятом репюне (штриховая стрелка влево) прмведст к переходу в состояние с той же локацней !ос, но с интерпретацией часов в регионе г*=(О<я=у<!); 0 прн продолженнн хода часов нз ннтерпрепщнн г, все нмгерпрепшдн я!+а для любого неотрицательного И располапжпся на сшюшной стрелке, идущей под 45', т, Рнс.
12.12. Структура регионов лля двух часов .т, у с пстолкамн 2 н ! ЛЕММА И.1 (аюйстаа регненев) Для любых двух ннтерпрстацмй часов г, н, находящихся е одном репнню [[я[=[я!), выполняются следующиесвойства: (2 (тЯвКш)(М'вК~)([г+г([=[я+И[) если добавлением любой неотрицательной велнчнны г( к показанням г локальных часов мм шипдаем в какой-ннбудь репюн г.
то сушвствуег Глава !2 Мно по е! по г) авто! (г;» (х;х такая величина /Г, что добавлением И' к показаниям локвльиых часов и мы попадем В тат же регион г; (2 ] т(х:=0)1=] и(»-.-0)1 прн сбросе значений одних и тех же часов из интерпретаций г, и мы попадем в один и тот же репюн; (2 (т/лег()(]э+и]=]иьи]) добавление натурального л к показаниям.всех часов переводит эти две интерпретации в один н тат же регион; (2 (г/7 !)(]+=у [к]1=7) интерпретации часов г, и эквивалентны относительно любого свойств/Ь выраженного с помощью ограничений на лоюиьные часы. Рнс.
12.12 иллюстрирует эту лемму. Действительно, пусть т!--(»=13,у 04), тз =(х=!.1,у=072). В аоатветствин с определением 12.7, этн две интерпретации часов эквивале!пны. Переход автомата по временной задержке кж! из аостолння (1о«, г! ), так и из состояния ()аа; тэ) приведет в один и тат же следующий регион (1 < х < 2, у = 1), Если интерпретации часов находатся в разных регионах (например, т, и тэ на рис. 12.12), то следукнцие регионы, в которые будет выполнен переход по временной задержке из соопмтствукицих состояний, будут разные. Пример 12.0 Временной автомат Аэ а двумя таймерами (локальными чааамн) х, у и ыю граф регионов представлены на рис.
12.13. Любвя последовательность соа/павий и переходов графа регионов /т(Аэ) представляет вычисления временнога автомата А!. Одна из возможных паследовательносгей изменения часов х н у в зюм автомата прн следующем вычислении графа регионов =01 т "+02 т +03 т ь/)х о Фсэ т-+0!3 т +см т + Ч!а т +Фп с +0!э т +0)е т +сп с-+Ум -т-+0!с -т-+-. показана на рис. 12.14.
Каждый переход т (звдеряжа по времени) переводит автомат гт(Аэ) в соседний регюн по направлению изменения обоих локаль- ных часов. / / / / / / ! ! ! Ъ !ей;В!н О,у: О а г ! ! ! ! ! ! ! ! ! ! ! ! Ъ и б рнс. 12.13. а1 Временной автомат А! с двумя таймер!ми! б1 его граф репюнов Многие свойства системы переходов временного автомата можно проверить по его графу регионов, который имеет конечное число состояний.
Например, по графу регионов решаетая проблема достнжнмости состояний временного автомата: состояние (1сс; т) доспскимо во временном автомате А тогда н только тогда, когда регион ~(!ос; г)] доспеким в графе регионов й(А) этого автомата. В частности, нз рнс,12.13 можно заключить, что состояние (жх=!,у=1) автомата Аз недосппкнмо из его начаиьного сосгояння (я;х О,у=О).
Славе Щ В ка врем имен врем где с мадис свойс форн гово1 водя! Рис. 12.14. Последовательность изменений поюэаиий часов я а у на одном нэ внчнсленнй аатомюа Ал Рассл 12.9. Анализ временных автоматов." логика СТ1 Прлн Пров ЕРА котог меча Форе нов 1 инй, гл г'э .г"э ф: Поскс Верификацию временного автомата А при спецнфюацни его свойств формулами логики СТЬ можно свести к анализу наполненна этих формул для лрафа регионов Й(А) . Этот граф строится как раэ таким образом, чтобы для любых двух наборов значений часов г и и, которые принадлеяат одному временному региону, два состояния, (1ос;[т)) и (1ос;(и)), графа регионов удовлетворяли одним и тем же формулам темпоральной логики. Если Ф— формула СП„то: Я = (и )) ю ((1ос; Ц 1= Ф и (1сс; (и)) Н Ф) .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
