安全关键系统需求形式化建模分析实例研究*

张维珺，胡 军，李宛倩，陈 朔，石梦烨，唐红英

南京航空航天大学 计算机科学与技术学院，南京 211106

1 引言

20世纪70年代，飞机电子系统迅速向数字化、综合化和模块化方向发展，80年代末更是出现了综合模块化航空电子系统（integrated modular avionics，IMA）[1]的概念。微电子和软件技术的迅速发展使得综合模块化航空电子系统[2]日益成熟，其包含的系统组件逐渐完善。然而，随着系统中各组件之间的交互变得更加紧密，组件之间的相互作用更可能产生故障进而演变成事故，机载系统的安全性至关重要。

近年来，基于模型的安全性分析技术及其应用越来越受到工业界的关注，在航空等领域有着广泛应用。相关学者亦对其进行研究和实践，例如使用MBSA（model-based safety analysis method）[3]方法及NuSMV（new symbolic model verifier）语言对飞控系统的前主桨舵机进行建模与验证[4]；基于MBSA对高速铁路牵引供电系统进行安全风险评估[5]；分析及验证MBSA能够解决传统安全性分析中飞机级安全性评估不足的问题[6]等。

本文主要研究以xSAP（extended safety assessment platform）系统安全性评估平台为核心的MBSA方法，对实际数字自动飞行控制系统GFC700中的飞行引导系统进行需求性建模、系统故障设计以及安全性分析。

文章组织结构安排如下：第2章简单介绍基于模型的系统安全性评估技术和形式化模型；第3章介绍基于形式化模型的系统安全性分析框架及其核心问题，即层次化建模、故障注入以及模型扩展等；第4章简要介绍飞行引导系统，详细阐述对其设计的两种故障模式，描述如何使用xSAP平台对飞行引导系统进行形式化建模、故障设计以及模型扩展，运行xSAP工具对飞行引导系统进行安全性分析，生成故障树[7]及 FMEA（failure mode and effect analysis）表[8]；第 5章对已有工作进行总结。

2MBSA和形式化模型

2.1 基于模型的安全性分析方法

基于模型的安全性分析方法（MBSA）采用一种基于模型的系统开发过程去创建一个“共享的系统模型”,这个共享的系统模型可以同时被系统设计过程和系统安全评估过程所使用[9]，即在系统设计过程中使用一种建模语言描述正常运行条件下的系统架构以及安全关键功能行为，在系统安全评估过程中基于所建立的系统正常模型进行失效行为的语义扩展，生成用于安全性分析的故障扩展模型。

2.2 形式化建模与分析

形式化方法即在对计算机系统中的硬件和软件进行规约、设计和分析的过程中所使用的基于数学理论的描述形式和分析技术。在系统工程领域中，对于系统建模而言，采用基于数学语义的形式化建模语言可以使得所建立的系统模型具有严格的语法和语义定义，采用形式化分析的技术可以对系统模型进行分析和判定，进而支持和指导系统的开发过程。因此形式化方法在基于模型的系统工程中极为重要。

3 基于形式化模型的系统安全性分析

3.1 基于形式化模型的系统安全性分析框架

图1给出了基于形式化模型的系统安全性分析框架。起点是基于系统需求的形式化模型，通常它只包含正常系统的功能行为，即没有考虑故障行为。该模型或直接被使用于系统的安全性与功能性验证，或被进行故障注入与模型扩展，而后用于系统的故障分析等安全性评估。需要注意的是将正常模型扩展成系统故障模型的过程基于故障注入的概念，即不能一次性地建立既包含系统正常行为又包含故障行为的模型，否则考虑因素太多，建模过程太复杂。

Fig.1 Framework of system safety analysis based on formal model图1 基于形式化模型的系统安全性分析框架

基于形式化模型的安全性分析方法的重点是如何构建系统的形式化模型以及如何对系统行为中的故障进行设计并将故障扩展到系统正常模型中。层次化建模、故障注入和故障模式及模型扩展是该方法必须解决的核心问题。

3.2 安全框架中的核心问题

3.2.1 层次化建模

