Вельдер С.Э. и др. Верификация автоматных программ

Подождите немного. Документ загружается.

150

Глава 3. Обзор верификаторов

3.1. SPIN

SPIN [46] – это верификатор, который поддерживает проверку

моделей и разработку систем асинхронных процессов.

В верификаторе SPIN процессы могут взаимодействовать между

собой следующими способами:

 с помощью примитивов rendezvous [46];

 с помощью асинхронных передач сообщений через

буферизованные каналы;

 через общие переменные;

 комбинированным способом.

Кроме собственно верификации, инструментальное средство

поддерживает еще и режимы интерактивной и случайной эмуляции.

При этом запускается интерпретатор модели. Недетерминированные

переходы в режиме интерактивной эмуляции выбираются

пользователем, а в режиме случайной эмуляции выбираются

случайно.

SPIN допускает симуляцию спецификации, написанной на языке

PROMELA (PROtocol Meta-Language) и верификацию некоторых

типов свойств, например, проверку моделей LTL-формул (без

оператора следования X) и верификацию свойств состояний,

недостижимого кода и т. д.

Общая структура инструмента SPIN приведено на рис. 3.1.

Алгоритмы, которые использует SPIN при проверке LTL-формул на

моделях, базируются на конвертации LTL-формулы в автомат Бюхи.

Интерфейс

XSPIN

Promela-

парсер

LTL-парсер

и транслятор

Генератор

верификаторов

Интерактивная

симуляция

Сообщения об

ошибках синтаксиса

Оптимизированный

верификатор

Исполнимая

верификация «на лету»

Контрпримеры

Рис. 3.1. Структура симуляции и верификации с использованием SPIN

Типичный способ работы с инструментальным средством SPIN –

начать со спецификации высокоуровневой модели алгоритма. При

этом обычно используют графическую оболочку Xspin. После

исправления синтаксических ошибок выполняют интерактивную

эмуляцию до тех пор, пока не наступает уверенность, что модель

151

ведет себя, как планировалось. После этого на третьем шаге SPIN

используется для того, чтобы сгенерировать оптимизированную на

лету программу проверки спецификации высокого уровня.

Полученная программа компилируется с возможностью выбора во

время компиляции алгоритмов проверки, которые будут

использоваться. Если обнаруживаются какие-нибудь контрпримеры к

требованиям корректности, то они могут быть возвращены в

интерактивный эмулятор и рассмотрены подробно для того, чтобы

можно было установить и устранить их причину.

Синтаксис языка PROMELA напоминает синтаксис языка C. Модель

на языке PROMELA состоит из следующих элементов:

 объявления типов данных;

 объявления каналов передачи переменных;

 объявления переменных;

 объявления и определения процессов;

 процесса init.

Понятие «процесс» в данном случае отдаленно можно рассматривать

как процедуру, выполняемую в отдельном потоке. Приведем пример

объявления и определения процесса (листинг 3.1):

Листинг 3.1. Объявление и определение процесса

proctype proc(int a; int b)

{

byte b; /* локальная переменная */

/* тело процесса */

}

Процессы могут иметь параметры и локальные переменные. Процесс

может быть запущен в нескольких экземплярах, если для него

используется модификатор active. Запускаются процессы с

помощью модификатора run.

Язык PROMELA имеет пять базовых типов данных:

 bit;

 bool;

 byte;

 short;

 int.

Тело процесса состоит из последовательности операторов. Операторы

могут быть активными либо блокированными. Активный оператор –

это оператор, который может быть выполнен немедленно.

152

Блокированный оператор – оператор, который не может быть

выполнен в данный момент. Такой оператор блокирует выполнение

процесса до тех пор, пока он не станет активным. Например, оператор

x < 7

может быть активен тогда и только тогда, когда x меньше семи.

В противном случае он останавливает выполнение процесса до тех

пор, пока условие не выполнится. Некоторые операторы (например,

оператор присваивания) активны всегда.

Язык PROMELA содержит также операторы ветвления и цикла,

синтаксис которых (листинг 3.2) основан на охранных командах

Дейкстры [47].

Листинг 3.2. Операторы ветвления и цикла

:: guard1 -> S1

:: guard2 -> S2

...

:: else -> Sk

:: guard1 -> S1

:: guard2 -> S2

...

:: else -> Sk

Поясним работу оператора if. Если условие guard

истинно, то

выполняется действие S

