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

• 作者: 周从华
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 有界模型检测 抽象 平行组合
• 年，卷（期）: 2009,（6）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 1414-1424
• 页数: 11页
• 分类号: TP301
• 字数: 4854字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2009.00558

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0