0 概述

近年来, 国内外航天产品的质量稳步上升, 发射任务连续成功, 但是在总装和测试过程中仍出现不少质量问题。当前航天器的飞行任务愈加复杂, 在轨寿命越来越长, 大型航天器还要长期支持并完成各项试验任务, 软件系统需要发挥更重要的作用, 在这种情况下, 软件产品出现问题的次数在航天器发生质量问题的总次数中的占比可能会升高。航天飞行器的安全可靠离不开高质量、高安全性的软件, 而对于其中至关重要的控制系统软件, 即使其发生极其微小的故障, 也可能导致发射或飞行任务失败^[1]。文献[2]在对各类航天事故发生的原因进行分析后发现, 控制系统的开发在其需求描述阶段就已存在问题。一方面, 错误的需求描述直接导致设计的系统无法满足功能性要求; 另一方面, 模糊的、二义性的需求描述同样会使系统存在安全隐患^[3]。因此, 需求的规范描述是保障航天器控制系统安全与可靠性的第一步。

SCADE(Safety-Critical Application Development Environment)^[4]作为一个高安全性软件开发环境, 一直以来被广泛应用于航天器控制系统的设计和开发中, 其基于模型的开发方式备受青睐^[5]。同时, 形式化验证技术逐渐成为保障需求描述和软件系统一致性的手段^[6], 这是因为形式化验证以数学理论为基础, 使用严格定义的形式化语义来描述系统性质并建立模型, 其表达准确且无二义性^[7]。Design Verifier^[8]是一种SCADE的形式化验证组件, 能够用来描述和验证控制系统的需求, 通过基于SAT的模型检查算法验证系统的安全性^[9]。然而, 随着现代控制软件的应用场景愈加丰富, 软件需求愈加苛刻和多样, 软件系统的安全性与可靠性要求也逐步提高。在进行形式化逻辑时态描述时, 上述性质通常可以通过线性时态逻辑(Linear Temporal Logic, LTL)、计算树逻辑(Computation Tree Logic, CTL)等来实现^[10]。但是, Design Verifier并不支持时态逻辑规范描述, 无法使用LTL或CTL来规范系统的安全性需求, 这就意味着Design Verifier描述安全需求的能力是有限的, 尤其在描述与时序相关的性质时, 效果较差。然而, 时序性质对于安全攸关领域是十分重要的^[11], 特别是在航空航天领域, 控制系统的时序错误会造成无法预计的后果。因此, 安全攸关领域迫切需要SCADE拥有验证多种时序性质的能力。

为满足航空航天等领域对控制系统软件的安全性和可靠性要求, 本文构建基于STP方法的SCADE状态机(SCADE State Machine, SSM)模型验证框架, 将SSM转换成模型检查器NuSMV的输入模型, 为SCADE形式化验证引入时序性质验证, 以完善SCADE高安全性软件开发过程的系统设计, 使用户能够在系统设计阶段减少潜在的模型设计错误, 保证航天器系统的安全性与可靠性。

1 相关概念 1.1 SCADE层次化状态机的定义

SCADE既是一种模型语言, 也是广泛应用于安全攸关系统上的基于模型开发的建模工具。许多SCADE模型都是由状态机与数据流这2种建模方式混合建立而成的。而在安全攸关领域, 非常适合利用以状态机为主导的建模方式来描述控制系统的行为。

SCADE模型通常包含许多操作模块, 每一个模块都有输入变量、输出变量和局部变量。SCADE支持基本的操作符, 例如数学运算操作符、逻辑运算操作符、比较运算操作符以及时间运算操作符等。对于用SSM建立的模型, 其行为由各个状态机决定, 而状态机中的状态可描述具体的操作, 其既可以用数据流表示, 也可以用一个子状态机来描述。因此, 在SCADE中, 通常会使用层次化状态机来建立控制系统模型。为方便描述本文内容, 首先对SSM进行形式化定义。