. Если одновременно выполняются несколько

условий, то происходит недетерминированный выбор одного из них.

Если все условия ложны, то выполняется действие S

соответствующее else. Конструкция else может отсутствовать.

Тогда в случае, если все условия ложны, выполнение процесса

блокируется до тех пор, пока хотя бы одно из них не начнет

выполняться.

Оператор do имеет такую же форму, как оператор if, с единственной

разницей, что if заменяется на do, а fi на od. Отметим, что

оператор do – это в принципе всегда бесконечный цикл, так как если

все охранные команды блокированы, то он ждет до тех пор, пока одна

из них не станет активной. Выполнение оператора do, таким образом,

может быть прекращено с помощью оператора goto или break.

Язык PROMELA позволяет определять каналы передачи данных.

Процессы могут быть соединены через однонаправленный канал

произвольной (но конечной) емкости. Каналы емкости 0 также

153

разрешены (примитив rendezvous в терминах SPIN). Каналы

специфицируются так же, как и обычные переменные. Например,

chan c = [5] of byte

определяет канал, называемый c, емкостью 5 байт. Канал может быть

рассмотрен как буфер в виде очереди. Посылка сообщения

обозначается восклицательным знаком, прием сообщения –

вопросительным знаком. Пусть c имеет положительную емкость.

Тогда команда c!2 активна, если c не полностью занят. Ее

исполнение помещает элемент 2 в конец буфера. Команда c?x

активна, если c не пуст. Она удаляет голову буфера c и присваивает

ее значение переменной x. Если c не буферизована, то есть имеет

размер 0, то c! (и c?) активна, если имеется команда c? (и c!,

соответственно), которая может быть выполнена в то же время (и

типы параметров соответствуют друг другу). Эта возможность

полезна для моделирования синхронных коммуникаций между

процессами.

Протокол выбора лидера

Рассмотрим использование верификатора на примере протокола

выбора лидера [1, 48]. Пусть имеется N процессов (N ≥ 2) в кольцевой

топологии, соединенных неограниченными каналами. Процесс может

посылать сообщения только по часовой стрелке. Первоначально

каждый процесс имеет уникальный идентификатор ident, который

ниже предполагается натуральным числом. Цель протокола выбора

лидера в получении уверенности, что ровно один процесс становится

лидером. Также задано дополнительное условие: процесс с

наивысшим идентификатором должен быть выбран лидером.

Объяснение заключается в том, что идентификатор процесса отражает

его возможности, и желательно, чтобы процесс с максимальными

возможностями выиграл выборы. В протоколе каждый процесс в

кольце выполняет следующую задачу (листинг 3.3):

Листинг 3.3. Протокол выбора лидера

active:

d = ident;

while (true)

{

send(d);

receive(e);

if (e == d) stop; // Процесс d является лидером

send(e);

receive(f);

if e >= max(d, f)

{

154

d = e;

}

else break;

}

relay:

while (true)

{

receive(d);

send(d)

}

Из рассмотрения протокола следует, что первоначально каждый

процесс активен (active). В течение того времени, пока он активен,

процесс отвечает за определенное процессное число (сохраненное в

переменной d). Это значение может изменяться в ходе работы

протокола. Когда процесс определяет, что он не несет идентификатор

текущего лидера, он начинает уступать. Если процесс уступает (relay),

он передает сообщения слева направо прозрачным способом – без

просмотра или модификации их содержимого.

Каждый активный процесс посылает свою переменную d своему

соседу по часовой стрелке и потом ждет до тех пор, пока не получит

значение (e) от своего ближайшего активного соседа против часовой

стрелки. Если процесс получает свое собственное значение d, он

заключает, что остался единственный активный процесс и что это d в

действительности является идентификатором нового лидера, и

прекращает работу. (Отметим, что процесс сам по себе не обязан

становиться новым лидером!) В случае если принято другое значение

(e ≠ d), процесс ждет второго сообщения (f), содержащего значение d,

которое несет второй ближайший активный сосед против часовой

стрелки. Если значение ближайшего активного соседа против часовой

стрелки наибольшее среди e, f и d, то процесс обновляет свое

локальное значение (d := e). В противном случае он начинает

уступать. Таким образом, из любого множества активных соседей

один будет уступать в каждом раунде.

Для того чтобы проиллюстрировать, как работает протокол,

рассмотрим пример его запуска для четырех процессов с

