Описание метода верификации однопоточных автоматов и инструментального средства Converter

В рамках бакалаврской работы [20]и магистерской диссертации [32]автором был разработан метод верификации однопоточных автоматных программ, написанных при помощи инструментального средства Unimod[81], позволяющего реализовывать систему вложенных автоматов.

3.6.1. Описание метода

Идея метода состоит в следующем:

1. Построить модель системы графов переходов автоматной программы на языке Promela.

2. Преобразовать LTL-формулу с требованиями к автоматной программе к виду, который понятен верификатору Spin.

3. Построенную модель и формулу подать на вход верификатору Spin.

4. Проанализировать отчёт, выданный верификатором Spin, и построить контрпример.

Опишем метод построения модели.

5. Подготовка исходных данных.

5.1. Для каждого автомата Ai завести переменную stateAi, в которой будет храниться номер текущего состояния. На языке Promelaэто описывается следующим образом:

int stateAi;

5.2. Для каждой пары автоматов (Ai, Aj) завести два канала передачи сообщений. На языке Promelaэто описывается следующим образом:

chan AiAj = [1] of {byte};

chan AjAi = [1] of {byte};

5.3. Завести два канала передачи сообщений для процесса, который эмулирует источник событий:

chan epin = [1] of {byte};

chan epout = [1] of {byte};

5.4. Завести одну переменную для событий:

int lastEvent;

5.5. Завести две переменных для выходных воздействий:

int o;

int z;

5.6. Каждому состоянию присвоить уникальный номер, используя сквозную нумерацию для всех автоматов. Переход в новое

состояние с номером k будет осуществляться присвоением переменной StateAi числа k:

StateAi = k;

5.7. Событие exx (xx - номер события) на переходе между состояниями описывается в модели следующим кодом:

lastEvent = xx;

6.

6.1. Для каждого автомата Ai создать процесс. На языке Promelaэто записывается следующим образом:

active proctype Ai() {

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

}

Модификатор active означает, что процесс будет запущен в начальном состоянии модели.

6.2. Для каждого автомата Ai в теле созданного процесса выполнить шаги 2.3 - 2.18.

6.3. Определить переменную x для приема сообщений от других процессов и переменную y, в которой будет храниться номер процесса, от которого получено сообщение:

byte x;

byte y;

6.4. Для стартового автомата: инициализировать переменные o и z значением -1:

o = -1; z = -1;

6.5. Определить начальное (стартовое) состояние s. Присвоить:

StateAi = S;

6.6. Для всех автоматов, кроме стартового: ждать, пока данному процессу не придёт сообщение; в переменную yзаписать номер автомата, приславшего сообщение; на языке Promelaэто записывается следующим образом:

::A1Ai ? x ->

y = ¹;

::A2Ai ? x ->

y = 2;

::AnAi ? x ->

y = n;

fi;

6.7. Для всех автоматов, кроме стартового, построить цикл:

do

::(x == 1) ->

::(x == 9) ->

break;

od;

Здесь сообщение о запуске автомата имеет номер 1, а сообщение о завершении работы системы имеет номер 9.

6.8. Построить цикл:

do

::(stateAi == s1) ->

printf("State Ai l : Имя состояния\п");

::(stateAi == s2) ->printf("State 2 : Имя состояния\п");

::(stateAi == sk) ->printf("State k : Имя состояния\п"); od;

Здесь s 1, ..., sk - номера состояний автомата Ai.

Инструкция printf аналогична соответствующей инструкции из языка C.Пометка используется в дальнейшем для восстановления контрпримера. Для всех автоматов, кроме стартового, этот цикл записывается в условие (x == 1) цикла, построенного на шаге

2.6.

6.9. Если состояние содержит выходные воздействия, то для каждого выходного воздействия oi.zj записать следующее:

printf("Action oi.zj\n");

o = i;

z = j;

o = -1;

z = -1;

6.10.

Ai_STATE_j:

6.11. Оповестить источник событий. Для этого требуется по каналу epin отправить число 1. На языке Promelaэто описывается следующим образом:

epin ! 1;

6.12. Ждать ответ. Если текущий автомат - стартовый, то ждать пока по каналу epout от источника событий придёт число 1. На языке Promelaэто записывается следующим образом:

epout ? 1;

Если текущий автомат не является стартовым, то выполнить шаг

2.6.

6.13. Для каждого состояния sj найти все возможные переходы (sj, sl) из него. К условию (stateAi == sj) дописать конструкцию if, а для каждого перехода (sj, sl) дописать в конструкции if следующее:

::условие ->

printf("Going to state Ai l : "); stateAi = sl;

Условием может быть наступление события, условие на состояния автоматов и т. д.

6.14. Если в некоторое состояние sj вложен автомат Am, то дописать в условие (stateAi == sj) передачу сообщения на запуск автомата Am для процесса этого автомата и ждать завершения и

сообщения от поставщика событий (если текущий автомат - стартовый) либо сообщения от другого автомата (если текущий автомат не является стартовым):

AiAm ! 1;

if

::AmAi ? x;

::eoput ? 1 ->

goto Ai_STATE_sj;

fi;

либо

AiAm ! 1;

if

::A1Ai ? x ->

y = 1;

::A2Ai ? x ->

y = 2;

::AnAi ? x ->

y = n;

fi;

6.15. Если состояние st - конечное, то в условие (stateAi == st) дописать инструкцию завершения цикла:

break;

6.16. Для всех автоматов, кроме стартового: после цикла, построенного на шаге 2.7 дописать отправку сообщения о завершении работы автомата Ai процессу автомата, который запустил автомат Ai.На языке Promelaэто записывается следующим образом:

if

