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

周从华

江苏大学;

摘要：

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

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

所属期刊栏目：20

分类号：TP301(计算技术、计算机技术)

资助基金：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

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

页数：共11页

页码：1414-1424