基于时序描述逻辑的故障树分析方法研究

Research on Fault Tree Analysis Based on Temporal Description Logic

故障树分析法是工业界常用的安全分析方法之一。然而由于其非形式化方法的局限性,难以对软件故障进行形式化验证,更难以描述嵌入式实时系统中事件之间的时序逻辑关系。因此,提出了一种基于时序描述逻辑的故障树分析方法,以解决故障树难以对时序关系进行描述以及难以形式化验证的问题。首先,通过时序描述逻辑对故障树进行时序特征的扩充与规约;其次抽取出用描述逻辑表示的软件安全属性;最后对软件系统进行安全属性建模并通过模型检测工具SPIN形式化验证软件系统是否满足这些属性。以某一机载控制系统环境输入模块为案例,对该案例进行故障树分析和建模并给出该案例的待验证安全属性以及实验分析结果。结果表明,提出的方法是有效的和可行的。

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.