定义1  一个层次化SSM的结构是一个5元组〈I, O, SM, Op, Fun〉。其中, I、O分别为输入、输出变量的集合, SM={SM₁, SM₂, …, SM_n}是子状态机集合, SM_i代表第i个子状态机, Op为状态机中用到的运算操作符集合, Fun为状态机调用的用户自定义函数节点的集合。

层次化状态机可以包含多个子状态机SM_i, 其中, SSM为最顶层的状态机^[12]。状态中的数据流操作会用到一些运算操作符, 即为集合Op的元素。由于SCADE支持用户将一些较复杂的函数单独建立在某个函数节点中, 供建模时复用, 因此在状态中也能调用上述函数, 这些用户自定义的节点组成Fun集合。

定义2  子状态机SM_i的结构也是一个5元组, 表示为〈S, s₀, Sub, Trans, Act〉。其中, S为子状态机中状态名的集合, s₀为其初始状态, Sub:S→P(S)是描述状态及其子状态机之间关系的一个函数映射, Trans $ \subset $ S×G(Var)×S是状态迁移关系的集合, Act$ \subset $ S×O×2^Op×2^Fun为该子状态机中各状态的行为操作集合。

函数定义了一个状态与其子状态的映射关系, P(S)代表状态s_i∈S的子状态机集合。G(Var)是由变量组成的转移条件表达式, 当该表达式为真时发生状态转移, 并且一个子状态机的转移只会发生在同一层次的状态之间。集合Act中的元素用来描述在特定状态下对特定输出变量的操作行为, 且这些状态会用到运算操作符或用户自定义的函数节点。

图 1是一个SSM的示意图。在图 1中, SSM有一个输入变量x和一个输出变量o, 并且有2个子状态机SM₁和SM₂。该SSM的状态使用加法运算操作符(plus)、乘法运算操作符(multi)以及一个用户自定义的函数节点(fun)。基于以上定义, 可以将顶层状态机表示为:

$ S S M=\left\langle\{x\}, \{o\}, \left\{S M_{1}, S M_{2}\right\}, \{\mathrm{plus}, \text { multi }\}, \{f u n\}\right\rangle $

对于子状态机SM₁而言, 其状态集合表示为S={A, B}, 初始状态s₀=A。由于状态B的子状态机是SM₂, 因此子状态关系(B, SM₂)∈Sub。Act的元素代表在某状态中对特定输出变量的操作, 因此, SM₁中有(A, o, {plus, multi}, $\emptyset $)∈Act, 类似地, 在SM₂中则有(B, o, $\emptyset $, {fun})∈Act。

1.2 模型检查器NuSMV

NuSMV^[13]是一个开源且成熟的模型检查工具, 其由卡耐基梅隆大学开发的基于行为驱动开发(Behavior Driven Development, BDD)的模型检查器发展而来。新版本的NuSMV整合了基于SAT的模型检查算法, 非常适用于时态逻辑的模型检查, 能够用来描述各种异步或是同步的, 抽象或是具体的有限状态机。用NuSMV语言描述的有限状态机通常包括状态变量声明、初始化状态定义、状态转移关系以及变量赋值等。图 2给出一个NuSMV模型的例子。其中, MODULE关键词定义一个状态机模型, VAR声明一个状态变量s, 且其拥有2个状态s1和s2, IVAR声明一个布尔变量a, 在ASSIGN代码块中, init语句定义状态机的初始状态为s1, 而next语句则定义状态转移关系。在NuSMV中, 与模型相关的性质可以使用LTL与CTL逻辑表达式描述, 通过NuSMV模型检查算法便可验证模型是否满足上述性质规范。

本文方法将SSM模型转换为NuSMV模型是基于以下4个原因:

1) NuSMV拥有准确的模型语言, 可确保SSM模型转换后的目标模型拥有正确的语义。

2) NuSMV内置高效的模型检查算法, 支持时序性质验证。

3) NuSMV的形式化规范描述简单易写, 在性质表达式前加上LTLSPEC或CTLSPEC关键词即可, 使用方便。

