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 |