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 条
  • [1] Fesq M.L., Current fault management trends in NASA's planetary spacecraft, Proc. of IEEE Aerospace Conference, pp. 1-9, (2009)
  • [2] Chen Y.Y., Wu G.W., Fault-tolerant verification platform for systems modeled at high level of abstraction, Proc. of the 1st Annual IEEE Systems Conference, pp. 1-7, (2007)
  • [3] Roemer J.M., Dzakowic J., Orsagh R.F., Et al., Validation and verification of prognostic and health management technologies, Proc. of IEEE Aerospace Conference, pp. 3941-3947, (2005)
  • [4] McMillan K.L., Symbolic Model Checking, (1993)
  • [5] Cimatti A., Pecheur C., Cavada R., Formal verification of diagnosability via symbolic model checking, Proc. of the 18th International Joint Conference on Artificial Intelligence, pp. 363-369, (2003)
  • [6] Williams B.C., Nayak P.P., A model-based approach to reactive self-configuring systems, Proc. of American Association for Artificial Intelligence, pp. 971-978, (1996)
  • [7] Liu H.G., Studies on theory and strategy of intelligent fault diagnosis for liquid-propellant rocket engine, (2002)
  • [8] Nelson S., Pecheur C., New V & V Tools for Diagnostic Modeling Environment (DME), (2002)
  • [9] Umeda T., Kuriyama T., O'Shima E., Et al., A graphical approach to cause and effect analysis of chemical processing system, Chemical Engineering Science, 35, 12, pp. 2379-2388, (1980)
  • [10] Liu M.H., Research on fault diagnosis based on SDG and its application, (2005)
12