4) 考虑到SSM的层次化特性, NuSMV的模块化建模方式非常适合表达层次化结构的SSM。

2 SCADE状态机形式化验证框架

本文提出的SCADE状态机验证框架基于Scade2Nu验证工具, 将形式化验证中的时序性质验证技术引入系统模型的安全需求验证中, 具体结构如图 3所示。

由图 3可知, 该框架将SCADE模型与模型检查器NuSMV连接起来, 把SCADE模型有效地转换到NuSMV模型上。SCADE支持用户将图形化模型转换为对应的SCADE文本模型。通过Scade2Nu进行语法解析, 能够得到1.1节所定义的SCADE状态机实例, 从而得到最终的NuSMV模型。此外, 需要将自然语言需求重写为LTL或CTL规范, 然后同模型一起输入到NuSMV中, 便能得到验证结果, 确定SCADE模型是否满足系统需求, 再根据反馈结果调试模型。利用Scade2Nu工具实现形式化验证框架后, 在使用其进行安全性验证时, 需要用到相应的组件, 其具体过程可分为SCADE文本模型解析、符号表容器装载和目标模型转换3个步骤。

2.1 SCADE文本模型解析

导出的文本模型实际上是由SCADE语言描述的, SCADE的数据流语言由同步数据流语言Lustre^[14]发展而来, 其控制状态机是基于StateCharts^[4]的。目前, SCADE语言已形成成熟的词法及语义, 其官方参考手册^[15]定义了具体的语言结构。ANTLR^[16]是一个强大的解析工具, 可以用来读取、处理、执行以及翻译结构化文本。Scade2Nu根据《SCADE语言参考手册》将SCADE语言的静态语义以特定的格式写入ANTLR语法文件中。在这一过程中, 可以得到对应SCADE模型的语法树, 并在生成基础的监听器接口之后进行语法树的遍历。

2.2 符号表容器装载

Scade2Nu使用ANTLR Runtime API遍历语法树的监听器。Scade2Nu将定义1与定义2转换为一个符号表, 将遍历后模型的语法树信息存储进符号表容器中, 作为后续步骤中模型转换器的输入。

在进行下一个步骤之前, 需对SCADE模型中的变量边界进行优化。系统规模会影响Scade2Nu的验证, 而状态爆炸一直是模型检查中的一个重要问题^[17]。许多抽象优化方法可用于减少状态爆炸发生的概率, 当前版本的NuSMV由于同时支持基于BDD和基于SAT的模型检查, 其解决状态爆炸问题的能力大幅提高^[18]。然而, 实际SCADE应用的变量区间可能较大, 因此, 即使NuSMV使用符号模型检查技术, 当变量规模太大时, 也会难以验证。Scade2Nu可提供对变量边界的优化选项, 从而减少模型中的状态爆炸。该技术属于一种简单的抽象技术, 通过设置变量的边界来降低NuSMV模型中状态的复杂性, 减少状态空间, 从而提高验证效率^[19]。

2.3 目标模型转换

在进行目标模型转换时, Scade2Nu将SCADE状态机实例转换到NuSMV输入模型中, 最终生成4类目标代码块, 分别是子状态机模块SM_i、变量监控模块Set_Var、函数模块以及顶层状态机模型。本文基于STP方法^[20], 从2个方面定义转换规则:1)层次化状态机的转换; 2)改进后的SCADE变量监控机制。

2.3.1 状态机层次化结构

SCADE模型中的每一个子状态机对应于目标模型中的一个SM_i模块, 通过引入STP模型, 转换框架中的参数active与default可在NuSMV目标模型中构建状态机的层次化结构。

引入参数active的目的是为了消除SCADE状态机与NuSMV状态机模型在激活时间上的差异。在SCADE状态机上, 当一个父状态被激活时, 该父状态下的子状态机也随之激活。而对于NuSMV语言结构, 简单地将每一个子状态机直接转换成对应的SMi模块, 并不能建立SCADE的激活方式, 因为NuSMV模型中的所有模块都会在最开始时进行初始化, 并在之后一直处于激活状态。显然, 当对应的模块不应该在某些周期中被激活时, 目标NuSMV模型需要以某种方式明确指出, 从而防止该模型对变量造成错误操作。

