嵌入式控制系统时序安全性建模及验证

范宝文，包 健

(1.杭州电子科技大学网络空间安全学院，浙江 杭州 310018；2.杭州电子科技大学计算机学院，浙江 杭州 310018)

0 引 言

嵌入式控制系统在工业领域的应用愈发普遍，如何保证控制系统时序逻辑的正确性一直是学术界和工业界研究的热点。传统测试方法的效果往往取决于测试用例的规模，很难保证程序运行时的逻辑符合系统设计[1]。此外，C语言编写的嵌入式控制系统引入了时间相关的模块和控制逻辑，和普通的C语言程序有较大不同，增大了测试难度。形式化方法是对系统安全性进行验证的有效工具，主要分为模型检测和定理证明。模型检测方法运用验证工具穷举系统的状态空间，较好地利用验证工具来验证有穷程序，如借助Uppaal和时间自动机[2-4]对可编程逻辑控制器(Programmable Logic Controller，PLC)程序建模，或使用SMV[5-6]来验证PLC程序的时序性质，但该方法不适用于带有时间模块的C语言程序等复杂递归的情况，容易出现状态空间爆炸问题。定理证明方法基于霍尔逻辑等形式逻辑系统对系统状态进行推理，借助交互式证明助手进行证明：基于Coq的研究[7-9]对PLC程序语义进行探讨，但仅采用一阶谓词等低层次的规约公式来描述系统约束，不利于方法的推广；Gerwin等[10]使用Isabell[11]对C语言的程序进行验证，但忽略了时序性质的形式化描述与建模，使得模型在时序性质表达能力上有所欠缺。本文采用定理证明方法，提出一种基于Coq的嵌入式控制建模和系统时序性质验证方法，采用线性时序逻辑(Linear Temporal Logic，LTL)描述安全性质，建立控制系统和LTL公式的形式化模型，有效验证了系统是否符合提出的时序安全约束。

1 中间模型建模方法

由于直接采用验证工具来描述系统有较大的难度，所以通过中间模型建模的方法应用广泛[12]。本文选取有限自动机作为实现中间模型的工具，将系统的运行描述为自动机的状态转移，制定转移的语义公式，并将得到的自动机中间模型作为形式化建模方法的输入。

本文的实验对象是1个C语言编写的3轴直角坐标机器人控制系统，机器人示意图如图1所示。机械臂可以在2个水平方向和1个竖直方向上移动，分别用X，Y，Z表示。此外有1个带有受控机械手的球桶释放小球，使得小球可以在Z轴方向自由下落。

图1 直角坐标机器人示意图

1.1 控制系统到自动机的建模

建模路线与思路如图2所示，主要分为6个步骤：前4个步骤分别定义自动机相关的数据类型；第5步以推导公式的形式建立自动机的语义模型，规范其转移规则；第6步在保持语义不变的情况下优化自动机模型，使其更贴近原系统。

图2 基于自动机的系统建模过程示意图

(1)定义系统的变量空间。定义系统的变量空间State是当前自动机模型中变量值的集合。为了区别普通的变量类型，将系统的变量空间称为“系统的状态”。系统的状态是1个3元组(c,v,w)，分别表示当前机械臂终端所在坐标、寄存器的值和机械手的开关状态。

(2)定义系统运行阶段集合。系统运行过程根据其特点被逻辑划分为5个阶段，用Mode={idle,static,ready,run,pending}表示。idle表示系统上电复位但未运行；static表示系统完成初始化；ready表示运动的准备工作已就绪；run表示系统发出脉冲信号后，电机驱动皮带开始运转；pending表示机械臂末端根据计时器保持一定时间悬空的状态。

(3)定义系统抽象指令集合。机器人控制系统的一系列行为均通过改变寄存器的值或全局变量的值来实现，可以抽象为“行为指令”的集合Instr={start,stop,calculate,move,delay,return,hold,release}，其作用在于改变系统内部数值。行为指令集合可直接应用于自动机模型，作为其标签事件的集合。

