Расширенный пример формальной верификации в Engee

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

Модель WM.engee представляет из себя соединение трех блоков Chart: LEFT_DU, RIGHT_DU и CURSOR_LOGIC (для компактности изображений подсистемы распакованы):

formal verification advanced 1

Предполагается, что тройки входов [LEFT_SWITCHBANK_EICAS, LEFT_SWITCHBANK_PFD, LEFT_SWITCHBANK_MAP] и [RIGHT_SWITCHBANK_EICAS, RIGHT_SWITCHBANK_PFD, RIGHT_SWITCHBANK_MAP] получают данные с трехпозиционных переключателей, т.е. в каждой тройке в каждый момент времени только на одном из трех входов может быть сигнал true.

Блоки LEFT_DU (слева) и RIGHT_DU (справа) — диаграммы переходов:

formal verification advanced 2 formal verification advanced 3

Блок CURSOR_LOGIC:

formal verification advanced 4

Задана спецификация модели из 9 требований:

R1: Если дисплей (DU) готов к работе, тогда он должен отображать некоторое приложение;
R2: Если дисплей (DU) не готов к работе, тогда он не должен пытаться отображать никакое из приложений;
R3: Курсор не должен отображаться на дисплее (DU), который не готов к работе;
R4: Курсор не должен отображаться на дисплее (DU), который отображает приложение, отличное от приложения MAP (система индикации аэронавигационных карт и схем);
R5: Когда для вывода на дисплей (DU) выбирается приложение MAP, тогда на этот дисплей (DU) должен быть переведен курсор;
R6: Когда нажата кнопка выбора отображения системы индикации рабочих параметров двигателя и предупреждения экипажа (SELECT_EICAS), на дисплее должно выводиться приложение EICAS;
R7: Когда нажата кнопка выбора отображения основного пилотажного дисплея (SELECT_PFD), на дисплее должно выводиться приложение PFD;
R8: Когда нажата кнопка выбора отображения системы индикации аэронавигационных карт и схем (SELECT_MAP), на дисплее должно выводиться приложение MAP;
R9: Каждой переменной выводимого на дисплей приложения DU_APPLICATION должно назначаться значение от 0 до 3.

В связи с тем, что блоки Inport в нашем случае всегда генерируют нулевые значение, симуляция модели малоинформативна, а верификация невозможна, поэтому изменим Promela-модель таким образом, как будто вместо блоков Inport в модели — генераторы случайных логических величин, причем, как уже было сказано выше, сигналы внутри троек [LEFT_SWITCHBANK_EICAS, LEFT_SWITCHBANK_PFD, LEFT_SWITCHBANK_MAP] и [RIGHT_SWITCHBANK_EICAS, RIGHT_SWITCHBANK_PFD, RIGHT_SWITCHBANK_MAP] связаны между собой и имитируют трехпозиционные переключатели.

Обычно случайный логический сигнал в Promela моделируется с помощью недетерминированного условного оператора:

if
:: s = true;
:: s = false;
fi

или оператора select (подробнее см. select):

select(s: false .. true);

Трехпозиционный случайный переключатель можно смоделировать как

if
:: s1 = true; s2 = false; s3 = false;
:: s1 = false; s2 = true; s3 = false;
:: s1 = false; s2 = false; s3 = true;
fi

Поэтому, поскольку входы определены в Promela-модели как

typedef Ext_WM_U {
    bool RIGHT_SWITCHBANK_MAP               /* /RIGHT_SWITCHBANK_MAP */
    bool LEFT_SWITCHBANK_EICAS              /* /LEFT_SWITCHBANK_EICAS */
    bool LEFT_DU_AVAILABLE                  /* /LEFT_DU_AVAILABLE */
    bool LEFT_MANUAL_REQUEST                /* /LEFT_MANUAL_REQUEST */
    bool RIGHT_SWITCHBANK_PFD               /* /RIGHT_SWITCHBANK_PFD */
    bool RIGHT_DU_AVAILABLE                 /* /RIGHT_DU_AVAILABLE */
    bool LEFT_SWITCHBANK_PFD                /* /LEFT_SWITCHBANK_PFD */
    bool RIGHT_SWITCHBANK_EICAS             /* /RIGHT_SWITCHBANK_EICAS */
    bool RIGHT_MANUAL_REQUEST               /* /RIGHT_MANUAL_REQUEST */
    bool LEFT_SWITCHBANK_MAP                /* /LEFT_SWITCHBANK_MAP */
};

