Режимы верификации и спецификации Spin

После генерации формальной модели на языке Promela из среды Engee пользователю доступна возможность проверки ее корректности с помощью инструмента Spin.

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

В данной статье описаны основные режимы Spin: симуляция и верификация, а также порядок добавления спецификаций LTL, генерации верификатора, анализа результатов и поиска контрпримеров.

Ниже рассмотрены основные режимы работы Spin и практические шаги по верификации моделей, сгенерированных из Engee.

Spin: режим симуляции

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

Для полученного путем генерации кода из модели Engee файла Promela можно немедленно запустить симуляцию модели средствами Spin:

spin <имя-файла.pml>

Если попытаться выполнить эту операцию с файлами Promela, полученными напрямую от генератора кода Engee, то это приведет к бесконечному выполнению spin, так как генерируемая Promela-модель содержит бесконечный цикл.

В то же время этот режим запуска spin может быть полезен для исследования свойств модели путем добавления в исходный текст Promela инвариантов (assertions) и операторов генерации значений входных данных.

Spin: режим верификации

Наиболее полезный режим использования программы Spin — порождение программы-верификатора. Режим верификации используется для строгой проверки логических свойств модели (LTL-спецификаций) и поиска возможных ошибок или противоречий

Верификатор — это программа на языке Си, и ее жизненный цикл состоит из дополнения текста модели на языке Promela спецификацией, генерации и компиляции программы-верификатора, а также тестовых запусков и анализа сообщений пользователем.

Вставка спецификаций

Наиболее простой способ передать программе Spin логические формулы спецификации — добавить их в конец файла Promela-модели в виде одного или нескольких операторов языка Promela ltl:

...
описание модели
...
ltl spec_name_1 { ... текст формулы ... }
ltl spec_name_2 { ... текст формулы ... }
...
ltl spec_name_3 { ... текст формулы ... }

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

Например, формулы

ltl spec1 { !promela_a_S.Chart.state.A.is_active }
ltl spec2 { <>promela_a_S.Chart.state.A.is_active }
ltl spec3 { !promela_a_S.Chart.state.is_active }
ltl spec4 { [] (!promela_a_S.Chart.state.is_active U promela_a_S.Chart.state.A.is_active) }

могут быть переписаны как

#define a promela_a_S.Chart.state.A.is_active
#define chart promela_a_S.Chart.state.is_active

ltl spec1 { !a }
ltl spec2 { <>a }
ltl spec3 { !chart }
ltl spec4 { [] (!chart U a) }

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

Приведенный выше пример не следует начинать с определения макроса с именем state, так как этот идентификатор уже используется внутри составных имен promela_a_S.Chart.state.A.is_active и promela_a_S.Chart.state.is_active. Аналогично не стоит использовать макрос с именем U, поскольку это обозначение зарезервировано под оператор LTL until, применяемый в формулах примера.

Генерация и запуск верификатора

Существует два основных подхода к генерации и запуску верификатора с помощью программы Spin: совмещенный и раздельный.

Общим предварительным условием для успешного выполнения верификатора в обоих случаях является наличие установленного компилятора языка Си, поддерживающего стандарт ISO C99 или выше.

Совмещенные генерация и запуск верификатора

Утилита Spin может выполнять роль оболочки, которая:

Преобразует .pml-файл Promela-модели в промежуточные файлы на языке Си;
Вызывает компилятор для трансляции промежуточных Си-файлов в двоичный исполняемый файл верификатора с именем pan и запускает его в режиме верификации модели.

Командная строка img 41 1 2 для режима совмещенной генерации и запуска должна содержать параметр -run. Пример команды:

spin -run <путь-к-файлу-модели.pml>

Если файл Promela-модели содержит только один оператор ltl, то этой командной строки достаточно, чтобы запустить верификацию формулы, заданной в операторе ltl.

Если же файл Promela-модели содержит более одного оператора ltl, то при запуске этой командной строки будет верифицирована формула первого по порядку оператора.

Чтобы выбрать, какая из формул будет верифицироваться при запуске spin -run, следует дополнительно указать параметр -ltl с именем оператора ltl.

Например, если файл Promela-модели имеет путь ./model.pml и оканчивается блоком операторов:

ltl spec1 { []a }
ltl spec2 { <>b }

то вызов:

spin -run ./model.pml

сгенерирует и выполнит верификатор формулы []a с именем spec1. А чтобы сгенерировать и выполнить верификатор для формулы <>b с именем spec2, нужно вызвать:

spin -run -ltl spec2 ./model.pml

В режиме совмещенной генерации и запуска Spin не сохраняет промежуточные файлы на языке Си. После успешного выполнения программы в текущей директории автоматически создается исполняемый файл верификатора с именем pan (в UNIX-подобных системах). Этот файл можно использовать для повторных запусков верификатора, например, чтобы проверить формулы, которые еще не были верифицированы.

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

Когда программа Spin используется в режиме раздельных генерации и запуска верификатора, ее основная задача — преобразование модели на языке Promela в исходный код верификатора на языке Си. Предполагается, что пользователь самостоятельно скомпилирует промежуточные Си-файлы и запустит полученный верификатор.

Раздельная генерация верификатора

Типичная командная строка для генерации исходного кода верификатора на языке Си:

spin -a <имя модели.pml>

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

В результате успешной генерации Spin создает или перезаписывает файлы с именами pan.c, pan.h, pan.b, pan.m и pan.t (эти имена являются фиксированными, настройка Spin для их смены не предусмотрена). Как минимум два из них — pan.c и pan.h — необходимы для следующего шага.

Компиляция верификатора

Для дальнейшей трансляции файлов, полученных на предыдущем шаге, требуется компилятор языка Си, поддерживающий стандарт ISO C99 или выше. Командная строка для компиляции может выглядеть так:

