中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 会议论文
Title:
efficient loop-extended model checking of data structure methods
Author: Yi Qiuping ; Liu Jian ; Shen Wuwei
Source: Software Engineering, Business Continuity, and Education
Conference Name: Software Engineering, Business Continuity, and Education International Conferences ASEA, DRBC and EL 2011
Conference Date: FGIT 2011
Issued Date: 2011
Conference Place: Jeju Island, Korea, Republic of
Keyword: Model Checking – ; Loop ; Extended – ; Symbolic Execution
Indexed Type: SPRINGER ; EI
ISSN: 1865-0929
ISBN: 978-3-642-27207-3
Department: Institute of Software Chinese Academy of Sciences Beijing 100190 China
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.
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.
Language: 英语
Content Type: 会议论文
URI: http://ir.iscas.ac.cn/handle/311060/16234
Appears in Collections:软件所图书馆_会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Yi Qiuping,Liu Jian,Shen Wuwei. efficient loop-extended model checking of data structure methods[C]. 见:Software Engineering, Business Continuity, and Education International Conferences ASEA, DRBC and EL 2011. Jeju Island, Korea, Republic of. FGIT 2011.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Yi Qiuping]'s Articles
[Liu Jian]'s Articles
[Shen Wuwei]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Yi Qiuping]‘s Articles
[Liu Jian]‘s Articles
[Shen Wuwei]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace