支持模型检测的故障树生成方法研究

A Fault Tree Analysis Method Supporting Model Checking

论文运用时序逻辑对传统故障树进行形式化规约,并从中抽取出描述软件安全属性的时序逻辑公式,来支持对安全关键软件的模型检测。文章以对某一机载控制系统软件数据交互模块的模型检测为案例研究,实验结果证明本文提出方法有效。

The paper specifies formal specification of fault tree with temporal logic.It extracts the temporal logic formula which describes the software safety property from the formal fault tree.Expert can use the extracted safety property do model checking of the safety-critical software and implement formal verification and analysis of its reliability and safety.The paper does the model checking to a part of a safety-critical software on the plane to demonstrate the method in detail.