cc pan.c -o <результирующий-файл>

Или, если верифицируемая формула содержит оператор neXt (подробнее см. Временная логика линейного времени (LTL) в Spin:

cc -DNXT -DNOREDUCE pan.c -o <результирующий-файл>

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

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

Пример командной строки, когда исполняемый файл верификатора имеет имя pan:

./pan -a

Параметров этой командной строки достаточно, если файл Promela-модели не содержит операторов ltl или содержит только один такой оператор.

Если же операторов ltl несколько, то требуется выбрать единственную формулу, которую собираемся верифицировать. Для этого требуется указать параметр -N с именем оператора ltl.

Например, если в файле Promela-модели есть оператор ltl spec1 { … }, то верификация выполняется с помощью команды:

./pan -a -N spec1

Анализ сообщений верификатора

Если верификатор выполняет проверку LTL-формулы спецификации, то информация об успехе или ошибке верификации следует искать в сообщениях, выдаваемых верификатором на консоль и начинающихся со строки:

<имя-исполняемого-файла-верификатора>: ltl formula <имя-оператора-ltl>

Успешная верификация

В случае успешной верификации, если исполняемый файл верификатора имеет имя по умолчанию pan, а верифицируется оператор ltl с именем spec1, то результат успешной верификации выглядит так:

pan: ltl formula spec1
...
State-vector ... byte, depth reached ..., errors: 0
...

Выше следует обратить внимание на сообщение errors: n, где n в случае успешной верификации равняется нулю.

Ошибка верификации

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

<имя-верификатора>: ltl formula <имя-оператора-ltl>
<имя-верификатора>:1: assertion violated ... (at depth ...)
<имя-верификатора>: wrote <имя-файла-модели>.trail
State-vector ... byte, depth reached ..., errors: 1

Например, если имя файла модели — model.pml, исполняемый файл верификатора имеет имя по умолчанию pan, а верифицируется оператор ltl с именем spec2:

ltl spec2 { []a }

то результат ошибки верификации может выглядеть так:

pan: ltl formula spec2
pan:1: assertion violated  !( !(a)) (at depth 0)
pan: wrote model.pml.trail
...
State-vector 20 byte, depth reached 5, errors: 1
...

Ошибка нехватки памяти

Кроме того, в случае больших моделей использования большого количества переменных и/или переменных «широких» типов short или int, в результате роста пространства состояний верификатору может не хватить предоставленной ему памяти. В этом случае об ошибке могут сигнализировать сообщения вида:

pan: out of memory

или

error: max search depth too small

Если последнее в некоторых случаях можно обойти с помощью параметра -m N, например:

spin -run -m10000000 model.pml

то первое чаще всего свидетельствует о том, что модель нуждается в огрублении, так как ее пространство состояний слишком велико для анализа с помощью spin.

Поиск контрпримера

Консольная выдача верификатора в примере неудачной верификации, приведенном выше, содержит строку:

pan: wrote model.pml.trail

Это строка свидетельствует о том, что в ходе верификации был создан файл трассы model.pml.trail.

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

Минимальная командная строка Spin для анализа трассы:

spin -t -p -g -l -k <имя-файла-трассы.trail> <имя-файла-модели.pml>

Например, файл модели model.pml содержит текст простой модели:

bool a = true;          /* объявление глобальной логической переменной "a",
                         * инициализированной значением "true"
                         */
active proctype fsm() { /* объявление типа процесса "fsm" и его немедленный запуск */
    do                  /* оператор недетерминированного бесконечного цикла */
    :: a = true;        /* первая возможная ветка цикла */
    :: a = false;       /* вторая возможная ветка цикла */
    od                  /* окончание оператора цикла */
}
ltl spec1 { []a }       /* LTL-формула: "a" истинно всегда */

Семантика вышеприведенного примера на языке Promela: глобальная переменная a инициализируется значением true, а затем ее значение случайным образом меняется на false или true.

В то же время оператор ltl spec1 утверждает, что значение a должно быть истинным все время жизни переменной a.

Вызов spin для совместной генерации и верификации в этом случае может выглядеть так:

spin -run -a model.pml

В результате в консольной выдаче Spin можно обнаружить текст:

pan:1: assertion violated  !( !(a)) (at depth 2)
pan: wrote model.pml.trail
...
State-vector 20 byte, depth reached 2, errors: 1
...

Первая строка указывает на имя spec1 оператора ltl, верификация которого закончилась ошибкой. Третья строка содержит имя файла трассы model.pml.trail, которое можно использовать для генерации контрпримера далее:

spin -t -k model.pml.trail model.pml

ltl spec1: [] (a)
starting claim 1
Never claim moves to line 4     [(1)]
  2:    proc  0 (fsm:1) model.pml:7 (state 2)   [a = 0]
                a = 0
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!(a)))
Never claim moves to line 3     [assert(!(!(a)))]
spin: trail ends after 3 steps
#processes: 1
                a = 0
  3:    proc  0 (fsm:1) model.pml:5 (state 3)
  3:    proc  - (spec1:1) _spin_nvr.tmp:2 (state 6)
1 processes created

Здесь основная информация о контрпримере содержится в строках:

  2:    proc  0 (fsm:1) model.pml:7 (state 2)   [a = 0]
                a = 0
spin: _spin_nvr.tmp:3, Error: assertion violated

Показывается, что переменная a приобретает значение false в строке 7 файла model.pml. Это является конструктивным доказательством того, что модель в достижимой ее части, где значение a становится ложью, и LTL-формула, требующая противоположного, противоречат друг другу. Для устранения этого противоречия нужно модифицировать либо модель, либо ее спецификацию (оператор ltl spec1).