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

Volume

4

fYear

2009

fDate

10-11 Oct. 2009

Firstpage

521

Lastpage

524

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ICICTA.2009.840

Filename

5288345