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

A Type-Theoretic Framework for
Certified Model Transformations

Daniel Calegari 1 , Carlos Luna 1 , 2 Nora Szasz 2 ,and Alvaro Tasistro 2

1 Instituto de Computacion, Universidad de la Republica, Uruguay
{ dcalegar,cluna } @fing.edu.uy
2 Facultad de Ingenierıa, Universidad ORT Uruguay
{ luna,szasz,tasistro } @ort.edu.uy

Abstract. We present a framework based on the Calculus of Inductive
Constructions (CIC) and its associated tool the Coq proof assistant to al-
low certification of model transformations in the context of Model-Driven
Engineering (MDE). The approached is based on a semi-automatic trans-
lation process from metamodels, models and transformations of the MDE
technical space into types, propositions and functions of the CIC techni-
cal space. We describe this translation and illustrate its use in a standard
case study.

1 Introduction

Model-Driven Engineering (MDE, [1]) is a software engineering paradigm based
on the specification of models of a system as the primary development activity.
The feasibility of the approach is based on the existence of a semi-automatic
construction process driven by model transformations, starting from abstract
models of the system and transforming them until an executable model is gener-
ated. In consequence, the quality of the whole process strongly depends on the
quality of the model transformations. The highest level of quality is achieved by
proving desired properties of the transformations. Although formal verification
techniques may be expensive, they can be helpful in guaranteeing the correctness
of critical applications where no other verification technique is acceptable. Since
the MDE approach is intended to succeed in a broad spectrum, we think it is
worth exploring how formal verification techniques could be applied within it.
As summarized in Figure 1, a model transformation takes as input a model
Ma conforming to a given source metamodel MMa and produces as output an-
other model Mb conforming to a given target metamodel MMb . The model
transformation can be defined as well as a model Mt which itself conforms to
a model transformation metamodel MMt . There are well known metamodeling
languages like the MOF [2] and KM3 [3]. In some cases, there are conditions
(called invariants) that cannot be captured by the structural rules of these lan-
guages, in which case modeling languages are supplemented with another logical
language, e.g. the Object Constraint Language (OCL) [4]. There are different
model transformation approaches, as described in [5,6]. In our case we select a