:: y = 1 ->

A1Ai ! x;

:: y = 2 ->

A2Ai ! x;

:: y = n ->

fi;

6.17. Для всех автоматов, кроме стартового, ждать, пока данному процессу не придёт сообщение. Выполнить шаг 2.6.

6.18. Для стартового автомата.

AiA1 ! 9;

AiA2 ! 9;

AiAn ! 9;

epin ! 9;

6.19. Дописать в модель источник событий.

active proctype eventProvider() {

byte x;

do

::epin ? 1 ->

if

::lastEvent = 0;

::lastEvent = M;

::lastEvent = -1;

fi;

epout ! 1;

::epin ? 9 ->

lastEvent = -1;

epout ! 9;

break;

od;

}

Здесь все события имеют номера от 0 до M.Минус единица означает, что никакого события не произошло.

6.17. Дописать в модель требования (проверяемые свойства), преобразованные с помощью верификатора Spinс языка LTLна язык Promela.

Этот метод был доработан для многопоточных программ (см. разделы 3.1 - 3.5).

3.6.2. Описание инструментального средства Converter

Converterявляется практической реализацией описанного выше метода верификации автоматных программ и позволяет проводить верификацию программ указанного класса с высоким уровнем автоматизации.

По автоматной программе Converterсоздает модель, в которой отброшены несущественные детали. LTL-формула преобразовывается в пригодный для верификатора Spinвид.

При построении модели используются:

• графы переходов автоматов;

• взаимодействие автоматов по вложенности;

• выходные воздействия, обозначаемые, как z с соответствующими индексами;

• события на переходах.

Построенная модель абстрагируется от следующих сущностей:

• входных переменных, обозначаемых, как xс соответствующими индексами;

• выходных переменных, обозначаемых, как yс соответствующими индексами.

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

Инструментальное средство принимает следующие входные параметры:

• путь к XML-описанию автоматной программы;

• имя файла, в который инструментальное средство сохранит построенную модель;

• LTL-формулу;

• имя файла, в который инструментальное средство сохранит отчёт о проведённой верификации.

Если LTL-формула не была задана, то верификация проводиться не будет. В этом случае Converterтолько построит модель автоматной программы.

Если не был задан какой-то из остальных параметров, то инструментальное средство использует значение по умолчанию. В частности, если не был задан путь к XML-описанию автоматной программы, Converter будет использовать в качестве входного файла A1.xml.

Для построения LTL-формул используются следующие переменные:

• stateAiдля проверки условий на состояние автомата Ai;

• lastEventдля проверки условий на произошедшие события;

• Две переменные oи zдля проверки условий на выходные воздействия.

Переменная о используется для обозначения номера объекта управления, переменная zиспользуется для обозначения индекса выходного воздействия.

3.6.2.1. Архитектура Converter

Первичное отображение

В первичном отображении представлены диаграмма классов (рисунок 3.6.2.1.1) и представление декомпозиции на модули в виде диаграммы компонентов (рисунок 3.6.2.1.2).

Рисунок 3.6.2.1.1. Диаграмма классов

Рисунок 3.6.2.1.2. Диаграмма компонентов

Каталог элементов

Каталог элементов приведён в таблице 3.6.2.1.1.

Таблица 3.6.2.1.1. Каталог элементов

3.6.2.2. Пользовательский интерфейс

Инструментальное средство Converter 2.0запускается в пакетном режиме и имеет консольный пользовательский интерфейс. Командная строка для запуска инструментального средства выглядит следующим образом:

Converter [список ключей].

Входные параметры задаются при помощи следующих ключей:

• -s - задать путь к Х\//.-описанию автоматной программы. Если данный параметр отсутствует, то будет использоваться значение по умолчанию A1.xml.

• -m - задать путь к файлу, в который будет сохранена построенная модель. Если данный параметр отсутствует, то будет использоваться значение по умолчанию model.ltl.

• -r - задать путь к файлу, в который будет записан отчёт о проведённой верификации. Если данный параметр отсутствует, то будет использоваться значение по умолчанию report.txt.

• -f - задать LTL-формулу. Если параметр отсутствует, то верификация не проводится.

• -h - вывести справку и завершить работу.

3.6.2.3. Обратное преобразование контрпримера

Инструментальное средство Converterна выходе выдает текстовый файл с отчетом, в котором содержатся полные сведения о проведённой верификации. В начале отчета содержатся общие сведения о сгенерированной модели Крипке, о режиме работы верификатора, об использованной памяти, о числе ошибок в модели (если они есть) и т. д. Если модель не удовлетворяет LTL-формуле, в отчете будет следующая запись:

pan: claim violated!

Если модель не содержит ошибок, то в отчете будет строка следующего вида:

State-vector 24 byte, depth reached 0, errors: 0.

Верификатор Spinвыдает контрпример в виде пути в модели, описанной на языке Promela. Опишем, как из него вернуться к автоматной программе.

Строка отчета

StateAk s :

(stateAk- состояние автомата Ak, s- номер состояния) обозначает вход автомата Akв состояние s.

Строка отчета

Going to StateAk s :

(stateAk- состояние автомата Ak, s- номер состояния) обозначает переход автомата Akиз текущего состояния в состояние s.

Строка отчета

Event = exx

(exx- некоторое событие) обозначает, что был совершен переход по событию

exx.

Строка отчета

Action oi.zj

обозначает, что было вызвано выходное воздействие zjобъекта управления oi.

Таким образом, строится путь в автоматной модели из файла отчета, выданного инструментом Converter.

Основным ограничением данного метода является отсутствие поддержки многопоточных систем. Поэтому был разработан усовершенствованный метод верификации.

3.7.