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.

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.

Click here for full paper!

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.

Click here for full paper!