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. © 2014 Springer International Publishing.
Meller, Y., Grumberg, O., & Yorav, K. (2014). Verifying behavioral UML systems via CEGAR. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8739 LNCS, pp. 139–154). Springer Verlag. https://doi.org/10.1007/978-3-319-10181-1_9