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

Она будет некорректной в двух случаях когда во всех последующих состояниях будет истинно р, а q будет ложно, или есливстретится состояние, в котором не будут истинны ни р, ни q.Если первый оператор цикла выполнится (т.е. найдется состояние, в котором р истинно, а qложно) то вычисление будет продолжено с метки accept.В состоянии, помеченном этой меткой, цикл также имеет два условия выбора. Один из путей– вечное пребывание в цикле по условию р истинно, а q – ложно. Если такое вычислениесуществует, то это соответствует нарушению свойства G (p → (p U q)). Бесконечноеповторение этого состояния соответствует ошибочному вычислению.

Поэтому это состояниепомечено меткой accept. Нарушение будет найдено верификатором как цикл сбесконечным выполнением оператора с меткой accept.Другое возможное нарушение возникнет, когда p становится ложным до того, как q сталоистинным. Этот тип нарушения приведет к завершению процесса never. Завершениепроцесса never интерпретируется, как найденное ‘ошибочное” поведение, котороесовпадает одним из с поведений, которое не должно было бы произойти при выполнениисвойства.30Если оба выражения, p и q, окажутся истинными при выполнении второго оператора, цикла,то ни одно из условий выбора невыполнимо, следовательно, процесс never заблокируется.Блокировка процесса never не ошибка, а желаемое поведение! Блокировка процесса neverговорит о том, что он не завершился и не проходил бесконечный цикл с меткой accept, т.е.не нашел ошибочных поведений модели.Важно заметить, что в состоянии S0 возможна ситуация, когда оба условия (guard)исполнимы.

Здесь недетерминированный выбор имеет критическое значение. Если вприведенном выше примере процесса never заменить условие с true на оператор else, топроцесс будет реагировать только на первое выполнение выражения p, которое сразу должноприводить к выполнению выражения q. Наличие недетерминированного условия позволяетсформулировать более сложное условие G (p → (p U q)).Отметим еще раз, что процесс never не должен оказывать влияния на поведение системы,поэтому в нем, как видно из примеров, используются лишь операторы условия и assert.Любая метка, начинающаяся словом accept, например, accept1, accept_init,accepting и т.п., играет ту же роль в процессе never, что и метка accept.Отметим, что построение процесса never для обнаружения ошибочных поведений моделине всегда является простым.

Spin позволяет описать проверяемые свойства моделиформулами линейной темпоральной логики, используя темпоральные операторы F, G и U,определенные пользователем атомарные условия (атомарные предикаты), построенные какбулевы ыражения языка Promela, и обычные булевы операторы &&, || и ! (и. или и нет).Темпоральный оператор X не может быть использован при построении LTL формул всистеме Spin (поскольку понятия “следующее состояние” в системе параллельных процессовнет: в общем случае каждый из параллельных процессов может выполнить независимыйшаг). По историческим причинам, в системе Spin темпоральный оператор G представляетсяпарой квадратных скобок [], а темпоральный оператор F – парой угловых скобок <>.Импликация представляется парой символов ‘->’.

Указанная выше формула LTLG (p → (p U q)) будет записана в Spin, как [](p -> (p U q)).acceptptrueaccept1!(p||q)ptrueРис. Недетерминированный автомат Бюхи для формулы !G(p → (p U q)), которыйпереходит в заключительное (принимающее) состояние accept, если, начиная с любогосостояния (переход true в состоянии s0) встретится бесконечная цепочка состояний,помеченная p, или же после конечного числа состояний, помеченных р, встретитсясостояние, в котором не истинны ни р, ни q.По введенной темпоральной формуле Ф, выражающей требуемое свойство поведениямодели, Spin строит ее отрицание !Ф (формулу, описывающую все “ошибочные” поведения),и по формуле !Ф строит автомат Бюхи B!Ф, конечным образом описывающий все такиеповедения. Далее, по автомату Бюхи B!Ф Spin строит процесс never, который в режиме31верификации будет пытаться обнаружить хотя бы одно “ошибочное” поведение моделианалогично тому, как это описано в приведенном выше примере.323 Примеры задач для верификации в SpinВ данном разделе подробно описаны несколько задач, модели которых составлены на языкеPromela и верифицированы средствами Spin.

Кроме того, здесь изложены основы работы сграфической оболочкой XSpin. Ознакомление с этой частью раздела позволит читателям нетолько самостоятельно моделировать интересующие его задачи, но и проверять корректностьразработанных ими моделей при помощи Spin.3.1Протокол выбора лидера в однонаправленном кольцеОписание протоколаРассмотрим протокол выбора лидера в однонаправленном кольце (алгоритм предложенДолевым, Клаве, Роде (Dolev, Klawe, Rodeh) и независимо Петерсоном (Peterson) в 1982году) [2, 3].

До создания этого алгоритма считалось, что при выборе лидера воднонаправленном кольце количество сообщений не может быть меньше, чем O(N2), где N –число узлов в кольце. В данном алгоритме достигается количество сообщений2Nlog2N+O(N). Рассмотрим этот алгоритм.Дано N распределенных узлов с некоторыми весами. Узлы асинхронно взаимодействуюттолько с соседями, образуя однонаправленное кольцо.

Количество узлов фиксировано и неменяется. Порядок сообщений в каналах не меняется. Требуется построить протокол – наборлокальных правил для каждого узла, которые позволят получить глобальный результат –каждому узлу определить единственного лидера (например, узел с наибольшим весом).Изначально алгоритм был разработан длядвунаправленных колец, и при обходекруга активный процесс сравнивал себя сдвумя соседними активными процессамипо часовой стрелке и против нее. Такимобразом, если его номер являлся локальным максимумом, он оставался в круге, иначе онстановился пассивным. Активным узлом считается узел, который создает сообщения с новойинформацией. Пассивный узел лишь передает полученные сообщения соседу, никак их неизменяя.В ориентированных кольцах сообщения можно посылать только по часовой стрелке, чтозатрудняет получение номера соседнего активного процесса, находящегося в этомнаправлении.

