Formalizing the four-layer metamodeling stack with METAMORPH: potential and benefits

Enterprise modeling deals with the increasing complexity of processes and systems by operationalizing model content and by linking complementary models and languages, thus amplifying the model value beyond mere comprehensible pictures. To enable this amplification and turn models into computer-processable structures, a comprehensive formalization is needed. This paper presents the formalism METAMORPH based on typed first-order logic and provides a perspective on the potential and benefits of formalization that arise for a variety of research issues in conceptual modeling. METAMORPH defines modeling languages as formal languages with a signature Σ—comprising object types, relation types, and attributes through types and function symbols—and a set of constraints. Four case studies are included to show the effectiveness of this approach. Applying the METAMORPH formalism to the next level in the hierarchy of models, we create M2FOL, a formal modeling language for metamodels. We show that M2FOL is self-describing and therefore complete the formalization of the full four-layer metamodeling stack. On the basis of our generic formalism applicable to arbitrary modeling languages, we examine four current research topics—modeling with power types, language interleaving & consistency, operations on models, and automatic translation of formalizations to platform-specific code—and how to approach them with the METAMORPH formalism. This shows that the rich knowledge stack on formal languages in logic offers new tools for old problems.