采用CPAChecker的动态程序验证

doi:10.19665/j.issn1001-2400.2019.01.006

西安电子科技大学学报 ›› 2019, Vol. 46 ›› Issue (1): 33-38.doi: 10.19665/j.issn1001-2400.2019.01.006

采用CPAChecker的动态程序验证

段钊¹,刘锟龙²

^1. 西安电子科技大学计算机学院,陕西西安 710071
^2. 合肥工业大学电气与自动化工程学院,安徽合肥 230009

收稿日期:2018-06-27 出版日期:2019-02-20 发布日期:2019-03-05
作者简介:段钊 (1990-),男,西安电子科技大学博士研究生,E-mail: duanzhao_xidian@163.com
基金资助:
国家自然科学基金(61732013)

Dynamic program verification via a CPAChecker

DUAN Zhao¹,LIU Kunlong²

^1. School of Computer Science and Technology, Xidian Univ., Xi’an 710071, China;
^2. School of Electrical Engineering and Automaton, Hefei University of Technology, Anhui 230009, China

Received:2018-06-27 Online:2019-02-20 Published:2019-03-05

摘要/Abstract

摘要：

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法. 首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程。其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化。实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率。

关键词: 模型检测, 抽象精化, 动态执行, 程序验证, 状态空间爆炸

Abstract:

To overcome the state space explosion problem in model checking, a CPAChecker based dynamic program verification approach is proposed. The proposed approach first verifies the program statically by unwinding the control flow chart. In the process, dynamic execution is applied to accelerate the verification on the basis of the determinism of branch statements. Specifically, abstract verification effectively reduces the size of the system models, while dynamic detection not only effectively reduces false positives, but also guides the construction of more accurate system models. As a result, the proposed approach makes counterexample-guided abstraction refinement more efficient and accurate in practice.

Key words: model checking, abstract refinement, dynamic execution, program verification, state space explosion

中图分类号:

TP302.7

段钊, 刘锟龙. 采用CPAChecker的动态程序验证[J]. 西安电子科技大学学报, 2019, 46(1): 33-38.

DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker[J]. Journal of Xidian University, 2019, 46(1): 33-38.

图/表 2

参考文献 16

[1]	CIMATTI A, CLARKE E, GIUNCHIGLIA F , et al. NUSMV: a New Symbolic Model Checker[J]. International Journal on Software Tools for Technology Transfer, 2000,2(4):410-425. doi: 10.1007/s100090050046
[2]	逄涛, 段振华, 刘晓芳 . Verilog程序的命题投影时序逻辑符号模型检测[J]. 西安电子科技大学学报, 2014,41(2):79-84. doi: 10.3969/j.issn.1001-2400.2014.02.013
	PANG Tao, DUAN Zhenhua, LIU Xiaofang . Symbolic Model Checking of Verilog Programs with the Propositional Projection Temporal Logic[J]. Journal of Xidian University, 2014,41(2):79-84. doi: 10.3969/j.issn.1001-2400.2014.02.013
