Введение

АНИС — это инструмент для динамической верификации на основе формальных моделей. Он позволяет проверять свойства во время динамической верификации, записанные в виде формальной модели на языке Event-B.

АНИС позиционируется как средство интегрирования существующих инструментов динамической верификации (не использующих формальные модели) с формальными моделями. Инструмент динамической верификации должен мониторить поведение тестируемой системы и генерировать файлы с трассами. Эти файлы содержат выполнявшиеся системные операции и описание состояния системы перед первой операцией. АНИС проверит, что эти операции выполнялись в соответствии с формальной моделью.

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

1. название операции;

2. список аргументов операции;

3. список результатов операции (за исключением числового кода – статуса завершения);

4. предусловия операции (условие, при котором операция должна завершиться успешно);

5. постусловия операции (условие, описывающее значения результатов операции).

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

1. список переменных состояния;

2. указание, какой тип имеет каждая переменная;

3. инварианты (условия, при которых переменные состояния описывают правильные, безопасные, корректные состояния системы).

Для моделей с состоянием предусловия операций – это выражения от аргументов операции и переменных состояния, постусловия операций – это выражения от аргументов операции, результатов операции и переменных состояния. Кроме того, спецификация операции дополняется еще одним компонентом – описанием того, как надо изменить состояние модели при выполнении этой операции.

Проверка трасс на соответствие формальной модели выполняется следующим образом:

1. модель переводится в состояние, соответствующее начальному состоянию из трассы;

2. затем последовательно для каждой операции трассы:

   1. проверяется предусловие;

   2. если операция завершилась неуспешно и предусловие истинно, фиксируется несоответствие трассы модели и проверка завершается;

   3. если операция завершилась успешно и предусловие ложно, фиксируется несоответствие трассы модели и проверка завершается;

   4. если операция завершилась успешно, то проверяется постусловие;

   5. если постусловие ложное, фиксируется несоответствие трассы модели и проверка завершается;

   6. иначе выполняется переход в новое состояние модели согласно спецификации операции.

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

В языке Event-B формальная спецификация операций (они называются событиями) выглядит несколько иначе. Нет разделения на аргументы и результаты операции — они называются параметрами событий. Нет разделения на предусловия и постусловия — они называются охранными условиями событий. Тем самым проверка предусловия и постусловия будет выполняться совместно.

Итого, чтобы выполнить динамическую верификацию в АНИС пользователь должен сделать следующее:

• подготовить модель;

• задать директорию с трассами и их формат;

• реализовать медиатор.

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