2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 76
Текст из файла (страница 76)
Убр(а)-У.. (- ) Рассмотрим теперь формулу Пбр. Поскольку Пбр = - Р ~р, то У (Сбр) У ( Р р) У„(Р р). Даме, У (Пр) ~, (Р р), Уз Хб ут )(П"р) еР(,, )(Р у). рз Для н зуем б Хз Дюз~ .Уз .гз гз=зрз Пример 11.11 Проанализируем свойство "мягкого деллайна" для упрощенной версии протокола аяьтернирующего бнгк Свойство "мягкого делдвйна" устаиавяиваст вероятность наступления события во временных рамках. Арипектура протокола (рис. 11Уч а) содержит три блока: передатчик, приемник и ненадежный канал. В этой версии подтверждение оса посылается по нвдежному каналу и никогда не терастся и не искшкштсж Модель переходов пропжола (рис. 11.8, 01 является вероятностной структурой: обнаружшаемые покри в канале происходят с вероятиостью 20%.
Проверим, будет ли для этого протокола выполшпъсл свойспю: Аб-'((ибо ~ бзелУ (изб) Ер (®зе ~ (кзсзр Жзб) То есть что не более чем за 5 шагов,по времени с вероятностью не ниже ОУ переданное сообщение будет достаавено. Синтаксический анализ дает следующие подформулы этой формулы: у) =Еле Л Ела елее 15 сивое про- ивест рис, 11д. Архвтекгуре упрюнсююго врогоколв яяьюренругооюю бню 1а) и ею моюль (6) Последовательно помечен состояние модели подформулвми, получим, что: А, Вбс ~~~~~ ~поместив~И г1И51. Ут и Евб ВЫПОЛИЯЕКЯ Ня Миавсетес СОСТОЯНИЙ 15б) . Для нвхснлснбю мисюеотел ссстОяний, ня которых еыполняеюя ~5 „вспоив.
зуем елгорюм! 1.1. Построюнюя табл. 11.2 имеет вид: ирисе по юдов емые г для уб ге Гб ~Р5 57= Уб Теблнив ПД. Ьгнакютес состояния, на нстсрсм вынслняекн УТ тая»ннм 1»л (окоибаеие) г»»аз% г» выполгшется'на м»вхбшсззю шюгоя»гнй 18» з» в», 54) Уг .~б не выполняется ни на одном состоянии. Если в таблицу добавигь еще одни столбец, т. е. увеличить на единицу времени интервал, на коп»ром производятся оценка вероятности доставки сообщения, то зта формула оквжегсв выполнимой во всех состояниях модели.
Л=/»=»Л. 45 У4 Уб =ВРУ» вмполняегся иа миакестве соспмний (з», з», г», 541 выполнвегса на мнакестве состовний (гс1 вмполнлешв на всех состоанилх (зс,зн в», гз, 441 системе усп во выполшг нспояьзояш обласшй. Для верояп качесгвеню вероятност| ния свойсп лиз вероят» свойство б "плохое" са Описанные системах в РК1БМ (Рп те г. Бирм К им»коим! учебных и зователей. деленных в биологи» 11.6. Заключение Вероятностную структуру можно рассматривюь с двух точек зрения.
Вопервых, зто расширение дискретной цепи Маркова введенном пометок в сссциниях — атомарнык предикатов, которые истинны в этих состояниях. Но вершпностшш структура явлются также и расширением структуры Кринке введением вероятностной меры на переходах сгрукгуры.
Марковские цепи широко используются во многик областях, не только в математике и информатике, но и в исследовании операций, биологии, демографии. Добавление возможности анализа логических ушержденмй и учета временных ограничений в Марковских цепях открывает новые горизонты для анализа во всех »тих областях. С другой стороны, введение в структуру Крипке аероятносгиых оценок на переходы также позволяет расширить сферу применения классической верификации, выполнять более тонкий анализ свойств поведения дискретных систем.
Мстодм трааиционной верификации могут лять ответ, выполняетсв лн некоторое свойство в системе с вероюностью 0 или 1. Веров»постный и временной анализ позволжот ответить на вопрос, удовлегворяет ли вероятность выполнения некоторого свойсша в М.6. 3 Попытки 1 ке, в нащх ле 90-х гг. с веров»и< вона (Нап предложм нован на. лекций(й Эта обла~ опьпные поведали~ ральных» ст упомя~ результат теяескош явее 11 мчаяюе! ицу вра- ки сосб- ели. системе установленной (мюкней нли верхней) границе, н будет ли иго свойет.
во выполнаться в заданном интервале дискретного времени. Таким обрюом, использование юроятносчмых струатур дает новое качество в каждой из этих областей. Для верояпкктмых структур может выполняться квк количественный, так н качественный анализ свойств. Количественный анализ позволяет определить вероятности выполнения темпорального свойства илн вероятношь выполне. ния оаойства в рамках щламного числа временных шагов, Качественный анализ вероятностной структуры позволвет проверить, что некоторое "хорошш" свойспю будет выполнено в ней "почти обязательно" или что некоторое "плохое" свойство не случится "почш никогда".
Описанные в этой главе подходы и влгорипаы реализованы в нескольких системах верификации. В частности, можно упомануть систему верификации РКУБМ (РгойаЫ11зг)с БушЬойс Мобе! СЬесйег), разработанную в Универснтетег. Бирмингема, Англия, под руководством Марты Квятковски (Мама Ки[абюмзйв). Зта система верификации распространяется свободно дяя учебных и исследовательских целей. У этой системы несколько тысяч пользовпелей. Система РК[БМ использовалась для анализа ишюжностн распределенных компьютерных систем, проверки криптогрвфическнх протоколов, в биологии, анализе квантовых вычислений.
:иня. Воток в со~ниях. Но я Кринке ~ько в ма- демогра(чета вреюнты лля структуру ~рить сфеий анализ шфикации св ероятпюппь на .войства в 11.6. Замвчання Попытки расширить формальный анализ, основанный на темпорвльиой логике, в направлении анализа количесшенных параметров, были сделаны в начале 90-х гг. прошлого века [47]. Расширение темпоральной логики для работы с вероятностными моделями было предложено в работе Ханссона и Дконссона (Наля Напэюп, Вепбг )опшол) [65).
В этой же работе переходы модели преллшкено использовать как шаги по времени. Материал данной главы основан на этой работе. Пример 11.4 с анализом игры в кости заимствован из лекций [86]. Зта облжть находится в сталин интенсивных исследований. Существуют опытные инструментальные системы дая анализа количесгвеннмх свойств поведения веровтностных систем в рамках различных расширений темпоральных логик. Кроме упомянутой выше системы РК1$М ([182], [89)), следует упомянуть систему ЕТМСС, которая описана в [66]. В [64) нзлояшны результаты исследования надежности ~петены управления космического телескопа Хаббл с помощью системы вернфшащии ЕТМСС. гневе щ 11.7. Задачи к главе 11 Вели являл П велич в) У~07 (чП ') б) Ухаг (тре!УьегХ ")) 11,1.
Для вероятностной структуры примера 11Л подсчипйнн, выполняется ли на ней формула Уст(Ус!Ха)6 тг. 1!.2. Ставка "ТЬе ))слт Ром Вег" при игре в косзн (Крепе) ставне на.вариант развития событий, противоположный тому, что делается при ставке "Тйе Розг Ве~" (пример 11.5). А именно, деньги ставвкя на то, что игрок а первом броске выбросит 2 или 3. При выпадении 12 засчитываегся ничья, ставка возвращается игроку. В случае выпадения 7 или! 1 стажа проигрывает.
Если игра переходит во второй раунд, ставка вмигрывает, если игрок выбрасывает 7 до того, как выпал пункт. Проверьте, какая нз двух ставок, "ТЬе Рагг Вег или "ТЬе Юалу Рпм ВеР, выгоднее игроку. 11Л. Другой вариант ставки "Т)м Юолт Рпгз Вег при игре в кости (Крепе) отличается от того, который описан в задаче 112, следующим. Ничья при первом броске засчитывается при выпадении суммы очков 2, а не 12. Чем от- личаются условия выигрыша в этих двух вариантах7 1!.4.
Для вероятностной структуры примера !1.1 подсчнтайге. выполняется лифориула УяезеП лр. П.б. Для вероатностной структуры примера 11.1 подсчннзйгв; в каком вре- менном инюрмню с выполняегся формула Уп л еП~Р. 11.б. Для произвольной вероятностной структуры с заданной разметкой вер- шин атомарными предиквтами проверьте, выполняются ли на ней следукнние формулы: Н.7. Постройте программу, которая по заллнимм вероятностной структу- ре М и темпоральной формуле Ф логики РСП. определяет, выполняется ли формула и на структуре М.
!1В. Существует вариант вычисления вервпности У(апаПб,г) с помощью умножения матриц. Зтот способ вьпмает из алгоритма!1.1. Определите квал( л) Опре,, с) Рога бро- возясли ыааВе~ мпс) при я от- ея ли квалратиую матрицу А с чныюм строк н стоабиов, равным чжну состояний структуры: А(ГПЯД=ГУ Я,абятйЕЛР(!4Е!ЯЕЯГ ЯГаб™аИГ!У'=Гтйал1ЕЯГЕО Определим темке вектор-столбец С: С[я,) !г я, аале гйеи ! ейе 0 Величина вероятности Уа(я„аб!», г) определжтся как !-й элемеиг вектора, являющегося результатом умвпкеиия г-й степени матрицы А ив вектор С.
Постройте матрипу А и аекгор С и подсчипйте с помощью этого метода величину Ра(я„абсг, 4) для задачи 11.!. гл~ Си Смети рантиг ни. Пр вано с раоярт инте!л мах ре реакнг анях г !98! г завуея итона, тр8 назыв: от "жз ния в! ин (гн "мяты реалы грани~ ва "яи Для ж нол нз !8 раз 88 рае глдвд 12 Системы реального времени Системы реального времени — зто такие снсгемы, в которых требуется гарантия выполнения критических операций в ограниченном интервале времени. При прыжке с парашютом нас не очень успокоит, что лля него гарантировано свойспю. ""Если дсрнугь за кольцо, то когда-нибудь в будущем парашют рвскрспшя".
Нам вюкна гарантия того, по парашют раскроется в заданном интервале времени. Гарантия выполнениа временных ограничений е аистемвх реального времени чрезвычайно вшкна. Превышение вреыенной границы реакции на внешнее событие нри работе программы в критических прилшкениях может привести к катастрофе. Например, во время "войны в завнве" в 1981 г. ошибка в системе управления противоракеты "Ран йп" задержала ее запуск всего на полсекунды. Это привело тому, что ракета "Скад" была упущена, ст се взрыва погибли 29 и были ранены 79 американских солдат.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
