Verifying Networks of Phase Event Automata
Walid Haddad
There is a growing interest in research related to presenting correct and efficient model checking approaches for complex computing systems. Abstraction model checking is one example which proved its success as a model checking approach for infinite-state systems.
In this thesis, we present an approach for translating CSP-OZ-DC specifications into transition constraint systems (as a part of a model checking approach for infinite-state systems). In previous works, the CSP-OZ-DC specifications are translated into phase event automata, then, the product of the phase event automata is translated into a transition constraint system.
For large specifications, the obtained transition constraint system can result in a large number of transitions. In our approach, we provide an improved representation of transition constraint systems consisting of a notably lower number of transitions in the transition constraint system with the aim of achieving faster model checking for available model-checkers.
Master Thesis.