/* External inputs */
Ext_WM_U WM_U;

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

active proctype fsm() {
do
:: true -> atomic {
    if
    :: WM_U.LEFT_DU_AVAILABLE = true
    :: WM_U.LEFT_DU_AVAILABLE = false
    fi
    if
    :: WM_U.LEFT_SWITCHBANK_EICAS = true; WM_U.LEFT_SWITCHBANK_PFD = false; WM_U.LEFT_SWITCHBANK_MAP = false;
    :: WM_U.LEFT_SWITCHBANK_EICAS = false; WM_U.LEFT_SWITCHBANK_PFD = true; WM_U.LEFT_SWITCHBANK_MAP = false;
    :: WM_U.LEFT_SWITCHBANK_EICAS = false; WM_U.LEFT_SWITCHBANK_PFD = false; WM_U.LEFT_SWITCHBANK_MAP = true;
    fi
    if
    :: WM_U.RIGHT_DU_AVAILABLE = true
    :: WM_U.RIGHT_DU_AVAILABLE = false
    fi
    if
    :: WM_U.RIGHT_SWITCHBANK_EICAS = true; WM_U.RIGHT_SWITCHBANK_PFD = false; WM_U.RIGHT_SWITCHBANK_MAP = false;
    :: WM_U.RIGHT_SWITCHBANK_EICAS = false; WM_U.RIGHT_SWITCHBANK_PFD = true; WM_U.RIGHT_SWITCHBANK_MAP = false;
    :: WM_U.RIGHT_SWITCHBANK_EICAS = false; WM_U.RIGHT_SWITCHBANK_PFD = false; WM_U.RIGHT_SWITCHBANK_MAP = true;
    fi

Теперь модель подготовлена к верификации.

Сократим имена:

// Inputs:
#define LEFT_DU_AVAILABLE WM_U.LEFT_DU_AVAILABLE
#define LEFT_SWITCHBANK_EICAS WM_U.LEFT_SWITCHBANK_EICAS
#define LEFT_SWITCHBANK_MAP WM_U.LEFT_SWITCHBANK_MAP
#define LEFT_SWITCHBANK_PFD WM_U.LEFT_SWITCHBANK_PFD
#define RIGHT_DU_AVAILABLE WM_U.RIGHT_DU_AVAILABLE
#define RIGHT_SWITCHBANK_EICAS WM_U.RIGHT_SWITCHBANK_EICAS
#define RIGHT_SWITCHBANK_MAP WM_U.RIGHT_SWITCHBANK_MAP
#define RIGHT_SWITCHBANK_PFD WM_U.RIGHT_SWITCHBANK_PFD

// Outputs:
#define RIGHT_DU_APPLICATION WM_Y.RIGHT_DU_APPLICATION
#define LEFT_DU_APPLICATION WM_Y.LEFT_DU_APPLICATION
#define CURSOR_LOCATION WM_Y.CURSOR_LOCATION

Также для наглядности определим символические имена для номеров приложений:

#define BLANK 0
#define EICAS 1
#define PFD 2
#define MAP 3

Для каждого неформального требования составим формальную спецификацию.

R1: Если дисплей (DU) готов к работе, тогда он должен отображать некоторое приложение.

Для первого дисплея:

ltl r1_1 { [] (LEFT_DU_AVAILABLE -> LEFT_DU_APPLICATION != BLANK) }

Для второго:

ltl r1_2 { [] (RIGHT_DU_AVAILABLE -> RIGHT_DU_APPLICATION != BLANK) }

R2: Если дисплей (DU) не готов к работе, тогда он не должен пытаться отображать никакое из приложений.

ltl r2_1 { [] (!LEFT_DU_AVAILABLE -> LEFT_DU_APPLICATION == BLANK ) }
ltl r2_2 { [] (!RIGHT_DU_AVAILABLE -> RIGHT_DU_APPLICATION == BLANK ) }

R4: Курсор не должен отображаться на дисплее (DU), который отображает приложение, отличное от приложения MAP (система индикации аэронавигационных карт и схем).

ltl r4_1 { [] (LEFT_DU_APPLICATION != MAP -> CURSOR_LOCATION != 1) }
ltl r4_2 { [] (RIGHT_DU_APPLICATION != MAP -> CURSOR_LOCATION != 2) }

R5: Когда для вывода на дисплей (DU) выбирается приложение MAP, тогда на этот дисплей (DU) должен быть переведен курсор.

ltl r5_1 { [] (LEFT_DU_APPLICATION != MAP -> X (LEFT_DU_APPLICATION == MAP -> CURSOR_LOCATION == 1)) }
ltl r5_2 { [] (RIGHT_DU_APPLICATION != MAP -> X (RIGHT_DU_APPLICATION == MAP -> CURSOR_LOCATION == 2)) }

Требование r5_2 верифицируется с ошибкой (при другой реализации Engee-модели ошибку вызвало бы требование r5_1).

Легко увидеть, что ошибка не в модели, а в самих спецификациях:

Из постановки задачи известно, что курсор может одновременно находиться только на одном дисплее;
После того как было выбрано приложение MAP, курсор должен переместиться на дисплей, где оно отображается;
Ничто не мешает выбрать приложение MAP на обоих дисплеях одновременно.

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

Все остальные требования верифицируются успешно.

R6: Когда нажата кнопка выбора отображения системы индикации рабочих параметров двигателя и предупреждения экипажа (SELECT_EICAS), на дисплее должно выводиться приложение EICAS.

ltl r6_1 { [] (LEFT_DU_AVAILABLE && LEFT_SWITCHBANK_EICAS -> LEFT_DU_APPLICATION == EICAS) }
ltl r6_2 { [] (RIGHT_DU_AVAILABLE && RIGHT_SWITCHBANK_EICAS -> RIGHT_DU_APPLICATION == EICAS) }

R7: Когда нажата кнопка выбора отображения основного пилотажного дисплея (SELECT_PFD), на дисплее должно выводиться приложение PFD.

ltl r7_1 { [] (LEFT_DU_AVAILABLE && LEFT_SWITCHBANK_PFD -> LEFT_DU_APPLICATION == PFD) }
ltl r7_2 { [] (RIGHT_DU_AVAILABLE && RIGHT_SWITCHBANK_PFD -> RIGHT_DU_APPLICATION == PFD) }

R8: Когда нажата кнопка выбора отображения системы индикации аэронавигационных карт и схем (SELECT_MAP), на дисплее должно выводиться приложение MAP.

ltl r8_1 { [] (LEFT_DU_AVAILABLE && LEFT_SWITCHBANK_MAP -> LEFT_DU_APPLICATION == MAP) }
ltl r8_2 { [] (RIGHT_DU_AVAILABLE && RIGHT_SWITCHBANK_MAP -> RIGHT_DU_APPLICATION == MAP) }

R9: Каждой переменной выводимого на дисплей приложения DU_APPLICATION должно назначаться значение от 0 до 3.

ltl r9_1 { [] (LEFT_DU_APPLICATION <= 3 && LEFT_DU_APPLICATION >= 0) }
ltl r9_2 { [] (RIGHT_DU_APPLICATION <= 3 && RIGHT_DU_APPLICATION >= 0) }

Итоги верификации

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

Расширенный пример формальной верификации в Engee

Итоги верификации

Полезные ссылки