Описание предложенного метода верификации

Для того чтобы провести верификацию программы при помощи верификатора Spin[73, 74], требуется создать модель программы на языке Promela[73, 74]и формализовать требуемые свойства (спецификацию) на языке линейной темпоральной логики (LTL).

Обозначим автоматный тип - AType, автоматный объект - aObject. Пусть для автоматного типа ATypeсостояния s₀, s₁и т. д., а события - e₀, e₁и т. д. Переменные этого автомата - x₀, x₁и т. д., а внешние воздействия (второго типа - вызываемые функции) z0, z1и т. д. Пусть автоматный тип ATypeимеет вложенный автомат nested. Пусть ATypeзапускает автомат fork.

Метод верификации состоит из следующих этапов:

1. Генерация кода на языке Promela [4].

2. Преобразование LTL-формул.

3. Запуск верификатора Spin.

4. Преобразование контрпримера.

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

3.2.1. Построение Spin-модели для управляющего автомата

Этап 1. Подготовка данных

Все состояния каждого автоматного типа нумеруются, и для них создаются константы. Для каждого автоматного типа состояния нумеруются отдельно. Имя константы состоит из имени автоматного типа и имени состояния, разделённых знаком подчеркивания. Это сделано для того, чтобы состояния разных автоматов с одинаковыми именами не конфликтовали друг с другом. Пример:

#define AType_s0 0

#define AType_s1 1

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

#define e0 1

#define el 2

Все выходные воздействия второго типа (вызываемые функции) нумеруются, и для них создаются константы аналогично состояниям.

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

Для каждого типа автоматов создаётся следующая структура:

• byte state - номер текущего состояния;

• byte curEvent - номер обрабатываемого события;

• byte ID - номер автомата;

• byte functionCall - номер последней запущенной функции, если такая есть;

• byte nestedMachine - номер текущего вложенного автомата, если такой есть;

• все переменные автомата.

Для каждого автомата создаётся экземпляр этой структуры.

Этап 2. Моделирование шага автомата

Для каждого автоматного типа создаётся функция, которая моделирует один шаг работы автомата

inline Machine(machine, evt),

где machine - это переменная соответствующего автоматного типа, а evt - событие при входе в состояние.

Переходы записывается при помощи охранных команд Дейкстры [77] - охранных условий. На листинге 3.2.1.1 приведён код на Promelaдля перехода из состояния s₁в s₂по событию e₁с выходным воздействием z₁.При этом (evt == el) - охранное условие.

Листинг 3.2.1.1. Переход автомата из состояния s₁в s₂по событию e₁

if(machine.state == sl)

if

::((evt == e1)) ->

machine.curEvent = el;

machine.state = s2;

machine.functionCall = 1;

::((evt == e2)) ->

fi

fi

Если переход на графе помечен условием, то оно дописывается к охранному условию. На листинге 3.2.1.2 приведён код на Promela,который моделирует условие v₁> 0 (на переходе из листинга 3.2.1.1).

Листинг 3.2.1.2. Условие v₁> 0 на переходе

if

::((evt == e1) &&(machine.v1 > 0)) ->

machine.curEvent = e1;

machine.state = s2;

machine.functionCall = 1;

fi

3.2.2.

Все вложенные автоматы нумеруются.

Пусть автомат A₂вложен в состояние s₂автомата A₁. Так как переход автомата A₂осуществляется, когда пришло событие, по которому нет перехода в автомате A₁,то переход дописывается при помощи охранного условия else:

:: else ->

machine.nestedMachine = a2_call;

A2(a2, evt);

где evt - событие, которое пришло на вход автомату A1.

3.2.3. Построение Spin-модели для параллельных автоматов

Для каждого автомата создаётся канал, по которому происходит передача событий. Каналу присваивается имя _ch. Канал для автомата a₁будет называться a1_ch.

Для каждого автомата, кроме вложенных, создаётся процесс, который извлекает из канала событие и запускает функцию перехода автомата с этим событием. На листинге 3.2.3.1 приведён процесс c автоматом a₁типа A₁.

Листинг 3.2.3.1. Процесс с автоматом a₁

proctype a1Proc ()

{

byte newEvt;

a1.started= true;

a1_ch ? newEvt;

a1ParamChange();

do

:: a1.finished == false ->

a1_ch ? newEvt;

A1(a1, newEvt);

:: else -> skip;

od;

}

Жирным выделен запуск функции, моделирующей шаг автомата. Построение функции описано во втором этапе раздела 3.2.1.

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

Для публичных переменных перед каждым шагом автомата вызывается функция, которая их недетерминированно изменяет. Этой функции присваивается имя VolatileChange. На листинге 3.2.3.2 для автомата a1приведена функция для изменения массива b, состоящего из пяти четырёхбайтных элементов (массивы используются для того, чтобы верифицировать автоматы Stateflow).

Листинг 3.2.3.2. Функция изменения переменных для автомата a₁

inline a1VolatileChange()

{

int r;

int ind = 0;

do

:: ind < 5 ->

random(r, 32);

a1.b[ind] = r;

ind = ind + 1;

:: else -> break;

}

Для переменных-параметров автомата строится аналогичная функция, которая вызывается один раз при его запуске.

Множество отношений σ,описывающих запуск автоматов, кодируется следующим образом: пусть автомат a₁запускает автомат a₂в состоянии s₁. Тогда в модель дописывается следующий код:

assert (!a2.started);

run a2Proc();

Множество отношений р, описывающих коммуникацию между автоматами, кодируется следующим образом: пусть автомат a1отправляет событие e₂на переходе в состояние s₂по событию e₁автомату a₂.Тогда в код соответствующего перехода в функции, моделирующей шаг автомата a1, дописывается отправка события e₂в канал автомата a₂(листинг 3.2.3.3).

Листинг 3.2.3.3. Коммуникация между автоматами

if

::((evt == e1)) ->

machine.state = A1_s2;

machine.curEvent = e1;

sendEvt = e1;

a2_ch ! sendEvt;

:: ... ->

fi;

Множество отношений ω,описывающих совместно используемые переменные, моделируется так: пусть переменная x1автомата a1является

входной переменной x₂автомата a₂.Тогда на каждом переходе автомата a₁ дописывается следующая инструкция:

a2.x2 = x1;

На рисунке 3.2.3.1 схематически изображена модель параллельных иерархических автоматов.

Рисунок 3.2.3.1. Модель параллельных иерархических автоматов

Основные компоненты модели:

• A_i- процессы, содержащие автоматы. Каждый процесс содержит один автомат. Процесс состоит из цикла, который принимает события при помощи каналов Spinи запускает функцию, реализующую шаг автомата. Каждая функция реализует один автоматный тип и принимает на вход автомат и событие.

• init- процесс, запускающий процессы A_i.

• S_i- процессы-модели поставщиков событий.

• X_i- переменные автоматов.

3.2.4. Преобразование LTL-формул

Расширим нотацию LTL-формул верификатора Spin.В фигурных скобках будем записывать высказывания в терминах рассматриваемой автоматной модели. Перечислим эти высказывания:

• aObject.si - автомат aObjectперешёл в состояние s_i.

• aObject.ei - в автомат aObjectпришло событие e_i.

• aObject.zi - автомат aObjectвызвал функцию (выходное воздействие) zi.

• aObject->nested - автомат aObjectпередаёт управление вложенному автомату nested.

• aObject || fork - автомат aObjectзапустил автомат fork.

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

aObject.x0 >= fork.x0[fork.x1].

Пример LTL-формулы в расширенной нотации:

[] ({aObject.x0