| 基于SAT的软件验证 |
| |
| 引用本文： | 周从华,陈振宇,鞠时光.基于SAT的软件验证[J].计算机研究与发展,2008,45(Z1):124-130. |
| |
| 作者姓名： | 周从华 陈振宇 鞠时光 |
| |
| 作者单位： | 1. 江苏大学计算机科学与通信工程学院,镇江,212013
2. 东南大学计算机科学与工程学院,南京,210096 |
| |
| 基金项目： | 国家自然科学基金
,
江苏省自然科学基金
,
江苏大学校科研和教改项目 |
| |
| 摘 要： | 线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.
|
| 关 键 词： | 模型检测 SAT 软件验证 形式化分析 |
| 修稿时间： | 2007年7月10日 |
SAT-Based Software Verification |
| |
| Zhou Conghua,Chen Zhenyu,Ju Shiguang.SAT-Based Software Verification[J].Journal of Computer Research and Development,2008,45(Z1):124-130. |
| |
| Authors: | Zhou Conghua Chen Zhenyu Ju Shiguang |
| |
| Affiliation: | Zhou Conghua1,Chen Zhenyu2,, Ju Shiguang11(School of Computer Science , Telecommunication Engineering,Jiangsu University,Zhenjiang 212013)2(School of Computer Science , Engineering,Southeast University,Nanjing 210096) |
| |
| Abstract: | For concurrent software systems, linear temporal logic SE-LTL is a specification language with high expressive power and the ability to reason about both states and events. Until now, the SE-LTL model checking algorithm is still explicit, and the state explosion is the primary verification difficulty. A bounded model checking procedure is introduced for SE-LTL which reduces model checking to propositional satisfiability. This new technique avoids the space blow up of BDDs, and sometimes speeds up the verifi... |
| |
| Keywords: | model checking SAT software verification formal analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
