基于符号模型检测的SDG模型可诊断性验证

摘要：

由于定量信息和非线性因果关系的丢失,符号有向图(signed directed graph,SDG)模型的可诊断性需要进一步地进行校核与验证.为此,提出了基于符号模型检测的SDG模型可诊断性形式化验证方法.首先定义了SDG模型的有限状态变迁系统形式化描述,建立了符号模型验证器(symbolic model verifier,SMV)模型;其次利用SDG的深层知识,构造了可诊断性函数,设定了可诊断性上下文,给出了可诊断性定义.然后,构造了SDG耦合孪生SMV模型,定义了可诊断性的计算树时态逻辑公式,提出了验证算法SDGD-CSMV.最后,通过一个实例验证了可诊断性的判定和算法的有效性.

关键词：有向图形学、可诊断性、符号模型检测、符号有向图模型

所属期刊栏目：33

分类号：TP206(自动化技术及设备)

在线出版日期：2011-06-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：390-394