形式化模型检验在飞机系统演绎式安全分析中的应用研究  

The Applied Research of Formal Model Checking in Aircraft System Deductive Safety Analysis

作　　者：马径梁 吴海桥[1] 王华伟[1] 葛红娟[1] 

机构地区：[1]南京航空航天大学民航学院

出　　处：《飞机设计》2014年第1期47-51,共5页Aircraft Design

基　　金：国家自然科学基金与民航局联合资助项目(60879001);江苏省自然科学基金资助项目(BK2009378);南京航空航天大学基本科研业务费专项科研项目(NS2010179)

摘　　要：随着飞机系统复杂度的日益增长,对飞机设计人员和安全性分析人员能力的提升也提出了相应要求。但是传统的安全性分析方法都存在一些弊端:高度主观并且依赖分析人员的技能和经验,而且不太可能做到完整无错。形式化验证技术,如模型检验方法,能够很好地处理复杂度较高的系统,并且能在一定程度上克服这些弊端。本文运用模型检验的方法对系统进行演绎式安全性分析,得到定性的结果。With the growing complexity of the aircraft systems, it requires an adequate increase in the capability of aircraft designers and safety engineers. However, there＇re some drawbacks of traditional safety analysis techniques： highly subjective and dependent on the skill of the analysts, hardly error- free and complete. Formal verification techniques, such as model checking methods, have the ability of dealing with systems of such highly complexity and overcoming these drawbacks to a certain extent. This paper uses the model checking method, conducts the deductive analysis of certain system and obtains the qualitative results.

关 键 词：飞机系统 演绎式安全分析 形式化模型检验 

分 类 号：V945.1[航空宇航科学技术]