Генерация Promela в Engee

Формальная верификация в Engee основана на автоматической генерации формальных моделей на языке Promela (PROcess MEta LAnguage), поддерживаемом системой Spin.

Генератор Promela преобразует диаграммы конечных автоматов (Chart), входящие и выходные порты, а также виртуальные подсистемы модели Engee в текстовую формальную спецификацию — .pml-файл.

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

Запуск генератора кода

Генерация кода на языке Promela из файла модели Engee выполняется при помощи обращения к API Engee, например, из окна командной строки img 41 1 2 :

engee.generate_code(source, destination, target="promela")

где

source — строка, путь к файлу модели .engee;
destination — строка, путь к директории, куда будет помещен сгенерированный файл.

В качестве имени сгенерированного файла API использует имя файла модели (суффикс ".engee" при этом исключается), завершающееся новым суффиксом ".pml".

Например, если путь к файлу модели source — "/user/models/large_model.engee", а директория для генерации файлов destination — "/user/spin", то сгенерированный код на языке Promela будет помещен в файл, путь к которому — "/user/spin/large_model.pml".

Процесс формальной верификации в Engee

Создание модели конечного автомата (внутри блока Chart) в Engee.
Генерация формальной модели Promela с помощью функции generate_code с указанием целевого (target) языка: engee.generate_code(source, destination, target="promela").
Добавление формальных свойств в виде формул LTL.
Проверка модели средствами Spin.
Анализ результатов: успешные доказательства, контрпримеры, трассы исполнения.

→

Ограничения модели

Если в модели присутствуют блоки или типы, которых нет в списке, попытка вызова API для генерации кода Promela завершится неудачей.

Не поддерживаются:

Множественный шаг дискретизации;
Темпоральные операторы блока Chart (t, before, after…);
Операторы блока Chart count и duration;
Библиотечные функции Julia, такие, как pow, floor, ceil… .

Поддержка блоков

В настоящее время функциональность генератора на языке Promela ограничена поддержкой нескольких видов блоков модели:

Поддержка типов данных

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

Тип Julia	Тип Promela
`Bool`	`bool` или `bit`
`UInt8`	`char` или `byte`
`Int16`	`short`
`Int32`	`int`

Тип Julia

Тип Promela

Bool

bool или bit

UInt8

char или byte

Int16

short

Int32

int

Поддержка синтаксиса Julia

Генератор кода Promela поддерживает почти весь синтаксис Julia, встречающийся в кодовых вставках блока Chart и поддерживаемый генератором кода языка Си.

Ряд конструкций не имеет прямых аналогов в Promela и поэтому не поддерживается:

Оператор continue;
Вложенные циклы for (или циклы со сложными условиями);
Циклы for с шагом, отличным от 1;
Оператор ,.

Реализован дополнительный синтаксис:

@goto
@label