This paper shows a rigorous approach based on algebraic specications and rewriting logic which makes up for the lack of current transformation languages and oers a balanced rigour-versus-intuition framework for model transformation, focusing on the MDA-QVT standards. To illustrate this approach, an example and some formal applications of these specications are sketched.
In recent years, the profound impact of the Model Driven Architecture (MDA)
proposal [
The aim of this short paper is: on the one hand, to show how a rigorous
approach based on algebraic specication and rewriting logic [
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.
The rst metamodel specied is the so-called simple UML metamodel (taken
from annex A of [
Analogously, the textual description of the simple RDBMS metamodel (taken
from annex A of [
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.
In this section, we will study the transformation from UML diagrams to RDBMS
diagrams (taken from [
Package to Schema relation transforms a package of a UML diagram into a schema of a relational data base diagram. Figure 3 shows this relation expressed in QVT (a) and how it is specied in Maude (b). In this relation, the object template expression can be directly expressed in Maude. The pattern matching binds the variable pn to a specic value that is used to create a new object which represents a schema in the target model. On the other hand, since a model is represented by means of objects in Maude, we have to use object identiers in the rules. In the righthand side of the rule appears both the object of the source model and the new object in the target model. Finally, once we have specied the metamodels and the QVT Relations in Maude, we can execute the transformation over any UML model. 3
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 the rewriting rules. The application shown checks if two models are semantically equivalent. In general, various models are semantically equivalent if they have similar meaning. Being more precise, in this work we consider that two models are semantically equivalent if they hold all the equivalence relationships (dened by means of QVT Relations) which, depending on the metamodels, express the semantics equivalence of concepts as dened by the analyst. In this way, if the (a) top relation PackageToSchema { pn: String; checkonly domain uml p:Package {name=pn}; enforce domain rdbms s:Schema {name=pn}; } (b) rl [PackageToSchema] : < packageOid(p:String) : Package | domain : "uml", name : pn:String,...> => < packageOid(p:String) : Package | domain : "uml", name : pn:String,...> < schemaOid(p:String) : Schema | domain : "rdbms", name : pn:String > . (c) (search UMLdiagram =>! C:Configuration C2:Configuration
such that (C:Configuration := RDBMSdiagram) .) semantic equivalence between two models is expressed as a relation, we can use 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. 4
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.