A Type-Theoretic Framework for Certified Model Transformations - Formal Methods: Foundations and Applications - page 113

Fig. 1. An overview of model transformation

model-to-model relational approach, which is based on specifying a transforma-
tion as a set of relations (rules) that must hold between source and target model
elements. Languages within this approach are QVT [7] and ATL [8].
There are basically two levels at which the verification of a model transfor-
mation can be exercised: the model and the metamodel levels. Model-level veri-
fication works on specific source and target models related by a transformation.
Verification techniques within this approach are mainly based on model-checking
or simply testing. This approach is in many cases a practical and valuable aid
but it cannot ensure the zero-fault level of quality since it checks a finite num-
ber of specific cases. Furthermore, there exist well-known limitations such as
the state-explosion problem within model checking. An interesting work on the
model-level verification of properties is [9] where the language Alloy is used for
writing declarative model transformations and the Alloy Analyzer tool is used
to conduct fully automated analysis of certain properties with the limitations
mentioned above.
In contrast, metamodel-level verification ensures that a model transformation
respects certain relations between model instances conforming to the source and
target metamodels. This requires the use of formal verification techniques. Works
within this approach are [10,11]. The first one is limited to the verification of
model refinement transformations whereas the second one is restricted to prove
semantic equivalence between source and target models.
We are concerned to metamodel-level verification of model transformations,
considering any kind of transformation and properties .Weexpecttheapproach
to be helpful whenever zero-fault model transformations are required.
We propose the construction of a type-theoretic framework for the certification
of model transformations, representing the schema in Figure 1. In particular, we
explore the idea of using the Calculus of Inductive Constructions (CIC) [12] as a
technical space for dealing with provably correct model transformations. Within
this framework, metamodels MMa and MMb above are represented as inductive
types. On the other hand, each transformation rule of the model transformation
Mt is represented as a logical formula (called TRule )of

form stating that for
every model element satisfying a certain (pre-)condition, there exists a target
model element which stands in the relation specified by the transformation rule
with the source model element.

∀∃