Title :
Formal Verification of SDG via Symbolic Model Checking
Author :
Ning, Ning ; Zhang, Jun ; Gao, Xiang-Yang ; Xue, Jing
Author_Institution :
Coll. of Autom., Northwestern Polytech. Univ., Xi´´an, China
Abstract :
The computation temporal logic (CTL) is introduced to Signed Directed Graph (SDG) and a modeling and verifying method via Symbolic Model Checking is presented. The requirements and constrains of SDG are specified firstly, and the properties related to the fault propagation are extended, then the correctness properties of SDG are defined by CTL. Finally SDG is transferred into the SMV module through an algorithm SDG2SMV and verified automatically by using NuSMV. As a result of comparison, it is shown that the properties of SDG can be verified correctly and effectively.
Keywords :
directed graphs; fault diagnosis; formal verification; symbol manipulation; temporal logic; SDG2SMV algorithm; computation temporal logic; fault propagation; formal verification; signed directed graph; symbolic model checking; Automation; Degradation; Educational institutions; Equations; Fault diagnosis; Formal verification; Fuzzy set theory; Inference algorithms; Logic; Safety; CTL; NuSMV; SMV module; fault diagnosis;
Conference_Titel :
Intelligent Computation Technology and Automation, 2009. ICICTA '09. Second International Conference on
Conference_Location :
Changsha, Hunan
Print_ISBN :
978-0-7695-3804-4
DOI :
10.1109/ICICTA.2009.840
