И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin, страница 10

Лишь один, недетерминировано выбранный процесс, инициируетпротокол, установив election_started = 1(между 19 и 20-ой строками добавим)::: atomic {(!election_started && !Active) ->/* Один процесс может начать выборы послав первое сообщение msg *//* и став активным */election_started = 1;out ! one(mynumber);first_message = 0;Active = 1}}Далее один из неактивных процессов, первым обнаруживший, что first_message=1, можетвступить в выборы, а потом установить first_message=0 (добавим следующий код между20 и 21 строчками и 37 и 38 строчками):if:: (first_message && !Active) ->if:: Active = 1; /* присоединиться к выборам */out ! one(mynumber):: skip/* не присоединяться к выборам */fi:: elsefi;first_message = 0;Проверим корректность измененной модели относительно свойства, что номер лидеравсегда будет максимальным:pan: assertion violated (nr==5) (at depth 45)pan: wrote pan_in.trail(Spin Version 4.2.7 -- 23 June 2006)Warning: Search not completed+ Partial Order ReductionFull statespace search for:never claim- (not selected)assertion violations +cycle checks- (disabled by -DSAFETY)invalid end states- (disabled by -E flag)State-vector 196 byte, depth reached 45, errors: 133 states, stored0 states, matched33 transitions (= stored+matched)13 atomic stepshash conflicts: 0 (resolved)Из результатов видно, что в поведении модели существуют пути, такие чтооператорassert(nr == N) не выполнился (assertion violated).

Почему это произошло?Потому что модель изменена таким образом, что теперь не все процессы участвуют вголосовании, т.е. будет выбираться не максимальный номер из существующих, амаксимальный из участвующих.42Остальные же свойства, проверявшиеся ранее, и на измененной модели останутсяистинными.3.2Задача о фермере, волке, козе и капустеОписание задачиВ качестве второго примера рассмотрим задачу, хорошо известную всем со школьных лет:фермер, волк, коза и капуста находятся на левом берегу реки.

Фермер хочет переправитьволка, козу и капусту на правый берег. В лодку вместе с собой фермер может взять лишьодного из них (либо волка, либо козу, либо капусту). Он может плыть в лодке и один. Однакоесли волк останется наедине с козой на одном берегу, то он ее может съесть, а коза,оставшись вместе с капустой, поедает капусту. Существует ли такая последовательностьпереправ фермера, чтобы доставить всех на правый берег целыми и невредимыми?В данном разделе мы покажем, что с помощью системы Spin мы можем получить решениеэтой задачи: сформулировав в качестве проверяемого свойства модели то, что несуществует решения с желаемыми свойствами.

Как результат верификации Spin выдасткотрпример – именно ту траекторию поведения системы <фермер-волк-коза-капуста>,которая нарушает проверяемое свойство. Этот контрпример и будет являться решениемзадачи.Модель задачи о волке, козе и капусте на языке PromelaВ данной модели достаточно одного единственного процесса river. За местоположениекаждого из участников задачи пусть отвечает своя битовая переменная, таким образом, всегобудет четыре таких переменных (f, w, g, c). Будем считать, что значение переменной равно 0,если соответствующий участник находится на левом берегу, и равно 1 в случае, еслиучастник находится на правом берегу. Применим недетерминированный подход кмоделированию задачи о волке, козе и капусте.

Недетерминировано выбираются партнерыфермера по переправе из числа тех участников задачи, которые находятся с ним на одномберегу. Например, изначально, партнерами фермера могут быть или волк, или коза, иликапуста, или же он может поехать в одиночестве. Повторяя такой выбор в цикле, фермер, впринципе, бесконечно будет перевозить своих подопечных с левого берега на правый и справого берега на левый. Поскольку по условию задачи все должны быть переправлены направый берег, то следует добавить условие выхода из цикла:(f==1) && (f == w) && (f ==g) && (f == c)Это условие будет истинным, когда все битовые переменные равны 1 (т.е.

волк, коза,капуста, фермер оказались на правом берегу). С его помощью мы можем остановитьвыполнение цикла всех возможных переправ.В результате получится следующая модель задачи на языке Promela:/* Задача о фермере (f), волке (w), козе (g) и капусте (c) *//* Булевы переменные, используемые в LTL формулах */bool all_right_side, g_and_w, g_and_c;active proctype river(){/* Вначале волк, коза, капуста и фермер находятся на левом берегу реки *//* положение фермера*/bitf = 0,/* положение волка*/w = 0,/* положение козы*/g = 0,/* положение капусты*/c = 0;43all_right_sideg_and_wg_and_c= false;= false;= false;printf("MSC: f %c w %c g %c c %c \n",f, w, g, c);do:: (f==1) && (f == w) && (f ==g) && (f == c) ->all_right_side = true; /* все на правом берегу *//* Завершаем цикл*/break;:: else ->/* недетерминированный выбор */if/* фермер и волк на одном берегу реки */:: (f == w) ->f = 1 - f; /* фермер переправляет волка */w = 1 - w;/* фермер и капуста на одном берегу реки */:: (f == c) ->f = 1- f; /* фермер переправляет капусту */c = 1- c;/* фермер и коза на одном берегу реки */:: (f == g) ->f = 1-f; /* фермер переправляет козу */g = 1-g;/* в любой ситуации */:: (true) ->f = 1 - f; /* фермер может пересечь реку один */fi;printf("MSC: f %c w %c g %c c %c \n",f, w, g, c);if/* проверяем выполнение ограничений *//* съела ли коза капусту? */::(f != g && g == c ) ->g_and_c = true;/* съел ли волк козу? */::(f != g && g == w ) ->g_and_w = true;::else ->skipfiod;printf("MSC: OK!\n")}Поиск решения задачи средствами SpinПри запуске симуляции обычно получаются реализации, где волк может съесть козу, а коза –капусту, и более того, такие возможности "поедания" могут встретиться несколько раз.

