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

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-10 发布日期:2018-10-13
通讯作者: 贺飞
作者简介:贾尚坤(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-10 Published:2018-10-13
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]. 计算机应用, 2021, 41(8): 2199-2204.
[2]	张杨, 董士程. 面向并发程序中锁机制的智能化推荐方法[J]. 计算机应用, 2021, 41(6): 1597-1603.
[3]	刘宏宇, 梁秀波, 吴俊涵. 基于Kubernetes的Fabric链码管理及高可用技术[J]. 计算机应用, 2021, 41(4): 956-962.
[4]	张舒瑶, 李勇华, 范家佳. 基于博弈论的散货港口堆场堆位分配算法[J]. 计算机应用, 2021, 41(3): 867-874.
[5]	邵建伟, 刘其群, 王焕强, 陈耀旺, 俞东进, SALAMAT Boranbaev. 资源约束下的基于类依赖关系的微服务识别方法[J]. 计算机应用, 2020, 40(12): 3604-3611.
[6]	潘春霞, 杨秋辉, 谭武坤, 邓惠心, 伍佳. 软件缺陷预测中的数据预处理方法[J]. 计算机应用, 2020, 40(11): 3273-3279.
[7]	秦楠, 马亮, 黄锐. 基于系统理论过程分析的软件安全性需求分析与验证方法[J]. 计算机应用, 2020, 40(11): 3261-3266.
[8]	张家奇, 牟永敏, 张志华. 基于控制流的软件设计与实现一致性分析方法[J]. 计算机应用, 2020, 40(10): 3025-3033.
[9]	张凌浩, 王胜, 周辉, 陈一凡, 桂盛霖. 基于MAVLink协议的无人机系统安全通信方案[J]. 计算机应用, 2020, 40(8): 2286-2292.
[10]	朱小杰, 赵子豪, 杜一. 模型驱动的大数据流水线框架PiFlow[J]. 计算机应用, 2020, 40(6): 1638-1647.
[11]	张文烨. 基于图像识别的移动端应用控件检测方[J]. 计算机应用, 0, (): 0-0.
[12]	廖浩宏韦宇炜刘强. 工业仿真系统动态导入OBJ模型的研究与实现[J]. 计算机应用, 0, (): 0-0.
[13]	孙天齐, 胡建鹏, 黄娟, 樊莹. 云环境下Web应用带宽资源预测与管理[J]. 计算机应用, 2020, 40(1): 181-187.
[14]	王曙燕, 郑佳妮, 孙家泽. 基于页面对象的Web应用测试用例生成方法[J]. 计算机应用, 2020, 40(1): 212-217.
[15]	范家佳, 刘洪星, 李勇华, 杨丽金. 基于博弈论的内河港口作业车辆协同选路方法[J]. 计算机应用, 2020, 40(1): 50-55.