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 speci cation facilitates developing dependable transformation languages/tools. This paper aims to provide a formal speci cation 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 simpli ed version of the classic object-relational transformation is speci ed. Additionally, we show how the semantics clari es 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 uni ed manner in MDD.