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

Fault Tree Generation Based on Fault Configuration

作　　者：黄鸣宇[1] 魏欧[1] 胡军[1] HUANG Ming-yu WEI Ou HU Jun(Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211100, China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211100

出　　处：《计算机科学》2017年第2期182-191,共10页Computer Science

基　　金：国家自然科学基金项目(61170043);国家重点基础研究发展计划(973)项目(2014CB744904);航空科学基金项目(20155552047);江苏省研究生培养创新工程(SJLX15_0139);南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20161602);中央高校基本科研业务费专项资金资助

摘　　要：故障树分析是提高系统安全性和可靠性的有效方法。传统的人工故障树生成方式难以解决当前系统的庞大规模与复杂性的问题,且容易出错。为此,提出基于故障配置的故障树生成方法,引入软件产品线的可变性管理,用于系统故障建模与形式化分析。首先,定义故障特征图模型用于刻画系统故障间的约束关系,基于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.

关 键 词：故障树 故障配置 模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]