- Projects
- ATL-Maude
A Rewriting Logic Semantics for ATL
This work aims at providing a formal semantics to the ATL model transformation language, using rewriting logic and its implementation in Maude.
Formal semantics provide precise specifications of the expected behavior of the transformations, which are essential for both model transformations users (to be able to understand them and use them properly) and for tool builders (to develop correct model tranformation engines, optimizers, etc.).
We show how the ATL concepts and mechanisms are represented in Maude. In addition to providing a precise meaning to ATL concepts and behavior (by its interpretation in rewriting logic), this formalization provides additional benefits: the fact that Maude specifications are executable allows users to simulate the ATL programs, and also enables the use of the Maude toolkit to reason about the corresponding specifications. 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.
Resources
Class2Relational example
- A paper with the main ideas of the approach we follow for providing rewriting logic semantics to the ATL language (In Proceedings of the ICMT'10).
- A technical report with an extended version of the paper, that describes the approach with all details.
- The Maude files for executing the examples mentioned in the paper and in the technical report. The Maude files are organized in five folders:
- Files_to_import. Files needed to execute all the transformations. They include, among others, mOdCL and the source and target metamodels. You just need to load in the Maude system the file "LoadMaude.maude", and this file will load the others. Once these files have been loaded in Maude, any of the examples mentioned below can be executed.
- Matched_rules: contains the example of matches rules shown in Section 4.3 of the technical report. It contains six matched rules and the source model of the transformation. To execute it, load it into Maude and type rew ClassModel ..
- Lazy_rules: this folder contains the examples shown in Section 4.5 of the technical report about ATL lazy rules. "Class2RelationalLazyRule.maude" contains the first example and "Class2RelationalLazyRuleCollect.maude" contains the second one. To execute any of them, load it into Maude and type rew ClassModel ..
- Unique_lazy_rule: contains the example shown in Section 4.6 of the technical report with a unique lazy rule and the source model of the transformation. To execute this transformation, load it into Maude and type rew ClassModel ..
- Imperative_section: This folder contains all the definitions for the imperative instructions and all the matched rules that appear in the folder "Matched_rules". Here, one of the rules, MultiValuedClassAttribute2Column, has been extended with an imperative instruction of each type, as can be seen in the Section 4.7 of the technical report. The file also contains the source model of the transformation. To execute the transformation, load the file into Maude and type rew ClassModel ..
JavaSource2Table example
- A paper with the main ideas of the approach we follow for providing rewriting logic semantics to the ATL language (Submitted to the Journal of Object Technology 2010). Available soon.
- A technical report with an extended version of the paper, that describes the approach with all details.
- The Maude files for executing the example in default execution mode shown in the paper and in the technical report. The Maude files are organized in five folders:
- Files_to_import_1. Files needed to execute all the transformations excepting the two showing the use of the lazy and unique lazy rules. They include, among others, mOdCL and the source and target metamodels. You simply need to load in the Maude system the file "LoadMaude.maude", and this file will load the others. Once these files have been loaded in Maude, the examples mentioned below, excepting the last one, can be executed.
- Files_to_import_2. Files needed to execute the transformations to show the behavior of the lazy and unique lazy rules. The files included are the same as before execpting the one with the target model, since in this case a new class has been added, as explained in Section 2.3 of the technical report.
- Declarative_transformation. It contains the example of the declarative transformation shown in Section 4.3 of the technical report. It contains two matched rules, two lazy rules called with a collect construct, two helpers and the source model of the transformation. To execute it, load it into Maude and type rew JavaSource . after having loaded the Files_to_import_1.
- Imperative_section: This folder contains a file with a transformation that contains a matched rule that has been extended with an imperative instruction of each type, as can be seen in the Section 4.5 of the technical report. The file also contains the source model of the transformation. To execute the transformation, load the file into Maude and type rew JavaSource . after having loaded the Files_to_import_1.
- Lazy-UniqueLazy. This folder contains the examples shown in Section 4.4 of the technical report. It contains two transformation, one with a lazy rule and one with an unique lazy rules. The aim of this folder is to show the difference between lazy and unique lazy rules. To execute any of them, load it into Maude and type rew JavaSource . after having loaded the Files_to_import_2.
Public2Private example
- A paper with the main ideas of the approach we follow for providing rewriting logic semantics to the ATL language (Submitted to the Journal of Object Technology 2010). Available soon.
- A technical report with an extended version of the paper, that describes the approach with all details.
- The Maude files for executing the example in refining execution mode shown in the paper and in the technical report. The Maude files are organized in two folders:
- Files_to_import_. Files needed to execute the transformation. You simply need to load in the Maude system the file "LoadMaude.maude", and this file will load the others. Once these files have been loaded in Maude, the transformation can be executed.
- Transformation. It contains the transformation shown in Section 5.1 of the technical report. To execute it, load it into Maude and type rew UMLSimpModel . after having loaded the Files_to_import.
ATL2Maude plugin
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.
Companions
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
Download
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".