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 |
| 会议日期 | FGIT 2011 |
| 会议地点 | Jeju Island, Korea, Republic of |
| 关键词 | Model Checking – Loop Extended – Symbolic Execution |
| 页码 | 237-249 |
| 中文摘要 | 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. |
| 收录类别 | SPRINGER ; EI |
| 会议录 | Software Engineering, Business Continuity, and Education
 |
| 语种 | 英语 |
| ISSN号 | 1865-0929 |
| ISBN号 | 978-3-642-27207-3 |
| 源URL | [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]. 见:Software Engineering, Business Continuity, and Education International Conferences ASEA, DRBC and EL 2011. Jeju Island, Korea, Republic of. FGIT 2011. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。