基于Assume-Guarantee搜索复用的C程序验证方法
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

Supported by the National Natural Science Foundation of China under Grant No.60233020 (国家自然科学基金); the National High-Tech Ressearch and Development Plan of China under Grant No.2006AA01Z429 (国家高技术研究发展计划(863)); the Program for New Century Excellent Talents in University under Grant No.NCET-04-0996 (新世纪优秀人才支持计划)


Verification of C Programs Using Assume-Guarantee Reuse of Searching
Author:
Affiliation:

Fund Project:

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

    提出了一种基于Assume-Guarantee搜索复用的验证方法,对C程序源代码进行验证.其思想是,在程序的每点处都引入一个保守假设条件,并假设从任意点出发,变量取值满足该点假设条件的所有执行路径都不会违背给定性质,然后根据这些假设条件遍历所有可能的执行路径以验证给定的时序安全性质,并在遍历的过程中验证这些假设条件是否满足,如果不满足,则不断对其精化和加强.验证方法总是在保证假设条件可靠的前提下尽量使用较弱的条件,使得大量的执行路径由于满足假设条件而可以搜索复用,从而降低验证代价.应用该方法验证了Linux操作系统中SSL协议的实现程序openssl-0.9.6c满足SSL协议的初始握手规范.实验结果表明,该方法具有良好的实用性和可扩展性.

    Abstract:

    This paper presents a novel method,namely Assume-Guarantee reuse of searching,to verify C programs with respect to temporal safety properties.Its idea is to introduce a conservative assume condition for each program location,and to assume that every path starting from the program location will never violate the property if the evaluation of its variables at that location satisfy the assume condition.All the possible execution paths are traversed based on the assume conditions,and the temporal safety property is checked on the fly.If some assume condition is too weak,it will be continually strengthened based on the spurious counterexamples.The presented verification method can try to adopt the weak assume conditions so as to let more execution paths satisfy the conditions and to reuse the searching efforts.Therefore,a significant reduction of verification cost can be achieved.The verification method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c.The experimental results demonstrate that the method is both effective and practical.

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

易晓东,王戟,杨学军.基于Assume-Guarantee搜索复用的C程序验证方法.软件学报,2007,18(9):2130-2140

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

京公网安备 11040202500063号