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
Conference Name	Software Engineering, Business Continuity, and Education International Conferences ASEA, DRBC and EL 2011
Source	Software Engineering, Business Continuity, and Education
Pages	237-249
Conference Date	FGIT 2011
Conference Place	Jeju Island, Korea, Republic of
Indexed Type	SPRINGER ; EI
ISSN	1865-0929
ISBN	978-3-642-27207-3
Department	Institute of Software Chinese Academy of Sciences Beijing 100190 China
English Abstract	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.
Keyword	Model Checking &#8211 Loop Extended &#8211 Symbolic Execution
Language	英语
Content Type	会议论文
URI	http://ir.iscas.ac.cn/handle/311060/16234
Collection	中国科学院软件研究所
Recommended Citation GB/T 7714	Yi Qiuping,Liu Jian,Shen Wuwei. efficient loop-extended model checking of data structure methods[C],2011:237-249.

Files in This Item:
There are no files associated with this item.

If you have any objections to this item, please fill out the form below and the administrator will contact you as soon as possible.
Content:
Email：	*
Institution:
Verification Code:	Refresh

Any comments and suggestions are welcomed.
Title:	*
Content:
Email：	*
Verification Code:	Refresh

中国科学院软件研究所机构知识库