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

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

随着飞机系统复杂度的日益增长,对飞机设计人员和安全性分析人员能力的提升也提出了相应要求。但是传统的安全性分析方法都存在一些弊端:高度主观并且依赖分析人员的技能和经验,而且不太可能做到完整无错。形式化验证技术,如模型检验方法,能够很好地处理复杂度较高的系统,并且能在一定程度上克服这些弊端。本文运用模型检验的方法对系统进行演绎式安全性分析,得到定性的结果。

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.