主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
周从华.一种基于满足性判定的并发软件验证策略.软件学报,2009,20(6):1414-1424
一种基于满足性判定的并发软件验证策略
SAT-Based Compositional Verification Strategy for Concurrent Software with States, Events
投稿时间:2007-05-30  修订日期:2008-03-06
DOI:
中文关键词:  有界模型检测  抽象  平行组合
英文关键词:bounded model checking  abstract  parallel composition
基金项目: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 (江苏省高校自然科学基金)
作者单位
周从华 江苏大学 计算机科学与通信工程学院,江苏 镇江 212013 
摘要点击次数: 3945
全文下载次数: 3667
中文摘要:
      对线性时态逻辑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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利