Formal Verification of SDG via Symbolic Model Checking
- Resource Type
- Conference
- Authors
- Ning, Ning; Zhang, Jun; Gao, Xiang-Yang; Xue, Jing
- Source
- 2009 Second International Conference on Intelligent Computation Technology and Automation Intelligent Computation Technology and Automation, 2009. ICICTA '09. Second International Conference on. 4:521-524 Oct, 2009
- Subject
- Computing and Processing
Communication, Networking and Broadcast Technologies
Formal verification
Fault diagnosis
Automation
Inference algorithms
Safety
Educational institutions
Logic
Equations
Fuzzy set theory
Degradation
fault diagnosis
SMV module
CTL
NuSMV
- Language
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.