对于SCADE状态机, 当其子状态机从激活状态变为非激活状态时, 该状态机中的状态转移关系将会重置, 以确保下次被激活时会首先激活其初始状态。在NuSMV中, 当一个状态机的active参数为假时, 则等同于该状态机为非激活状态, 但是如果不设置参数, 则无法保证下次一定是初始状态被激活。通过引入参数default能解决上述问题, 设其为真, 目标模型就能确保每次进入子状态机时激活初始状态。

假设S是状态机SM_i的一个状态, SM_j是状态S的子状态机, 且该子状态机有状态s₁, s₂, …, s_n。在NuSMV目标模型中, 状态机SM_i与SM_j的层次化结构如图 4所示。其中:规则1为参数default的转换规则; P₁, P₂, …, P_n是状态S的前继; 规则2为参数active的转换规则, 即当SM_i激活且处于状态S时, 其子状态机SM_j也被激活。在每一个子状态机模块中还需定义状态转移。状态转移只有当所处状态机被激活时, 才会经过转移条件到达目标状态。图 5给出一个状态转移规则, 其中, guard(s, t)是状态s到状态t的迁移条件, 规则3定义了状态转移的转换方式。当子状态机第1次被激活时, 会触发其初始状态转移s₀, 这类初始状态转移的情况由规则4定义。

2.3.2 SCADE变量监控机制

在STP方法中, 监控机制是指对于StateCharts中的每一个事件变量或者条件变量var, 都有一个对应的模块通过监控参数来进行操纵。然而, 该方法将事件或者条件变量抽象为一个布尔型变量, 其不适用于SCADE的每个状态都拥有不同数据类型操作的情景。在SCADE转状态机中, 一个状态s会对输出变量var进行特定的操作, 因此, 将STP方法中的2类监控参数set_m与reset_m精化为set_{(var, s)}与reset_{(var, s)}。

令v₁, v₂, …, v_i, …, v_n是一个SSM的所有变量, 状态s₁, s₂, …, s_m中拥有对变量v_i的操作。图 6给出变量监控模块的转换规则。其中, 规则5读取相关的监控参数(re)set_{(var, s)}, 该参数在特定状态中对输出变量v_i进行赋值。这些赋值表达式属于数据流操作, 转换器会将其直接翻译成对应的NuSMV表达式。由于其中一些表达式会调用到用户自定义的函数节点, 因此当操作中使用到这些函数节点时, 需要在模块上添加function₁, function₂, …, function_k的声明。此外, 这些监控参数还需要在子状态机的模块SM_i中定义赋值语句, 保证其值随着状态改变而不断更新, 从而控制输出变量的操作。

1) set_{(var, s)}的赋值规则

令当前起始状态为s, T₁, T₂, …, T_m是状态s的后继状态, guard(s, T_i)表示从状态s到T_i的转移条件, i∈{1, 2, …, m}。在SCADE状态机中, 若状态s的所有转移条件都不满足, 则下一个状态依旧是s, 并在下一周期执行状态中的操作。如图 7所示的规则6, 当状态s所在的状态机一直被激活时, 若不满足转移条件, 则设置set_{(var, s)}的值为True, 否则为False。规则中的set_var_s等同于set_{(var, s)}。

2) reset_{(var, s)}的赋值规则

令状态s是P₁, P₂, …, P_m的目标状态, 从状态P_j到状态s的转移条件记作guard(P_j, s), i∈{1, 2, …, n}。当guard(P_j, s)的其中一个转移条件满足时, 系统会到达状态s, 监控参数reset_{(var, s)}会被设置, 赋值规则如图 8所示。需要注意的是, 若目标状态s是某个子状态机的初始状态, 要将该监控参数设置为True。规则中的reset_var_s等同于reset_{(var, s)}。

