一种基于满足性判定的并发软件验证策略
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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 (江苏省高校自然科学基金)


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

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    对线性时态逻辑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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2007-05-30
  • 最后修改日期:2008-03-06
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号