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

Volume

2

fYear

2010

fDate

13-14 March 2010

Firstpage

305

Lastpage

308

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ICMTMA.2010.103

Filename

5459819