主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第7期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
王博,卢思睿,姜佳君,熊英飞.基于动态分析的软件不变量综合技术.软件学报,2020,31(6):1681-1702
基于动态分析的软件不变量综合技术
Survey of Dynamic Analysis Based Program Invariant Synthesis Techniques
投稿时间:2019-11-25  修订日期:2019-12-19
DOI:10.13328/j.cnki.jos.006014
中文关键词:  不变量|动态分析|软件规约|软件验证|软件测试
英文关键词:program invariant|dynamic analysis|software specification|software verification|software testing
基金项目:国家自然科学基金(61922003,61672045)
作者单位E-mail
王博 北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871
高可信软件技术教育部重点实验室(北京大学), 北京 100871 
 
卢思睿 北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871
高可信软件技术教育部重点实验室(北京大学), 北京 100871 
 
姜佳君 北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871
高可信软件技术教育部重点实验室(北京大学), 北京 100871 
 
熊英飞 北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871
高可信软件技术教育部重点实验室(北京大学), 北京 100871 
xiongyf@pku.edu.cn 
摘要点击次数: 869
全文下载次数: 1289
中文摘要:
      软件不变量是软件的重要属性,在软件验证、软件调试和软件测试等领域有重要作用.自20世纪末以来,基于动态分析的不变量综合技术成为相关领域的一个研究热点,并且取得了一定的进展.收集了90篇相关论文对该领域进行系统总结.基于动态分析的不变量综合技术是该领域的核心问题,提出了“学习者-预言”框架统一描述相关方法,并且在此框架内根据学习者的归纳方法将综合技术大致分为4类,分别是基于模板穷举的方法、基于数值计算的方法、基于统计学习的方法以及基于符号执行的方法.其次,讨论了基于动态分析综合的不变量在软件验证和软件工程等领域的重要应用.随后,总结不变量生成技术中常用的实验对象程序和开源的不变量综合工具.最后,总结该领域并展望未来的研究方向.
英文摘要:
      Program invariants are important properties of software, which play important roles in many software research fields, such as verification, debugging, and testing. Since the end of 20th century, research on dynamic analysis based program invariant synthesis has become a hot topic in related research areas and made remarkable progress. This paper collects 90 related papers to survey researches within this topic. To dynamically synthesize invariants is the key problem of this field. An abstract framework, “learner-oracle”, is proposed to model and subsume synthesis approaches. In general, the synthesis approaches can be classified into four types, i.e. pattern enumeration based approaches, numerical calculation based approaches, statistical learning based approaches, and symbolic execution based approaches. Furthermore, important applications are discussed of dynamic invariants in software engineering and software verification. Then, important subject programs and synthesis tools are briefly summarized. Finally, the remaining opportunities are presented and a conclusion is reached.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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