0 引言

基于ARP 4754A^[1],ARP 4761^[2]的传统安全性评估流程在民用航空领域已经得到了广泛的应用。然而,近20年来计算机科学与集成电路制造工艺的发展促使了产品机电系统的深度融合,嵌入式软件控制方式逐渐代替传统的机械控制,系统复杂度急剧上升。传统安全性评估流程严重依赖于安全分析人员的经验,面对新型安全关键系统软硬件深度集成,复杂度高的特征时,面临着系统描述能力不足、分析结果不准确、分析工作迭代困难等问题^[3-4]。

针对系统安全性研制流程中产生的新问题,在系统工程思想指导下,一种面向基于模型的系统工程的新型安全性评估理念^[5-8]——基于模型的安全性评估(Model-Based Safety Assessment, 简称MBSA),得到了学术界与工业界的广泛认可。在基于模型的安全性评估过程中,安全性要求的评估通过模型检查等形式化方法自动实现^[9-10]。通过在安全性评估过程中引入形式化的模型与规范,将评估过程转化为系统模型的规范验证过程。

本文采用当前MBSA研究领域较为成熟的模型检查方法,针对模型检查的建模特点,基于SMV语言提出安全性建模与规约方法。以某延程型宽体客机飞控系统为对象,构建该机型飞控系统的功能模型,并定义形式化的安全性要求,开展安全性评估,从而验证基于形式化方法的安全性评估在民机系统安全性工作中的可行性。

1 模型检查的基本内涵

模型检查是形式化方法的重要分支^[11],基本思想是利用时态逻辑描述目标系统所需满足的性质φ,有限状态机(FSM)描述系统的状态转移关系s,以及模型检查的算法遍历FSM来检验时态逻辑公式的正确性,即s╞φ,如图1所示。对不满足的系统规范,可以得到一个反例,说明系统不满足要求的状态路径。

模型检查所构建的系统模型往往并非目标系统实际所采用的建模形式,因此必须将目标系统转换为某一模型检查工具所支持的输入形式。构建系统模型时需要结合待验证的属性对系统进行必要的抽象和简化。建模时抽象度过高会导致模型与真实系统差别增大,导致验证工作漏掉某些真正的错误,而抽象程度过低则会增加验证模型的复杂性,因此对模型抽象的过程在整个模型检查过程中需要占用大量的时间。

1.1 有限状态机

模型检查中系统模型的有限状态机称为Kripke结构。Kripke结构是一种严格的数学结构,是状态转移图的一种变形,能够很好地描述系统的状态转移及时序逻辑关系。典型Kriple结构是一个五元组:

$M=⟨S,S_0,R,L,AP>$

其中:S是有限状态集合,$S_0\subseteq S$是初始状态集合,R表示状态转移关系,$R\subseteq S\times S,L:S\to 2^{AP}$称为标记函数,用于标记每个状态中成立的所有原子命题集合,AP是所有原子命题与其否命题的集合,该集合是AP的一个子集。

在一个Kripke结构M中,从任意某一状态s开始产生的无限长的状态序列n=s₀s₁s₂...被称为该结构中的一条路径,该路径中s₀=s,对所有i ≥0,都有R(s_i,s_i+1)成立。系统动态运行中的属性通常描述为一系列原子命题的动态满足过程。

图2左边为一个简单Kripke结构的示例,圆表示状态,箭头线代表状态转移关系,箭头两端的状态及转移的首位两个状态,没有起始端的箭头表示系统进入初始状态,状态内标注的原子命题组成Kripke的标记函数,当某一状态激活时,状态内的原子命题成立。

对于该Kripke结构,$S=\left\{s_o,s_1,s_2\right\},S_0=\left\{s_o\right\}$,$AP=\{a,b,c,\neg a,\neg b,\neg c\},R=\left\{<s_0,s_1>,<s_1,\right.s_2>,\left.⟨s_2,s_0>,⟨s_0,s_2⟩\right\},L\left(s_0\right)=\{a,b\},L\left(s_1\right)=\{a,c\},L\left(s_2\right)=\{b,\neg c\}$,将系统状态关系展开得到图2右侧所示结构。

可以得出以下结论,Kripke结构的状态关系展开类似树状结构,除去根节点外,每一节点仅有一个前端节点,可以任意访问其后端节点,从而构成一棵无限深度的树。

1.2 时态逻辑

时态逻辑公式是模型检查中用于描述动态系统属性的形式化命题方法。常见的时态逻辑包括两种:线性时态逻辑(linear temporal logic,简称LTL)与计算树逻辑(computation tree logic,简称CTL)。

线性时态逻辑将系统时间定义为无限长的时态序列,称为计算路径,当前时刻存在唯一的下一时刻状态,对于存在多种未来状态的系统,利用一组路径表示不同的时态序列。线性时态逻辑命题由时态算子与原子命题组成。常用时态逻辑算子包括:

G(Glabal):未来所有状态;F(Final):未来某个状态;X(neXt):下一个状态;U(Until):直到…都;R(Release):直到…才;W(Wait):弱…直到。

线性时态逻辑无法描述多条路径之间的相互关系,在描述分支并发系统时,采用计算树逻辑描述系统时间特性。计算树逻辑以Kripke初始节点为根节点,将Kripke结构展开为无线树形结构,相比线型时态逻辑,计算树定义路径量词A(对于所有路径)与E(存在一条路径),且不存在时态算子R、W。

2 系统建模方法及安全属性定义

2.1 系统模型构建方法

不同模型检查工具对应不同的自动机语言,构建系统模型时需要根据特定语言的特点确定模型结构与部件描述方式。以SMV为例,构建系统SMV模型的基本步骤如下:

1)确定目标系统的基本结构,包括系统层次划分与同一层次的部件,为每个部件及系统层级定义Module,按照系统自上而下结构从模型main模块开始逐层实例化。

2)根据部件内部工作情况与部件间接口关系,定义各个模块所需内部变量及类型,确定每个模块输入变量。系统模型的状态空间规模由变量数量决定,在定义变量过程中应尽量减少冗余变量。

3)在每个模块的ASSIGN及DEFINE部分定义系统行为。根据MBSA模型构建的两种策略,失效建模分为名义系统+故障注入以及直接失效行为两种,图3和图4分别描述了两种建模方式。名义系统+故障注入的方式将部件模型分为名义模块nominal_comp与失效模块failure_comp两部分,在另一模块extend_comp中实例化两类模块,根据部件状态调用nominal_comp与failure_comp中参数值;直接故障行为描述则在同一模块中同时定义正常与失效状态输出。

2.2 安全属性的定义

传统安全性评估过程中,通过FHA确定初始安全性要求,并在研制流程中逐渐细化分解。模型检查的验证与分析工作在原有研制流程基础上开展,通用自动化检验是否满足安全属性来判断系统的安全性水平。系统安全属性的来源包括:FHA结论,初步故障树结论及FMEA,前一阶段模型检查所得结论等。

将已知的安全性需求形式化表示为时态逻辑命题,要针对时态逻辑命题所涉及的部件,在模块中定义相应原子命题的标识变量。以图4为例,如果需要定义安全属性为:部件在failure_mode1时value值不能低于5,利用CTL公式可以定义为:

$\mathrm{A}\mathrm{G}\text{( work=failure\_mode1}>\text{failure\_comp.value}>=5\text{)}$

选择CTL或者LTL的基本原则是依据命题的描述特性。对于存在类型的命题,例如证明系统能否到达某一状态,可以采用CTL描述特性;对于强调状态序列特性的问题,例如某些状态的先后次序,可以采用LTL描述。

3 某民用飞机案例验证

3.1 民机飞控系统

某民用飞机采用电传+机械的组合控制模式,其功能控制模型是软件、硬件、机电结构高度综合的复杂系统,以副翼控制功能为例,考虑影响副翼控制功能的飞控部件,简化飞控系统功能模型如图5所示。

杆位移传感器、惯性测量组件将动作数据及测量数据输入至飞控计算机,由飞控计算机解算得到的相应控制信号经伺服放大回路输出值左右副翼舵机。28V交流发电机与永磁发电机为飞控计算机供电。建立系统模型时,考虑飞机在AFCS、DDC、EFCS三种工作状态下的部件接口关系差异,其中飞控计算EFCS板仅在EFCS模式下运行,DDC模式下MBI与AIN板工作状态对副翼控制功能无影响。根据系统描述构建SMV模型,图6所示为飞控计算机MBI板SMV模块示例。

定义系统安全属性为左右副翼舵机不能同时进入失效状态,将命题形式化描述如下:

$\text{AG! (}\text{left\_servo}\text{.status=failure\&}\text{right\_servo}\text{.}\text{sta}\text{-}\text{tus}=\text{failure})$

3.2 NuSMV仿真

模型检查在检测系统规范时会遍历系统状态空间,基于BDD的NuSMV模型检查器目前能够支持2¹²⁰的状态空间,但是运算时间会随着系统状态空间的扩大迅速增加。因此在执行系统规范的严格检查之前,运用仿真方式模拟系统状态变化路径,对系统行为进行初步的分析。案例所建系统包含69个变量,系统可达状态数达到2⁶³次。通过仿真寻找系统失效路径,图7所示为其中一条包含50个仿真步长单位的系统失效路径。

图7所示的一条状态路径展现了一个特定失效场景,State1.1为系统初始状态,飞控系统处于PFCS工作模态,部件运行正常,State1.2时28V发电机发生失效,State1.18时系统进入DDC工作模态,惯性测量组件失效对系统功能无影响,State1.51时右副翼舵机失效。

3.3 系统规范验证

NuSMV系统模块运行方式分为同步与异步两类,模型检查及仿真过程中状态空间与模块运行方式有关,在验证系统规范时,采用同步运行方式以降低状态空间规模,提高检查效率。在NuSMV Shell中执行:

$\text{check\_ctlspec}\text{\&}\text{show\_property}$

命令得到规范检查结果如图8所示。

检查发现命题:

$\text{AG! (}\text{left\_servo}\text{.status=failure\&}\text{right\_servo}\text{.status}=\text{failure})$

是错误的,分析生成的反例可知系统在EFCS模式下发生了EFCS板的同时失效,此时可以根据系统反例所描述的失效场景通过限制条件的异步仿真寻找EFCS板同时失效的原因。

4 结论

本文针对模型检查器NuSMV的特点,提出基于SMV语言的安全性模型构建思路,阐述了系统规范的来源与实现方式,并通过典型民用飞机电传飞控系统案例演示利用NuSMV建模与属性验证过程。

NuSMV作为最经典的模型检查工具,基于BDD的运算方法虽然提高了执行效率与建模规模,但仍在定量计算、反例优化等方面存在局限。作为MBSA的核心工作,如何协调安全评估与模型检查的关系仍然值得研究。

参考文献