(4)定义系统的格局与转移关系。定义系统的格局Configuration是系统运行某一时刻所有描述元素的数据结构，是1个3元素的笛卡尔积。将时间离散化处理，1个格局可写为(μ,τ,σ)，其中μ表示当前系统所处的阶段；τ是离散化全局时间变量，表示当前时刻；σ表示τ系统的状态。系统的转移关系是1个3元组(C,f,C0)。其中C表示系统的格局，f表示迁移函数，C0表示系统的初始格局。

通过上述步骤，建立图3(a)所示机器人控制系统自动机，其中自动机的状态来自步骤2定义的系统运行阶段，自动机的输入来自步骤3定义的抽象行为指令。图3(b)为机器人机械手的状态转移图。idle为起始状态，on和off分别表示机械手的开合。

(5)建立自动机转移的语义模型。模型的语义标注不仅能详细描述模型内部的细节，还能为不同层次模型的抽象、部件间的并发行为提供形式化的支持。以延时计时器指令delay为例，其对系统格局改变的语义公式如下：

(1)

(2)

横线上的内容描述了系统状态的改变，A(i)标记当前要执行的指令，横线下的内容描述系统格局的改变。式(1)表示，收到delay指令后，系统由“run”状态进入“pending”状态，并启动计时器开始计时，时间变量x开始自增。式(2)表示，当计时器时间变量x大于等于设定的时间参数y时，x清零，系统由“run”状态进入“static”状态。

(6)组合自动机。步骤4分别建立了机械臂和机械手的状态转移自动机，但无法表现出机械臂移动与机械手开合的并发执行关系。因此，采用平行同步组合的方法，将图3(a)与图3(b)中自动机进行组合，得到新的自动机，更好地展示并发执行的时序细节。新自动机的状态空间来自2个输入自动机状态空间的交叉乘积，新的转移关系来自原自动机中转移关系的交集，得到的结果如图3(c)所示。

图3 控制系统、机械手状态转移自动机及组合结果

1.2 时序安全性约束

结合图3(c)中的系统组合结果，提出直角坐标机器人控制系统必须满足的几个时序约束，并对应使用LTL公式描述为系统属性。

属性1当机械手松开小球后，状态机立即进入“pending,on”状态。令φ1表示指令为机械手松开时为true，φ2表示系统处于“pending”状态为true，公式表述为G(φ1→Fφ2)。

属性2在机械臂运动阶段时，机械手应保持“off”状态，以保证系统的安全运行。令φ3表示系统处于“run”状态时为true，φ4表示机械手处于关闭状态为true，公式表述为G(φ3∧φ4)。

2 在Coq中形式化建模与验证

第1节将控制系统的运行用状态转移图表示为自动机中间模型，并使用LTL公式描述系统应满足的时序安全约束。本节在此基础上建立系统在Coq中的模型，并验证时序结束是否成立。首先，基于自动机语义，形成系统在Coq中的模型；然后，在Coq中建立LTL的模型，以便形式化地描述1.2节中提出的系统时序安全属性；最后，将属性表述为Coq中的定理，并选择合适的策略证明。建模与验证的总体思路如图4所示。

图4 Coq中的建模与验证过程示意图

2.1 Coq中系统模型的建立

通过数据类型映射的方法，逐步将描述系统运行的自动机转换为Coq中的形式化模型，作为时序性质验证的载体。

(1)形式化定义系统变量。定义基础变量类型。全局时钟、距离均为自增整数，使用Coq中的自然数类型nat定义，分别命名为为Distance和Time。为了简化建模过程，将机械手的状态ClawState定义为布尔类型的变量，足以描述其特性。定义坐标类型变量Coordinate为1个3元组。

使用Coq中的Inductive类型将1.1节步骤1定义的系统状态描述为1个3元组。其中参数c表示机械臂末端当前坐标，v表示寄存器变量的集合，函数total_map表示字符串类型的编号到多态类型数值的映射关系。

(2)形式化定义系统运行阶段。对照1.1节中运行阶段的定义，使用枚举的方法定义系统的运行阶段Mode，表示如下：

(3)形式化定义系统行为指令。行为指令在定义时分为2种类型S_Instr和M_Instr，分别使系统的状态或系统的格局发生改变。S_Instr类型定义了更新系统状态的指令，包括机械手开合指令Release，Hold，写内存操作Write和坐标更新操作Move_S。M_Instr类型定义了更新系统格局的指令。

