计算机技术与发展2017，Vol.27Issue(12)：89-92,97,5.DOI:10.3969/j.issn.1673-629X.2017.12.020
基于时序描述逻辑的故障树分析方法研究
Research on Fault Tree Analysis Based on Temporal Description Logic
摘要
Abstract
Fault Tree Analysis ( FTA) is one of safety analysis methods which is commonly used in industry. However,as the limitation of its non-formal method,it is difficult to be formal verification of software fault and even to describe the temporal logic relation between events in embedded real-time system. Therefore,in order to solve the problem,a formal fault tree analysis based on Temporal Description Logic ( TDL) is proposed. Firstly,the fault tree is extended and constrained in temporal sequence characteristic by TDL. Secondly,safety attributes of software are extracted in the representation of TDL. At last,the safety attributes modeling is carried out in software system which is verified whether to meet these attributes or not by SPIN,a model checking tool. A case of environment input module of airborne control system is given where the analysis and modeling of fault tree is conducted,and its security attributes to be checked and experimen-tal results are achieved. It is showed that the proposed method is effective and feasible.关键词
故障树分析/时序描述逻辑/安全属性/形式化验证Key words
fault tree analysis/temporal description logic/safety attributes/formal verification分类
信息技术与安全科学引用本文复制引用
司佳,朱羿全,马琳..基于时序描述逻辑的故障树分析方法研究[J].计算机技术与发展,2017,27(12):89-92,97,5.基金项目
国家自然科学基金资助项目(61272083,61100034,61170043) （61272083,61100034,61170043）
中央高校基本科研业务费专项资金(NS2014099) （NS2014099）
江苏省自然科学基金青年基金项目(BK20130812) （BK20130812）