идентификаторами 1 — 4, как показано на рис. 3.2. Здесь процессы

обозначаются вершинами, а коммуникационные каналы – стрелками.

Содержимое канала указано в метке возле стрелки, точка с запятой

используется для разделения различных сообщений. Каждая вершина

помечена тройкой, содержащей значения локальных переменных d, e

и f. Черная вершина обозначает, что процесс уступает, в противном

случае он активен.

155

(2,-,-)

(3,-,-)

(1,-,-)

(4,-,-)

(2,-,-)

(3,-,-)

(1,-,-)

(4,-,-)

(2,4,-)

(3,-,-)

(1,-,-)

(4,-,-)

2; 4

(2,4,-)

(3,-,-)

(1,-,-)

(4,1,-)

(4,4,1)

(3,2,-)

(1,3,-)

(4,1,-)

(4,4,1)

(3,2,4)

(1,3,-)

(4,1,3)

2; 4

(4,4,1)

(3,2,4)

(3,3,2)

(4,1,3)

(4,4,1)

(4,2,4)

(3,3,2)

(4,1,3)

(4,3,1)

(3,2,4)

(3,4,2)

(3,1,3)

(4,3,4)

(3,2,4)

(4,4,3)

(4,1,3)

Рис. 3.2. Пример запуска протокола выбора лидера

Моделирование протокола выбора лидера на языке PROMELA

Спецификация PROMELA состоит из трех частей (листинг 3.4):

определения глобальных переменных, описания поведения процесса в

кольце и инициализационной секции, в которой процессы стартуют.

Поведенческая часть процесса process в действительности

получается прямым переводом описания протокола, приведенного

выше. В протокол добавлены два комментария, выводящихся на экран

для упрощения симуляции. Процесс соединен со своим соседом

против часовой стрелки через канал in, и через канал out – со своим

соседом по часовой стрелке.

Листинг 3.4. Протокол выбора лидера на языке PROMELA

proctype process (chan in, out; byte ident)

{ byte d, e, f;

printf("%d\n", ident);

activ:

d = ident;

do :: true -> out!d;

in?e;

156

if :: (e == d) ->

printf("%d является лидером\n", d);

goto stop

:: else -> skip

fi;

out!e;

in?f;

if :: (e >= d) && (e >= f) -> d = e

:: else -> goto relay

od;

relay:

end:

do :: in?d -> out!d

od;

stop:

skip

}

Процесс может быть в одном из трех состояний: activ («active» не

используется, так как это зарезервированное служебное слово в

PROMELA), relay и stop. Процесс может достичь состояния stop,

только если он распознал нового лидера. Процесс, который не

распознал лидера, завершится в состоянии relay. Во избежание

генерации неверного завершающего состояния (состояния, которое не

является концом тела программы и которое не помечено меткой

«end:») пометим состояние relay как завершающее. Если пытаться

верифицировать вышеуказанную спецификацию PROMELA без этой

метки end:, то SPIN нашел бы неверное завершающее состояние и

выдал ошибку.

Отметим, что, например, оператор in?e выполним, только если канал

in не пуст. Если канал пуст, то оператор блокирован, и выполнение

процесса приостановлено до тех пор, пока он не станет выполнимым.

Следовательно, in?e должно читаться следующим образом: ждать,

пока сообщение не попадет в канал in, и затем поместить его

значение в переменную e.

Спецификация PROMELA начинается с определения глобальных

переменных (листинг 3.5):

Листинг 3.5. Глобальные переменные спецификации на языке PROMELA

#define N 5 /* число процессов */

#define I 3 /* процесс с наименьшим идентификатором */

#define L 10 /* размер буфера (>= 2*N) */

/* N каналов емкостью L каждый */

chan q[N] = [L] of { byte };

157

Константа I используется только с целью инициализации. Она

определяет процесс, который будет обладать наименьшим значением

ident. Емкость L соединяющих каналов должна быть как минимум

2N, так как каждый процесс посылает максимум два сообщения в

каждом раунде выборов. Так как сообщения в протоколе выбора

лидера несут только один параметр (идентификатор процесса), то

каналы с q[0] по q[N–1] могут содержать элементы типа byte.

Для того чтобы создать топологию кольца и запустить экземпляры

процессов в кольце, используется конструкция init. Эта часть

спецификации PROMELA имеет следующий вид (листинг 3.6):

Листинг 3.6. Запуск экземпляров процессов

