Model-Driven Engineering (MDE) promotes models as first class citizens of the software development process.
Models are manipulated through model transformations (MTs), which is considered to be the "¯heart and soul" of MDE [1].
Dedicated languages based on different paradigms emerged naturally during the last decade, to express MTs.
Since they are executed on a family of conforming models, the validity of such model transformations becomes a crucial issue.
From the MDE point of view, a transformation has a dual nature [2]: seen as a transformation model,
a transformation can denote a computation, whose expression relies on a particular model of computation (MOC)
embedded in a transformation language; and seen as a model transformation, emphasis focuses on the particular
artefacts manipulated by a transformation (namely, metamodels for its specification and models for its execution).
The computational nature will require that the underlying language ensures desirable properties
(like termination and determinism) needed for the purpose of the transformations, independently of
what a particular transformation expresses. On the other hand, manipulating models implies that specific
properties of interest will be directly related to the involved models as well as the intrinsic intention
behind the transformation: e.g., one may be interested in always producing conform models by construction,
or ensuring that target models still conserve their semantics.
Some work has already been produced on the testing of Model Transformations.
Despite the fact that testing Model Transformations is still a relatively young research domain,
the challenges are by now well understood.
However, the verification of Model Transformations by applying manual or automated proof techniques
is still far from being understood. Despite the fact that scattered work exists in the domain,
only recently in an attempt has been made at providing a taxonomy for such proof techniques.
The classification provided in the Volt paper refers to a
sample of publications in the domain is based on three dimensions: the type of transformation considered,
the properties being proved; and the applied proof technique.
Finding the right "values" (classes of equivalence) for transformations, properties and proof techniques
has to be done both in isolation for each of those dimensions,
but also (and possibly more importantly), considering their interactions.
The three dimensions explored in [cite VOLT paper here] imply three binary relations:
transformation / property, transformation / proof technique and property / proof technique.
We think exploring these relations will be helpful in coming up with a table for helping engineers
choosing what properties should be proved for a given model transformation, using which technique.
The property / proof technique relation is the best understood.
This is not surprising as the properties and their associated proof techniques are often borrowed
from program or model verification, which is a field that is by now relatively well understood.
However, both the transformation / property and the transformation / proof technique relations are poorly understood.
This seems to be due to the fact despite existing classifications of model transformations [cite Mens, Czarnecki],
additional work still needs to be done on the granularity of the classification of the intention behind a model
transformation. Intention is important especially regarding the transformation / property relation because
properties to be proved encode at a meta level the intention of the transformation.
The transformation / proof technique relation is also poorly understood, although it seems to be that the
paradigm used by the model transformation language (purely declarative, purely imperative, or hybrid)
is the most determinant aspect for choosing a given Model Tranformation verification technique.
It would seems however that if a property is identified for a given Model Transformation,
that could be more determinant for finding the adequate proof technique than the transformation type.
On the other hand, from the three individual dimensions it would seem that the properties one is the least understood.
Properties of the transformation computations themselves such as termination or confluence are of importance,
but they do not address the meaning of a model transformation. Unlike tranditional computations,
the meaning of model transformations is heavily dependent on the input and output languages (or metamodels),
given those languages have their own meaning. In the Volt paper two types of properties regarding the meaning of
a transformation were identified: model syntax relations and model semantics relations.
While the former relate the input and output models of a given transformation via their syntax
(classes, relations and their instances), the latter relate the meaning of the input and output models
of a transformations, by establishing relations between the elements of the explicit semantics of those models.
Juergen Dingel has proposed an encompassing theory to present both these kind of properties uniformly
(as well as hybrids of the two), but additional work to build his theory needs to be done.
To conclude I propose working on better understanding the nature of the verification of model transformations.
Assuming we would depart from the three dimentions (transformation / property / proof technique) it would be
important to indentify classes of equivalence of transformations regarding their semantics,
equivalence classes (e.c.) of properties for model transformations, the relation between e.c. of transformations and e.c.
of properties, and finally the relation between e.c. and transformations and e.c. of proof techniques.
[1] S.Sendall and W.Kozaczynski, Model Transformation:
The Heart And Soul Of Model-Driven Software Development,¯ IEEE Software, vol. 20, no. 5, pp. 42 -- 45, 2003.
[2] J. Bezivin, F. Buttner, M. Gogolla, F. Jouault, I. Kurtev, and A. Lindow,
"Model Transformations? Transformation Models!" in MODELS, 2006.