一个安全关键复杂系统的需求规约数量较为庞大，有时甚至有数千条。如果将这些规约放在同一层次进行建模和分析，会使得建模工作变得繁杂混乱，对于模型的形式化验证也可能会出现状态空间爆炸的问题，从而无法进行验证。因此，需要考虑层次化的建模方式，使用渐增式的方法进行分层验证。以飞行引导系统（flight guidance system，FGS）为例说明分层验证的必要性。

由于飞行引导系统中的飞行模式总类较多，相互之间存在层次关系，对飞行引导系统完全建模的工作较为复杂，代码量较大，在运行的过程中错误不容易修改，因此将飞行引导系统分为四层，逐层建模，如表1所示。

Table 1 Layer structure of FGS表1 飞行引导系统分层结构

3.2.2 故障注入机制

故障注入机制即在正常功能模型中添加已设定好的故障事件，该事件仅为相应故障模式在正常功能模型中的声明，亦为将故障模式扩展到正常功能模型的接口。通常一个正常功能模型包含多个功能模块，故障注入需要应用于每一个模块。对于同一模块，需要设置不同的故障模式控制变量；对于不同模块，可以有相同的故障模式控制变量，以表示不同模块间的同一种故障事件。故障注入机制如图2所示。

Fig.2 Fault injection图2 故障注入机制

3.2.3 故障模式及模型扩展

上述故障注入机制发生在正常功能模型建模阶段，故障模式的设定以及故障模型扩展则发生在故障分析阶段。故障模式的规约信息被包含在故障事件及相应的控制变量中，而其具体定义则体现在故障扩展指令文件 FEI（fault extension instructions）中。故障模式的具体定义依赖于故障模式模板，由故障分析工具中的故障库提供。例如，基于模型的安全性分析平台xSAP会为使用者提供一个故障模式的预定义库，即通用故障模式库，其模板包括：反转故障inverted、卡死故障stuck_at(value)（在某个值卡死）及cstuck_at（在某个变量卡死）、随机random（不确定的输出）等。在故障模式的设定过程中，可直接使用故障模式库中已定义好的故障模板，也可自定义故障模板。故障可以被声明为永久性的或偶发性的，当故障被声明为偶发性时，表明该故障只是暂时出现或者会随着系统的维修而消失。

模型扩展[10]即为将包含有故障事件的系统正常模型（在模型扩展前，系统模型虽包含有故障事件，但此时故障事件并没有被明确定义，仅为一个声明，因此现阶段的模型仍为系统正常模型）与已定义的故障模式结合，形成故障扩展模型，以实现系统安全性评估与分析。

4 飞行引导系统的实例建模与安全性分析

4.1 GFC700实例系统概述

本研究选用了一个某机型上的综合航电系统（Garmin G1000[11]）中的GFC700自动飞行控制系统来进行实例系统分析验证。自动飞行控制系统包括飞行引导系统（flight guidance system，FGS）、飞行管理系统（flight management system，FMS）、飞行指引（flight director，FD）、自动驾驶（autopilot，AP）等子系统。其中飞行引导系统主要由模式逻辑以及飞行控制律两大模块构成。模式逻辑是一组离散算法，其作用是在系统处于激活状态的任意时刻，选择合适的飞行控制律。本文主要研究飞行引导系统的模式逻辑。飞行引导系统的飞行模式[12]通常可分为两大模块：横向模式和垂直模式。横向模式通过调整飞机的侧滚角度来控制飞机水平方向的运动。垂直模式通过调节飞机的俯仰角度来控制飞机竖直方向的运动。典型的飞行模式见表2。

Table 2 Flight modes表2 飞行模式

由于每一个飞行模式都有三种基本状态，即选择激活状态、取消选择状态和默认状态，因此针对模式的状态设计了两种模式故障：模式输出卡死故障和模式输出紊乱故障。

模式输出卡死故障即为不论该飞行模式被取消或是选择，其永远保持一种状态，例如若某一飞行模式卡死在选择激活状态，则无论对其进行取消或选择操作，该飞行模式永远保持选择激活状态，如图3所示；模式输出紊乱故障即为该飞行模式最终呈现的状态与其被指定的状态不符，例如若某一飞行模式输出紊乱，则对其进行选择操作，该飞行模式可能处于取消选择状态而非选择激活状态，如图4所示。针对某一飞行模式自身出现的故障，不仅对该飞行模式有影响，也会对与该飞行模式相关联的其他飞行模式造成巨大影响。

