一种基于满足性判定的并发软件验证策略(英文)  

SAT-Based Compositional Verification Strategy for Concurrent Software with States,Events

作　　者：周从华[1] 

机构地区：[1]江苏大学计算机科学与通信工程学院,江苏镇江212013

出　　处：《软件学报》2009年第6期1414-1424,共11页Journal of Software

基　　金：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~~

摘　　要：对线性时态逻辑SE-LTL提出了一种基于SAT的有界模型检测过程,该过程避免了基于BDD方法中状态空间快速增长的问题.在SE-LTL的子集SE-LTL?X的有界模型检测过程中,集成了stuttering等价技术,该集成有效地加速了验证过程.进一步提出了一种组合了基于SAT的有界模型检测、基于反例的抽象求精、组合推理3种状态空间约简技术的并发软件验证策略.该策略中,抽象和求精在每一个构件上独立进行.同时,模型检测的过程是符号化的.实例表明,该策略降低了验证时间和对内存空间的需求.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.

关 键 词：有界模型检测 抽象 平行组合 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]