Lazy Slicing for State-Space Exploration |
| |
Authors: | Shao-Bin Huang Hong-Tao Huang Zhi-Yuan Chen Tian-Yang Lv Tao Zhang |
| |
Affiliation: | 1. College of Computer Science and Technology, Harbin Engineering University, Harbin, 150001, China
|
| |
Abstract: | CEGAR (Counterexample-guided abstraction refinement)-based slicing is one of the most important techniques in reducing the state space in model checking. However, CEGAR-based slicing repeatedly explores the state space handled previously in case a spurious counterexample is found. Inspired by lazy abstraction, we introduce the concept of lazy slicing which eliminates this repeated computation. Lazy slicing is done on-the-fly, and only up to the precision necessary to rule out spurious counterexamples. It identifies a spurious counterexample by concretizing a path fragment other than the full path, which reduces the cost of spurious counterexample decision significantly. Besides, we present an improved over-approximate slicing method to build a more precise slice model. We also provide the proof of the correctness and the termination of lazy slicing, and implement a prototype model checker to verify safety property. Experimental results show that lazy slicing scales to larger systems than CEGAR-based slicing methods. |
| |
Keywords: | counterexample-guided abstraction refinement spurious counterexample over-approximate slicing local refinement lazy slicing |
本文献已被 CNKI SpringerLink 等数据库收录! |
|