Formalizing the main characteristics of QVT-based model transformation languages

Model-Driven Development (MDD) aims at developing software more productively by using models as the main artifacts. Here, the models with high abstraction levels must be transformed into lower levels and nally executable models, i.e., source code. As a result, model transformation languages/tools play a main role on realizing the MDD goal. The Object-Management Group (OMG) presented the Query/View/Transformation (QVT) as a standard for the Meta-Object Facility (MOF)-based model transformation languages. However, implementing a model transformation language, which supports the full features of the QVT proposal requires a formal model of the underlying concepts. Having common terminology and a formal, precise, and consistent specication facilitates developing dependable transformation languages/tools. This paper aims to provide a formal specication of the main characteristics of a QVT-Relations (QVTr) model transformation language using the Z notation. The proposed formal model can be adapted for formalizing other domain and language concepts too. To show the applicability of the proposed formalism, a simplied version of the classic object-relational transformation is specied. Additionally, we show how the semantics claries some outstanding semantic issues in QVTr. The proposed formalism of this paper will pave the way to building support tools for model transformations in a unied manner in MDD.