Deductive Model Checking with Transition Constraint Systems
Dominik Brill
This thesis presents an extension of deductive model checking that uses phase event automata to verify, if a given reactive system satisfies a specification, typically a temporal logic formula. Both the reactive system and the specification are encoded in an initial phase event automaton that is repeatedly refined and transformed until a counterexample computation or a correctness proof is found. Additional heuristics concerning the refinement and transformation rules are used to further improve the model checking algorithm. These heuristics lead to large state-space savings. To preserve full automatism, the specification language is restricted to state safety properties. The use of phase event automata allows the integration of CSP, Object-Z and Duration Calculus into the framework.
Diploma Thesis.