(4)形式化定义系统格局与转移关系。依据1.1节步骤4所定义的系统格局Configuration，使用Inductive类型将其描述为1个3元组，其中的3个元素分别表示系统运行阶段m、系统状态v和全局时钟变量t。

转移关系定义为Coq中的函数，输入参数分别为当前系统格局Configuration(设为g)和当前指令M_Instr(设为I)，输出参数为新的系统格局。限于篇幅这里仅给出函数的定义。

2.2 Coq中LTL公式模型的建立

将LTL公式的语法和语义转换为Coq中的形式化模型。1.2小节中提出的属性可被描述为Coq中的定理，并嵌入2.1小节中建立的系统模型进行验证。在Coq中建立LTL公式的形式化模型分为3步。首先，声明LTL公式的语法，定义不同的函数运算；然后，定义路径的变量类型和辅助函数；最后，结合语法和路径类型变量定义LTL公式的语义函数。

(1)形式化定义LTL语法。类型LTL_Formula定义了线性时序逻辑公式的语法。AP表示原子命题的类型。Statement和Neg_Statement定义了基于原子命题的LTL公式，分别表示其肯定和否定的形式。Conj，Disy和Imply是作用于2个LTL公式的谓词，分别定义了语法中合取、析取和蕴含这3种逻辑连接符。这3个函数接受2个LTL公式作为参数，返回1个新的LTL公式。Until表示基础时序算子“U”，Release是Until运算符的扩展，这2个函数接受2个LTL公式作为参数，返回1个新的LTL公式。Next表示基础时序算子“X”，接受1个LTL公式作为参数，返回1个新的LTL公式。

(*LTL语法定义*)

|Statement∶AP→LTL_Formula|Neg_Statement∶AP→LTL_Formula

|Conj∶LTL_Formula→LTL_Formula→LTL_Formula|Disy∶LTL_Formula→LTL_Formula→LTL_Formula|Imply∶LTL_Formula→LTL_Formula→LTL_Formula

|Until∶LTL_Formula→LTL_Formula→LTL_Formula|Release∶LTL_Formula→LTL_Formula→LTL_Formula|Next∶LTL_Formula→LTL_Formula.

(2)形式化定义LTL路径变量类型。LTL中的“路径”可以看作1个无限长度的状态序列，路径类型Path是原子命题类型到布尔值的映射。Index_Path函数获取1条路径和1个状态作为参数，返回1条路径中该状态的布尔值。Sub_Path函数同样需要1条路径和1个状态作为传入参数，不同之处在于使用了匿名函数机制，函数返回类型变成了路径。

(3)形式化定义LTL语义。借助Coq中Fixpoint类型递归地定义LTL公式语义函数，包括路径类型变量σ和LTL公式类型变量φ两个参数。函数使用match结构分情况讨论参数φ，类似于C语言中的case结构，共有8种可能性，分别为：

① |Statementa⟹(Index_Pathσ0)a=true

② |Neg_Statementa⟹(Index_Pathσ0)a=false

③ |Conjφ1φ2⟹(LTL_Semanticsσφ1)∧(LTL_Semanticsσφ2)

④ |Disyφ1φ2⟹(LTL_Semanticsσφ1) ∨ (LTL_Semanticsσφ2)

⑤ |Implyφ1φ2⟹(LTL_Semanticsσφ1) → (LTL_Semanticsσφ2)

⑥ |Untilφ1φ2⟹existsi,LTL_Semantics(Sub_Pathσi)φ2∧ (forallj,jLTL_Semantics(Sub_Pathσj)φ1)

⑦|Releaseφ1φ2⟹(foralli,LTL_Semantics(Sub_Pathσi)φ2) ∨existsi, (LTL_Semantics(Sub_Pathσi)φ2) ∧(forallj,j⟸i→LTL_Semantics(Sub_Pathσj)φ1)

⑧ |Nextφ1⟹LTL_Semantics(Sub_Pathσ1)φ1end.

LTL的语义函数按功能的不同可归纳为4种情况，具体的说明如下：

(1)分支1、分支2：“Statement a”表示1个真值为true的原子命题类型的公式，其中a是AP类型变量。该公式和“Neg_Statement a”是递归边界，表示该命题对路径起始状态是否成立。

