efficient loop-extended model checking of data structure methods

ISCAS OpenIR

	efficient loop-extended model checking of data structure methods
	Yi Qiuping; Liu Jian; Shen Wuwei
	2011
会议名称	Software Engineering, Business Continuity, and Education International Conferences ASEA, DRBC and EL 2011
会议录名称	Software Engineering, Business Continuity, and Education
页码	237-249
会议日期	FGIT 2011
会议地点	Jeju Island, Korea, Republic of
收录类别	SPRINGER ; EI
ISSN	1865-0929
ISBN	978-3-642-27207-3
部门归属	Institute of Software Chinese Academy of Sciences Beijing 100190 China
摘要	Many methods in data structures contain a loop structure on a collection type. These loops result in a large number of test cases and are one of the main obstacles to systematically test these methods. To deal with the loops in methods, in this paper, we propose a novel loop-extended model checking approach, abbreviated as LEMC, to efficiently test whether methods satisfy their own invariant. Our main idea is to combine dynamic symbolic execution with static analysis techniques. Specifically, a concrete execution of the method under test is initially done to collect dynamic execution information, which is used to statically identify the loop-extended similar paths of the concrete execution path. LEMC statically checks and prunes all the states which follow these loop-extended similar paths. The experiments on several case studies show that LEMC can dramatically reduce as many as 90% of the search space and achieve much better performance, compared with the existing approaches such as the Glass Box model checker and Korat.; Many methods in data structures contain a loop structure on a collection type. These loops result in a large number of test cases and are one of the main obstacles to systematically test these methods. To deal with the loops in methods, in this paper, we propose a novel loop-extended model checking approach, abbreviated as LEMC, to efficiently test whether methods satisfy their own invariant. Our main idea is to combine dynamic symbolic execution with static analysis techniques. Specifically, a concrete execution of the method under test is initially done to collect dynamic execution information, which is used to statically identify the loop-extended similar paths of the concrete execution path. LEMC statically checks and prunes all the states which follow these loop-extended similar paths. The experiments on several case studies show that LEMC can dramatically reduce as many as 90% of the search space and achieve much better performance, compared with the existing approaches such as the Glass Box model checker and Korat.
关键词	Model Checking &#8211 Loop Extended &#8211 Symbolic Execution
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16234
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Yi Qiuping,Liu Jian,Shen Wuwei. efficient loop-extended model checking of data structure methods[C],2011:237-249.