Title :
Formal Verification for Quality Analysis of SDG Fault Diagnosis Model via Symbolic Model Checking
Author :
Ning, Ning ; Zhang Jun ; Gao Xiangyang ; Xue Jing
Author_Institution :
Coll. of Autom., Northwestern Polytech. Univ., Xian, China
Abstract :
The verification for quality property of SDG fault diagnosis model is originally placed at the framework of symbolic model checking (SMC). SDG model is translated to the symbolic model verifier (SMV) module based on the finite state transition system definition firstly, and the quality property are formally analyzed and extended, then the verification approach are characterized and verified automatically by using NuSMV. The practical applicability within a satellite power system proves that the extended quality property of SDG can be verified correctly and effectively.
Keywords :
directed graphs; fault diagnosis; formal verification; SDG fault diagnosis model; finite state transition system; formal verification; quality analysis; satellite power system; signed directed graph; symbolic model checking; symbolic model verifier; Automation; Educational institutions; Fault diagnosis; Formal verification; Mechatronics; Power system analysis computing; Power system modeling; Satellites; Sliding mode control; Virtual manufacturing; NuSMV; SMV module; quality property of SDG;
Conference_Titel :
Measuring Technology and Mechatronics Automation (ICMTMA), 2010 International Conference on
Conference_Location :
Changsha City
Print_ISBN :
978-1-4244-5001-5
Electronic_ISBN :
978-1-4244-5739-7
DOI :
10.1109/ICMTMA.2010.103
