基于模型检验的飞机系统安全性分析方法研究吴海桥，刘超，葛红娟，王华伟（南京航空航天大学民航学院，南京210016）摘要：传统的安全性分析方法，受到分析人员自身技能和经验等因素的影响，容易疏漏系统的失效状态或误判失效的影响。模型检验利用遍历算法，既可以从数学上保证搜索出系统的所有状态，不会发生疏漏；又可以利用计算机检验工具，实现自动分析过程，减少对分析人员技能和经验的依赖。将模型检验引入飞机系统安全性领域，提出了一种基于模型检验的安全性分析方法，以SAEARP4761标准附录中的机轮刹车系统为例，利用模型检验工具NuSMV对其安全性进行了分析，自动识别出导致某系统顶事件发生的最小失效组合，完成了传统故障树分析的目的。关键词：飞机系统；安全性分析方法；模型检验；NuSMV：V37；N945.1文献标志码：A：1674－5590（2012）02－0017－04ResearchforaircraftsystemsafetyanalysismethodbasedonmodelcheckingWUHai-qiao，LIUChao，GEHong-juan，WANGHua-wei（CollegeofCivilAviation，NUAA，Nan激ng210016，China）Abstract：Traditionalsystemsafetyanalysis，influencedbythepersonalskillsandexperiencesofanalyzers，maycausetheerrorofsystemfailurestatesandfailureeffects.Modelchecking，bymeansoftraversingalgorithm，cansearchallsystemstatusinmathematicalmethodwithoutomitting.Byusingtheverificationtool，analysisprocesscanbeconductedautomaticallyandthedependenceofexperiencescanbereduced.Modelcheckingisintroducedintoaircraftsystemsafetyanalysisinthispaperanditsapplicationprocessispresentedaswell.ThewheelbrakesystemintheappendixofSAEARP4761istakenasanexample.WithverificationtoolNuSMV，theminimumfailurecombinationwhichleadtothetopeventcanbegotautomatically，thepurposeoffaulttreeanalysiscanbeachievedatthesametime.Keywords：aircraftsystem；safetyanalysis；modelchecking；NuSMV机载系统是现代飞机的重要组成部分，重要的适航标准均在第1309条对机载系统的安全性提出了明确要求，并指出必须通过分析来表明对该条款的符合性[1-4]。研究发现，故障树分析（faulttreeanalysis，FTA）等传统安全性分析方法，主要依靠分析人员的技能和经验，受人类认知能力的限制，难以预测系统所有可能的行为（包括正常和异常行为），容易疏漏某些系统失效状态或者误判系统失效的影响，不适用于当前高度复杂与综合的机载系统，经过评估的个别系统仍发生了未曾预料的失效[5]。为此，2001年开始将计算机学科形式化验证中的模型检验（modelchecking）引入复杂机载系统的安全性评估领域[6]。基于模型检验的飞机系统安全性分析方法，利用遍历算法，既可以从数学上保证搜索出系统的所有状态，不会发生疏漏；又可以利用计算机工具运行算法，自动实现FTA分析目的，减少对分析人员技能和经验的依赖。目前，基于模型检验的方法已成为复杂机载系统安全性分析的发展趋势之一。欧盟在过去10余年间先后完成了ESACS（enhancedsafetyassessmentforcomplexsystems）[6]和ISAAC（improvementofsafetyactivitiesonaeronauticalcomplexsystems）[7]两个项目，目前正在进行MISSA（moreintegratedsystemssafetyassessment）[8-9]项目，美国航空航天局（NASA）也开展了类似研究[10]，国内尚无该领域的研究报道。收稿日期：2011-12-08；修回日期：2012-02-27作者简介：吴海桥（1968—），男，江苏南京人，副教授，工学博士，研究方向为飞机系统安全性工程、可靠性系统工程.-18-中国民航大学学报2012年4月本文利用模型检验方法自动实现FTA的分析目的，即识别导致顶事件发生的最小失效组合（即最小割集），提出一种基于模型检验的飞机系统安全性分析方法。1.建模准备基于模型检验的飞机系统安全性分析方法1安全性规范1.1模型检验方法简介模型检验方法最早由Clarke、Emerson以及Quielle、Sifakis于1981年分别提出，可从数学上完备地证明或验证所实现的系统是否与规范（Specifica－tion）一致。模型检验首先将系统模型转化为一个有限状态机，如Kripke结...