Fig.3 HDG stuck at selected_state图3 HDG模式卡死在选择激活状态

Fig.4 Disordered output of HDG图4 HDG模式输出紊乱

4.2 基于模型的系统安全性评估平台xSAP

xSAP[13]是基于模型的系统安全性分析平台，主要功能包括对系统需求及功能的验证、模型扩展、系统安全性分析等。该平台的特点包括：提供可自定义故障模板的故障库；自动化实现模型扩展；实施全面的安全分析，包括故障树分析（fault tree analysis，FTA），失效模式与影响分析（FMEA），使用定时故障传播图（timed failure propagation graphs，TFPG）的故障传播分析和共因分析（common cause analysis，CCA）等。

xSAP平台主要由两个工具来支持：nuXmv以及xSAP。nuXmv[14]是NuSMV模型检验器的扩展版本，主要用于需求分析及需求模型的功能性验证。NuSMV[15]符号模型检测器从卡内基梅隆大学版本的SMV(symbolic model verifier)模型检测器演变而来，是基于二元决策图（binary decision diagrams，BDDS）重新实现的SMV的扩展。基本执行思路是将模型状态空间用符号化的形式和二元决策图来存储和处理。本研究采用的工具版本为NuSMV 2，扩展了NuSMV版本，新增特性包括：结合基于BDD符号化技术和基于SAT（satisfiability）模型检测组件的新模型检测算法及验证技术等[16]。xSAP主要用于模型扩展和安全性评估。xSAP构建在nuXmv上，在SAP中正常模型及故障扩展模型均用nuXmv的形式化语言（NuSMV建模语言）表达，且待验证安全性属性也用NuSMV中的时序语言进行构造，如全局不变式、线性时序逻辑（linear temporary logic，LTL）或计算树逻辑（computation tree logic，CTL）公式等[17]。

基于xSAP平台的系统安全性分析包括对系统进行需求性建模（NuSMV模型），以及根据系统设计故障模式。通过对NuSMV需求模型进行模型扩展得到故障扩展模型，以实现安全属性验证及故障分析。安全性评估与分析主要包含两方面：第一，使用NuSMV模型验证工具，以正常NuSMV模型为基础检验系统需求及安全性属性。其验证结果分为两种：模型符合安全属性，则该条安全属性通过验证，返回True；否则返回False，并给出反例路径。第二，使用xSAP故障分析工具，以模型扩展后的NuSMV模型为基础进行故障分析，自动化生成相应的故障树及FMEA表。图5即为以xSAP为核心的基于MBSA的系统验证与安全性分析框架。

Fig.5 Model-based system safety assessment based on xSAP图5 以xSAP为核心基于模型的系统安全评估

4.3 飞行引导系统建模及模型扩展

4.3.1 NuSMV建模

本研究主要对飞行引导系统的第一层模型进行建模及故障注入。图6为飞行引导系统初级模型概观，包括四种常见飞行模式（侧滚模式ROLL、航向选择模式HDG、俯仰保持模式PITCH和垂直速度模式VS），以及与上述飞行模式相关的飞行仪表和边缘组件（自动驾驶仪AP和飞行指引仪FD）。

Fig.6 Overview of FGS first level model图6 飞行引导系统初级层次模型概观

使用RSML-e（requirements state machine language without events）语言对飞行模式以及边缘组件进行需求性建模[12]。由于RSML-e模型仅能清晰、详细、直观地描述系统需求，并不能被模型检测工具进行模型验证，因此将其转换成能够实现安全性属性验证的NuSMV模型，此模型即为未包含故障扩展的NuSMV模型。对于模型转换而言，模型间的相似度越高，转换越容易建立[18]。RSML-e模型与NuSMV 2模型相似度较高，具有语义一致性，能够建立相互间的转换规则并确保转换规则的正确性。RSML-e模型到NuSMV 2模型的语法转换包括[19]：类型和变量的转换、转换时的时态对应关系、状态迁移条件转换、扁平化处理以及宏的转换等。

