基于模型检验的飞机系统安全性分析方法研究

吴海桥，刘 超，葛红娟，王华伟

（南京航空航天大学民航学院，南京 210016）

机载系统是现代飞机的重要组成部分，重要的适航标准均在第1309条对机载系统的安全性提出了明确要求，并指出必须通过分析来表明对该条款的符合性[1-4]。

研究发现，故障树分析（fault tree analysis，FTA）等传统安全性分析方法，主要依靠分析人员的技能和经验，受人类认知能力的限制，难以预测系统所有可能的行为（包括正常和异常行为），容易疏漏某些系统失效状态或者误判系统失效的影响，不适用于当前高度复杂与综合的机载系统，经过评估的个别系统仍发生了未曾预料的失效[5]。为此，2001年开始将计算机学科形式化验证中的模型检验（model checking）引入复杂机载系统的安全性评估领域[6]。

基于模型检验的飞机系统安全性分析方法，利用遍历算法，既可以从数学上保证搜索出系统的所有状态，不会发生疏漏；又可以利用计算机工具运行算法，自动实现FTA分析目的，减少对分析人员技能和经验的依赖。

目前，基于模型检验的方法已成为复杂机载系统安全性分析的发展趋势之一。欧盟在过去10余年间先后完成了ESACS（enhanced safety assessment for complex systems）[6]和 ISAAC（improvement of safety activities on aeronautical complex systems）[7]两个项目，目前正在进行MISSA（more integrated systems safety assessment）[8-9]项目，美国航空航天局（NASA）也开展了类似研究[10]，国内尚无该领域的研究报道。

本文利用模型检验方法自动实现FTA的分析目的，即识别导致顶事件发生的最小失效组合（即最小割集），提出一种基于模型检验的飞机系统安全性分析方法。

1 基于模型检验的飞机系统安全性分析方法

1.1 模型检验方法简介

模型检验方法最早由 Clarke、Emerson以及Quielle、Sifakis于1981年分别提出，可从数学上完备地证明或验证所实现的系统是否与规范（Specification）一致。模型检验首先将系统模型转化为一个有限状态机，如Kripke结构。再将描述系统特性的系统规范表示为一组时态逻辑公式，如计算树逻辑（CTL）。最后使用检验工具验证状态转移关系是否满足逻辑公式，如果不满足，验证工具将会给出一个反例，其示意图如图1所示[11]。

图1 模型检验方法示意图Fig.1 Sketch of model checking

最初发展起来的模型检验工具以显式表示系统状态及其转移结构，容易出现状态爆炸的问题。而符号模型检验（symbolic model checking，SMC）方法的引入，大大地缓解了状态空间爆炸问题，基于该方法开发的模型检验工具已用于状态数目超过10120的硬件电路的验证[12]。

1.2 基于模型检验的安全性分析方法

本文提出的基于模型检验的飞机系统安全性分析方法，旨在识别导致顶事件发生的最小失效组合（即最小割集），实现FTA的分析目的。该方法的流程如图2所示。

1.2.1 准备工作

建模准备工作的主要目的是获取模型检验所需的飞机系统相关信息。对飞机系统安全性分析前，需要做的准备工作包括：确定用户要求，获取现行的适航认证文件，明确系统功能，了解用户对安全分析的期望和要求等。通过对获取的系统资料分析，确定系统需求规范（system requirement specification），系统需求规范通常包括系统及其分系统的定义、构成、性能参数等内容。

图2 基于模型检验的安全性分析方法的流程Fig.2 Safety analysis process based on model checking

系统模型化是在熟悉系统需求规范的基础上，对飞机系统的功能、层次、结构以及系统输入输出内容的抽象过程。系统需求规范虽然包括建模所需要的所有信息，但是模型建立时要考虑模型层次和模型复杂度的问题，尤其对于复杂的飞机系统，单层模型往往不能够描述整个系统功能。因此多层子系统之间接口和架构、同层系统内部模块接口和功能、模块的复杂度等问题都是系统模型化要解决的问题。系统模型化的结果是以伪代码描述的飞机系统初始模型。

