A Formal Foundation for Metamodeling

The concept of formal metamodel will contribute significantly to the core principles of the OMG Model Driven Architecture (MDA). The OMG standard for metamodeling is the Meta Object Facility (MOF) meta-metamodel that defines a common way for capturing the diversity of modeling standards and interchange constructs that are used in MDA. A combination of UML (Unified Modeling Language), OCL (Object Constraint Language) and natural language is used to describe the abstract syntax and semantics of MOF. In this paper, we propose an algebraic formalization of MOF metamodels. We describe how to translate MOF metamodels into algebraic specifications. As an example, we describe a formalization of the core of the Query, View, Transformation (QVT) metamodel, the OMG standard for expressing transformations. The goal of this formalization is, on the one hand, to reason about ambiguity and consistency of metamodels and, on the other hand, to support tests and proof's in model transformations.