Stepwise increasing bounded model checking with variable step length

At present, the functionality and performance verification of software and hardware system becomes more and more important. It relates to the country and people´s property and life safety. In numerous validation methods, model checking techniques have got the attention of many researchers because that have characteristic of good completeness, error positioning accuracy and automation degree higher. However, when the system scale increasing, there will be a state space explosion problem in model checking. This paper puts forward a new model detection algorithm to reduction the states: stepwise increasing bounded model checking with variable step length (VSIB). First of all, we do some preparations for this algorithm can be implemented. Such as defining bounded semantics, proving that there is an infinite approximation between bounded semantics and unbounded semantics, and describing the fixed point of Computation Tree Logic (CTL) operator under bounded semantic. Then the algorithm thinking and pseudo code are introduced. Finally, the experimental data show that this algorithm is effective in reducing the states. To some extent, this method can alleviate the problem of state space explosion and can improve the efficiency of software and hardware verification.