通过系统需求定义可获得飞机系统的外部功能描述，即系统规范。失效模式定义确定系统或其部件发生功能丧失或者故障的方式。系统安全性需求确定系统部件功能失效或故障对系统状态的影响。

1.2.2 系统建模

系统建模主要包括形式化建模和系统模型扩展：1）形式化建模

形式化建模是将飞机系统初始模型和系统规范转化为模型检验工具验证代码的过程。因为飞机系统正常模型的功能要符合系统规范，同时模型的描述语言要遵循模型检验工具的语言规范，所以模型建立后，首先要验证其是否满足系统规范。这一点可以通过模型检验工具实现。如果模型通过验证，则飞机系统正常模型建立完成；如果系统模型没有通过验证，可能是飞机系统设计存在缺陷或者模型建立存在错误。如果是系统设计存在缺陷，则要修改系统设计，再对系统重新进行建模验证；如果是系统模型存在问题或者系统规范的时序逻辑描述错误，则要修改系统模型或者时序逻辑描述。

2）系统模型扩展

系统模型扩展是向飞机系统正常模型中的部件状态添加失效模式的过程，在基于模型检验的飞机系统安全性分析过程中，除了考虑元件（系统）正常的工作模式（状态）外还要考虑其失效模式（状态）。这是模型检验方法在应用于飞机系统时的特别之处。

1.2.3 安全评估

利用模型检验工具实现的算法，可以对飞机系统状态进行搜索。假设飞机系统功能在系统需求定义被描述为系统规范表达式p，那么时序逻辑表达式“AG p”为真，表示飞机系统在任何条件下都具有这个功能；逻辑表达式“EF p”为真，表示飞机系统中具有这个功能但仅在特定的条件下有效。通过对得到飞机系统失效模型状态分析，也能够得到相应安全性分析结果，如本文下面举例的与最小割集等价的最小失效组合。

2 实例应用

SAE ARP4761附录中机轮刹车系统（wheel brake system）因为本身的规模大小和复杂程度适于分析演示，并且在民用安全分析领域的认知度高，所以本文以其为例，使用模型检验的方法，对其安全性进行了分析。

2.1 刹车系统建模

机轮刹车系统是飞机起落架系统的子系统，在飞机滑行、着陆和中断起飞的情况下，起到对飞机机轮安全减速的作用[13]。

以机轮刹车系统的顶层系统为分析对象，为了简便说明，不考虑原有系统中的防滑功能。系统输入为人工刹车时的脚蹬位置或自动刹车时用户面板设定的刹车速率，系统输出为机轮接收到的液压压力。建立刹车系统模型，且对模块进行编号以简化后续输出，如图3所示。

选用NuSMV作为模型检验工具。NuSMV源于CMU开发的基于BDD的模型检验器CMU SMV，它是一个高水平的符号模型检验器。NuSMV允许同步和异步有限状态的表示，它使用基于BDD和基于SAT的检验技术进行模型检验，并且支持对强公正约束的检验支持[14]。

利用NuSMV语言写出描述机轮刹车顶层系统功能的代码。以液压源为例，液压源在飞机液压系统中的动力来源于飞机发动机或电动泵。然而在机轮刹车系统中，将液压源简化为一个无输入，输出为液压能力的元件，其NuSMV代码如图4所示。state为液压状态，一般包括正常工作模式和失效模式，因为后面分析中插入的是基本失效状态，所以在此选择布尔型。pressure为输出压力状态，在定性的分析中简化为布尔型已经可以满足分析需要，在定量的分析中，则详细数值来支持模型建立。

系统功能规范描述为机轮能接收到刹车压力，用计算树逻辑语言可以描述为“AG!Wheel.pressurefail”。利用NuSMV对包含有系统模型和时序逻辑的代码文件进行检验，输出结果为“AG!Wheel.pressurefail is TRUE”，说明模型功能满足系统需求，至此系统正常模型建立完成。

