Towards a Base Model for UML and OCL Verification.
Frank Hilken, Philipp Niemann, Robert Wille, Martin Gogolla · 2014
Abstract. Modelling languages such as UML and OCL are more and more used in early stages of system design. These languages offer a huge set of constructs. As a consequence, existing verification engines only support a restricted subset of them. In this work, we propose an ap-proach using model transformations to unify different description means within a so called base model. In the course of this transformation, com-plex language constructs are expressed with a small subset of so-called core elements. This simplification enables to interface with a wide range of verification engines with complementary strengths and weaknesses. Our aim is that, guided by a structural analysis of the base model, the developer can choose the most promising verification engine. 1