2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 88
Текст из файла (страница 88)
Поэтому асс интерпретации часок х и у е локации т до аозможното еыхода нз нее описыааются зоной Уа =(1лх)л(2эук7)л(-2кх-укз). Далее, асс аозможные показания пары локальнык часоа, прн которых козьнякен дискретный переход по дейстаию а, определяет зона 27 (3<х)л(2ьуп7)л(-2 ах-уьЗ). Последняя зоне 24 =(3<хцр)л л(у=б) яеляется проекцией зоны Уз на ось х, поскольку часы у сбрасыааются на этом переходе. Таким образом. есе аозможные аычнсления, сказанные с этим переходом, предстаяляются следующей цепочкой снмаольных состояний и переходов; (м;2т)-т-+(жт Уз)-а-ь(~42т) Очеандно, что зоны дают зцачнтелыю более компекпюе предсталлеине аычислений, чем регионы. йгб Операции над зонами Часто встречмощиеся задачи при верификации временнмх автоматов — зго проверка лоспскимостн некоторого состоянна и построение графа зои (чалю зта операция выполняется "на лету").
Обе задачи сводятся к последовательности построений очередного символьного состоания автомата по его текущему состоянию. Аналогично тому, что символьным состоянием графа регионов временного автомата являеюя пара: ((ос;[г]], где ]т] — чюовой регион, сосюянием графа зон являстса пнж: (1ос;2], которы состоит ю локации 1сс временного автомата и зоны. Так же, как и следующие репюнм в графе регионов временного автомата, следующие зоям в его графе зон определяются однозначно. Как видно нз примера 12.20, переход к очередвгй зоне требует выполнения следующих операций над зонами: (2 пересечение текущей юны с ннвариантом локации и с защитой перекода; П приращение времени: П сброс некоторых локальных часов в зоне. Рассмотрим эти операции последовательно.
0врвсвчение зоны С СГгЗВНИЧВНИНМИ НВ НСЦВЗЕНИН ЧВССВ Если 2 — юна, а З вЂ” ограничение на показания часов, то операщы пересе. чсиия вмрвкается просто квк конъюнкция: Ул й, посколыгу н У, н й вырикены логическими формуламн нак значениями локальных часов. Прирви(ение времени Операция "прирмцение вРемени" для текущей зонм г часпз нюымгсгся ощ...
ражий посгроання сняьлеелего лссябсяоегм (йпопйеаг Розг сонбйюп) О обозначасюя о)'(У) или 2 . Операция БР для зоны 2 опрпкелжт все мнот жество значений локальных часов при пронзволыюм течении времени, если текущие значения часов принавясжат зоне 2. У =]г+Ф~ггца,твх] В алгоритмах обратного поиска (Ьаакмагб юасйаЫ1йу) по графу зон нспользусюя операция построения слабейиего лрсдуслсеия (%саксы Ргссопййюп). Этв операция таске Лает единственную зону. Она обозначается йгР(2) или 2 .
Операция )РР дпя зоны 2 определяет то множество значений ло- Глвяв гз каляных часов, которые при произвольном тсченни времена юнуг сить значениями, которые прниадлемат зоне 2, 2 =(т!т+»1е2 ллянекоторого»1выээ) Сброс локальных часов к опрвделяеюя просто: (эк 0)2=(т(хюб)!те2) Окюывается, что мномсство зон замкнуто относительно всех операций над зонамн, т. е. в результате любой указанной выше операции нвд зонамн снова получим зону. Рис Прммвр 12.21 Пв рис.!2.23 представлен временной автомат с тремя состояниями.
Все аоз- мшкные вычисления этого мпомата могут бмть описаны следующими пере. хспвмй графа эон: (т; 2в) — т — ь (вг 2» ) - а -+ (щ 2з) — т — ь (в' 2э ) — Ь -ь (г; 2» ) - т -ь (щ2~)-с-ь(ж2с) ДООтижимппть Зц Один цззг Построение слелующего состояния лисс(1сс! 2) графа зон лля текущего состояния (1ас; 2) определяется однозначно следующими операциями. Пусть 2 удовлетворяет инаарнанту, 2 = 2 г» лгг(1сс) . Переход по задермкм (1сс;2)-т-ь(1сс!2'), где 2' 2 г»йш(1ос) Переход подействию а на переходе е (1гк,й,»ь(л),1сс)пй;тлл йг — 'ющнщ перехода: (1ос;2)-а-+(1ос!2), 2' (лщй)(2лл)!У2',"»1Ь1гс и 2'»» 1лт(1ос) = 2'. По построенному графу зон проблема достюкнмоети реипеюя очень просто: символьное состояние (1ос'! 2') досгмпнмо ао временном автомате, если в »рафе зон этого автомата найдется такое символьное состояние (1ос'! 2'), »по 2'~ 2" и (1ссс! 2,)-ь '(1сс! 2').
Ша 1 шешг' ,ршяе'ч Сь лег час лве Прпывр 12.)г2 Рис.!2.24 представляет временной автомат, различающий одинарный и двойной щелчок мыши. Если второй щелчок мыши приходит до истечения г( единиц времени (например, миллисекунд), автомат выдает операционной системе снгнве 'а'. Если между последовательными ншкатиями на кнопку мыши прошло более (т единиц времени, автомат выдает сигнал 'Ь'. При Ь(м20 в графе регионов зтого автомата более сотни состояний. Граф зон зтого автомата (рис. 12.24, 6) при любом Ь( содержит только 10 состояний е 2(А»: г хо хво оях*н ' »И Рнг.
12Д4. Временной нпомвг, разянчмшций швшарный н двойной щелчок ммиш, н его граф зон Пример 12.23 Вернемся к анализу вершина протоколе Фишера (см. пример12.!7). На рнс. 12.15, е представлен фрагмент графа регионов, показьшшощий, чзо про- одн лен тив м(ж ло( аер токол Фишера корректен: при любом развитии событий примасы не могут одновременно находиться в своих критических областях.
Однако предсшзь ленные на рис. 12.15, а параялельно протекающие процессы слишком примитивны: они используют в ограничениях локальных часов минимально возмошное целое значение! . Если бм в защитах переходов этих процессов спело бы более реальное число, например 10, грвф регионов, по которому можно верифицировать этот протокол, содеривл бы много сотен состояний. Рр Ряс. ! 2.25.
Протокол Фишера и фрагмент его графа зои С использованием временных эон такой шшшп мошег быть выполнен очень лшзю. Рис. 1225, а показывает зти параллельные процсссм с огранмченнями часов в лг единиц времени (например, мнллнсекунд), рнс. 12.25, б предспшласт начальнмй фрагмент графа зон для этого протокола.
Рнс. 12.26 покшы- вант последошпельносп зон, в которых но~уз находиться ннтерпрсшцни локальных часов процессов Р, и Рд при укаэаннмх на рис. 12.25, б траекториях графа эон этого протокшш. Фрагмент графа зон показывает, что одновременное нахожление в критической секции обоих процессов невозможен. При любом Дг граф зон для протокола Фишера содержит только 17 состояний. При гГ 1О граф зон имеет на три порядка меньше символьных состояний, чем граф регионов этого протокола. Например, только одна зона 2з =(0<У-хд7Гг)л(ОЯУ<1!г) пРн У=10 обьедннаетвссбе 500 Регшшов.
Струйтуры данных для представления временных зон Рассмотрим формальное определение зон и то, как зоны могут быть представлены в памяти компьютера. Простейшие временные зоны определяются наборами ограничений, которьш встречаются во временном авгомате. Прн построении графа зон с юнами выполияюэся операции, отраяшюшие изменения показаний часов прн нахождении автомата в локации и при переходах макду локацнями. Оказыяаеюя, что любые псстроениые таким образом зоны могут быль представлены еднимм обриюм, одной структурой данных.
Временная эона 2 — зто ограничение на показания часов в форме коиьюнкцин элементарных ограничений, задакнцаяся грамматикой: гь,— !,—,- !Хлг где х, хг — локальные часы временного ангомата, с — целое число, х;. я иХ, отношение, а '- ' — все аозмолшые нерввенснза: — и(«,я,д,и). Пример эоны для двух локальных часов, «~ и хэ.' 2! (~-э~д!)л(0<х,<1)л(ОяхЗ<3). На рис. 12.27 эона 2! вмлелена сплошными прямыми, шютаетошующнми этим неравенствам.
Дла удобного единообразного задания зон вводятся специальные часы яе, значения которых всегда равны О. тогда, если временной автомат содерлпп Нз ри пр зо~ яс пс йб сп ви Оя не! ме Оп вс до! виз и локальных часов Х (х!,хз,...х„), 'то любав зона может быль задана коньюнкцней однотипных неравенств: Лсямз „х, -хз -сг Такой набор неравенств можно свести толью к отношениям < или и.
Например, зона 21 может быть представлена следующим набором однотипных неравенств: У! =(х, - хз К -1) л(хе — х, < О) л(х, -хе < 1) н(хе - хз < О) л (х, — «с < 3) я,о ял! Рис. 12лт. Зона с!, опрелеяаемая набором границ й!атрица разностей границ (О!тгегепсе Воипд й!а!г!х, 0Вйб) Любую зону, щаанную коныонкцией однотипных неравенств. можно задать слелующей мвтрицей зз(2) (ыг, < ы), где згг = х, —.т . такая матрица лля зоны с! имеет вид: хз оц где хз ны од~ ну 12 га Определенные ранее операции над зонами могут быть легко реализованы в случае, если зоны представлены матрицами разностей границ. После каж- дой операции необходимо выполнить приведение матрицы к каноническому виду.
Сущеатвует простой алгоритм, выполняющий зту операцию. ля На диагонали матрицы 0(У) всегда стоят пары (О, д). Первая колонка матрицы представляет верхние границы часов в зоне. Например, г)зд =(3, <) в этой матрице, поскольку хз-хс <3 в зоне 21. Верхняя строка матрицы представляет нижние грвницм часов. Если какая-либо граница в задании зоны не определена (в нашей матрице это г7з ~ ), она счнтветсв бесконечной, и в соответствующем месте ьштрицы ставится пара (ез, <) . Подобная матрица называется Матрнлей рпшостей гранил (О)йегепсе Вопиб Манях, РВМ).
Фактически, ОВМ вЂ” это структура данных, символьное представление множества значений локальных часов временного автомата, эквивалентных относительно свойств, проверяемых при верификации. Оквзывавюя, что одна и та же эона может быть задана разнымн наборамн неравенств и, следовательно, разными матрицами.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
