Model checking is a technique for finding errors in systems and algorithms. The technique 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 contributions 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 identifying symmetries via graph isomorphism. Soundness proofs arc 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 stimulated 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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:485295 |
| Date | January 2007 |
| Creators | Turner, Edward Nanakorn |
| Publisher | University of Southampton |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0022 seconds