Этирезультаты связаны с тем, что на поведение участников не накладывались никакиеограничения. Приведем пример одного из прогонов симуляции. При выводе используютсясоглашения, принятые ранее: значение переменной, отражающей местоположение участникаравно 0, если участник находится на левом берегу и 1, если на правом.44Волк и коза на левом берегу без фермера.Волк может съесть козу!Коза и капуста на правом берегу без фермера.!Обычно Spin используется как средство верификации модели. Однако в данном случаепредставляет интерес задача: обнаружить во всем разнообразии переправ такую, что фермерпереправит все свое имущество (волка, козу и капусту) на правый берег реки в целости.Зададим следующую LTL формулу:<>fin && [] ( wg&& gc )где значения предикатов таковы (all_right_side, g_and_w, g_and_cпеременные, определенные в тексте программы):#define fin#define wg#define gcбулевские(all_right_side == true)(g_and_w== false)(g_and_c== false)Предположим, что не существует ни одной реализации (устанавливается флаг No Executionsв пункте Property holds for окна проверки LTL формул), в которой выполняется заданноеправило: "Когда-нибудь в будущем все участники задачи окажутся на правом берегу, и приэтом всегда будет выполняться условие, что волк не съест козу, и коза не съест капусту".При верификации Spin выдаст ошибку, сообщая тем самым, что он обнаружил веткуповедения процесса river, в которой заданное условие выполняется.State-vector 20 byte, depth reached 73, errors: 156 states, stored (57 visited)8 states, matched65 transitions (= visited+matched)0 atomic stepshash conflicts: 0 (resolved)Spin предложит перейти к управляемой симуляции (Run guided simulation):45При прогоне управляемой симуляции будет отображено одно извозможных решений задачи:1.

сначалавсевчетверомнаходятсяналевомберегурекиf = 0 w = 0 g = 0 c = 02. фермер отвозит козу на правый берег, волк и капуста остались налевом берегу,f = 1 w = 0 g = 1 c = 03. фермер возвращается в одиночестве на левый берег,f = 0 w = 0 g = 1 c = 04. фермерзабираетволкаипереплываетснимнаправыйберег,f = 1 w = 1 g = 1 c = 05. фермер с козой переправляется на левый берег,f = 0 w = 1 g = 0 c = 06. взяв капусту, фермер плывет на правый берег,f = 1 w = 1 g = 0 c = 17.

оставшиеся шаги посвящены переправе козы на правый берег.Таким образом, система верификации Spin СГЕНЕРИРОВАЛА решение задачи о волке,козе и капусте, как контрпример свойства «интересующего нас решения задачи НЕСУЩЕСТВУЕТ”.463.3Криптографический алгоритм Нидхама-ШредераОписание алгоритмаВ данном разделе рассматривается алгоритм аутентификации – построения доверительныхотношений между двумя партнерами A и B, широко применяемом в разных пакетах,например, в Kerberos. Алгоритм, предложенный в 1978 Нидхамом (Needham) и Шредером(Schroeder), использует криптографию публичных ключей. Каждый участник имеет паруключей. Один ключ – открытый или публичный, известный всем другим участникам, другойключ – закрытый (хранящийся скрытно), известный только самому владельцу.

Связь междудвумя ключами такова, что информация, зашифрованная одним ключом, может бытьрасшифрована только вторым ключом в паре. Таким образом, отправитель может бытьуверен в том, что сообщение, зашифрованное им публичным ключом А, сможет прочестьлишь сам А.В алгоритме аутентификации Нидхама-Шредера стороны обмениваются сообщениями,состоящими из открытой части и зашифрованной части. В открытой части сообщениясодержатся сведения об отправителе, получателе сообщения, и номер сообщения согласноалгоритму. Вторая часть сообщения шифруется публичным ключом предполагаемогополучателя сообщения. В зашифрованной части содержится, так называемый, “nonce” –случайное число, генерируемое каждой стороной для очередного сеанса доверительногообмена.