Verifying Behavioral UML Systems via CEGAR

This work presents a novel approach for applying abstraction and refinement in the verification of behavioral UML models.

The

Unified Modeling Language

(UML) is a widely accepted modeling language for embedded and safety critical systems. As such the correct behavior of systems represented as UML models is crucial.

Model checking

is a successful automated verification technique for checking whether a system satisfies a desired property. Nevertheless, its applicability is often impeded by its high time and memory requirements. A successful approach to avoiding this limitation is

CounterExample-Guided Abstraction-Refinement (CEGAR)

. We propose a CEGAR-like approach for UML systems. We present a model-to-model transformation that generates an

abstract

UML system

from a given concrete one, and formally prove that our transformation creates an

over-approximation

.

The abstract system is often much smaller, thus model checking is easier. Because the abstraction creates an over-approximation we are guaranteed that if the abstract model satisfies the property then so does the concrete one. If not, we check whether the resulting abstract counterexample is

spurious

. In case it is, we automatically

refine

the abstract system, in order to obtain a more precise abstraction.