一个基于形式化方法的系统安全性建模分析实例研究

摘要 随着安全关键性系统的日益复杂，如何提高安全关键系统的安全性成为急需解决的问题.基于形式化模型的复杂系统设计与分析是一种重要的安全性分析方法.本文工作对AIR6110标准中的机轮刹车实例系统进行了基于形式化方法的安全性分析研究，包括：在系统模型设计层级对机轮刹车系统（WBS）的架构进行层次化分析，将自然语言描述的WBS系统功能用形式化语言（AADL的子集SLIM）进行严格的建模描述，消除AIR6110标准中自然语言描述存在的需求语义的二义性，从而建立了WBS系统的形式化模型；考虑系统可能发生的故障并设计多种类的故障模式，基于这些故障模式对建立的形式化功能模型进行失效行为语义的扩展，然后对获得的扩展系统模型进行安全性分析.实例分析论证了基于模型的安全性分析方法在工业系统中的有效性和实用性