Engee中形式化验证的扩展示例

此示例演示如何验证包含多个相互关联的图表块的模型，以及如何验证复杂的功能依赖关系和冲突的需求。

模型 WM.engee是三个嵌段的化合物图表：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]从三个位置开关接收数据，即在任何给定时间的每个三元组中，三个输入中只有一个可以具有真

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）上，该显示器显示地图应用程序（航空图表和图表显示系统）以外的应用程序;
R5：当选择地图应用程序进行显示(DU)时，则光标应移到此显示(DU)。;
R6:当按下用于选择发动机运行参数和机组警告系统(SELECT_EICAS)的显示的按钮时，eicas应用程序应显示在显示器上;
R7：按下主飞行显示选择按钮(SELECT_PFD)时，显示器上应显示PFD应用程序;
R8:当按下用于选择航空海图和图表显示系统(SELECT_MAP)的显示的按钮时，应在显示器上显示地图应用程序。;
R9：显示的DU_APPLICATION应用程序的每个变量都必须从 0 以前 3.

由于这样的事实，块输入端口在我们的例子中，总是生成零值，模型的模拟是无信息的，并且验证是不可能的，所以让我们改变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(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，其作为阶跃函数，用于产生进入左右输入的随机数据的部分:

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）上，该显示器显示地图应用程序（航空图表和图表显示系统）以外的应用程序。

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

R5：当选择地图应用程序进行显示（DU）时，则光标应移动到此显示（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会导致错误）。

很容易看出错误不在模型中，而是在规格本身中。:

从问题声明中可以知道，光标一次只能在一个显示器上。;
选择地图应用程序后，光标应移动到显示它的显示器。;
没有什么可以阻止您在同一时间在两个显示器上选择地图应用程序。

这导致光标位置的不确定性，这与要求不一致—要求是相互矛盾的，需要澄清。

所有其他要求都已成功验证。

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）的显示的按钮时，地图应用程序应显示在显示器上。

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中形式化验证的扩展示例

验证结果

有用的连结