From UML/OCL to base models: Transformation concepts for generic validation and verification

Abstract

Modeling languages such as UML and OCL find more and more application in the early stages of today’s system design. Validation and verification, i.e. checking the correctness of the respective models, gains interest. Since these languages offer various description means and a huge set of constructs, existing approaches for this purpose only support a restricted subset of constructs and often focus on dedicated description means as well as verification tasks. To overcome this, we follow the idea of using model transformations to unify different description means to a base model. In the course of these transformation, complex language constructs are expressed by means of a small subset of so-called core elements in order to interface with a wide range of verification engines with complementary strengths and weaknesses. In this paper, we provide a detailed introduction of the proposed base model and its core elements as well as corresponding model transformations.