为了验证该模型的正确性与完整性，以及飞行引导系统需求的安全性与可靠性，设计29条属性进行模型验证，内容包括图6中所有飞行模式及边缘组件的功能性和安全性的验证。属性验证可分为两部分：第一，对每个组件和模式自身的功能性及安全性进行验证，例如每个飞行模式是否能够正常被选择或者取消；第二，对模式间的交互进行安全性验证。经验证，该29条属性均正确，整个验证耗时0.53 s。验证结果的部分截图如图7所示。

Fig.7 Verification results of FGS first level model(part)图7 飞行引导系统初级模型验证结果部分截图

4.3.2 故障注入与不变式的定义

4.3.2.1 故障注入

飞行引导系统初级模型的故障分析重点是对每个模式自身的故障进行分析，因此仅在NuSMV模型中表示模式状态变化的状态变量中添加故障事件。选择航向选择模式（HDG）和垂直速度模式（VS）作为故障扩展单元，对在HDG和VS上可能发生的故障行为进行扩展。在飞行引导系统初级NuSMV模型的建模过程中，设定HDG和VS状态变量的可能取值为Un_Defined、Cleared和Selected。以HDG飞行模式为例具体模型代码如图8所示。

Fig.8 NuSMV code of state variable of HDG图8 航向选择模式HDG状态变量的NuSMV代码

根据4.1节定义的两种模式故障对HDG和VS模式进行故障注入。

（1）模式输出卡死故障。结合NuSMV建模，该故障可能导致模式状态变量的取值卡死在Un_Defined或Cleared或Selected，因此该类型故障将有三个故障事件：

--模式的输出保持Selected，即模式一直处于选择激活状态

fault_event_stuck_at_Selected:boolean;

--模式的输出保持Cleared，即模式一直处于取消选择状态

fault_event_stuck_at_Cleared:boolean;

--模式的输出保持Un_Defined，即模式一直处于默认的未被选中状态

fault_event_stuck_at_Un_Defined:boolean;

（2）模式输出紊乱故障。结合NuSMV建模，当发生模式输出紊乱时，模式的输出值可能为Un_Defined、Cleared及Selected中的任意一个。对该故障模式定义一个故障事件Disorderoutput，即：

--模式的输出值与正确的输出值不对应

fault_event_disorderoutput：boolean;

当上述两类故障事件发生时，飞行模式不能通过自行修复使得其从失效状态变回正常状态，因此模式的失效是不可逆的。如下代码即表示失效状态的不可逆：

将上述代码分别添加到HDG和VS模式中即完成故障注入。

4.3.2.2 不变式

在模型的故障分析中，故障树及FMEA表均需要顶层失效事件才能得以生成，因此需要在NuSMV模型的验证属性中以“INVARSPEC”为关键字添加不变式，该不变式的“非”即为相应的顶层失效事件。添加的不变式如下：

INVARSPEC((m_HDG.HDG=Un_Defined)&!(next(m_Select_HDG.result))->next(m_HDG.HDG=Cleared))&(((m_VS.VS=Selected)&next(m_Deselect_VS.result))->next(m_VS.VS=Cleared));

上述不变式由两条子不变式以“&”关键字连接而成，可以验证两条属性的组合故障分析。其中前一条不变式与HDG模式中的状态变量HDG相关，后一条不变式与VS模式中的状态变量VS相关。该不变式的含义为：在全局状态下，如果HDG模式处于默认无操作状态且其未被选择，则HDG模式将处于未被选择状态；同时，如果VS模式处于被选择状态且被取消选择，则VS模式将处于选择取消状态。经验证，该不变式属性验证为真。

4.3.3 FEI故障模式

本小节将利用xSAP工具中的故障模板，对4.3.2小节中的两种故障类型进行详细定义，编写FEI文件形式的故障模式。

