An Automated Approach for the Interpretation of Counter-Examples

Model checking is an automatic technique used for the verification of finite systems. A model checker explores the full state space of a given model and checks it against a set of requirements. If a state exists in which a requirement is not satisfied most tools will generate a counter-example. Counter-examples are useful for debugging a model and determining if an error exists in the modelled system. However, they can be difficult for end users to understand and this may limit the take-up of model checking in industry.This paper describes a domain-specific approach to automatically interpreting counter-examples and presenting the results in an intuitive form to the end user. Our research extends previous work on model checking railway signalling control tables with signalling engineers from Queensland Rail.