2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 34
Текст из файла (страница 34)
В соответствии с семантикой асинхронной композиции парюимльных процессов, в юокдый момент времени в системе может выполниться любое одно нз возможных действий. Если два автомата готовы выполнить свои действия в некотором глобальном состоянии, то выполняетсл либо только одно, либо только другое действие, но не оба вместе. Таким образом, асинхронная композиция порождает недетерминюм, даже если каждый нз параллельно функиионируюших процессов полностью детерминированный. Недаюрыинизм алесь обусловлен не вероятностью наступления событий, а возмоэкностью вмполнения тех или инмх действий. Прн верификации методом тоде! сйесИпй мы как пзз проверяем выполнение заданных требований на всех возможных путям, а не оцениваем вероятность каких-либо траекторий. Такая семантика параллелизма (она называетса чередующинсл исполнением, или иитеряиэилган, от английского 'юшйеагйпй) явлаетсл следствием основного правила теории пэраллельнмх процесаов: лри аиаяюе ларввгльиых процессов игльв делать иикакгт лредиолажеиий об относительных скараслвл еылолиеиил процессов ияи стратегии тивирсагцика процессов, Только в этом случае результаты анализа булуг справелливы при любых условиях прерываний процессов, при любых скоростях процессоров н т.
и. Таким образом, поведение двух параллельных процессов представяяется недетермниированным нитерливингом некоторого абстрактного последовательного процесса: эффетн ат игцилигеяьлого аылалиеиия двух игделлиямх операций а и В равен эффекту от иосзедааательиого амлаяиения явит операций а любам порядке, 3л.е.
а43 ияи (яц. Формально асинхронная композиция параллельных процессов, взаимодействующих с помощью хэндшейка (ранлеву), определвется следуюшим образом. Пусть р3 =(аг ь3 ь3 аэ3) ' лва параллельных процесса с множеавами состояний о„множествами операций (пометок на переходах) Вы мнвкествами переходов -ь, и нножествами начальных состояний Яе3. Пусть операции вэанмодействив рандеву обозначаются одинаково в обоик процессах. Обозначим О = Е3 г3 Тт — множество этих операций (алфавит нлн словарь взаимодействмя).
Рез3 ра3л дел,' ЯВЛ3 ком дей (П) ЕСЛ3 вал3 выл ПП) Дсй3 ся о Два ЛИВ3 ЕСЛ3 мол ком Нвее 5 сли кроте авг мойюи опе- 1ХРОи!е сощтов, , проодно стеня либо ком- рунк1ННЗМ !стью пкк)е! всех снов- 1ЬЛЫК коро!лька !ВИЯХ эбрэ. !ини- проа и абаи опе- Результат операции асинхронной паряллелыюй композиции процессов авив' рациями взаимодействия рандеву из алфавите Н (абознэчяетсл Р, (~ Рз) определяется квк следующий вкледовательный процесс У ! =Рт=(З б.Е °,б б ), где множество -+ переходов процесав У определяетая слелукнцим обрюом: ()) для возможных действий процесса )) в состоянии з! .
з -а-ь з' (зм зз> -ц-+ (з,', 22> если в процессе Р, есть переход из з! в 21' с выщщнением оперении а, не ° вляющейся операцией рвндеву, то в процессе У вЂ” результате параллельной композиции — этот переход молит быль выполнен независимо аг возможных лействий процесса Рз; ((!) то же для ва!можных лействий процесса Р, в состоянии 22: (з! з2) 1х "+ (з! 22 ) если в процессе Рз ЕСть пЕРеход из з! в 22' С Выпаливинсм Операции Кз, не являющейся операцией рандеву, то в процессе, У этот переход манит бызв выоолнен независимо от возможных действий процессе Р,; ((И) общее действие процессов Р, м Рз, ЕСЛИ КяждЫй ИЗ НИХ ГОтОв к этому действию: З -а З!'Л 22-а-+ при циН! (з! з2) 1" "+ (з! *22 ) кслн в обоих процессах есть переход с выполнением операции и, лвлвющей. ся операцией рандеву, та в параллельной композиции это действие выполняется обонмн процессами одновременно.
Лвв первых правила перехода пврющельной композиции определаот и!пер. ливинг, треп е правило определяет взаимодействие пврвллельных процессов. Если процессы параллельной программы взаимодействуют только с помощью общих переменных, то правило Ш взаимодействия отсутствует в их ° ампозицни. 102 ' Гляев 0 Р1с х++ х++ ш(ш(х) апгм--- -- п1:вгю Атом ра К! в лро Прмвюр 0.1 Рассмотрим параллельную программу, состояшую из двух посдедошпсльных процессов, взаимодейсгвуюшин через обшую переменную к: Егы Ргы КО: хг+г поз рг1ве 1х)г хы х++г сз: епэ Пусть вначале х-о. Какое значение будет напечвтаноф Для завершения параллельной программы оба процесса должны завершиться, выполнив все свои операторы. Однако эффект аг выполнения операторов бу- дет различным (мшкет быть напечатано О, 1 или 2) в зависимости от того, в какой последовательности эти операторы будут выполняться.
Рйс. 5.5 схе- матично показывает все возможные последовзтгльнссгн. Р1 !!Ряс н зг — н )г-,— — июль Ф 1 ! н,з ь, ) — — — н ) Рнс.5.5. Эффект ннтерливннга — возможные зраехторин выполнения параллельной нршраммы Ввриемся к примеру построения модели протокша РАВ. Возможные действия в параллельной композиции автЬматов нашего примера, У = л х о х СЫ х СЬ2х )(х  — это независимый переход любого компонентного автомата (интерлнвинг) илн взаимодействие двух автоматов, готовых к этому взаимодействию в соотаеютвнн с семантикой рандеву. Для протокола РАК параллельная композиция представляется автоматом У, глобальное состовние которого — это шестерка состояний. Всего в этом автомате около 2000 состояний (ЗхбхЗх2хбхЗ), хотя и не все они достюкнмы из начального состояния. Первый компонент состояниа автомата У вЂ” состояние автомата л, второй — состояние передатчика Я, третий — состояние канала СЫ ° т,д 0,0,0 все в рис, '. Аюзх вые е Зрес ! вольв рядке Зресг оымь Для 1 с поь юмт вперз прись ,ных ъся, ~ бу- ого, схе.
ные ера, »нт~х к ола сооло ого ~ага 20! н т. д. Начальное состояние произведения 'автоматов У вЂ” состоание (0,0,0,0,0,0) (будем такую шестерку представлять просто 000000). Единственное возможное действие У в этом состоянии — это синхронное взаимодействие компонентов А н Е с одновременным переходом нх в следующие сопояния, что в ввтомате У соответствует переходу в состояние 110000. На рнс. 5.6 показан начальный фрагмент графа переходов У. Автомат У можно рвссматримпь как структуру Кринке. Некоторые возможные вычисления (вкяедовательностн состоаний) системы переходов У: 000000 -+ Н ОООО-+121000-+! 20010 -+ 110010 -+1!0021-+121!31-+ ...
000000-+1 !0000 » 121000-+ 120000-»1 10000-+ 121000-+1!1000-+1 100!О-»... Рне. 0.6, Начааьный фрагмент грвфа переходов протокола РАй Атомарные предикаты системы переходов У, рассматриваемой как структура Кринке, определяютса теми свойствами, которые мы хотим проверить в протоколе РАК. Спецификация прттльного поведения протокола вытекает нз его задачи: брес1: Все сообцмнпа, пэвм»нные ппеьзовотелем А, домены бытыюлучены пользователем В без потерь н дублнроеонаа, причем пазучены в том асе порядке, е коком бьмн носаты. брсс2: Если А хочет посеоть сообцпнне, он сможет это сделать (мажет быть, нв сроэуд Лля доказательства того, что бесконечный поток сообщений, передаваемый с помощью коммуникационного протокола через ненадежный канал, сохраняет свой порядок, требуетса всего трн различных элемента данных.
Это впервые было показано в (148). Мм будем нсполиовать здесь следующий прием. Введем следующие атомарные предикаты: зл . А»юслвл сообщение, занумерованное (г ! г»: В принял сообпмнне, занумерованное е . Глаша 1100. 12 ПК 1211: 13103 !3002 24002 25202 25213 25013 20003 110031 !2!031 120021 120131; И003!( 240031) В разул обнарул (требуе« это и др 7«м 3«м Поскольку различных нумераций сообщений всего два,б н 1, то в нашей структуре Кринке будет четыре атомарных предивна: ге.г,,г«,«; . Очевидно, что предикат ге нстииен в состоянии 1 автомата А, г! истииен в его состоянии 2. Преднкат «в истинен в состоянии! автомата В, г! истииен в его состоянии 2.
В каждом состоянии струкгуры Кринке, моделирующей протокол. какие-то нз этих атомарных предикатов будут истинны, другие иет. Приведенное выше вычисление структуры Кринке У снабдим специфиизцией— мншкеопюм истинных в каждом состоянии атомарных предикатов: 000000( ) -+!!0000(ге) - 121000(гс) - 120010(ц«) - Ц0010(гв)- !0(12Ц~аб) ... Для верифшощнн протокола по этому вычислению построим т!юекп«рню— цепочку подмножеств атомарных преднкатов, истинных в соспшйнмх вычисленив: ( )(гс)(ге)(гс)(ге)(гс,гг)....
Именно такие траектории будут проверяться на выполнение требшкшнй спецнфшощнн. Формально требования специфнялцнн протокола РАК представим формулами (.ТЕ. Зрел!: О(гс ~(-~!П е)) л О(Ъ =«(-ЧВг!)) л П(г! ш(-~еПц)) л О(0 =«(-~еПге)): "если А послал сообщеиие, во пока В яе примет гго, А ие лосьиаев ггедуюиггг, и если В щилсы сообигеииг, во ои ие ирилниагт имшкого другою сообщения. лака А ле лоиомт следующее". Зре 2: О((гс шйг$)л(г3=«рге)): "есги А леоны сообщглие, во когда-иибудь в будущем оя оиожит лосиапь сягдуюь;ие". Анализ композиции покшывшт, что не все вычисления сиошмы переходов У удовлепюряют специфиющни.
Рассмотрим, например, вычисление (в скобках указывтотся атомарные преднквты, истинные в состоянии): 000000( ) -+ пользовшель А посылает сообщение «(е передатчику Я -+ 110000(гс) -+ Япосылаетдс вканал СЫ -+ 121000(гс) -+ СЫ доставласт Ае приемнику В -+ 120010(гс) -+ "пегерпеливый перевпчик" не дакдавсл подтвср;.кдения -« 1!0010(ге) -+ приемникйдосзжмиетде пользоватешо В -+ шее 5 вшей идно, о со- окал, ривеей— ~ю— гчнс- !ула- 'а)): сле- одов ение 110021(я,ге) -+ "нетерпеливый передатчик" повторно шюылает Ае в канал СЫ -+ 121021(ге,ге) -+ приемник К шюыласт в канал Сй2 подтверждение приема Ас + 121131(зс,гс) -+ перешпчнк 8 получаетиз СЬ2 подтверждение приема Ас -+ 13103 1(хс,га) -+ канва СЫ повторно досоьвшмт Ас приемнику Я -+ 130021(гс,гс) -г перелатчик У принимает от А новые данные А! -+ 240021(г„гс) -+ Л передает эти ленные в канав СЫ -+ 252021(з!,ге) -+ Я передаст в СЬ2 подтвержление повторного получения Ас -+ 252131(з„гс) -+ канал СЫ теряет сообщение А! -+ 250131(з„гс) -+ Я получает подтверждение от Сйу (счипшт, что с(, дошло) -+ 200031(з!,гс) -+ Я принимает от А новмедвннме Ае -+ ! 10031(зе,гс) -+ 8 посылает ас в канал СЫ; здесь нарушение свойшпа ы(я! нэ( э~(!г!)) -+ 121031(зс,гс) -+ СЫ доставляет Ае приемнику й -+ 120021(гс,гс) -+ Ж ожидал А!, он посылает в СЬ2 подтверждение у ияАс- 120131(яс,!0) -+ Я получает полтверяшение поставки Ас, готов приншь А! -+ 130031(гс,ге) -+ А посылает перелатчику б четвертое аюбшение, А! -+ 240031(г!,гь) — ....
В результате А послал три сообщения, два иг них пропали. Эи пропажа не обнаруживается протоколом, но выяшшстсв по невыпояненню спепифнввпии (требуемого свойства Брас!). Читателю рекомендуется тщательно проверить зю и другие вычисление протокшпь чтобы убеднтьса, насколько сложнмми и Пима 5 явв Расо Пуст (кача перез в сос перез полуз перез госте непредсказуемыми могут быть последовательности событий в простой параллельной системе процессов, дюкс если в ней поведение кюкдой компоненты предельно понятно. Ручное построение асинхронного произведения автоматов для подобнмх систем чрезвычайно трудоемко. Как видно иэ примера протокола, в асинхронном произведении систем переходов рост числа состояний экспоненциальный, по означает следующее: добавление к системе каждого нового компонента с ЛГ состояниями увеличнмют число состояний в асинхронной композиции в ЛГ раз.
Этот эффект нюывается "еэрыесм числа сасмоллнй" (звпе ехр1озюл ргоЫею), и он составаяст одну нз главных проблем верификации. В реальных системах колнчесгво возможных состояний достигает астрономических величин — ! О и более (108]. Процесс построения асинхронной композиции систем переходов мокло автоматизировать, т.е. инструментальному пакету верификации задавать верифицируемую модель не в виде структуры Кринке, а квк набор отдельных взаимодействующих модулей. Операцию асинхронной композиции этих модулей с получением структуры Кринке обычно выполнает сам инструмент верификации до тою, как выполнить верификацию. 5.4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
