基于概率模型检测的动态故障树定量分析方法

摘要

本发明公开了基于概率模型检测的动态故障树定量分析方法，属于动态故障树定量分析技术领域，首先将动态故障树进行形式化描述，将逻辑门转换成相应的连续时间马尔科夫链模型，并将逻辑门之间的连接关系一一对应到CTMC模型上，结合连续时间马尔可夫链和连续时间马尔科夫链之间连接关系的自动生成PRISM代码，并定义CSL属性规约公式，将CSL公式和PRISM代码输入工具得出定量分析的结果。本发明结合层次化分解和PRISM自带的模块同步，将整个动态故障树转换成有限个模块，通过自动转换算法将单个马尔可夫链模型自动转换为PRISM代码，并自动验证顶事件的故障发生概率，通过同步机制实现多个模块、命令之间的同步。