Будем считать, что направление обхода в кольце по часовой стрелке, и толькопо этому направлению посылаются все сообщения.В алгоритме Долева, Клаве, Роде на каждом активном узле хранятся два параметра:локальный максимальный вес maximum и параметр предыдущего активного соседа,находящегося против часовой стрелки neighbourR. Локальный максимальный весвычисляется по данным от двух предшествующих против часовой стрелки активных соседей.Алгоритм состоит из повторяющихся раундов, на которых обновляются значенияпараметров на активных узлах. За один раунд не менее половины активных узлов переходитв пассивное состояние.

Именно за счет этого правила достигнуто сокращение общегоколичества сообщений, необходимых для выбора лидера. Каждый из раундов состоит издвух шагов: на первом шаге A1 активные узлы получают сообщения типа one, а на второмшаге A2 – типа two.Пассивные узлы только передают по кольцу полученные сообщения. Опишемпоследовательность действий активного узла.

В начале работы алгоритма все узлы являютсяактивными:33A0. maximum := собственный вес. Послать сообщение one(maximum) ближайшему соседу.A1. Если пришло сообщение one(q), то:1. Если q != maximum, то присвоить neighbourR значение q и послать сообщениеtwo(neighbourR).2. Иначе, maximum и есть глобальный максимум. Лидер найден.A2. Если пришло сообщение two(q), то:1. Если neighbourR больше и q, и maximum, то присвоить maximum значениеneighbourR и послать сообщение one(maximum).2.

Иначе узел становится пассивным.На каждом узле чередуются раунды А1, А2, А1, А2 и т.д., пока не будет найден лидер.Этот протокол неочевиден, его непросто понять и, тем более, невозможно гарантировать безглубокого анализа, что он будет выполнять задачу нахождения единственного лидерамножества процессов при любом числе процессов и любой расстановке их весов. Такаяситуация характерна для параллельных взаимодействующих процессов: мы имеем точноеописание того, что делает каждый процесс, но из этого описания невозможно заключить,выполняется ли некоторое глобальное свойство, которое должно быть обеспечено при работевсех процессов.

Именно поэтому этот пример используется здесь для демонстрации анализа(симуляции и верификации), который может быть выполнен с помощью пакета Spin.Описание модели протокола на языке PromelaКаждому узлу ставится в соответствие процесс типа p. Запускается N таких процессов. Укаждого процесса есть один входящий канал in, через него приходят сообщения от соседапротив часовой стрелки, и один исходящий канал out, в который процесс посылаетсообщения ближайшему соседу по часовой стрелке.Процесс p является активным, если у него флаг Active установлен в true.

Иначе p являетсяпассивным и просто пропускает через себя все получаемые сообщения. Активный процесспосылает свой текущий локальный максимум следующему активному процессу, и получаеттекущий локальный максимум предыдущего активного процесса, используя сообщения типаone. Полученный номер сохраняется в переменной neighbourR, и если процесс невыбывает из числа активных, он будет текущим локальным максимумом p в следующемкруге.

Чтобы определить, остается ли номер neighbourR в кольце, его сравнивают смаксимальным номером maximum, пришедшим в этот процесс, и активным номером,полученным в сообщении типа two. Процесс p посылает сообщение two(neighbourR),чтобы следующий активный процесс мог провести такое же сравнение. Исключениевозникает, когда neighbourR = maximum: в этом случае остался один активный процесс, иоб этом сообщается всем процессам в сообщении winer(nr).Для перевода модели на язык описания Promela сделаны следующие допущения:•пусть каналы между процессами будут не бесконечными, а с глубиной, например, 10,т.е.

как только в канале накопится 10 сообщений, произойдет переполнение канала, иследующие сообщения не смогут в него поступать до того, как освободится место;•ограничимся количеством процессов равным 5, т.к. в языке Promela необходимозадать какое-либо произвольное, но конкретное число процессов;•допустим, что все процессы подключаются одновременно, т.е. никакой процесс неможет включиться в выбор лидера на более поздней стадии.34Модель алгоритма выбора лидера на языке Promela1 #define N 52 #define I 33 #define L 1045 mtype = {one, two, winner};6 chan q[N] = [L] of {mtype, byte};8 byte nr_leaders = 0;/* количество процессов *//* порядковый номер процесса,которому будет присвоено наименьшее значение *//* размер буфера (>= 2*N) *//* 3 возможных типа сообщений *//* массив асинхронных каналов с буферомразмером L *//* переменная, равная количеству процессов,считающих себя лидерами кольца */910 proctype node (chan in, out; byte mynumber) /* определение процесса *//* значение 1 переменной Active показывает,11 { bit Active = 1,что данный процесс активен *//* переменная know_winner показывает,know_winner = 0;что процесс еще не знает, кто лидер */12byte nr, neighbourR, maximum = mynumber;/* объявляется три переменных типаbyte, одной присваивается значениеmynumber */13/* запрашивается эксклюзивный доступ14xr in;к получению сообщений из канала in *//* запрашивается эксклюзивный доступ к посылке15xs out;сообщений по каналу out *//* В Promela, в случае если по алгоритму процесс будет единственным осуществляющим запись в канал (иличтение из канала), для уменьшения числа состояний рекомендуется запросить эксклюзивный доступ на запись(или на чтение), что здесь и сделано.