2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 51
Текст из файла (страница 51)
мер находится на тюм же берегу. Наща задача — найти такой путь в структуре Кринке, на котором выполняется формула »(в и и) ч(й и с) ~ (й и / ))Н(~гйс) — когданибудь в будущем все переберутсяя на правый берег, а до этого во всех состояниях пути соблюдается требуемое ограничение. На рнс. З.б зги запрещенные состояния перечеркнуты. Используем дяя ивхожления плана переправы систему верификации Брю. Описание этой задачи на языке рплие! а чрезвычайно проспи Ъсоз Г, с, д, ч Свзеег /* ввтвлъисе сссгая»»е / все»юви»м альтернатив аегмтег»енирсввио вилис»ется олив '/ -»г г /* Варищ исае» ппмехвгв аги / и+с гг»и /» или с вас»си "/ с-»т Ггс с /* и»и с «всусттж */ д-+г- гг д- д /* и»и с »свая Ф/ и ьь д ы с -+ Ьгевх /* останов, кегле все ли»смыв»гав / Пров ° сох прав~ вое с Сноп мым Рм Замен гересн с фер» 5 взв З сун пра Л при чещ Ме~ в к обък' шаче>м бе.
ояние устой зеков левом Го эяиий н, чго ояния 70 оянне вв нв >а ле- Со Го г)— фергвкой >мула ребе> эрегы. Зр>я. Проверяемое условие: . А-~(((8 и с)» (8 и >г) ю (8 и у )) Щэ>гйс)) — среди всех воэможнмх пуюй не существует твкого, нв котором все переправятся нв правый берег, и при этом во всех состояниях этого пути выполняется задан- ное ограничение. Система верифнкэции Вр>п выдвст контрпрнмер. который н является неко.
мым планом (см. рис. 8.7). Ив>одное состояние Фермер с >овсе - нв нрееый ФермеР адин - ие леаюй Фермер с ваном - ие ернзый Фермер с зовов - нв левый Фермер с юпзопя> - ив Миммйю* Фермер одни - не левый Фермер с имей - не прелый Рнс.8.7. Гимн переправы через реку.
сгенерированный сястеной вервфюиния дяя лробяемм "фермер, волк, ине, мюуста" Заметим, что, используя темпорвльную логику, можно выразить м>югнв интересные полем>ые свойстве строящихся пввноа. Например, для. проблемы с фермером и его командой: П в запиочитсльное состояние мшкно попасть: ЕЗ>(>мйс); П существует такое решение задачи, прн котором, если коза переедет нв правый берег, онв твм нввсегдв и оствнется: Е(Р( йгйс)»(( 8)ЗЖй)); П при любом варианте решения задачи фермер доюкен будет возвращаться через реку один: А(((8 не) ч(8 н и) м>(8 и /))77(йгйс) и> З>((у' л Х л->у)»(м и Хн>) л(б и Хй) л(с и Хс))1 йге /леся в В бпыпч И Ыюг Ь - Гаг Ьусп и Нг ьгсе с и/ /* пкачопп лодка па пчжм берегу */ /* начальное число м ссиоиеров */ /' качппькоч число «пккибплов */ /' псч попыопкые периконы системы */ /"'испи жжап пп пекем береги, пе ьюпио испоиьзовать такг '/ /* гмссиоипр ппрчгмпвилсп кп правый берег */ * «аииибвп перппрппипсп кп правый берег */ /* два ыиссзпжпрп порчпрпвикись / /* якп кммибапв ппрппрапипись */ О и>а-пп - и-1 ::.
с>О-ьс с-1 :: и>1-ги н-2 ы Ы-ю с-2 Проблема "миссионеры и каннибалы". Трн миссионера н три аборигенаканннбапа должны перепльпь реку с левого берега на правый. Их лодка может выдерхать не более двух человек. Кшкдый миссионер и квклый каннибал могут управлять лодкой, но если на одном берегу каннибалов окажется больше, чем миссионеров, то голодные аборигены могуг позавтракать миссионерами.
Проблема планирования состоит в построении такого плана переправы через реку, чтобы все миссионеры остались в живых, н при зтом через реку должны переправитьов н миссионеры, и аборигены. Задача зга очень исхака на предыдушую. Состоянием здесь можно выбрать тройку: (Ь,ш,с), где Ь вЂ” шшшкение лодки 1Ь =1 — лодка на левом берегу, Ь = 0 — лодка на правом берегу), а ш и с — число миссионеров н число каннибалов на левом берегу.
Например, шктояние (0,0,2) говорит о том, что лова на правом берегу, на левом берегу нет миссионеров и два каннибала га трн миссионера и один каннибал на правом берегу, потому что обшее число миссионеров и общее число аборигенов не меняетсв). Как и в предыдущей задаче, будем счмппь, что перекоды межау состояниями неделимы, онн не вюкны для анализа поведения системы. Пример возможной траектории системьс (1,3,3) -+ (0,2,2) -+ (1,3,2) -+ (О, 1,2) — неудача: миссионера свели на левом берегу. Запрограмьшруем все переходы в языке РгопюЬ, и с помошью системы ЗР1л будем искать безопасное решение задачи. Для этого проверим в системе БР1п угвержаение: "безопасного решения задачи ие сущпсшеуеш", которое постараемсв формализовать на шыке формул линейной темпоральной логики. Опишем проблему для произвольного числа Ы миссионеров и каннибаяов: :: ь- В каче тах неь п1мвы ~ Для зн чслови (1,3, (0,0 Обкол ~ чтобы ь торой н Снова с нечногс решить На рис.
мннаетс иран втс глава В )брать ерегу, число ги оь>о) ьа)с>а) -+ ькеаь )а<й) аа)пос) -ь Ксеав :: )н -о) - ьеак и, что нбапа с чнс- )иямн скной )ЕВОМ ) бр!а ) Зр!и юста- г / '/ нгенака мо- ганниското я ь мкс) пере- через ;: в>ошс>о -+ в в-1)с с-1 /* )тсспснар и каннибал перап)вкивьсь */ йю :: ь-+ь ь) / асин лота на плакс» берегу, ее искно иеаопькопаеь таш '/ 12 ~~ ам -+ ачы1 /* мтсиснер переправпка на лвкт берег */ :: с<н -> с с+1 /* юн)вбал серепрааипся на лекса берег */ :: век-1-+ в а+2 /* Лаа нпссиснера перепрааплись / :: ссн-1 -+ с с+2 '. /* лаа каннибала перещааклись '/ . .
"аскаассн -ь аче+1)с с>1 /* ьтссионер и каннибал перепраакпись екаоеи */ /* ииссионерок спели на лемм берегу */ /* нкс«ионероп свели на аракс» бакст '/ /* псе благапал)чно перебраппсь на прения берег '/ В качеспш проверяемого условна амберем слелуккцее) А (( (т>Оййс>т)йй (т<Фййт>с))ЩтесмО)) — на коек путях неверно, что можно всем переправиться (т+с = 0), н к процессе переправы не будет условий для сьеденна миссионеров. Дпя значения /У =3 система верификации Зр)п выдаст опровержение кино условия, т. с, безопаснмй план действий: (1,33)ь(0 3,1)-+(13,2)-+(0 30)-+(!3,1)-+(01,1)-+(1,2.2)в (00 2) -+ (1,03) -+(О 0,1) -+(102) -+(О О О) Дяя ))/ = 4 решения втой залачн неп бр!н не нашел опровержения.
' Обхед нолем шахматной доски. Известная логическая задача состоит в том, чтобы найти план обхода конем шахматной доски размером У к )т нз некоторой иачалыюй позиции (1, /), побывав на каждой клетке только один раз, Снова система вернфншщнн бр!к, проведя нсчерпывакиций анализ всего конечного множества возмвкных состояний построенной модели, позволяет )юшкть задачу. На рнс.
8.8 представлена идея решения проблемы. Состояние снсшмы запоминается в булевом масснве А размером Ф к У, в котором, фактически, хранятся те клетки, на вторых конь укт побывал прн сбхолв Зуб ' гласе В Для п! будем напра! просто испол! ТОР, НЭ лаемо! раядел манин ненте ргогпе! хм! .! Вначав чальио та л!В нмн. В Оо ПРО! сели кс /* дом ! Оегг! оо ходов ' >>2! :; г>г! Рнс, 3,3. Выбор хола в задаче обхола конем шахматной доскй Пр р Х ник! Игра ! КОТОРО! нироаа! 277 Гласе В Для простоты в представленном нике фрагменю программы на псевдокоде будем использовать двумерный булев массив А(г/,))/!. Хотя в языке Рплпе!а напрямую возмакио использование только одномерных массивов, в нем есть простой способ опиапь н использовать двумерные массивы.
Эго делается с использованием оператора определения ело!кных типов сугесег. Зтот оператор, например, можно использоввть для ъщания структуры сообщения, посылаемого в кажа. Мы увидим использование этого оператора в следующем разделе. Кроме того, эту конструкцию можно использовать и дяя зщпнпя и манипулирования многомерными массивами. Например, в следуюцюм фрагменте показыммтся, квк описать и использомпь двумерный мясбив в языке Ргоще)щ суд ег скопи [ пзс «[в) [ скопе А[В! г А[!).е[5) А[)).е[!)г Вначале все элемапы мессина А имеют значение «ие за исюпоченнем начальной позиции коня, когда конь попадет на клетку (Ау), значение элемента А(А/) становится равным Уа[ге, и далее на зту квстку ход будет запрещен. Возмо)кная смена состояний системы определяется следующим циклом с программы на языке Ргщпе1а.
Кмкдая из В альтернатив, соопмтствукяцих возможным холам коня, вьпюлняеюя, если конь можят сделать этот ход и если конь не был на этой клетке: /' псевдокод / Ф Сет)де К )г М, ) Спмг А[Г,Л - Гегзег Со /* лроеерхе всех В еариеизое хода иищ и еьеюлиеиие вонищах холов / ~: кщщ)<и щ Аы-г, )+и ч ьщ-щ )-)е)г мы ))-гезеег к++ . :: »геь)>! ы А[э-г, )-ы -+ Ащ-г~ ) )-ы Ан, )1 газиев к++ :: « и'н -пиеа)г /* прием есе идее>и со одиоиу Разу '/ сс хола Проверяемое свойспю: АС( (К Фе)У)) — на всех путях счетчик ходов К никогда не достигнет значения А/ ° А/. Игра 15. Всем известная "игра 1уи является классическим примером, на ° отором часто оценивается зффекпщвють эвристических алгоритмов пиа.- вироааниа, подобных извеспюму алгоритму А». Правила игры просты.
Нз /хасав ас ес! мгст! стн к лящи! 8.4. кри Проверяемое свойство: Рве. Вр. Возммкныс аяьтсрнатнвные действия на очередном ходе а игре "! 5" начального состояния, предо)падающего собой произвольное рзсположенис 15 коствшек на поле 4к4, перемещением в пустое поле соседних с ним костяшек разместить их в порядке номеров (рис. В.р). Известно, что ровно половину из 1б[ возмшкных начальных поло)пений в игре "! 5" нельзя свести к искомому упорялоченному поло:кению. Эта головоломка имеет очевидные обобщения, в которых нухшо в квадрате А/ х Аг яибо в прямоугольнике ))/ я А/ от произвольного располшкения костяшек прийти к их расположению в порядке номеров. Основной фрагмент программы иа Ргоше[в этой игры для квадрата со стороной /у = 3 представлен нюке.
ьусе н 3! со /* З,З вЂ” ксорлянати пустого наста с мвмрсм Н"И '/ ::Ть) м анар! ащ,л), а[т-Ыщ )! .т т-) /' пустая вверх */ :щ Н М анар[ а[т/а), ащ+),Т) )! т т+) /* пустая анна '/ г:з>1 м зяар! ащ,)1, а[Х, )-1) )! д" Г-1 /* пустая влево / ::)«н ! зьар[ а1т,щ, а[тАИ)) )! .т )+) /' пуста» ащмво / ос АО+,„,1! . „! И),4=(1-!)'А[+/)), Одно! жгррс! кол— тей по сеть, ! то!рай случа! рассм! ются ! лино ! вок, о! значит прове[ можно сти ап ную и а этОЙ ностьк лсльно ники. Атака! пользо ние тр! стоит ! ходим! всех вс улвстс! ння бс лля ве с))ес[г[п невозм! до вате! сти про яа егея лупил никогда ле дсстщнеи состоюнц лрк котором есе косямиин еыстрсятса ло порядку. Если исходное положение косшшек возмолщо спа- сти к упорядоченному, сисщма аернфтщцин найдет план действий, приво- дящий к нему. ение кос- овоч исгные чике зже! нг- 8.4. Верификация криптографических протоколов Одной ю областей прнложениа аягоритмов тоде! сйесипб является авалю корректности криптографических протоколов.
Криптографический прото. кол — зто правилц выщшнение которых пользователями компьютернмх сетей позволяет обеспечить безопасность обмена информацией через открьпую сеть. Правила безопасного взаимодействия по сети включмот базовые криптографические операции: шифрование и дешифрование, генерация псевдослучайных чисел и т. п. Проверка корректности таких протоколов должна рассматриваться с двух точек зрения. Во-первых, такие протоколы реалюуются параллельными взаимодействующими процессами, поэтому нх необходимо проверять на отсутствие типичных ошибок параллелизма — блокировок, ограничений живости, доступа к разделяемым ресурсам и т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
