2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 75
Текст из файла (страница 75)
11 Прин ПРИМВ инй дз ... глвев ы Миожества О~, У" и ~5 опредеюпотса по вытюлиеиию в иик формул 0 и Р: Оы =(з ), Ум (зр) и без 81(евсин ') (зс.зизз). Сисгема уравнений: хе = 0.5 х1 + 0.2 лз + ОЗ хе х3 0.4 хз + 0.2 х4 + 0 В хе лз=1 х3 = 1.0 хз 34 0 Решеиие системм — вектор вероятиостей выполпеиив формулы дБр в втой структуре.
имеет вид: (хв =0.5, х, 0.6, хз =1, лз 1, х4 =0). Векюр Иаз(изс ь (0%Ур)) = (О, 1, 1, 1, 0) показывает, по формула состояний сесе (сцр) удОвлегигфяегтл В ООстсяиихх 31 33 и 83 ° Мы пшзучили те же результкп 3 что и в примере 11.б, одиако здесь зти результаты получены при выполнении описанного выше алгоритма шойе! сйесапй для вероятиостиых структур. Слвквкть алгоритма верификации формул логики РС'П. лииейиа по чисху подформул проверяемой формулы и полииомивльиа отиосительио числа состовиий вероятиостиой структуры. 11.3. Проверка свойств, зависящих от дискретного вреййени и вероятностного выбора Вероятиостиая структура, используемая в качестве модели лля имгерпретации формул вероятиостиой темпоравьиой логики РСП., может быль использовала дла проведения совместного анализа ие только повелеических и вероятиостиых, ио также и времеииых свойств систем, если юпкдый переход системы свюываст состояния, отстоящие в дискретном времени иа один шаг.
Тогда временной авалю состоит в подсчеге количества шагов между событиями и можит быть использовал для таких сиихроииых систем. Расширим возможиые формулы пути вероятностной темпорвльиой логики РСП. еше одной конструкцией: йцжй! 01~Р,О433(У, (а), где -и где л ° т0130м мом пу дет вы МОДЕЛ3 милли< Путь 1 шее 43 Совме мы дз утверл П "Пс бол ьг "Ве без Для п1 иия те ПОВЕД4 теме, выпол гов ал мула ( Для и магри шине буду як 44, ЗЛ 4 Пр) аты, енин иску в со- Зста- юль- юро- сис- обы«рим еше где -и !ч,к,=,ц,>), а формула а — формула пупс оыж Х9! 9!Прз ~ 9!П Путь удоаастворяст формуле Рзьр, если иа нем состояние, удовлпшоргво.
шее 9, может быль достигнуто не более чем и л шаде. Совместный анализ логических, вероятностных н временных свойств сношмы даст возможность строго докшыяать корректность, например. тшшк угверлшений о поведении систем: !5 "После любого отказа, с вероятностью 0,9999, анрепа воссгаиовитса не более чеы через 5 временных шагов". «У "Вероятность того, что сигнал геаф будет получен в течение следунпцнх 6 единиц времени, больше 50 %." Для проведения такого аналнш достаточно определить вероятность выполнения темпоральной формулы аЩ3 на ограниченной ло числу шагов Рюирпи поведениа структуры. Об«плачам Уз!з,иПР,Т) вероятность того, что.в аютеме, нзхшбпцейся в состоянии з, темпоральшш формула луги аВб будет выполнена в рамках временного интервала Т, т.
е. не более чем через Т шагов влгорипаа будет доспаиуто состояние, в котором удовлетворяется фор. мула р по пути, во всех состояниях которого удовлетворяется формула а . Для подсчеш Уч(з,иВ5,Т) по вероятностной структуре с вероятноспвцй ьатрицей Р шютроим дерево — развертку этой структуры с корнем в шц». шине з с длиной пути, не более предельного ннтерваза Т.
Вселжтьядереш1 будут помечены 0 нли ! а соатэектвии с правилом: зк(з, о«йг, шзя с<о еа«и о агав ая реиш заев з // ограничение пс панне «раект«С«м // гтзесззпв«м р зивмяяе«.с» з з где и — натУРвльное число. ФоРмУла пУги 9«!!«ьрз с огРаниченным опеРв' тором г/пб! упюржлвст, что формула 9« будет выполнена на рзссматрнвасмом луги не более чем через и шагов, а до этого во всех состояниях пути бу.- лет выполняться формула 9,.
В реальной системе кшкдый шаг выполнения модели может предсшвлять любой временной интервал; час, секунду илн миллисекунду. Для ограниченного оператора !/пб! имеем: Рз"9 = В ие!!я" р. КОЛИЧ дихп Яйс Глава ы аасто ии Р мере МНОЖ листь носта Вычи тс сэч писан гегэзэ что в МЕНИ1 со ьы О1 52 См оэ а 12 12 14 ° эвв вс ааьге1 сьев о l/ гтверваенне е вв мвкяявмттл в е вэее В,ыр(е, в'эх ваге', СЮР, с-И Подсчет Ув(в,аВ!3,1) по построеиной развертке прост — зто сумма вероят- ностей Всех путей нз ВВчвяьногО состояния Втермннаээьныс сссэ'Сания, пома чеипые 1.
Пример 11.9 Вычислим ВСРепность того, что ие баке чем за тедээ шага веРоатиостиал структура М, рнс. 11.1, а, из начального состояния .Яе макет достичь состояния, в котором выполняется р по пути, во веех состоапиях которого выполняется ! . Иными словами, подсчитаем Ус(гс, СПр, 3) для структуры М, .
Для подсчета втой вероятности построим развертку структуры М~ из начального соспэяпия с длиной путей ие более 3. Зто дерево представлено нв рие. 11.6. !Оскдый путь моямт оборватьсв раиыие в состояниях, которым прпписывасшя коикрспкэе значение вероятности выполиешы формулы в атом состоаиии: либоб, либо1. Значение вероятиости 1 приписывается состояниям мпонества б (в нашем примере помеченным втомариым пре- Рас. ! 14. Рвысрсш асрсятлсстяой сэрувтурм со мывм врмыэш Вмссэ форм, с с=! прави ос 05 ос 06 07 ш св оз 15 11 ев ш !юяг- о вы- ю на орым мулы астся ! пре 00 Ввз«п 0> О в«пи«ление вероятиоотеа л«я 02 яеи еьэ ваэ «Ь оз ья реыэ> тьа я>4«, сир, о> 4- з 04 ° Зае «Ч>«, ппР, 0> 4 0> 05 оэ 06 //' «нчиолание внооятн«стаи И«я от я с:- > то т Е оз яее взз вез ао 05 зя р ь<в> и эт>я, впр, и г- з >о зв пм№н зз ЗЗ>В, «аР, С> 4- ОГ // р выполняется в в // р ие «««Юлняется в в воен с«0 // Р внполияется в в // если в не «нполняатоя в в, то а! 0 зз зг паыв> тане >з Я14В> Гай.
С> У и Эяв."З'>ИЯН" ЕПР«С-И« 14 - емз дикатом р ). В примере зто состояние яз. Значение вероятное>п О приписывается состояниям множества 8~ (т. е. таким. которые не помечены ни р, ни е, н таким, из которых недостижимы соспшння, помеченные р ). В примере зто состояние «4. Это же значение б приписывается тем состояниям мнекесшв 8, которые отсювт ровно нв г шагов от корня. В примере это листья (зс, г>, зз! . Таким образом, все листья этого дерева помечены вершг>- нсстими либо О, либо ~. Вычисление искомойч>ер>мтносги по построенному дереву состоит в подсчете суммы вероятностей тех путей, которые эаканчияаютса вершиной с приписанным ей значением вероятшктн 1. На рис.! 1.6 таких путей два: зсз,зз н ч>аз«э.
СУмма вероапиютпй этих путей ОА. Следовательно, веровтносгь того, что в состоянии зе выпслняспм формула пути ОНР не более чем эа три временных шага, равна ОД. Вместо построения дерева удобно строить таблнцу веровтшктей выполнения формулы Уе(«,пщ>,г) для всех «прн Различных значениях г, начиная с г = О. Дпя этого используем алгоритм, вмтекающий нз вышеприведенного правила: .;,- !змее Гг 15 се 16 еп 17 ееа стоян нии .
мере гих о При выполнении этого алгоритма удобно строить таблицу для аспг состояний вероятностной сгруатурм и лля всех значений г от 0 до Т . 1здео Пример 11И О На рис. 11.7 приведена вероятностная структура простого протокола передачи сообщений. Из ивницкого состояния впг протокол Оереходит в состояние лу, находясь в котором он пьпается передать сообщение. С вероятностью 0.2 канав оказывается закатим, с вероятностью 0.7 канал свободен и сообщение успешно передвезся, с вероятностью 0.1 переданное в канал со.
общение искмкзстся, н передача этого сообщения поаторяегсв. Будем считать. что квмдмй шаг алгоритма требует 1 едйницм времени. Иски 11И вы~ Рве. П.7. Мояеяь просюго вротокшм Проверим, вмпаливетоя ли для этого протокола следующее ушерящение: "Сообщение будет успешно доставлено в течение не более чем б единиц времени с вероятнастью.
большей 0.95". Иными словами, проверим, вмшиняегся лн длв ного протокола (т. е. в его начальном состоянии ШП ) формула РСТЬ: '$ам(р Емнт). Дяя этого подсчитаем вероятность Уе(ощ,лиеП®васс.б) по алгоритму 11.1. Построим таблицу подсчета Уе(г, с иеУфяисс, г) для всех состоянийструкгурм рис.11.6 пасек г от г=О до г=б. Прн г = 0 значение вероятности 1 спшт только в состоянии звсс, в оствльнмх соспмннях вероятность того. что за 0 шагов из ннк мошно достичь со- Как ь что п рм м! сказа РСТ! Эквн~ лениг ка РС носта Напр~ Рог!и ~ий ш!ие тев мпд.пе шюватиняияжши р с а р л з ег' гн !н. Искомая вероятность при г=б оказалась равной 0,971. Следовательно, утверждение глй ! Р е е,( Рш г(рпкс ) для этого протокола истинно.
11.4. Примеры свойств, выражаемых в РС'П. Как мы видели выше, формулы логики РСП. отличаются от формул СП. тем, что по южшбй формуле пути Е в квхшом состоянии вероятностной струхтуры можно вычислить вероятность того, гго зта формула мяполнится. Можно сказать, что логика РСП.
— зто логика СТ(. плюс вероятность: РСТЬ = СТЬ + РгоЬаЬг7ау Эквивалентность формул РСТ). устанавливается по ппюшению к нх выполнению на вероятностных структурах. В частности, две формулы Ф и Ч' языка РСП. будут эквивалентны (записывается Ф и Ч', если дяя любой вероят постной струкгуры М и любого се состояния з спршедливо: М,г!=ФиМ,з1=Ф. иц го Например, формула пути а выполняется на всех возможных вычислениях Рагдг(М) с яеролпнктью самое меньшее р тогда и только тогда, когда стояния хасс, равна О.
При всех значениях г искомая вероятность в соснжннн жкт также равна ! (строка 09 алгоритма 11.1). Поскольку в нашем примере а =лве, то при всех значениях г > 0 искомая вероятность ао всех других иктоянивх г определяется по формуле (строка 13 алгоритма 11.1): йге(з,пие П®гнсс, с) Е,хэр(з,з ) к Уе(з',ене () ®зксс, г -1) (здесь Р(г,г') — элемент вероятноспюй матрицы, т. е, вероятность перекопа из сосговння г в з'). Последовательный подсчет этих вероятностей дшт табл. 11.1. глвев ы формула пути а вмполнвется нв этих вычислениях с вероятностью самое большее 1- р. Отошла можно определить: Ур(а)жУа р( а) Ух (а)еУн р( а) У,р(а)жф, р( а) .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