在系统正常的模块中插入失效状态，建立扩展系统模型。本例中对除机轮以外的模块，插入标准失效状态。标准失效状态下的模块，状态有TRUE和FALSE两种情况，在TRUE状态下，模块可用且下一状态是TRUE或FALSE。在FALSE状态下，模块失效且下一状态始终为FALSE。

2.2 安全性分析

完成扩展系统模型的建立后，本文利用NuSMV自动验证了模块和模块组合的失效对系统功能的影响。使用 CTL 公式“EG（p→ q）”，其中 q为”Wheel.pressurefail”，p为模块和模块组合失效状态，总共有1 024（210）种情况，通过枚举验证一共有13种最小失效组合（即最小割集），如表1所示，其中事件定义如表2所示。

表1 最小失效组合Tab.1 Minimum failure combination

表2 事件定义Tab.2 Event definition

为检验本文方法的正确性，对上述系统使用FTA建立故障树，如图5所示。将表1中的最小失效组合与通过传统FTA得到最小割集进行了对比，两者完全相同，表明本文方法可以自动实现FTA的分析目的。

3 结语

基于模型检验的飞机系统安全性分析方法，利用模型检验方法，列出模型系统的状态，并用特定算法按照逻辑表达式描述对系统状态进行搜索检验，自动得出与FTA最小割集等价的最小失效组合。本文方法既可从数学上保证搜索系统所有的状态，不会发生疏漏；又可利用模型检验工具软件，自动实现FTA分析目的，减少对分析人员技能和经验的依赖。随着模型检验方法的不断发展，其能够处理的状态数量可基本满足复杂机载系统安全性分析的需要，基于模型检验的方法业已成为复杂机载系统安全性分析技术的发展趋势之一。

[1]CCAR-25-R3，运输类飞机适航标准[S].中国民用航空总局，2005.

[2]CCAR-23-R3，正常类、实用类、特技类和通勤类飞机适航规定[S].中国民用航空总局，2005.

[3]CCAR-29-R1，运输类旋翼航空器适航规定[S].中国民用航空总局，2002.

[4]CCAR-27-R1，正常类旋翼航空器适航规定[S].中国民用航空总局，2002.

[5]JOHN RUSHBY.Formalism in Safety Cases[C]//Making Systems Safer.London：Springer-Verlag London Limited，2010：3-17.

[6]ÅKERLUND O，BIEBER P，BÖDE E，et al.ESACS：an Integrated Methodology for Design and Safety Analysis of Complex Systems[C]//European Safety and Reliability Conference（ESREL）.Toulouse：Balkema publisher，2003：203-221.

[7]ÅKERLUND O，BIEBER P，BÖDE E，et al.ISAAC，a Framework for Integrated Safety Analysis of Functional，Geometrical and Human As pects[C]//ElectronicReciprocalTransferSystem，Toulouse.France：2006：145-162.

[8]VALÉRIE SARTOR，JEAN GAUTHIER.Model Based Safety Assessment In Dassault Aviation[C]//Model-based Safety Assessment（Journées MISSA）：2010，12：11-15.

[9]LAURENT SAGASPE NICOLAS MAY.MBSA in Aeronautics Experience Feed-back on modelling applications[C]//Model Based Safety AssessmentWorkshop（MBSAW2011），Toulouse.France：2011：53-59.

[10]ANJALI JOSHI，MICHAEL W WHALEN，MATS P E HEIMDAHL.Model-Based Safety Analysis Final Report[R].NASA/CR-2006-213953，NASA Contractor Report，2006.

[11]燕 飞.轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D].北京：北京交通大学，2006.

[12]袁志斌.基于模拟理论的模型检测研究[D].武汉：华中科技大学，2007.

[13]SAE.Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment[R].SAE ARP4761，1996.

[14]ROBERTO CAVADA，ALESSANDRO CIMATTI，CHARLES ARTHUR JOCHIM，et al.NuSMV 2.5 User Manual[EB/OL].[2011-12-01]http：//nusmv.fbk.eu/.