基于故障配置的故障树生成

摘要

故障树分析是提高系统安全性和可靠性的有效方法.传统的人工故障树生成方式难以解决当前系统的庞大规模与复杂性的问题,且容易出错.为此,提出基于故障配置的故障树生成方法,引入软件产品线的可变性管理,用于系统故障建模与形式化分析.首先,定义故障特征图模型用于刻画系统故障间的约束关系,基于Kripke结构定义故障标记迁移系统来描述系统的行为;然后,基于模型的语义建立通过模型检测生成故障树的过程;最后,通过时序逻辑描述系统安全属性,利用模型检测工具SNIP验证安全属性进而生成故障树.案例研究验证了该方法的有效性.%Fault tree analysis is an effective method to improve system safety and reliability.However,traditional manual fault tree generation is difficult to solve the problem of large scale and complexity of system and error-prone.In order to systematically support system faults modeling and formal analysis,a fault tree generation method based on fault configuration was proposed in this paper by introducing variability management form software product line into system faults modeling.Firstly,we defined fault feature diagram for describing the constraints among faults and proposed fault labeled transition system based on Kripke structure to describe system behavior.Secondly,a model checking procedure of generating fault tree was established based on the model semantics.Finally,using model checker SNIP,the safety properties specified with temporal logic were verified and fault tree was generated based on the result.Case study shows the effectiveness of the proposed approach.