一种面向SCR需求模型的形式化验证方法研究
2022-01-21王立松康介祥高忠杰
张 漾，胡 军，王立松，康介祥，王 辉，高忠杰
1(南京航空航天大学 计算机科学与技术学院，南京 211106)2(软件新技术与产业化协同创新中心，南京 210007)3(中国航空无线电电子研究所，上海 200233)
1 引 言
计算机系统软件本身的可靠性和安全性是安全关键系统[1，2]正常运行的先决条件.近年来航空事业发展迅速，航电系统[3]的复杂性急剧增加，机载软件适航认证标准DO-178C[4]支持采用形式化方法验证航空软件.基于模型的安全评估[5，6](MBSA)方法可以通过对安全关键系统建立模型，从而将复杂的系统行为描述为精确的、可读的数学表达式，并对相关需求规约[7，8]实现分析，检查需求模型的一致性和完备性，验证系统的正确性.
T-VEC是基于4变量模型[9，10]中的SCR方法，进行需求设计、需求建模的工具.通过表格表达式，它用模式转换表、条件表和事件表等形式化数学符号，描述系统在不同的模式、条件和状态下，状态变量不同的取值，表现系统状态迁移的逻辑关系，从而实现对系统行为形式化描述.
形式化验证[11]是用精确的、高效的数学方法验证系统的正确性或评估系统可能存在的缺陷，从而做出关于系统设计的正确决策.形式化方法有3大类分别是演绎证明(deductive proof)、模型检验(model checking)和抽象解释(abstract interpretation).本文主要介绍和使用在工业上应用最广泛的模型检验方法.模型检验[12]是一种自动化验证技术，其输入是描述成状态机的系统模型和描述成模态逻辑公式的待验证系统属性，通过验证“模型状态机可达路径是否满足模态逻辑公式”来给出结果；其输出是满足系统性质的肯定反馈或不满足系统性质的反例.时态逻辑[13](temporal logic)是计算机形式化研究中重要的分支，其将系统结构中所有的状态可达关系解释为基于时间的先后次序关系.本文主要将系统的动态待验证属性的状态集描述为形式化规约，转换成可执行、无二义的线性时序逻辑(Linear-time Temporal Logic，LTL)和计算树时序逻辑(Computation Tree Logic，CTL)公式，将其作为标准的模型检验输入.
nuXmv[14-16]是一种传统的符号化模型检测器.nuXmv是SMV扩展而来的，SMV最早是由卡内基梅隆大学的K.L.McMillan研发，是第1个基于BDD的模型检查器.之后，经由功能扩展和重新实现的nuXmv加入了基于SAT算法的验证引擎，能够对有限状态和无限状态的系统进行形式化验证.nuXmv的模型建模语言XMV通过对有限状态自动机[17]Finite State Machine(FSM)和无限状态系统的状态转换的描述对系统建模，用状态迁移定义事件触发下的系统变量取值的改变.
本文将T-VEC语言定义的表格关系模型转换为自动机状态迁移图，再将状态图解释为nuXmv可以理解的符号化模型检测语言XMV，进而为建模后的安全关键系统软件检查需求的一致性与完备性.基于ANTLR4语法解析工具，本文提出和实现了一种模型变量关系平展简化的方法，解决了T-VEC建模语言语法结构上的递归定义问题，完成了模型转换及状态图解释工具的开发.本文第2节对T-VEC和nuXmv模型进行形式化定义；第3节对SCR模型系统验证框架进行阐述；第4节对模型变量关系平展简化方法进行具体说明；第5节对模型转换规则进行定义并给出正确性证明；第6节对飞行引导系统(Flight Guidance System，FGS)进行分析，最后对本文相关工作进行总结，对未来应用进行展望.
2 T-VEC与nuXmv模型
2.1 T-VEC语义
T-VEC语言定义了以需求为中心，以表格表达式表示的系统模型形式，其将模型保存为以.SS为后缀的文件格式.为了方便，下文中均将T-VEC抽象需求模型称为SS模型.每一个SS模型都包含多个SS文件，每一个带有约束的和正向输出的中间变量和输出变量都保存为一个.SS文件.其中，每一个.SS文件包含了一个系统定义变量和多条系统控制约束语句，针对不同的系统控制约束，系统定义变量有不同的取值.
图1(a)描述了SS需求模型的文件结构，图1(b)描述了在该文件结构下的.SS文件组成逻辑.由图1(a)可见，SS模型的描述语言是一种对象离散的抽象语言，其没有顺序、循环等流程控制语句，也没有复杂多变的自定义方法和自定义过程.但是在图1(b)组成逻辑中可以发现，SS模型的变量结构上存在递归定义特征，针对当前的中间、输出变量，可以引入SS模型中包含的其他中间和输出变量作为控制约束.
在本节中，为了精确描述T-VEC语言语义的逻辑，本文使用SS模型扩展定义T-VEC的语言(下文中称为SSM)，给出如下形式化定义：
定义1.一个SS模型(SSM)是一个三元组SSM=
1)T是一个类型集合，是基本类型TBasic与自定义类型TCustom的并集：T=TBasic∪TCustom.
图1 SS模型文件结构和组成逻辑Fig.1 SS model′s file structure and file format
2)TBasic是基本类型，其中包含布尔型Boolean、整型Integer、浮点型float/double、字符串型String.
3)TCustom是自定义类型，其中包含3个字段，分别是类型名称、原始类型和类型范围.
4)V是一个变量集合，是输入变量Vin、中间变量Vterm和输出变量Vout的并集：V=Vin∪Vterm∪Vout.
5)Vin是输入变量，是不参加状态迁移的原子变量.
6)Vterm是中间变量，是包含变量约束的复合变量.
7)Vout是输出变量，是包含变量约束的复合变量，用于描述待验证属性.
8)C是一个约束集合，是条件约束Ccon和事件约束Cet的并集：C=Ccon∪Cet.
9)Ccon是变量取值笛卡尔积的一个子集，Ccon⊆{(V，val)|V∈V×V，val∈TypeRange}其中：V∉Ø，val∉Ø.
10)Cet带有时间属性的变量取值笛卡尔积的一个子集Cet⊆{(VT，val)|VT∈VT×VT，val∈TypeRange}其中：VT∉Ø，val∉Ø.
事实上，SS模型包含两个配置文件coreRTS.SS和runTimeData.SS，以及多个中间、输出变量定义文件.配置文件分别描述了所有基本类型、该基本类型的取值范围的定义和用户定义类型与基本类型间的传递定义.传递定义既提供了变量类型的灵活性，也保证了变量取值范围的一致性.变量定义文件运用了模型中的条件表、事件表、模式类等来描述模型中的状态迁移，体现了模型行为的动态性.SS模型包含了输入变量约束、中间变量约束和输出变量约束，约束本质上是变量与变量取值的选择，体现的是其他变量取值对待检查变量取值的影响，以及对整个系统运作和状态迁移的影响.
2.2 nuXmv语义
nuXmv定义了从系统状态出发，用状态迁移描述系统运作进程的模型形式，其将模型保存为以.SMV为后缀的单个文件格式.为了方便，下文中均将nuXmv需输入的抽象需求模型称为XMV模型.一个XMV模型由一个主模块(MODULE)与若干个子模块构成，模块之间由变量参数关联，子模块之间可以互相嵌套迭代，可以多次复用，最后都由主模块单独调用.与SS模型不同，XMV模型由状态驱动，以状态的迁移反映模型的动态行为，状态由最小单元状态变量(VAR)组成.在XMV模型中，用ASSIGN声明进入状态转换，定义状态变量赋值；用INIT代表新引入的状态变量初始赋值；用NEXT代表在当前状态约束下，下一状态的变量取值.
在本节中，为了精确描述nuXmv语言语义的逻辑，本文使用XMV模型扩展定义nuXmv的建模语言，下文中称为XMV，给出如下形式化定义：
定义2.一个XMV模型是一个七元组XMV=
1)M是一个模块(MODULE)的集合，是主模块Mmain与若干子模块Mi的并集：M=Mmain∪Mi，其中i=1，2…n.
2)Mi子模块是状态S与状态迁移关系T笛卡尔积的一个子集Mi⊆S×TS.
3)S是一个状态的集合，是初始状态S0、中间状态Si和终结状态F的并集：S=S0∪Si∪F，其中i=1，2…n.
4)S0是模型的初始状态，S0∈S，初始状态是变量INIT赋值集合.
5)Si是模型的中间状态，Si∈S，中间状态是变量NEXT赋值集合.
6)V是一个变量的集合，是输入变量组IVAR，状态变量组VAR和冻结变量组FROZENVAR的并集，V=IVAR∪VAR∪FROZENVAR.
7)C是状态转移约束的集合，此约束可以是触发的系统事件或者状态推进要求满足某种条件.
8)T是状态转移的集合，ti∈T，ti=Si→Si(Si×C×Si)，其中i=1，2…n，ti表示某个状态迁移至另一个状态的过程，其本质是两个状态集与约束集的笛卡尔积.
9)F是终结状态的集合，是状态集合的一个子集：F⊆S.终结状态不唯一，不同的属性规约要求有不同的终结状态，因此F由SPEC决定.
本质上，XMV语言由XMV模型和属性规约构成，其结构由关键字MODULE、ASSIG-N、DEFINE、INVAR、INIT、NEXT、IVAR、VAR、FROZENVAR、SPEC等描述.其中，MODULE是模块声明词，用于声明主模块或子模块，可以自定义名称和带有参数，用于关系的传递；ASSIGN提示了状态变量赋值开始，进入状态转换阶段；DEFINE是宏定义关键字，用于抽象预定义规则，利用宏名代替命令序列，在下文中，DEFINE主要将约束逻辑序列定义为约束名称，便于模型中变量根据条件和事件约束赋值使用；INVAR是定值声明词，用于定义系统中的常量；INIT是初始化操作关键字，在状态变量赋值开始后可以对变量初始赋值，组成初始状态S0；NEXT是下一状态赋值操作关键字，在状态变量赋值开始后，在满足DEFINE描述的特定约束下，可以对变量进行下一状态赋值；IVAR是输入变量声明词，用于定义输入变量，将外界环境作为变量参数引入模型，体现环境的影响；VAR是状态变量声明词，用于定义状态变量，是参与系统状态迁移的主要成分，体现系统的运作；FROZENVAR是冻结变量声明词，用于定义冻结变量，冻结变量没有赋值改变，保证状态稳定的变量；SPEC是属性规约关键字，使用LTL、CTL和PTL时序逻辑、变量不变规约等来描述待验证需求，说明系统性质.
3 面向SCR模型的系统安全性验证框架
本节对面向SCR模型的系统安全性验证框架进行描述，并对框架中的重要过程进行基本介绍.
nuXmv语言能够描述抽象自动机，满足对系统模型的需求规约安全性验证，因此本文将SS模型转换为XMV模型并进行验证.
图2 安全性验证框架Fig.2 Security verification framework
验证框架如图2所示，其中包括3个重要流程及其关键技术：
1)应用ANTLR4[18]语法解析工具对输入的SS模型语法分析获取复杂单元和原子单元；
2)将复杂单元的变量约束平展化为底层的原子单元约束；
3)根据模型转换规则将由原子单元约束构建的SS模型转换为XMV模型文件，进行安全属性验证.
本文整理了T-VEC语言的词法和语法结构，词法规则采用正则表达式描述，语法结构精确定义为扩展巴克斯-诺尔范式[19](E-BNF)消除左递归.借助ANTLR4，本文对输入的词法文件的字符流进行读取，将字符聚类为单词和符号(Token)；解析语法文件和识别语法结构，最终生成每一个输入的T-VEC语言模型的语法分析树，并构造语法结点遍历器.ANTLR4语法程序parser根据T-VEC语法文件(grammer.g4)构造生成语法分析树，语法树自上而下递归解析.其根结点是序列化语句的起始，包含了语法文件中描述的所有情况的文件结构；其子结点是组成该文件结构的所有递归词组名；最下层的叶子结点即为实例中对应该词组名的具体单词，整理出复杂单元和原子单元.
4 变量关系平展简化
4.1 平展简化算法
SS模型的递归定义体现在：在定义中间和输出变量时，变量约束可以引入输入变量、中间变量和输出变量三类相关约束.其中，带有中间变量和输出变量的约束包含递归调用，存在更底层的变量约束，不具有原子性.变量约束的递归定义逻辑如图3所示.
图3 变量递归定义逻辑Fig.3 Form of recursive variables
因为SS模型变量约束间存在递归嵌套，将每个包含约束定义的变量向上抽象为模型基本单元，其中：
1)ITO单元：带有输入、中间和输出约束的可解释变量单元；
2)IT单元：带有输入和中间约束的可解释变量单元；
3)IO单元：带有输入和输出约束的可解释变量单元；
4)TO单元：带有中间和输出约束的可解释变量单元；
5)T单元：仅带有中间约束的基础单元；
6)O单元：仅带有输出约束的基础单元；
7)I单元：仅带有输入约束的基础单元.
由图3可知，每一个模型单元都可以向下解释为包含同类单元约束的基本单元，即变量定义具有递归性；除基础单元(I、T、O)外，每一个模型单元都可以解释为下层基础单元，即变量定义具有嵌套性；带有同一种约束的基础单元最终都可以简化为仅带有输入约束的I单元，即变量定义具有分解性.I单元是最底层的基础单元，无法继续向下解释或化简，是整个系统的原子单元，没有递归性、嵌套性和分解性.
本文利用模型单元的可分解性，将可解释、可简化的变量单元向下层平展化简至原子单元I变量，打破SS模型递归、迭代和调用的特性，将复杂变量间的约束整理为上层单元与原子单元间的关系，满足XMV模型线性、非调用的要求，完成模型转换前的预操作.
本文提出的变量关系平展简化方式如图4所示，对每个表述变量约束的树形模型单元向下层平展，遍历这个复杂模型单元的每一个分支，对每一个分支进行深度检索，直至将该单元以及该单元下层的复杂单元分解成基础单元(I、T、O)，再将T和O单元简化为一组I单元.至此，将一个复杂单元向下平展简化为一个I基础单元组，即从SS模型上说，将一个含有递归、嵌套的复杂变量约束关系转换为一个仅含有输入变量的约束关系组.
这种变量关系平展简化方式将树形的SS模型变量约束定义转换为XMV模型可接受的线性约束组，简化了模型转换难度，达到了模型约束关系转换的一致性，一定程度上减少模型状态，使模型更加简洁.
图4 模型单元平展简化过程Fig.4 Process of flattening model unit
变量约束平展简化算法如算法1所示.OutputVarConstr-aint(第1行)、termVarConstraint(第2行)和inputVarConstraint(第3行)分别代表输入文件一个复杂单元中的输出变量约束(O基础单元)集合、中间变量约束(T基础单元)集合和输入变量约束(I原子单元)集合.平展时，首先针对输出变量约束集合中的每一个O单元，判断这个O单元是否为复杂单元，即存在其他的T、O单元(第5行)，如果存在，则向下递归，对这个O单元平展化，深度遍历出O单元这个分支上的所有I单元并加入inputVarConstraint集合(第6行)，随后将这个O单元的约束信息写入预先设计好的termxml文件中(第7行)；如果不存在，则将这个O单元包含的原子约束加入inputVarConstraint集合，作为递归出口(第9行).然后，针对中间变量约束集合中的每一个T单元，做相应操作，将每一个T单元平展简化为原子约束，加入原子约束集合，并将T单元的约束信息写入到一个termxml文件中.最后，将描述所有原子约束的inputVarConstraint集合写入到Modelname.pSS，完成平展简化后的文件输出.
算法1.变量约束平展简化算法variableFlat
输入：name.SS
输出：Modelname.pSS，variablename.termxml
1.outputVarConstraint ← getOutput(name.SS)
2.termVarConstraint ← getTerm(name.SS)
3.inputVarConstraint ← getInput(name.SS)
4.Foreacho∈outputVarConstraintdo
5.IfexistTOunit(o)then
6.inputVarConstraint ← variableFlat(o)∪ inputVarConstraint
7.Writefile(variablename.termxml，o)
8.Else
9.inputVarConstraint ← inputVarConstraint ∪ getInput(o)
10.End
11.Foreacht∈termVarConstraintdo
12.IfexistTOunit(t)then
13.inputVarConstraint ← variableFlat(t)∪ inputVarConstraint
14.Writefile(variablename.termxml，t)
15.Else
16.inputVarConstraint ← inputVarConstraint ∪ getInput(t)
17.End
18.Writefile(name.pSS，inputVarConstraint)
19.Return Modelname.pSS，variablename.termxml
4.2 平展简化的意义与问题
变量约束关系的平展简化将树形的约束逻辑平展为线性的约束逻辑，简化了后续的模型转换过程.平展后的约束消除了嵌套性，成为同构的线性约束，只需要制定好转换规则就能够对同构的线性约束进行批量操作.平展为线性的约束消除了递归性，直接构建输出变量与原子输入变量的约束，取消了中间繁杂的、递归的约束转换，减少了后续转换的遍历步骤，提高了运行效率.平展操作让输出变量关于其他复杂变量的粗粒度约束简化为输出变量关于原子变量的细粒度约束，有利于发现原本约束中重叠的部分，消除重复约束，优化模型.
由于直接构建顶层约束与底层约束的关联，经过平展简化后的变量约束会丢失中间过程和直接约束的信息，这不利于做完模型验证后追溯过程，找出存在问题的约束.这是平展简化存在的问题，省略了繁杂的中间信息，从而简化了模型转换的过程.
针对这个问题，本文提出一种存储中间信息的termxml格式.termxml文件基于xml格式，包含这个复杂单元下层的变量定义和对应的相关约束.每一个复杂单元就存在一个对应的中间信息文件.在对变量约束关系的平展简化中，算法同时对每一个复杂单元进行了描述，将该单元包含的直接变量和相关约束封装成预定好的规范化termxml格式文件，并进行单独文件输出.
5 模型转换规则定义
上一节主要介绍了变量关系平展简化，包括算法和平展简化的意义与问题.本节将在平展简化后的文件基础上，对模型转换过程中SS模型到XMV模型的规则定义与对应的算法设计进行详细地阐述.
5.1 运算符号转换
SS模型支持算术运算和逻辑运算，算术运算符包括四则运算、绝对值、最大值、最小值和三角函数等常见的基本运算符；逻辑运算符包括逻辑与或非等推演布尔运算符.XMV模型同样支持同种类型的算术运算和逻辑运算，只是两者所使用的符号不全一致，表1提供了运算符对照表，在模型转换过程中，每一个运算符按表中规则转换.
表1 运算符对照表Table 1 Operator comparison table
5.2 类型转换
SS模型支持基本类型的定义和基于基本类型的自定义类型定义，基本类型包括布尔型(Boolean)、整型(Integer)、浮点型(Float)和字符串型(String).自定义类型主要有两类，分别是字符型的自定义类型和数值型的自定义类型：字符型自定义类型基于枚举型(Enumerated)，可以拥有多个字符值；数值型自定义类型基于整型或浮点型，精确限制取值范围，赋予类型现实意义.
表2 类型转换对照表Table 2 Type conversion comparison table
XMV模型不支持字符串型和数值自定义类型的定义，因此用单例枚举型作为字符串型的对照结果，用向上回溯的浮点型和整型作为数值自定义类型的对照结果.因为原始类型的取值范围大于自定义类型，所以并不影响类型转换的一致性.精确定义：TBasic表示基本类型，TCustom表示自定义类型，TXMV表示XMV模型中的类型，则类型转换规则表示为TBasic∪TCustom↔TXMV，类型转换对照表如表2所示.
5.3 常量转换
5.4 变量转换
在上一节的平展简化的介绍中，将SS模型引入的变量分为两类：一类是不参与状态迁移的输入变量，对应于SCR方法中的监控变量，即原子单元(I)；另一类是通过状态迁移描述系统运行的中间变量和输出变量，即复杂单元(T/O).XMV模型支持只参与初始赋值的输入变量和贯穿整个系统的系统变量的定义，因此在变量转换算法中，将原子单元的定义转换为输入变量定义，将复杂单元装换为系统变量定义.SS模型中的变量在BNF中定义为VARIABLE
变量声明转换算法如算法2所示.其中，Var是SS模型平展化后的系统存在变量集合.平展后SS模型描述了复杂单元与原子单元一对多的约束关系，因此在Var集合中包含O单元与I单元.变量定义转换时，遍历Var集合中的每一个单元，判断其是否是原子单元(第3行)，如果是则将其转换为输入变量定义，如果不是则将其转换为状态变量定义(第6行).最后将转换好的变量定义写入到输出文件中.
算法2.变量转换算法
输入：Modelname.pSS
输出：Modelname.xmv
1.Var ← getModelVar(Modelname.pSS)
2.Foreachv ∈ Vardo
3.IfisIvar(v)then
4.ivar ← transform(v)
5.Else
6.var ← transform(v)
7.End
8.Writefile(Modelname.xmv，ivar)
9.Writefile(Modelname.xmv，var)
10.ReturnModelname.xmv
5.5 约束转换
变量间的约束关系构成了系统状态的迁移，SS模型中的约束在逻辑结构中指定，是基于谓词的表达式.在平展简化后，一个逻辑结构由一个或多个从属原子约束连接组合.在XMV模型中，使用DEFINE关键字对每一条约束宏定义，定义为多条逻辑表达式，用逻辑符号连接.精确定义：LS代表SS模型中的逻辑结构集合，C代表XMV模型中的约束集合，则约束转换规则为：SSLSi↔XMVCi，其中i=1，2…n.如图5所示.
图5 约束转换规则Fig.5 Constraint transformation rules
约束转换算法如算法3所示.其中logicS代表平展后文件中所有逻辑结构的集合，constraint用于存储转换后XMV模型中约束的集合，初始为空.在约束转换时，遍历logicS集合中每一个逻辑结构l，采用字符替代方法将逻辑关系符号NOT、AND和OR分别转换为对应的符号，然后将每一个l转换为一个宏定义的约束加入到constraint集合中，最后将集合写入到文件中.
算法3.约束转换算法
输入：Modelname.pSS
输出：Modelname.xmv
1.logicS ← getModelLogicS(Modelname.pSS)
2.constraint ← Ø
3.Foreachl∈logicSdo
4.If“NOT：”inlthen
5.Replace(“NOT：”，!)
6.If“AND”inlthen
7.Replace(“AND”，“&”)
8.If“OR”inlthen
9.Replace(“OR”，“|”)
10.con ← transform(l)
11.constraint ← constraint ∪ con
12.End
13.Writefile(Modelname.xmv，constraint)
14.ReturnModelname.xmv
5.6 输出赋值转换
在SS模型中，输出赋值表现了O单元在特定逻辑结构下的特定取值；在XMV模型中，关键字next表现了状态变量在特定条件下迁移到下一状态的活动；针对转换好的约束宏定义，关键字case描述在当前约束下状态变量的下一状态值.精确定义：f(ρ)=value代表SS模型中输出赋值函数，其中ρ代表逻辑结构，value代表变量值；next代表XMV模型状态迁移的赋值过程，则输出赋值的转换规则为SSf↔XMVnext，如图6所示.
图6 输出赋值转换规则Fig.6 Assignment conversion rules
输出赋值算法如算法4所示.其中outputVariable代表输出变量集合(第1行)，声明一个assignmMap，key是已经转换好的约束的名称，value是该变量在这个约束下的值.outAssignment代表转换输出赋值集合，其初值为空.在输出赋值转换过程中，遍历每一个输出变量，将其约束名称和值按对应的规则转换，并加入输出赋值集合，最后写入到对应文件中.
算法4.输出赋值转换
输入：Modelname.pSS
输出：Modelname.xmv
1.outputVariable ← getOutput(Modelname.pSS)
2.Statement assignmMap(constraintName，value)
3.outAssignment ← Ø
4.Foreachvout ∈ outputVariabledo
5.assignmMap ← getMap(Modelname.pSS)
6.assign ← transform(vout，assignmMap)
7.outAssignment ← outAssignment ∪ assign
8.End
9.Writefile(Modelname.xmv，outAssignment)
10.ReturnModelname.xmv
5.7 转换正确性证明
本章的前6节给出了SS模型到XMV模型的五条转换规则，记作双射函数φ(x).本节将给出相关逻辑证明，验证转换规则的正确性.要证明转换规则正确，需要对转换前后的模型语义进行分析，若语义不变，则转换正确，否则判定转换规则有错误.为了判定模型语义，本文给出如下方法：如果转换前后的SS模型和XMV模型都可以精确地描述同一个系统，则判定语义保持不变.本文使用有限状态机(Finite State Machine)描述系统，首先给出有限状态机的形式化语义描述.
定义3.一个有限状态机(FSM)是一个五元组M=
1)Q是一个有穷状态的集合；
2)Σ是输入字母表，状态机接收不同字母进入不同状态；
3)δ是状态转移函数δ×Σ→Q(扩展函数δ×Σ*→Q)；
4)q0是初始状态，q0∈Q；
5)F是终结状态，F∈Q.
假设存在一个系统，其运行状态用有限状态机M′描述为
1)有穷集合Q′=
3)对于状态中的每一组变量，不妨设变量类型type=
4)输入字母表Σ′=<σ1，σ2，…，σm>.
5)状态转移函数δ′=<δ1，δ2，…，δk>，δi=qa′×σb→qc′，其中i≤k，a≤n，b≤n，c≤m.
6)q0′为初始状态，q0′∈Q′.
7)F′为终结状态，F′∈Q′.
针对这个精确定义的系统，采用2.2节介绍的SS模型，对它进行形式化建模，系统模型SS′=
TBasic=
TCustom=
T=TBasic∪TCustom=
Vin=
Vterm=
Vout=
V=Vin∪Vterm∪Vout=
SSLS=Σ′=<σ1，σ2，…，σm>；
SSLS′={Σ′，δn-1}；
SSf=δ′=<δ1，δ2，…，δk>；
Ccon=SSLS∪SSf；
Cet=SSLS′∪SSf；
C=Ccon∪Cet.
根据转换双射函数φ(x)可知，针对每一个SS模型，都有唯一的XMV=φ(SS)与之一一对应；相反，针对每个XMV模型，都有唯一的SS=φ-1(XMV)与之一一对应.对于给定系统的SS′模型，若其转换后的模型XMV′=φ(SS′)=<φ(T)，φ(V)，φ(T)>依然可以精确描述该系统，满足系统状态不变，则转换前后语义不变，转换规则正确，具体的转换过程如下：
首先对系统模型变量关系平展简化，消除模型约束中的递归性和嵌套性，将整个系统模型定义为一个主模块Mmain，根据TBasic∪TCustom↔TXMV规则，将
M=Mmain；
S=
S0=q0′；
V=
C=<σ1，σ2，…，σm>；
T=<δ1，δ2，…，δk>；
F=F′.
现在需要证明模型XMV′描述的系统为M′定义的系统，由于XMV是类自动机模型，证明XMV′与M′模型等价，即证明其对应系统元素数值等价，非对应系统元素语义等价即可.
对应系统元素包括系统状态集合、初态、终态和转移函数集合.状态集合S=Q′=
非对应系统元素包括模块、变量集合和约束集合.其中，变量集合V与系统状态包含的变量组一一对应，变量类型也一致，达成语义等价；XMV′中的约束集合为引导状态转移的条件组，与M′系统中的字母表语义一致，且条件组均为<σ1，σ2，…，σm>；XMV′中的模块为单个主模块，是对整个系统的定义，没有对系统元素精确定义，因此非对应系统元素语义等价.
在上述证明中可知，XMV′模型满足M′系统的全部性质和属性，因此从语义上说，转换前的SS′模型和转换后的XMV′模型描述的是同一个系统M′，即可以判定转换前后语义没有发生改变，改变的只是模型的呈现形式，转换双射函数φ(x)包含的转换规则是准确的.
6 实例分析
6.1 系统描述
本章对航电系统中的飞行引导系统[20](Flight Guidance System，FGS)的控制单元进行nuXmv安全性验证.首先根据该系统的需求描述建立SS变量关系模型，根据模型转换规则φ(x)转换为XMV模型，定义待验证属性时序逻辑规约，最后一起作为模型检测工具的输入，进行需求验证，分析验证结果.
飞行引导系统(FGS)是自动飞行控制系统(Automatic Flight Control System，AFCS)的重要组成部分，FGS提供了飞行指引功能，接收大气数据系统、姿态量测系统、导航系统等终端信息，根据FGS的模式逻辑和飞行控制律，后台计算获取操作指令，给出响应，引导选择正确的飞行模式，并监督自动驾驶仪和飞行指引仪的工作情况.
飞行控制律监测飞行状态，比较当前飞机高度、姿态和速度等与模式期望值的差异，产生控制飞机趋近需求模式的飞行状态引导指令.模式逻辑是选择飞行模式的离散算法，描述了系统模式选择和状态激活的行为.本文将FGS中的模式逻辑作为研究对象，建立SS模型.
飞行模式可以分为横向模式、垂直模式和偏航模式3个部分，横向模式沿飞机轴线调整侧滚角度控制水平运动，垂直模式沿机翼轴线调整俯仰角度控制竖直运动，偏航模式沿第三轴线控制飞行旋转.本节主要构建前两种模式下的简单飞行状态的需求模型，其中横向模式仅包含侧滚模式ROLL和航向选择模式HDG，垂直模式仅包含俯仰模式PITCH和垂直速度模式VS.传统的建模分析方法如：Markov Process[21]和故障树分析[22]等与系统规约形式之间有很大的不同，无法直接应用.而XMV模型不能直接接受包含多种模式转换和数值计算的FGS模型给出的自然语言需求的输入，也无法将这些需求转换为XMV可接受的类状态机模型.另一方面，基于表格表达式的SS模型对需求关系的描述能力很强，对于规范好的FGS系统需求可以实现模型的自动建立，但是缺乏自我验证的能力，本文给出的方法同时具备上述两种模型的优点，对FGS系统变量提取建立模型，通过模型转换算法得到XMV模型，然后进行属性验证.
6.2 变量提取
首先对系统中所需要的变量进行类型定义，除了基本的变量类型之外，FGS系统的自定义类型有表示指示灯亮灭的yLamp，其原始类型为枚举，枚举值有off(灯灭)和on(灯亮)，默认初始值为off；表示飞机超速提示的yOverspeed，其原始类型为枚举类型，枚举值有undefined(未知)、yes(超速)和no(未超速)，默认初始值为undefined；表示开关的ySwitch，原始类型为枚举类型，枚举值为off(关)和on(开)，默认初始值为off.
根据FGS的简单层次架构，FGS系统引入的数据有飞机超速提示Overspeed、自动驾驶仪接通提示AP_Engage_Switch、飞机控制面板控制提示FD_Switch、同步开关SYNC_Switch、航向选择开关HDG_Switch和垂直速度开关VS_Switch，将其作为系统输入变量，如表3所示.
表3 输入变量Table 3 Input variables
在FGS简单层次模型中，有AP、FD、HDG、VS、ROLL和PITCH系统状态机，各子系统间系统内互相独立，系统外互相关联，本文选取其中航向选择模式(HDG)作为典型实例，阐述模式建模过程.
模式间存在复杂的优先级关系，在HDG子系统中引入中间变量HDGNoHigher、HDGPressed、HDGSelect和HDGDeselect分别用于表示没有优先级更高的事件发生、HDG开关打开且被系统有效接收、选择和取消HDG模式，如表4所示.
表4 中间变量Table 4 Intermediate variables
根据已经定义好的中间变量，可以建立HDG模式表，用于表示飞机在航向选择模式下的状态切换，包括未知(undefined)、未选中(cleared)和被选中(selected)3个模式取值.表5是HDG模式迁移表，初始值为undefined.
表5 HDG模式类表Table 5 Migration table of HDG
FGS系统的输出主要表现在飞行显示面板上的模式提示指示灯，依赖于系统输入在模式逻辑的控制下的状态改变.如果指示灯亮，则对应飞行模式激活；如果指示灯灭，则对应的飞行模式未工作.每一个飞行模式和系统输入对应一个输出变量，输出变量如表6所示.
表6 输出变量Table 6 Output variables
6.3 属性验证
完成FGS的模型建立后，按照第4节的算法对模型进行平展简化，将HDG模式包含的上层约束中的HDGNoHigher 、HDGPressed 和HDGSelect等TO单元向下简化为SYNC_Switch和HDG_Switch等I单元，消除变量间的间接约束，直接构建HDG模式undefined、cleared和selected状态与HDG模式开关的关系.
按照第5节中定义的转换规则，将平展好的SS模型转换为XMV模型，并解释为nuXmv可输入的smv文件.其中包括开关类型的转换，根据变量转换算法，将抽取出的关于控制开关信息的输入变量转换为IVAR，将关于模式优先级信息的中间变量和关于信号灯信息的输出变量转换为VAR；根据约束转换算法，将HDG模式类表和变量表中抽取出来的变量的条件和事件关系转换为约束集合；根据输出赋值转换算法，将输出变量表中提取的赋值关系，转换为状态迁移关系.
验证安全属性是保证FGS系统安全性和正确性的重要方法，本文从FGS系统中抽取了系统需求规约，添加到smv描述文件中，对系统安全性进行验证.
正例验证，本文选取HDG模式的状态迁移规约.航向模式有undefined、cleared和selected这3个状态，当飞行模式打开，系统确认HDG激活，则从cleared迁移至selected；当飞行模式打开，系统确认HDG取消，则从selected迁移至cleared.若规约安全，将返回True确认该属性安全，给出时序逻辑规约描述如下：HDG模式不可能一直处于激活状态LTLSPEC !G(HDG=Selected)，具体正例验证如图7所示.
图7 实验结果图Fig.7 Experimental results
反例验证，本文选取HDG模式的状态迁移规约，注入错误规约，HDG模式将一直处于激活状态，这显然是不正确的性质规约.若规约不符合模型，将返回反例路径，提示属性不安全，给出时序逻辑规约描述如下：LTLSPEC G(HDG=Selected)，具体反例路径如图7所示.
7 相关工作与结束语
目前在安全关键领域，系统的安全性分析是提高机载系统软件需求规约正确性和一致性的重要方法.很多工业界和学术界的研究者所做的相关工作可以分为两类，其一是针对系统及软件需求问题进行建模分析工作：文献[5]介绍了应用于计算机系统的模型的安全评估方法及其对系统进行安全性分析的工作；在基于模型的评估方法上，SCR模型是一种较为常用的建模方法，文献[9]介绍了基于变量关系的SCR模型，并根据其建模方法对灯光控制系统进行形式化建模工作；文献[10]介绍了SCR方法解决了变量关系建模问题，提供了一套完整的系统形式化方法；其二是应用形式化工具进行分析与验证工作：文献[11]介绍了演绎证明、模型验证和抽象解释3种形式化验证的重要方法，并解释了形式化验证的过程.文献[14]和文献[15]介绍了能够描述抽象自动机，基于状态的自动化验证工具nuXmv，实现了使用nuXmv模型工具进行安全性评估和分析.
相较而言，当前的建模分析工作缺少形式化工具的深度验证，在需求的完整性和一致性上要求不够.对安全关键系统建模仅能描述系统的需求设计，而不能遍历检查系统的全部状态，不足以满足对于系统模型的精确分析和验证的要求.尤其是当现代的机载系统功能越来越复杂，规模越来越庞大，对于大量的需求规约，停留在建模阶段的形式化工作无法支撑其安全等级的任务要求.因此，用模型映射的方法，对SCR模型转换，实现系统全部状态的验证是本文的研究重点.
针对机载系统的安全性分析问题，本文提出了一种采用模型映射的验证方法，设计了从描述变量关系的SS模型到模型检测XMV模型的转换工具，能够自动化地完成模型编辑、模型转换的功能.在具体实现上，首先根据系统软件的关系逻辑建立系统的SS模型，设计变量关系平展简化算法，消除变量间递归且嵌套的间接约束定义，获得简单状态模型.借助语法分析工具ANTLR4，建立输入描述SS模型的语法文件的语法分析树，定义模型语法映射规则，通过遍历语法树结点，实现转换为XMV模型.最后，基于XMV模型使用模型检验工具nuXmv对安全属性规约验证，根据返回的结果找出系统设计的安全性问题，在系统失效前及时修改，保证关键系统的安全性.
未来的进一步工作由以下两方面构成：
1)本文给出的模型映射规则在约束元素上还有改进空间，将对时间[23]等复杂约束继续进行研究；
2)安全属性的抽取仍需要人工解释自然语言为标准规约语句，存在一定的局限性，之后将进一步提高工具的自动化程度，扩展其适用范围.