图 9给出SCADE变量监控机制。系统变量的值以及状态中的操作会改变状态转移条件, 而这些状态转移则会更新监控参数的值。变量监控模块通过读取监控参数的值来更新输出变量, 变量值在被状态和迁移表达式读取后会再次影响各状态机的运行, 而这正是监控参数能间接控制SCADE状态机的原因。

函数节点模块通过集合Fun生成。每一个函数节点都有其输入与输出变量。由于本文的函数节点仅限数据流形式, 因此Scade2Nu可以直接转换每一个等式。在最终的NuSMV输入模型中, 有且仅有一个main模块来处理顶层状态机的事务, 其中包括在该模块中声明的输入输出变量、监控参数和实例化子状态机模块、变量监控模块以及函数节点模块。最终生成的模型整合了子状态机模块SM_i、变量监控模块Set_Var、函数模块以及顶层状态机模块这4类模块。

3 案例研究

本文使用上述架构验证一个卫星控制系统的安全性。卫星控制系统中一个子系统的SCADE状态机模型如图 10所示。该状态机用来控制卫星的各个不同的工作模式, 由SM₁和SM₂ 2个子状态机组成。当系统接收到分离信号(depart_signal)时, 开始进行星箭分离, 并且SM₁中的未分离状态(Before_Depart)发生状态转移。

在星箭分离后, SM₁中的分离后状态(After_Depart)被激活。由于SM₂是该状态的子状态机, 因此SM₂也随之运转。卫星的速度阻尼模式(Initial)也在此时被激活, 待时间信号(time_signal)大于4个时间单元后, 卫星进入等待模式。该模式会激活一个时间节拍计数器(Per_Count), 系统在满足一定的时间节拍后才能进行模式切换。在等待模式中, 节拍计数器会开始计时, 满足一定条件后(enterWheel), 卫星即可切换到飞轮控制模式(Wheel_Control)。飞轮控制模式是大多数卫星长期运行和进行业务的工作模式, 该模式也有一个节拍计数器。在卫星工作一段时间后继续回到等待模式, 以节约卫星能源。状态机拥有的变量如表 1所示, 系统的2个安全需求描述如下:

1) 卫星控制系统在星箭分离后总是会先进入速度阻尼模式, 当接收到的时间信号大于4个时间单元时再进入等待模式。

2) 在星箭分离后, 卫星控制系统进入等待模式, 经过5个时间单元进入飞轮控制模式开始工作, 再经过10个时间单元回到等待模式。

3.1 Scade2Nu状态机验证

本文使用Scade2Nu来验证卫星控制系统的2种安全需求, 同时验证本文方法的有效性。整个实验过程可分为变量边界优化、规范时序性质描述、SCADE文本模型导入及转化、模型性质验证4个步骤, 并对验证结果进行分析。

3.1.1 变量边界优化

首先需要为模型设置变量边界, 从而优化NuSMV中的状态规模, 边界设置如表 2所示, 其中布尔类型的变量只需设置默认值。从SCADE模型和需求可以看出, 最大的间隔时长是10个时间单元。时间信号(time_signal)需要判断的边界是10, 因此将该变量范围设置在0~10即可; 时间节拍计数器(Per_Count)对应变量的最大取值是12, 因此将其数值范围设置在0~12。从模型的工作模式可以看出, 卫星系统工作模式信号的取值只能是0、1、2、3, 因此该变量的范围可精确设置为0~3。

3.1.2 时序性质描述规范

为了使用本文方法进行形式化安全验证, 首先要使用时态逻辑规范将所需验证的自然语言需求重写成时序逻辑表达式, 具体如下:

需求1   ((sysmode =0 ∧ depart_signal → (X sysmode = 1)) ∧ (sysmode=1 ∧ X time_signal > 4 →X sysmode = 2))。

需求2   ((SM_SM1.state = After_Depart ∧ sysmode = 1 ∧ X sysmode = 2) →([1,6] sysmode = 2 ∧ [7,17] sysmode = 3))。