(2)分支3、分支4、分支5：描述了逻辑连接符对LTL公式的作用。合取公式“Conjφ1φ2”表明若φ1，φ2都对路径σ成立，则φ1，φ2的合取对路径σ成立；析取公式“Disyφ1φ2”表示若φ1,φ2中的1个对路径σ成立，则φ1，φ2的析取对路径σ成立；蕴含公式“Implyφ1φ2”表示若φ1对路径σ成立，则推出φ2对路径σ也成立。

(3)分支6、分支7：描述了时态算子的语义。“Untilφ1φ2”表示存在状态i>=0，使得所有的0⟸j⟸i，有φ2在后缀qj,qj+1,qj+2,...中成立，且φ1在后缀qi,qi+1,qi+2,...中成立；“Releaseφ1φ2”表明，若φ1可以一直成立，则该式对路径上的所有状态都成立；或存在状态i>=0，存在1个状态i>=0，使得所有的0⟸j⟸i，有φ2在后缀qj,qj+1,qj+2,...中成立，且φ1在后缀qi,qi+1,qi+2,...中成立。

(4)分支8：“Nextφ1”表明，若使“Nextφ1”对路径σ={q0,q1,q2,q3,...}成立，当且仅当公式φ1对后缀{q1,q2,q3,...}上的所有状态成立。

补充的时序算子G和F可根据时序算子U和V的定义扩展而来，定义如下：

2.3 时序安全性质的验证

以1.2小节中属性2为例展示定义的证明步骤，将其所述性质描述为定理Spec_2，如下所示。

①TheoremSpec_2∶forall(g∶Configuration)(σ∶Path),

② (eqb_mode(getModeg)run)g=true→

③σ//(G(Statement(ap((eqb_mode(getModeg)run)g))g)∧(Neg_Statement(ap(～(get_claw(getStateg))g))g)).

第1步使用Theorem 关键字定义定理，包括系统格局类型参数g和路径类型参数σ。第2步描述了定理的假设，即当前系统运行于“run”阶段，eqb_mode函数比较2个运行阶段是否相等，getMode用于获取1个格局中的运行阶段。第3步陈述了定理的内容，当满足第2步条件时，自动机应满足公式“G (φ3∧ φ4)”。其中“φ3：Statement (ap (p3_1 g)) g”表示系统处于“run”状态时为true，“φ4：Neg_Statement (ap (p3_2 g)) g”表示机械手处于关闭状态为true。ap是1个原子命题AP类型的变量，用于将自动机语法表示的命题转换为线性时序逻辑中的原子命题类型公式。

定理Spec_2证明过程的主要思路如下：首先，依据LTL恒等式“G (φ3∧φ4)≡Gφ3∧Gφ4”，将定理的形式化简为2个子公式的合取。然后，使用split策略分解定理为2个子命题，证明目标变为分别证明路径σ符合2个子公式。最后，分别使用关键字left和right进入子命题的证明上下文，选取合适的策略证明目标。后续证明的过程限于篇幅不再赘述。

属性2和属性3实现了完整的证明，表明控制系统满足1.2小节中提出的对应约束。属性1在推导过程中发现了错误：系统同时收到stop(外部开关指令)和delay(内部设定指令)这种极为少见的情况时，仍会进入到包含“pending”的悬停状态，如图5所示。从状态1出发，遇到stop指令时应转移到状态2，但通过推导，自动机错误地通过虚线转移到状态3。通过与控制系统开发工程师的交流验证了证明的结果，并修改了原系统，提高了外部开关指令处理的优先级，使得系统在收到外部开关指令时会优先处理，消除了1个隐藏的逻辑错误，提高了系统的时序安全性。

图5 错误状态转移示意图

3 结束语

本文针对C语言编程的嵌入式控制系统时序安全问题，提出一种基于Coq的系统建模和时序性质验证方法。通过分析1个机器人控制系统，发现了系统中传统测试方法无法检测出来的隐藏时序逻辑错误，证明了本方法的有效性。本方法可以推广到由C语言编写的更为复杂的嵌入式控制系统程序的建模及验证工作上。下一步将建立更精确的定时器模型，在代码层面对控制系统的函数及算法进行建模，分析系统的异步时序行为。