The mOdCL evaluator: Maude + OCL

The mOdCL evaluator is part of an initiative taken at the University of Malaga to provide support to OCL (Object Constraint Language) from Maude. OCL is a part of UML, used to provide textual descriptions to UML models. The use of OCL in the context of UML and in the field of Model-Driven Engineering (MDE ) has originated an increasing interest in tools supporting OCL from several scopes. Maude is a formal language with a wide number of tools to analyze specifications and there are a number of tools and papers proposing the use of Maude as a candidate to deal with UML specifications. In this context, an evaluator of OCL can play a central role. The mOdCL evaluator has been designed to be an evaluator of OCL expressions in general able to be used from others Maude tools which require OCL support. Although it assumes a given representation of the UML model, it basically coincides with the typical representation of UML models in Maude and therefore it can be easily used as an external component from other Maude tools which require an OCL evaluator.

What can mOdCL be used for?

The mOdCL evaluator has already been used either from our team or from external Maude based projects for:

 

Design of mOdCL

The mOdCL evaluator provides OCL syntax to Maude and support the OCL Specification 2.3.1. If you are a basic user of mOdCL you do not need to know about its design and implementation, you only need to know how to represent your UML model as it is assumed by mOdCL (go to the next section to see some examples). However, if you are interested in know more about the mOdCL internals you can get a detailed description here.

We want our tool be as reliable as possible, so that it has been checked be ourselves and by external developers in several situations. Finally we used a complete benchmark provided by Kuhlmann  et al. to perform an exhaustive test of mOdCL. You can get the results of the test here.

An example: The Cinema Model

To provide a basic intuition about the use of mOdCL we will use an UML model for a simple Tickets Sale System, we will show how to represent the model to be used from mOdCL, how to write the OCL constraints included in the class diagram and how to validate them. We will show how to check (statically) if given object diagrams corresponding to concrete system states (snapshots) fulfill the constraints and how to do it dynamically, during the execution of a Maude prototype of the UML model.

The cinema model: static validation

 

The cinema model: dynamic validation

 

More examples

 

 

From UML to mOdCL: A model to model transformation

With the aim of validating systems described by class and sequence diagrams with the mOdCL tool, a tool to generate executable code from UML class and sequence diagrams has been implemented. Model Driven Software Development (MDSD) is the methodology underlying the tool implementation. As UML and Maude have defined their own metamodels (see UML super-structure and Maude metamodel, respectively), the key idea of this work has been to develop a model to model transformation (coded in ATL) with UML as source metamodel and Maude as target metamodel. Once the output Maude model (conforming to Maude metamodel) is generated, it goes under a second transformation in order to generate the Maude code. A model to text transformation, implemented in Acceleo, makes this second transformation. This transformation is basicaly a map between each concept in the metamodel and its keyword in Maude and will not be included in this work.

The model to model mapping is illustrated through four case studies:

A description of the transformation can be found at
   - Verificación dinámica de modelos UML, Antonio Moreno-Delgado, Universidad de Málaga, 2013. PDF

The complete transformation can be downloaded here:


Downloads

 

 

 

free web stats