In recent years, the profound impact of the Model Driven Architecture (MDA)
proposal [1], promoted by the OMG as architecture for software development, has meant that the model transformation becomes a very active research and development direction. Within this scope, OMG also published the QVT standard [2], a language for the specication of model transformations within the MDA scope. Since transformations guide the whole software development cycle, it is crucial to oer a precise and rigorous infrastructure, in order to help to verify and guarantee correctness of them. However, current implementations of transformations languages lack this necessary mathematical underpinning.
The aim of this short paper is: on the one hand, to show how a rigorous approach based on algebraic specication and rewriting logic [3] can oer a suitable framework for model transformations; and on the other hand, to show how proving theoretical properties of transformations is possible if the transformation language or tool has a mathematical underpinning [4]. Maude [5] is the formal language used in this work. To illustrate this approach, the formal specications of two metamodels, and a transformation between them, have been created.
The main idea of this work is to specify metamodels through OO Maude modules, and the transformation rules as rewriting rules that rewrite source model Partially nanced by the Spanish Ministry of Science and Technology, project DEDALO (Development of Quality Systems based on Models and Requirements) TIN2006-15175-C05-03 elements (represented as terms) into other target model elements. In this section, as well as explaining the main principles of this approach, we will illustrate it by means of an example of transformation from UML Class diagram to a RDBMS diagram (extracted from [2]).
In QVT, model transformations are dened in terms of metamodels, existing source and target metamodels. Metamodel elements will be specied in Maude by means of the object oriented modules of Maude. Figure 1 summarizes the elements that make up the approach. This Figure shows the OMG standards' elements, the Maude elements and the relationship between them. Analogously, the textual description of the simple RDBMS metamodel (taken from annex A of [2]) will be formalized in Maude.
In this subsection, we analyze briey the basis of QVT Relations and how to formalize them by means of the strengths oered by Maude.
On the one hand, a transformation is expressed in QVT Relations by means of relations between metamodel elements. A relation declares constraints that must be satised by the two or more metamodels (or domains) that participate in the relation. Each domain establishes a pattern that must be matched with the candidate models in order to execute the transformation, known as object template expressions that are directly expressed in Maude, since this language oers pattern-matching in the simplication of terms. Regarding the specication of QVT transformations in Maude, they can be specied as rewriting rules that change and create the elements of the target model. Finally, constraints over the candidate models will be specied as conditions in the rewriting rules.
The main advantage of the use of this approach over other non-formal transformation techniques is that some applications can be carried out only dening Maude to infer if two particular models are equivalent using these rules.
If we dene a RDBMS model that is equivalent to the one in Figure 2, Figure 3 (c) shows the Maude command that checks this equivalence. We ask Maude if it is possible to obtain the RDBMSdiagram model from the UMLdiagram model using the specied rules. This execution will nd a solution since the models are equivalent.
The research presented shows the feasibility of integrating formal techniques with current software engineering standards (MDA-QVT). This approach may be particularly useful in model-driven engineering processes to develop critical or error-prone high quality systems. The metamodel specications made in this approach oer a powerful way to verify type properties and the correctness of the models without losing the legibility and practicality of other transformation languages. Furthermore, in the formal framework proposed the transformations are represented as mathematical entities and we can take advantage of all the power of mathematical inference mechanisms. This allows us to infer information and to prove properties of the transformations.