Lazy Slicing for State-Space Exploration
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.
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.
lazyslicing.pdf | |
File Size: | 1877 kb |
File Type: |
Model reduction using the orthogonality between overapproximate slicing and abstract
The orthogonality between static slicing and abstract method has been used to furtherly reduce the state space in model checking. However, static slicing can not always guarantee a slicing model with an desired size. This paper proposes a new approach which compute the over approximate slicing of an abstract state graph other than a counterpart of a static slicing. An overapproximate slicing is obtained by only considering the data dependence relations between predicates, which will always lead to a slice with an ideal size for verification. Though the overapproximate slice only has a weak property resistance power, it is an super set of the abstract state graph, which guarantees if a property $\phi$ is satisfied on the overapproximate slice, then the original specification is a model of $\phi$. And if there appears a spurious counterexample, then it increases the precision of the overapproximate slice by refinement to keep the verification cost as low as possible. We also provide sufficient proof for the correctness of our method. The experimental result shows that our method improves the scalability of model checking remarkably and scales better to a larger system.
Click here for full paper!
Click here for full paper!
产生式知识库的不动点计算建模方法
A modeling method based on fixed point computation for a production knowledge base
A modeling method based on the procedural nature of production rules was proposed to build a system model.The definition of the conditional transition system(CTS) was given by the concept of conditional transitions.Small fix point computing was introduced to build the conditional transition system.The system model represented by the conditional transition system was built by solving the small fix point of the constructing function of the states set,and the correctness and termination of this method was proven.The proposed dynamic modeling method improves the efficiency of the production knowledge base modeling process.The time complexity reduced one order of magnitude compared with the static modeling method.The conditional transition system built by this method contains all information about the state transition process,and solves the information loss problem of the transition system constructed by the static modeling method,increasing the efficiency of error diagnosis.
fixed_point_model.pdf | |
File Size: | 1061 kb |
File Type: |
A Formal Method for Verifying Production Knowledge Base (ICICSE`09)
Abstract: The most important thing of using model checking technology to verify production knowledge base is to build system model from rule set. It is a fundamental but time-consuming job. This paper presents an efficient formal method to verify production knowledge base. Two main contributions of this paper are as follows. Firstly, we propose a dynamic modeling method to build system model of knowledge base, this method utilizes the dynamic procedural nature of production rule to build system model, and it improves the modeling efficiency significantly; Secondly, a conditional transition system based on the standard transition system is given to represent system model, our conditional transition system contains the whole information about the actual state transition process, which solves the information loss problem of the static transition system built by static modeling method and improves the efficiency of error diagnosis.
4027a019.pdf | |
File Size: | 323 kb |
File Type: |