Formal verification of SDG diagnosability via symbolic model checking

被引：1

作者：

Ning N. ^{[1
]}

Zhang J. ^{[1
]}

Gao X.-Y. ^{[1
]}

Xue J. ^{[1
]}

机构：

[1] College of Automation, Northwestern Polytechnical University

来源：

Xi Tong Gong Cheng Yu Dian Zi Ji Shu/Systems Engineering and Electronics | 2011年 / 33卷 / 02期

关键词：

Diagnosability; Directed graphic; Signed directed graph model; Symbolic model checking;

D O I：

10.3969/j.issn.1001-506X.2011.02.32

中图分类号：

学科分类号：

摘要：

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.

引用

页码：390 / 394

页数：4

共 15 条

[11] Yang F., Xiao D.Y., SDG-based analysis of fault propagation principles for complex systems, Chinese High Technology Letters, 15, 10, pp. 33-36, (2005)
[12] Oyeleye O.O., Kramer M.A., Qualitative simulation of chemical process systems: Steady-state analysis, American Institute of Chemical Engineers Journal, 34, 9, (1988)
[13] Yang F., Xiao D.Y., Approach to fault diagnosis using SDG based on fault revealing time, Proc. of the 6th World Congress on Intelligent Control and Automation, pp. 5744-5747, (2006)
[14] Cimatti A., Giunchiglia E., Pistore M., Et al., Integrating BDD-based and SAT-based symbolic model checking, Proc. of Frontiers of Combining Systems, LNAI, pp. 49-56, (2002)
[15] Cimatti A., Clarke E., Giunchiglia E., Et al., NuSMV 2: an opensource tool for symbolic model checking, Proc. of the 14th International Conference on Computer Aided Verification, pp. 359-364, (2002)

← 1 2 →