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

doi:10.11772/j.issn.1001-9081.2018030733

计算机应用 ›› 2018, Vol. 38 ›› Issue (10): 2990-2995.DOI: 10.11772/j.issn.1001-9081.2018030733

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

贾尚坤, 贺飞

清华大学软件学院, 北京 100084

收稿日期:2018-04-10 修回日期:2018-05-16 发布日期:2018-10-13 出版日期:2018-10-10
通讯作者: 贺飞
作者简介:贾尚坤(1993-),男,山西大同人,硕士研究生,主要研究方向:概率程序、回归验证;贺飞(1980-),男,湖南永州人,副教授,博士,CCF会员,主要研究方向:抽象精化、概率模型检测、回归验证、组合验证。
基金资助:
国家自然科学基金资助项目（61672310）。

Software regression verification based on witness automata

JIA Shangkun, HE Fei

School of Software, Tsinghua University, Beijing 100084, China

Received:2018-04-10 Revised:2018-05-16 Online:2018-10-13 Published:2018-10-10
Supported by:
This work is partially supported by the National Natural Science Foundation of China (61672310).

摘要/Abstract

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

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

Abstract: In order to utilize the shared information between adjacent versions in multi-version program verification, and extract and reuse loop invariants in the witness automaton belonging to the previous version, a software regression verification based on witness automata was proposed. Firstly, the witness file applicable to the new version of programs was generated by witness preprocessing. Then, based on the auxiliary-invariant-enhanced k-induction, the regression verification process was implemented to validate the new witness file and verify the new version of programs. Finally, performance of three kinds of regression verification was compared by contrast experiments, including the so-called "direct" verification that did not use invariant information and verification methods combined with or without data flow analysis. Compared with the direct verification, the time consumption of the regression verification combined with or without data flow analysis was reduced by 49% and 75% respectively, and the memory consumption was reduced by 18% and 50% respectively. The results show that when the program satisfies its verification specification, the regression verification based on witness automata can greatly improve verification efficiency, and the regression method combined with data flow analysis can make it even better.

Key words: regression verification, witness automata, invariant reuse, Configurable Program Analysis checker (CPAchecker), k-induction

中图分类号:

TP311.5

贾尚坤, 贺飞. 基于证据自动机的软件回归验证[J]. 计算机应用, 2018, 38(10): 2990-2995.

JIA Shangkun, HE Fei. Software regression verification based on witness automata[J]. Journal of Computer Applications, 2018, 38(10): 2990-2995.

参考文献

[1] BJESSE P. What is formal verification?[J]. ACM SIGDA Newsletter, 2005, 35(24):Article No. 1.
[2] BEYER D, LÖWE S, NOVIKOV E, et al. Precision reuse for efficient regression verification[C]//Proceedings of the 20139th Joint Meeting on Foundations of Software Engineering. New York:ACM, 2013:389-399.
[3] ROTHERMEL G, HARROLD M J. Analyzing regression test selection techniques[J]. IEEE Transactions on Software Engineering, 1996, 22(8):529-551.
[4] YANG G, DWYER M B, ROTHERMEL G. Regression model checking[C]//Proceedings of the 2009 IEEE International Conference on Software Maintenance. Piscataway, NJ:IEEE, 2009:115-124.
[5] GODLIN B, STRICHMAN O. Regression verification[C]//Proceedings of the 46th Annual Design Automation Conference. New York:ACM, 2009:466-471.
[6] BEYER D, WENDLER P. Reuse of verification results[C]//Proceedings of the 2013 International SPIN Workshop on Model Checking of Software. Berlin:Springer, 2013:1-17.
[7] BEYER D, DANGL M, DIETSCH D, et al. Correctness witnesses:exchanging verification results between verifiers[C]//Proceedings of the 201624th ACM SIGSOFT International Symposium on Foundations of Software Engineering. New York:ACM, 2016:326-337.
[8] BEYER D, DANGL M, DIETSCH D, et al. Witness validation and stepwise testification across software verifiers[C]//Proceedings of the 201510th Joint Meeting on Foundations of Software Engineering. New York:ACM, 2015:721-733.
[9] BEYER D. Software verification and verifiable witnesses[C]//Proceedings of the 2015 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer, 2015:401-416.
[10] BEYER D. Software verification with validation of results[C]//Proceedings of the 2017 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer, 2017:331-349.
[11] BEYER D, HENZINGER T A, THÉODULOZ G. Configurable software verification:Concretizing the convergence of model checking and program analysis[C]//Proceedings of the 2007 International Conference on Computer Aided Verification. Berlin:Springer,2007:504-518.
[12] BEYER D, KEREMOGLU M E. CPAchecker:a tool for configurable software verification[C]//Proceedings of the 2011 International Conference on Computer Aided Verification. Berlin:Springer, 2011:184-190.
[13] CUOQ P, KIRCHNER F, KOSMATOV N, et al. Frama-C[C]//Proceedings of the 2012 International Conference on Software Engineering and Formal Methods. Berlin:Springer, 2012:233-247.
[14] SHEERAN M, SINGH S, STÅLMARCK G. Checking safety properties using induction and a SAT-solver[C]//Proceedings of the 2000 International Conference on Formal Methods in Computer-aided Design. Berlin:Springer, 2000:127-144.
[15] DONALDSON A F, KROENING D, RVMMER P. Automatic analysis of DMA races using model checking and k-induction[J]. Formal Methods in System Design, 2011, 39(1):83-113.
[16] HAGEN G, TINELLI C. Scaling up the formal verification of Lustre programs with SMT-based techniques[C]//Proceedings of the 2008 Formal Methods in Computer-Aided Design. Piscataway, NJ:IEEE, 2008:1-9.
[17] ROCHA H, ISMAIL H, CORDEIRO L, et al. Model checking embedded C software using k-induction and invariants[M]//LETTNIN D, WINTERHOLER M. Embedded Software Verification and Debugging. Berlin:Springer, 2017:159-182.
[18] BEYER D, DANGL M, WENDLER P. Boosting k-induction with continuously-refined invariants[C]//Proceedings of the 2015 International Conference on Computer Aided Verification. Berlin:Springer, 2015:622-640.
[19] BEYER D, HENZINGER T A, THÉODULOZ G. Program analysis with dynamic precision adjustment[C]//Proceedings of the 200823rd IEEE/ACM International Conference on Automated Software Engineering. Washington, DC:IEEE Computer Society, 2008:29-38.
[20] BEYER D, DANGL M, WENDLER P. Combining k-induction with continuously-refined invariants[EB/OL].[2018-01-02].https://arxiv.org/abs/1502.00096.
[21] JIA Y, HARMAN M. MILU:a customizable, runtime-optimized higher order mutation testing tool for the full C language[C]//Proceedings of the Testing:Academic & Industrial Conference-Practice and Research Techniques. Washington, DC:IEEE Computer Society, 2008:94-98.
[22] BEYER D, LÖWE S, WENDLER P. Benchmarking and resource measurement[C]//Proceedings of the 2015 International SPIN Workshop on Model Checking of Software. Berlin:Springer, 2015:160-178.
[23] 杨军, 葛海通, 郑飞君, 等. 一种形式化验证方法:模型检验[J]. 浙江大学学报(理学版), 2006, 33(4):403-407. (YANG J, GE H T, ZHENG F J, et al. A formal verification method:model checking[J]. Journal of Zhejiang University (Science Edition), 2006, 33(4):403-407.)
[24] 石海鹤, 肖正兴, 薛锦云. 循环不变式开发新策略及其应用[J]. 计算机工程与应用, 2006, 42(4):105-107. (SHI H H, XIAO Z X, XUE J Y. A new strategy for developing loop invariants and its application[J]. Computer Engineering and Applications, 2006, 42(4):105-107.)
[25] 李未, 黄雄. 命题逻辑可满足性问题的算法分析[J]. 计算机科学, 1999, 26(3):1-9. (LI W, HUANG X. The analysis of algorithms for the propositional logic satisfiability problem[J]. Computer Science, 1999, 26(3):1-9.)

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

