形式化方法在飞机轮刹系统安全性分析中的应用

在民机设计领域,大多数传统的系统安全性分析具有高度的主观性并依赖于工程师们的实践经验,其分析结果无法做到完整、一致、无误。而近年来兴起的形式化方法却能弥补这些不足。形式化方法就是用具有形式语义的记号和工具明确地表述出所设计系统的安全性需求,即给出系统的规范,并根据系统规范利用上述记号和工具对给定系统所具有的性质和最终实现的正确性进行严格的证明。本文将以ARP4761中所述的轮刹系统为例,简单介绍形式化方法是如何应用于验证民机设计方案的。虽然做不到面面俱到,但可以让人们对该方法的执行过程有一定的了解。

The application of formal methods in safety analysis of airplane wheel brake system

In the area of the design of civil aircrafts,most of the traditional system safety analysis techniques are highly subjective,dependent on the experience of the practitioner,and it is unlikely that the results will be complete,consistent,and error free.However,formal methods which emerge in recent years could be used to make up for all these lacks.By the formal notation and the relevant tools,formal methods can definitely describe safety requirements of the aim system,which is named as the specification of s...