Main Page/Resources/Atl2Maude

From Atenea

Jump to: navigation, search



The ATL2Maude plugin enables the automatic generation of specifications and execution of ATL transformations.

Model transformations (MT) are at the heart of Model-Driven Engineering, and provide the essential mechanisms for manipulating and transforming models. As the complexity of model transformations grows, the need to count on formal semantics of MT languages also increases. Formal semantics provide precise specifications of the expected behavior of the transformations which allow to reason about them and prove their correctness. This is specially important in case of large and complex MTs (with, e.g., hundreds or thousands of rules) for which manual debugging is no longer possible.

ATL is one of the most popular and widely used model transformation languages. The ATL language has been normally described in an intuitive and informal manner, by means of definitions of its main features in natural language. However, this lack of rigorous description can easily lead to imprecisions and misunderstandings that might hinder the proper usage and analysis of the language, and the development of correct and interoperable tools.

We have used Maude for giving semantics to ATL. The use of Maude as a target semantic domain brings interesting benefits, because it enables the simulation of the ATL specifications and its formal analysis.

Encoding ATL in Maude

To give a formal semantics to ATL using rewriting logic, we provide a representation of ATL constructs and behavior in Maude. We start by defining how the models and metamodels handled by ATL can be encoded in Maude, and then provide the semantics of matched rules, lazy rules, unique lazy rules, helpers and imperative sections.

This encoding is systematic and we have automated it using ATL transformations (between the ATL and Maude metamodels).

Modeling ATL rules

Each ATL rule is represented by a Maude rewrite rule that describes how the target model elements are created from the source model elements identified in the left-hand side of the rule (that represents the “to” pattern of the ATL rule). The general form of such rewrite rules is as follows:


The two sides of the Maude rule contain the three models that capture the state of the transformation (see 4.1): the source, the trace and the target models.1 The rule specifies how the state of the ATL model transformation changes as result of such rule.

The triggering of Maude and ATL rules is similar: a rule is triggered if the pattern specified by the rule is found, and the guard condition holds. In addition to the specific rule conditions, in the Maude representation we also check (alreadyExecuted) that the same ATL rule has not been triggered with the same elements.

As an example, consider the following rule:


The encoding in Maude of such a rule is as follows:


This rule is applied over instances of class DataType, as specified in the left hand side of the Maude rule. The rule guard guarantees that the rule has not been already applied over the same elements. The guard is also used to define some variables used by the rule (CLASSMODEL@, TR@ and T@).

After the application of the rule, the state of the system is changed: the source model is left unmodified (ATL does not allow modifying the source models); a new trace (TR@) is added to the trace model; the value of the counter object is updated; and a new element (T@) is created in the target model. We allow the evaluation of OCL expressions using mOdCL by enclosing them in double angle brackets (<< ... >>).

Further details can be found in our paper at the ICMT 2010. You can cite that paper as: J. Troya, A. Vallecillo. "Towards a Rewriting Logic Semantics for ATL"‎. In Proceedings of the Third International Conference on Model Transformation (ICMT 2010), LNCS, Málaga, Spain, June 28 - 29, 2010.


Hints and Tips

  • The current plugin version only works with one source model.
  • The input and output model names in the ATL transformation must match up with these in the model file.
  • mOdCL does not support for OrderedSet collections
  • Collections must be merged through the union collections operator

Known Bugs


The current version of ATL2Maude has been tested for Windows XP, Windows Vista, Windows 7 and Linux (in its Guadalinex distribution). It requires Maude 2.4 official site or see our local mirror for Maude . Once Maude 2.4 is installed on your computer, choose any of the following options to install the ATL2Maude tool.

To make this version of Eclipse work properly in Windows 7, it has to be run using the compatibility mode. To activate this option, right click on the eclipse.exe and select the compatibility mode.


Please note that the Windows version in the picture shown is in Spanish.

ATL2Maude plugin

To install ATL2Maude, extract files from ATL2Maude(1.0.0).zip to your Eclipse Ganymede (3.4.2) configuration plugin folder. Before running ATL2Maude the first time, Maude has to be configured. Go to "Windows->Preference...Maude" and set the "Maude binary file" option to the corresponding file, and assign a folder to store the "Temporal files".

Eclipse bundle for Windows

A full Eclipse configuration which includes the ATL2Maude tool can be dowloaded from here. Before running ATL2Maude the first time, Maude has to be configured. Go to "Windows->Preference...Maude" and set the "Maude binary file" option to the corresponding file, and assign a folder to store the "Temporal files".

Maude local mirror

Maude 2.4 for Windows mirror

Maude 2.4 for Linux mirror


Personal tools