Dynamic validation of maude prototypes of UML models

Abstract

We propose an approach for the validation of UML models annotated with OCL constraints. Specifically, we provide support for dynamically validating class invariants and operation pre/post conditions during the execution of prototypes automatically obtained from UML diagrams. The supported UML models specify both static and dynamic aspects, specifically, we focus on class and sequence diagrams. The proposal is based on Maude: UML models and OCL expressions are represented as Maude specifications, which allows us to evaluate OCL expressions on UML models by term rewriting. A model transformation allows us to accomplish this transformation automatically, and represents a first step towards the integration of the proposed facilities into development environments. The Maude specifications thus obtained can be seen as high-level executable prototypes of the annotated UML models. © 2014 Springer-Verlag Berlin Heidelberg.