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

Formal verification of SDG diagnosability via symbolic model checking

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

Because of quantitative and nonlinear causal information,diagosability of the signed directed graph（SDG） model needs to be further verified and validated.A formal verification approach to diagnosability via symbolic model checking is proposed.A formal characterization of SDG,as a finite state transition system,is transformed firstly,and a symbolic model verifier（SMV） module is modeled.In the framework of the finite state transition system,a diagnosis function is established,and then the diagnosable definition of a diagnosis condition is defined using the idea of diagnosis context.By means of NuSMV,a coupled SMV module is constructed,and then the SDGD_CSMV algorithm is designed with the computation temporal logic（CTL） definition of diagnosable property.Finally,the practical applicability within a simple water tank SDG model is demonstrated,which proves the validation of the diagnosable definition and SDGD_CSMV.