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 finally 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 specification facilitates developing dependable transformation languages/tools.This paper aims to provide a formal specification 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 simplified version of the classic object-relational transformation is specified. Additionally, we show how the semantics clarifies 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 unified manner in MDD.