基于证据自动机的软件回归验证

摘要：

为了在多版本程序验证中利用邻近版本之间的共享信息,提取并重用之前版本证据自动机中的循环不变式,提出基于证据自动机的软件回归验证.首先通过证据预处理生成适用于新版程序的证据文件,然后在辅助不变式增强的k-归纳方法的基础上实现了检验新证据文件及验证新版程序的回归验证过程,最后通过对比实验比较了不使用不变式信息的直接验证与结合或不结合数据流分析的三种回归验证的验证性能.与直接验证相比,不结合与结合数据流分析的回归验证的验证耗时分别减少了49％与75％,而内存消耗分别减少了18％与50％.实验结果表明,当程序满足其验证属性时,基于证据自动机的回归验证能极大地提高验证效率,而将证据自动机与数据流分析相结合的验证方式能得到更好的验证效果.

关键词：回归验证、证据自动机、不变式重用、可配置程序分析检测工具、k-归纳

所属期刊栏目：38

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目 61672310

在线出版日期：2018-11-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：2990-2995,3012