Software regression verification based on witness automata

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	吴海峰陶丽青程玉胜. 集成特征注意力和残差连接的偏标签回归算法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[2]	孙蒴, 张伟, 冯温迪, 张俞炜. 基于源码分析的自动化外部函数接口生成方法[J]. 《计算机应用》唯一官方网站, 2024, 44(7): 2151-2159.
[3]	万泽轩, 谢春丽, 吕泉润, 梁瑶. 基于依赖增强的分层抽象语法树的代码克隆检测[J]. 《计算机应用》唯一官方网站, 2024, 44(4): 1259-1268.
[4]	孙祥杰, 魏强, 王奕森, 杜江. 代码相似性检测技术综述[J]. 《计算机应用》唯一官方网站, 2024, 44(4): 1248-1258.
[5]	姚洪磊, 刘吉强, 童恩栋, 牛温佳. 基于 α-截集三角模糊数和攻击树的CTCS网络安全风险评估方法[J]. 《计算机应用》唯一官方网站, 2024, 44(4): 1018-1026.
[6]	刘祥, 华蓓, 林飞, 魏宏原. 面向深度学习应用的组件式开发框架的设计实现[J]. 《计算机应用》唯一官方网站, 2024, 44(2): 526-535.
[7]	胡轶涵, 杜金莲, 苏航, 高红雨. 面向不可移动文物自然灾害风险图生成的领域特定语言[J]. 《计算机应用》唯一官方网站, 2024, 44(1): 152-158.
[8]	宋其洪, 刘建勋, 扈海泽, 张祥平. 基于协同融合网络的代码搜索模型[J]. 《计算机应用》唯一官方网站, 2023, 43(12): 3896-3902.
[9]	李文博, 刘波, 陶玲玲, 罗棻, 张航. L1正则化的深度谱聚类算法[J]. 《计算机应用》唯一官方网站, 2023, 43(12): 3662-3667.
[10]	朱嘉豪, 郑巍, 杨丰玉, 樊鑫, 肖鹏. 基于蚁群算法优化反向传播神经网络的软件质量预测[J]. 《计算机应用》唯一官方网站, 2023, 43(11): 3568-3573.
[11]	叶盛, 王菁, 辛建峰, 王桂玲, 郭陈虹. 云边环境下微服务组合系统的动态演化方法[J]. 《计算机应用》唯一官方网站, 2023, 43(6): 1696-1704.
[12]	朱嘉豪郑巍杨丰玉樊鑫肖鹏. 基于蚁群优化反向传播神经网络的软件质量预测[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[13]	于振华, 刘争气, 刘颖, 郭城. 基于自适应混合粒子群优化的软件缺陷预测特征选择方法[J]. 《计算机应用》唯一官方网站, 2023, 43(4): 1206-1213.
[14]	王腾, 霍峥, 黄亚鑫, 范艺琳. 联邦学习中的隐私保护技术研究综述[J]. 《计算机应用》唯一官方网站, 2023, 43(2): 437-449.
[15]	陶玲玲, 刘波, 李文博, 何希平. 有闭解的可控人脸编辑算法[J]. 《计算机应用》唯一官方网站, 2023, 43(2): 601-607.