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

摘要

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