###
DOI:
Journal of Software:2009.20(6):1414-1424

一种基于满足性判定的并发软件验证策略
周从华
(江苏大学 计算机科学与通信工程学院,江苏 镇江 212013)
SAT-Based Compositional Verification Strategy for Concurrent Software with States, Events
ZHOU Cong-Hua
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3785   Download 3582
Received:May 30, 2007    Revised:March 06, 2008
> 中文摘要: 对线性时态逻辑SE-LTL提出了一种基于SAT的有界模型检测过程,该过程避免了基于BDD方法中状态空间快速增长的问题.在SE-LTL的子集SE-LTL?X的有界模型检测过程中,集成了stuttering等价技术,该集成有效地加速了验证过程.进一步提出了一种组合了基于SAT的有界模型检测、基于反例的抽象求精、组合推理3种状态空间约简技术的并发软件验证策略.该策略中,抽象和求精在每一个构件上独立进行.同时,模型检测的过程是符号化的.实例表明,该策略降低了验证时间和对内存空间的需求.
中文关键词: 有界模型检测  抽象  平行组合
Abstract:For the state/event linear temporal logic SE-LTL, an SAT-based Bounded Model Checking procedure which avoids the space blow up of BDDs is presented. For SE-LTL-X, it is shown how to integrate the procedure and the stuttering equivalent technique. The integration speeds up the verification procedure. Furthermore, a framework for model checking concurrent software systems which integrates three powerful verification techniques is presented: SAT-based Bounded Model Checking, counterexample-guided abstraction refinement and compositional reasoning. In the framework the abstraction and refinement steps are performed over each component separately, and the model checking step is symbolic. Example shows that the framework can reduce verification time and space.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant No.60773049 (国家自然科学基金); the Advanced Talent Foundation of Jiangsu University of China under Grant No.07JDG014 (江苏大学高级人才科研启动基金); the Fundamental Research Project of the Natural Science in Colleges of Jiangsu Province of China under Grant No.08KJD520015 (江苏省高校自然科学基金) Supported by the National Natural Science Foundation of China under Grant No.60773049 (国家自然科学基金); the Advanced Talent Foundation of Jiangsu University of China under Grant No.07JDG014 (江苏大学高级人才科研启动基金); the Fundamental Research Project of the Natural Science in Colleges of Jiangsu Province of China under Grant No.08KJD520015 (江苏省高校自然科学基金)
Foundation items:
Reference text:

周从华.一种基于满足性判定的并发软件验证策略.软件学报,2009,20(6):1414-1424

ZHOU Cong-Hua.SAT-Based Compositional Verification Strategy for Concurrent Software with States, Events.Journal of Software,2009,20(6):1414-1424