（1）模式输出卡死故障。此类卡死故障的故障模板可以在xSAP的故障库中找到，即“stuckatbyvalue”模板，因此可以根据该模板定义，直接编写故障扩展指令文件（FEI）。以HDG模式为例，模式卡死故障包含3个故障事件，其对应的3个故障模式分别为：

stuckAt_Selected：模式的输出卡死在Selected状态。

stuckAt_Cleared：模式的输出卡死在Cleared状态。

stuckAt_Un_Defined：模式的输出卡死在Un_Defined状态。

（2）模式输出紊乱故障。xSAP故障库并没有包含该类故障，因此需要自行定义故障模式模板，根据自定义模板编写故障扩展指令文件（FEI）。

①自定义模板：在xSAP工具中自定义故障效果模式disorderoutput，定义该故障效果模式的during事件和entering事件的smv文件，如图9、图10所示。

图9 entering.smv

图10 during.smv

图9 中entering.smv文件定义了作用对象从正常状态到失效状态的效果模式，其中next(varout)!=input表示，当发生输出紊乱故障时，得到的输出结果与期望的输出值不一致。

图10中during.smv文件定义了作用对象一直处于失效状态的效果模式，其中next(varout)=varout表示在发生输出紊乱故障的过程中，模式输出值一直处于紊乱状态。

输出紊乱故障模式的状态转换图如图11所示。

Fig.11 State transition of output disordered fault mode图11 输出紊乱故障模式的状态转换图

②故障扩展指令文件：根据自定义模板编写FEI文件，以HDG模式为例，模式输出紊乱故障包含一个故障事件，其对应的故障模式为Disorderoutput_HDG。详细定义见图12。

Fig.12 FEI of HDG mode as unit of influence图12 以HDG模式为影响单元的FEI文件

同样，VS模式也包含上述两种故障类型4种故障模式，即输出卡死在Selected、Cleared以及Un_Defined和输出紊乱故障。

综上，飞行引导系统第一层模型的安全性分析将选用HDG模式和VS模式作为故障影响单元，并定义8个故障模式用以模型扩展及故障分析。

4.4 使用xSAP运行工具对飞行引导系统进行故障分析

4.4.1 模型扩展

使用xSAP将正常NuSMV模型与FEI故障模式进行扩展，如图13所示，生成两个文件。其中extended_fgs_firstlevel.smv文件是模型扩展后得到的NuSMV故障扩展模型；fms_fgs_firstlevel.xml文件是FEI故障模式的配置文件，该文件详细阐述了FEI故障模式文件fgs_firstlevel.fei中每一行代码的含义以及每一个故障模式的作用。

4.4.2 验证系统性质

对正常NuSMV模型进行模型扩展后得到的扩展模型，其模型中的飞行模式状态包含了故障状态，因此受故障影响的飞行模式的验证属性在进行模型检验时会发生错误，模型检验器将给出反例路径。以4.3.2.2小节中的不变式为例，其在正常的NuSMV模型中属性验证为真，而在故障扩展模型中，HDG及VS的状态变量有可能会出现输出卡死和输出紊乱的故障情况，因此原本验证为真的属性在故障扩展模型中验证为假。具体结果（部分）如图14所示。

在正常模型中进行模型检验时若出现反例路径，或表明该反例路径对应的属性错误，或表明建模错误，需要进一步修改属性或者模型。而在故障扩展模型中进行模型检验若出现反例路径，则表明已成功进行模型扩展。

4.4.3 生成故障树

故障树分析是自顶而下的演绎分析，由顶层失效事件（top level event，TLE）逐步建立一个或多个由基本故障事件组成的导致顶事件发生的所有可能的故障链，此故障链以树形结构的形式组成一个故障树（fault tree）。本次故障树生成所使用的顶事件为4.3.2.2小节中不变式的“非”，即：

!(((m_HDG.HDG=Un_Defined)&!(next(m_Select_HDG.result))->next(m_HDG.HDG=Cleared))&(((m_VS.VS=Selected)&next(m_Deselect_VS.result))->next(m_VS.VS=Cleared)));

Fig.13 Result of model extension图13 模型扩展结果

Fig.14 Counterexample(Part)图14 反例路径（部分）

Fig.15 Result of generating fault tree图15 生成故障树的运行结果

