基于模型检查的民用飞机飞控系统安全性评估

Safety assessment of civil aircraft flight control system based on model-checking

在以大型民机为代表的安全关键系统研制中,系统复杂度的提升极大地降低了依赖设计人员经验的传统安全性评估手段的效率与有效性,并带来了反复迭代困难等问题,基于模型的安全性评估方法(MBSA)能够显著降低研制过程的分析复杂度,提高安全性评估的工作效率。民机系统安全性评估指南ARP 4761A中也增加了MBSA相关的安全性评估工作。阐述了利用有限状态机与时态逻辑构建形式化安全性模型,开展安全性评估的基本原理,详细的分析过程及定义安全属性的方法,并以某民用飞机为对象,建立飞控系统副翼控制功能的SMV形式化模型,定义了副翼控制功能的形式化安全性需求,给出了基于形式模型的安全性属性验证评估案例,证明了基于形式化方法的安全性评估在民机系统安全性工作中的可行性。

In the development of safety critical systems such as large civil aircraft,the increase of system complexity has greatly reduced the efficiency and effectiveness of traditional safety assessment methods by the experience of designers,and brought problems such as iterative difficulty.A novel safety assessment method called Model-Based Safety Assessment(MBSA)can significantly reduce development analysis complexity and improve the efficiency of safety assessment work.On the other hand,MBSA related safety assessment work has also been added in ARP 4761A.Based on the above background,this paper explains the basic principle of formalized security model,the basic principle of safety evaluation,detailed analysis process and the method of safety requirements definition by using finite state machine and temporal logic.A civil aircraft was taken as an example,the SMV formal model was established and the formal safety requirements of aileron control function were defined.This paper presents a case of the safety verification,and proves the feasibility of formal method based safety assessment in the security work of civil aircraft system.