Formal Verification of SDG via Symbolic Model Checking

摘要：

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.

关键词： SDG fault diagnosis SMV module CTL NuSMV

作者: Ning Ning Jun Zhang Xiang-Yang Gao Jing Xue

作者单位: College of Automation Northwestern Polytechnical University Xian, Shaanxi Province, P.R.China

会议类型: 国际会议

会议名称: 2009 Second International Conference on Intelligent Computation Technology and Automation(2009 第二届IEEE智能计算与自动化国际会议 ICICTA 2009)

会议地点: 长沙

会议语种:英文

页码: 3500-3503

在线出版日期: 2009-10-10（万方平台首次上网日期，不代表论文的发表时间）