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

Fig. 2. An outline of our approach
The first step of the process is the formalization of the KM3 source and target
metamodels as inductive types ( MMa and MMb ). Then, every ATL transformation
rule is transformed into a logical proposition involving both the source and target
metamodels ( TRules ). The third step is the translation of every OCL invariant
into a logical proposition. Source invariants are taken as pre-conditions ( Pre )
of the model transformation. Target invariants and the desired properties of the
transformation are taken as post-conditions ( Post ), which will be our proof goals.
Finally, the verification is interactively performed in Coq by proving the post-
conditions assuming that both the pre-conditions and the transformation rules
hold. Additionally, the verifier can use the full expressiveness of Coq in order to
include post-conditions that cannot be, or are not suitable to be, expressed in
OCL.
2.3 A Running Example
We will illustrate our proposal by using an example based on a simplified ver-
sion of the well-known Class to Relational model transformation [19]. Figure 3
shows both metamodels of this transformation. An UML class diagram consists
of classes which contain one or more attributes. Each attribute has a type that
is a primitive datatype. Every class, attribute and primitive data type is gene-
ralized into an abstract UML model element which contains a name and a kind
(persistent or not persistent). On the other side, a RDBMS model consists of
tables which contains one or more columns. Each column has a type, and every
RDBMS model element is generalized into an abstract RDBMS model element.
The transformation describes how persistent classes of a simple UML class
diagram are mapped to tables of a RDBMS model with the same name and
kind. Attributes of the persistent class map to columns of the table. The type
of the column is a string representation of the primitive data type associated to
the attribute.
This example is clearly not a critical application where our approach is par-
ticularly helpful. However, it is complete and simple enough to exemplify out
approach, and has been used as a standard test case for various transformation