Lazy Slicing for State-Space Exploration  

作　　者：黄少滨 黄宏涛 陈志远 吕天阳 张涛 

机构地区：[1]College of Computer Science and Technology,Harbin Engineering University

出　　处：《Journal of Computer Science & Technology》2012年第4期872-890,共19页计算机科学技术学报（英文版）

基　　金：Supported by the National Natural Science Foundation of China under Grant No. 60873038;the National Key Technology Research and Development Program of the Ministry of Science and Technology of China under Grant Nos. 2009BAH42B02 and 2012BAH08B02

摘　　要：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.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.

关 键 词：counterexample-guided abstraction refinement spurious counterexample over-approximate slicing local refinement lazy slicing 

分 类 号：V11[航空宇航科学与技术—人机与环境工程]