init {

byte i;

atomic {

i = 1;

do :: i <= N -> run process (q[i-1],

q[i%N], (N+I-i)%N+1);

i = i+1

:: i > N -> break

}

Здесь %N обозначает остаток по модулю N. Процесс запускается с

определенными фактическими параметрами оператором

run process(). Первый параметр процесса – это входящий канал,

второй параметр – выходящий канал, а третий параметр – его

идентификатор. Существуют, конечно, различные механизмы

присвоения идентификаторов процессам, здесь просто выбран один из

самых простых. Предполагается, однако, что каждый процесс

получает уникальный идентификатор. Это необходимо для

корректности алгоритма. С целью обеспечить всем процессам

возможность стартовать одновременно, воспользуемся конструкцией

atomic. Она защищает запуски процессов от того, чтобы исполнять

тело процесса, пока другие процессы еще не созданы.

Отметим, что здесь фиксировано одно индивидуальное присвоение

идентификаторов процессам. Результаты, которые получены

симуляцией и верификацией, верны только для этого присвоения.

С целью увеличения надежности протокола должны быть проверены

другие (фактически, все возможные) присвоения. Другая возможность

состоит в том, чтобы написать фрагмент на языке PROMELA, который

присваивает процессам идентификаторы случайно.

158

PROMELA-спецификация, полученная таким способом, может быть

теперь верифицирована. При этом не будет недостижимого кода или

блокировок. Для того чтобы улучшить понимание того, как работает

протокол, может быть выполнена (случайная, управляемая или

интерактивная) симуляция.

Проверка моделей для спецификации на языке PROMELA

Самое важное свойство, которым должен обладать протокол выбора

лидера, состоит в том, что он не должен позволять более чем одному

процессу становиться лидером. Это выражается в LTL как

G [#leaders ≥ 2],

или, эквивалентно,

G[#leaders ≤ 1].

Это свойство проверяется инструментом SPIN следующим образом.

Определяется формула []p, где [] соответствует G, а p определяется

так:

#define p (nr_leaders <= 1)

Здесь nr_leaders – вспомогательная глобальная переменная в

спецификации PROMELA, которая отслеживает число лидеров

в системе. Спецификация PROMELA на данном этапе должна быть

расширена следующим образом (листинг 3.7):

Листинг 3.7. Новая спецификация PROMELA

byte nr_leaders = 0;

proctype process (chan in, out; byte ident)

{ .....как раньше.....

activ:

d = ident;

do :: true -> out!d;

in?e;

if :: (e == d) ->

printf("%d является лидером\n", d);

nr_leaders = nr_leaders + 1;

goto stop

:: else -> skip

fi;

.....как раньше.....

}

Свойство [] p автоматически конвертируется средством SPIN в

размеченный автомат Бюхи. Автомат, полученный верификатором

SPIN, имеет следующий вид (листинг 3.8):

159

Листинг 3.8. Автомат Бюхи

* Введенная формула: [] p

* Ниже условие claim соответствует

* отрицанию исходной формулы !([] p)

* (формализующему нарушение свойства)

never { /* !([] p) */

T0_init:

:: (1) -> goto T0_init

:: (! ((p))) -> goto accept_all

fi;

accept_all:

skip

}

Напомним, что автомат Бюхи соответствует отрицанию проверяемой

формулы – A

φ

, где φ соответствует G[#leaders ≤ 1]. Если это свойство

сохранено в файле property1, то SPIN автоматически проверит его,

если добавить в конец (или начало) спецификации PROMELA

инструкцию:

#include "property1"

Результат верификации свойства положительный (листинг 3.9).

Листинг 3.9. Результат верификации протокола выбора лидера

Full state space search for:

never-claim +

assertion violations + (if within scope of claim)

cycle checks – (disabled by –DSAFETY)

invalid endstates – (disabled by never-claim)

State-vector 140 byte, depth reached 155, errors: 0

16585 states, stored

44589 states, matched

61174 transitions (= stored+matched)

18 atomic steps

hash conflicts: 1766 (resolved)

(max size 2^19 states)

Stats on memory usage (in Megabytes):

2.388 equivalent memory usage for states

(stored*(State-vector + overhead))

2.046 actual memory usage for states (compression: 85.65%)

State-vector as stored = 119 byte + 4 byte overhead

2.097 memory used for hash-table (-w19)

0.200 memory used for DFS stack (-m10000)

4.448 total actual memory usage