Generating Counterexamples for Model Checking by Transformation

G. W. Hamilton
(School of Computing, Dublin City University, Republic of Ireland)

Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking as a verification technique. Furthermore, when model checking does succeed in verifying a property, there is typically no independently checkable witness that can be used as evidence for the verified property. Previously, we have shown how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. However, no counterexamples or witnesses were generated using the described techniques. In this paper, we address this issue. In particular, we show how the program transformation technique distillation can be used to facilitate the construction of counterexamples and witnesses for temporal properties of reactive systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with counterexamples being generated for those properties which do not hold.

In Geoff Hamilton, Alexei Lisitsa and Andrei P. Nemytykh: Proceedings of the Fourth International Workshop on Verification and Program Transformation (VPT 2016), Eindhoven, The Netherlands, 2nd April 2016, Electronic Proceedings in Theoretical Computer Science 216, pp. 65–82.
Published: 6th July 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: