作者：司佳; 朱羿全; 马琳故障树分析时序描述逻辑安全属性形式化验证
摘要：故障树分析法是工业界常用的安全分析方法之一。然而由于其非形式化方法的局限性，难以对软件故障进行形式化验证，更难以描述嵌入式实时系统中事件之间的时序逻辑关系。因此，提出了一种基于时序描述逻辑的故障树分析方法，以解决故障树难以对时序关系进行描述以及难以形式化验证的问题。首先，通过时序描述逻辑对故障树进行时序特征的扩充与规约；其次抽取出用描述逻辑表示的软件安全属性；最后对软件系统进行安全属性建模并通过模型检测工具SPIN形式化验证软件系统是否满足这些属性。以某一机载控制系统环境输入模块为案例，对该案例进行故障树分析和建模并给出该案例的待验证安全属性以及实验分析结果。结果表明，提出的方法是有效的和可行的。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
