Information Technology Reference
In-Depth Information
The correctness of the model transformation is stated as the following logical
formula.
Ma:MMa. (Pre(Ma) →∀ Mb:MMb. (TRules(Ma,Mb) Post(Ma,Mb)))
where Pre is a translation of the source invariants, TRules is the conjunction of
the transformation rules, and Post is a translation of the target invariants plus
any other desired property to be proved. A proof of this formula ensures that the
transformation rules satisfy the target invariants as well as the desired properties.
We propose a semi-automatic translation process from the MDE technical space
-used by developers- to the CIC technical space -used for formal verification.
The choice of the CIC is dictated by its very considerable expressive power as
well as by the fact that it is supported by a tool of industrial strength, namely
the Coq proof assistant [13]. As one example of its applicability, Coq has been
used for the development and formal verification of a compiler of a large subset
of the C programming language [14].
The idea of using type theory in the context of MDE has been formulated be-
fore by Poernomo in [15,16]. He formulates a type theory of his own -a variant of
Martin-Lof's constructive type theory- and outlines a method for representing
MOF models as types. Then, he follows the classical approach in type theory
where pre- and post-conditions are represented as types, and a program (trans-
formation) is derived as a function between those types. Our work differs in
the representation of metamodels as will be explained later. Another important
difference is that he performs program derivation to obtain a transformation
whereas we translate a given transformation as a formula and verify this trans-
lation with respect to certain pre- and post-conditions. Finally, we base our
proposal on an existent type theory with its corresponding supporting verifica-
tion tool, which allows us to put into practice the ideas presented, unlike the
works in [15,16].
As compared to previous work by the authors, the representation of model
transformations described here differs substantially from the one presented in
[17], as will be explained later.
The remainder of the paper is structured as follows. We first describe our
framework in Section 2. In Section 3 we give some details about the formal
representation of models and metamodels, and about model transformations in
Section 4. Then, in Section 5 we explain how properties are verified. Finally, in
Section 6 we present a short summary with concluding remarks and an outline
of further work.
2 Outline of the Approach
We use the Calculus of Inductive Constructions (CIC) as a technical space for
dealing with provably correct model transformations. In the following sections
the CIC is introduced and our framework is outlined, using a running example.
 
Search WWH ::




Custom Search