Формальная верификация в Engee

Формальная верификация — это математический метод анализа, который позволяет полностью исследовать все возможные поведения модели в отношении заданных свойств.

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

Формальная верификация хорошо дополняет модельно-ориентированный подход в Engee: одна и та же модель может быть использована для симуляции, генерации кода и проверки свойств поведения.

Практическая реализация в Engee

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

Promela (PROcess MEta LAnguage) — язык спецификации моделей требований или программ.
Spin (Simple Promela INterpreter) — программа, позволяющая:
1. Интерпретировать описание модели на языке Promela (режим симуляции модели);
2. Генерировать из описания модели на языке Promela и спецификации, заданной формулой LTL, программу-верификатор на языке Си, позволяющую выполнять автоматическую формальную верификацию спецификации, в частности:
  - Проверять заданные в спецификации инварианты;
  - Искать контрпримеры, если инварианты не выполняются.

Подробнее о генерации Promela в Engee читайте в статье Генерация Promela в Engee.

Формальные методы

Формальная верификация в Engee основана на идее полного исследования поведения модели.

Например, когда создается модель конечного автомата (в блоке Chart), ее визуальная диаграмма сама по себе не может быть проверена автоматически. Поэтому перед запуском Spin модель преобразуется в строго определенное формальное описание на языке Promela.

Именно с этим формальным представлением работает Spin: он математически анализирует модель, перебирает возможные последовательности переходов и проверяет выполнение указанных свойств (LTL-формул).

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

В результате модель Engee становится математически строгим объектом: все состояния, переменные и переходы фиксируются в виде кода Promela, а Spin исследует все пространство состояний этой формальной модели и определяет, выполняются ли заданные свойства.

Формальные модели

В Engee формальная модель создается автоматически при генерации кода на Promela. Такая модель описывает:

Доступные переменные (глобальные и локальные);
Структуру состояний и переходов;
Условия активации и логику работы блоков Chart;
Порядок вычисления и взаимодействие элементов модели.

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

Формальный анализ

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

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

Свойства при формальном анализе — это верифицируемые требования к модели. Каждое свойство формулируется как отдельный случай верификации (например, в виде LTL-формулы). Определение полного набора свойств и проверка их выполнения позволяют убедиться, что поведение модели эквивалентно заявленным требованиям:

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

Связь с модельно-ориентированным проектированием

Модельно-ориентированное проектирование и формальная верификация естественным образом дополняют друг друга. Модель, созданная в визуальной среде (например, с использованием блоков Chart), уже является машиночитаемым описанием поведения системы.

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

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

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