Improving the process of model checking through state space reductions

Model checking is a technique for finding errors in systems and algorithms. The tech nique requires a formal definition of the system with a set of correctness conditions, and the use of a tool, the model checker, that searches for model behaviours violating these correctness conditions. The value of existing model checkers depends largely on the complexity of the system being checked. Systems involving complex data structures quickly encounter the problem of state explosion, and checking becomes intractable. Furthermore, auxiliary feedback originally designed to aid the practitioner (e.g., process automata) becomes less useful. This thesis develops of a set of techniques to address these problems. The main contri butions of this thesis are methods that improve model checking in the formal language of B, by reductions in the size of a system's state space. Methods are described that enable a user to view various succinct properties about a system's behaviour through automatic analysis of reached state spaces, and a technique is developed to improve the efficiency of generating state spaces during model checking using algorithms for identify ing symmetries via graph isomorphism. Soundness proofs are shown using refinement in B. Each technique has been implemented into the B model checker, called PRoB, and is shown to be effective through experimentation and evaluation. This research has stim ulated three complementary approaches for improving the generation of state spaces, which are also presented and evaluated. Although this work concerns the context of B and PRoB, the techniques could be generalised to verification tools of other languages.