Generating Counterexamples for Model Checking by Transformation

TL;DR

This paper presents a method using program transformation techniques, specifically distillation, to generate counterexamples and witnesses for temporal properties in reactive systems, enhancing model checking verification.

Contribution

It introduces a novel application of program transformation for constructing counterexamples and witnesses, addressing a gap in previous transformation-based verification methods.

Findings

Counterexamples generated for safety and liveness properties.

Application to mutual exclusion systems demonstrating effectiveness.

Supports verification with independently checkable evidence.

Abstract

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.