该顶层故障事件表示如果HDG模式处于默认无操作状态且其未被选择，则HDG模式将不会处于未被选择状态；或者，如果VS模式处于被选择状态且被取消选择，则VS模式将不会处于选择取消状态。

在xSAP工具上使用故障树生成指令“compute_ft”生成该故障扩展模型的故障树。运行结果如图15所示。

执行上述命令可以得到两个文件，分别为：

（1）extended_fgs_firstlevelevents.txt。该文件包含了能够导致顶层故障事件发生的基本故障事件，文件截图如图16所示。

图16 extended_fgs_firstlevelevents.txt

由图16可知，对于4.3.3小节定义的8个故障模式，其中只有6个故障模式能够导致顶事件的发生，分别为HDG模式输出紊乱、HDG模式输出卡死在Selected、HDG模式输出卡死在Un_Defined状态、VS模式输出紊乱、VS模式输出卡死在Selected以及VS模式输出卡死在Un_Defined状态。

（2）extended_fgs_firstlevelgates.txt。gates文件表示故障事件通过逻辑门到达顶事件（逻辑门指“与门”“或门”“非门”），即 extended_fgs_firstlevelevents.txt中的6个故障事件通过“或门”，导致了顶事件的发生。

生成故障树文件后，通过xSAP工具中的view_ft命令查看图形化的故障树，如图17所示。从该图中可以直观地看出顶事件的发生由哪些失效事件导致。此故障树表示，当HDG模式输出紊乱，或HDG模式输出卡死在Selected，或HDG模式输出卡死在Un_Defined状态，或VS模式输出紊乱，或VS模式输出卡死在Selected，或VS模式输出卡死在Un_Defined状态时，会发生顶层故障事件。

4.4.4 生成FMEA表

FMEA采用正向推理来评估系统可能的失效影响。本次生成FMEA表依据的不变式（顶事件的“非”）为：

Fig.17 Fault tree of NuSMV fault extended model图17 NuSMV故障扩展模型生成故障树

INVARSPEC((m_When_VS_Button_Pressed_Seen.result)->(m_Deselect_PITCH.result));

此不变式表示的含义为：当选择垂直速度模式时会导致默认垂直模式即俯仰保持模式被取消。

基于上述不变式的顶事件为：

!((m_When_VS_Button_Pressed_Seen.result)->(m_Deselect_PITCH.result))

生成的一阶FMEA表如图18所示。

图18表明当VS模式发生模式输出卡死在Selected故障或输出紊乱故障时会导致顶事件的发生。由此可知若VS模式出现故障不仅对其自身有影响，也会对与其相关联的其他飞行模式，如PITCH模式造成巨大影响。

5 小结

为了提高软件系统的安全性，基于模型的安全性分析和验证已经成为软件开发周期的重要组成部分。文献[11]详细介绍了Garmin G1000航空电子系统，并选取了文献第7章中描述的自动飞行控制系统（automatic flight control system，AFCS）进行分析。文献[12]利用RSML-e对飞行引导系统需求进行形式化建模。文献[19]提出了一种将RSML-e模型转换为NuSMV模型的方法，文献[13]详细介绍了xSAP工具，在对该工具熟练使用的基础上，本研究使用该工具对飞行引导系统进行模型扩展和故障分析。

与已有工作相比，本次工作首先针对NuSMV2提出了一种将基于飞行引导系统需求建立的RSML-e模型转换为可进行属性验证的NuSMV2模型的方法。其次，从Garmin G1000手册中推导出与飞行模式相关的安全属性，并对其进行验证。最后，根据飞行引导系统的实际工作情况，设计了两种飞行模式的失效行为，即模式输出卡死和模式输出紊乱，并利用xSAP将两种失效行为扩展到正常功能的NuSMV模型，生成故障扩展NuSMV模型，用于故障树分析和FMEA分析。

Fig.18 First order of FMEAtable图18 一阶FMEA表

综上，通过实际的航空电子系统，进行了系统需求建模、模型转换、模型验证、系统安全分析和故障分析。从结果来看，基于MBSA的安全评估方法对于实际系统的验证是有效的。