[3]	ABDULLA P A, ARONIS S, ATIG M F , et al. Stateless Model Checking for TSO and PSO[J]. Acta Informatica, 2017,54(8):789-818. doi: 10.1007/978-3-662-46681-0_28
[4]	GODEFROID P, SEN K . Combining Model Checking and Testing[M]. Cham: Springer, 2018: 613-649.
[5]	KOMURAVELLI A, GURFINKEL A, CHAKI S . SMT-based Model Checking for Recursive Programs[J]. Formal Methods in System Design, 2016,48(3):175-205. doi: 10.1007/978-3-319-08867-9_2
[6]	LOMUSCIO A, QU H, RAIMONDI F . MCMAS: an Open-source Model Checker for the Verification of Multi-agent Systems[J]. International Journal on Software Tools for Technology Transfer, 2017,19(1):9-30. doi: 10.1007/s10009-015-0378-x
[7]	TIAN C, DUAN Z. Detecting Spurious Counterexamples Efficiently in Abstract Model Checking [C]//Proceedings of the 2013 International Conference on Software Engineering. Washington: IEEE Computer Society, 2013: 202-211.
[8]	BATTISTA P, MERCALDO F, NARDONE V, et al. Identification of Android Malware Families with Model Checking [C]// Proceedings of the 2016 2nd International Conference on Information Systems Security and Privacy. Setúbal: SciTePress, 2016: 542-547.
[9]	BEYER D, STAHLBAUER A . BDD-based Software Verification[J]. International Journal on Software Tools for Technology Transfer, 2014,16(5):507-518. doi: 10.1007/s10009-014-0334-1
[10]	TIAN C, DUAN Z, DUAN Z, et al. More Effective Interpolations in Software Model Checking [C]//Proceedings of the 2017 32nd IEEE/ACM International Conference on Automated Software Engineering. Piscataway: IEEE, 2017: 183-193.
[11]	BALL T, MAJUMDAR R, MILLSTEIN T, et al. Automatic Predicate Abstraction of C Programs [C]//Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM, 2001: 203-213.
[12]	BALL T, PODELSKI A, RAJAMANI S K. Boolean and Cartesian Abstraction for Model Checking C Programs [C]//Lecture Notes in Computer Science: 2031. Heidelberg: Springer Verlag, 2001: 268-283.
[13]	BEYER D, LEMBERGER T. Symbolic Execution with CEGAR [C]//Lecture Notes in Computer Science: 9952. Heidelberg: Springer Verlag, 2016: 195-211.
[14]	TIAN C, DUAN Z, DUAN Z . Making CEGAR More Efficient in Software Model Checking[J]. IEEE Transactions on Software Engineering, 2014,40(12):1206-1223. doi: 10.1109/TSE.2014.2357442
[15]	BEYER D, JAKOBS M C, LEMBERGER T, et al. Reducer-based Construction of Conditional Verifiers [C]//Proceedings of the 2018 International Conference on Software Engineering. Washington: IEEE Computer Society, 2018: 1182-1193.
[16]	BEYER D, LÖWE S. Explicit-state Software Model Checking Based on CEGAR and Interpolation [C]//Lecture Notes in Computer Science: 7793. Heidelberg: Springer Verlag, 2013: 146-162.

采用CPAChecker的动态程序验证

Dynamic program verification via a CPAChecker

RichHTML

PDF (PC)

赞

可视化

摘要/Abstract

引用本文

使用本文

图/表 2

参考文献 16

相关文章 7

Metrics

本文评价

推荐阅读 10

程序包名	程序数	P_dn	P_an	N_T/包	Refine		通过率/(%)		正确率/(%)
程序包名	程序数	P_dn	P_an	N_T/包	新算法	原工具	新算法	原工具	新算法	原工具
bitvector-regression	10	10	0	-10	0	1	100	100	90	40
loop-lit	16	16	0	-5	0	29	94	88	94	88
loop-new	8	8	0	8	0	13	100	50	100	38
floats-cbmc-regression	31	26	5	-19	5	25	87	87	77	65
loop-invgen	18	18	0	7	0	123	89	83	78	50
loop-acceleration	36	30	6	29	10	334	94	39	83	22
bitvector-loops	3	3	0	1	0	65	100	100	66	33

[1]	沈利香,慕德俊,曹国,谢光前,束方勇. 针对硬件木马的形式化验证模型构造方法[J]. 西安电子科技大学学报, 2021, 48(3): 146-153.
[2]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[3]	丁明,张书玲,张琛,张军. 一种航空电子系统安全性需求验证方法[J]. 西安电子科技大学学报, 2019, 46(3): 66-73.
[4]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.
[5]	杨元原;马文平;刘维博;俞优;顾健. 带有异或运算安全协议的自动化检测[J]. J4, 2012, 39(4): 120-125+183.
[6]	杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.
[7]	刘秀英1;2;张玉清2;杨波1;邢戈2. TMN协议的形式化分析[J]. J4, 2004, 31(5): 785-790.