这些表达式通过时态逻辑操作符, 用严格的数学语义、逻辑命题方式和时间算子将需求描述清楚, 并作为NuSMV的性质输入。

3.1.3 SCADE文本模型导入及转换

SCADE支持用户直接导出其SCADE语言文本模型, 该文本模型是SCADE图形化模型的另一种等价表达。Scade2Nu工具将该文本模型和变量边界优化表作为输入, 通过模型转换算法将其转换成NuSMV模型。

3.1.4 模型性质验证

通过NuSMV中的关键字LTLSPEC, 将用时态逻辑表达好的性质规范追加到生成的NuSMV模型之后。Scade2Nu与NuSMV检查器进行整合后, 支持用户在图形界面中进行模型检查, 因此无需再使用命令进行操作, 通过右击生成的模型即可开始验证。

3.1.5 验证结果分析

Scade2Nu的验证结果表明, 需求1能够被系统满足, 而需求2不能满足, 因此输出反例。通过分析该反例找到原模型中的设计缺陷是模型检查的优点之一。Scade2Nu通过将状态执行的反例结果可视化成表格数据来增强反例的可读性, 如图 11所示。在图 11中, 每一行对应路径中的一个执行状态, 每一列对应该状态中变量的取值。分析需求2的描述可知, 卫星系统必须满足以下条件:切换到等待模式后(耗费1个时间单元), 继续持续5个时间单元, 之后切换到飞轮控制模式(耗费1个时间单元)并工作10个时间单元。这些时间单元通过输出变量Per_Count进行记录, 其中也给出反例执行路径中该值的变化情况。通过分析发现, 当前的模型在系统模式(sysmode)切换到等待模式(sysmode = 2)后, 节拍计数器又记录了6个时间单元, 同样地, 当前系统在系统模式切换到飞轮控制模式(sysmode = 3)后, 节拍计数器又经过了11个时间单元。导致该路径发生的原因是切换条件的设计错误, 从原SCADE模型中看到, 切换条件变量enterWheel与enterWait的赋值操作中都使用了严格大于操作符, 因此, 本文将其修改为大于等于操作符。经过再次验证后, 系统可以满足需求2。

3.2 Scade2Nu验证框架评估

使用Scade2Nu验证框架, 用户可以验证SCADE状态机模型的安全需求, 从而找出模型的设计错误, 直到需求能够被系统全部满足。Scade2Nu验证框架的优势在于其为SCADE模型引入新的需求规范表达方式, SCADE用户不再局限于使用Design Verifier来对需求进行图形化建模, 而是可以使用LTL和CTL逻辑表达式来描述性质。由于NuSMV支持LTL与CTL的表达, 因此拓展了SCADE对系统需求的描述能力。在时序相关的需求上, 与LTL和CTL相比, SCADE语言无法描述诸如总是(Globally)、最终(Finally)等无边界的时态逻辑。在Scade2Nu工具中引入带时间边界的LTL、实时CTL等, 使得该框架可以描述更复杂、更精确的时序性质。

4 结束语

本文构建一种SCADE系统模型形式化验证框架。将SCADE状态机转换成NuSMV模型, 通过时序性质规范进行模型检查。把时序性质验证技术引入SCADE的分析中, 使SCADE用户能够使用LTL以及CTL逻辑规范来描述系统模型的需求。分析结果表明, 该框架可有效验证系统是否满足时序安全需求, 帮助用户在系统模型设计阶段及早发现缺陷并进行改正, 减少开发成本, 缩短开发周期, 确保安全攸关领域软件系统的正确性与可靠性。同时, 根据检测出的安全漏洞的数量和危害, 可进行软件的可信度量和评估。由于SCADE状态机中的状态转移拥有优先级, 例如弱转移、强转移以及同步转移, 而Scade2Nu是基于转移优先级相同的假设, 因此下一步将对拥有不同转移优先级的SCADE状态机进行研究。