Formalizing the Four-layer Metamodeling Stack -- Potential and Benefits

TL;DR

This paper introduces a formal first-order logic-based framework for enterprise modeling, formalizes the four-layer metamodeling stack, and demonstrates its potential to enhance model consistency, translation, and operations.

Contribution

It presents a generic formalism for modeling languages, introduces M2FOL for metamodels, and shows how this formalism benefits research in model interleaving, consistency, and automation.

Findings

M2FOL is a self-describing formal modeling language.

The formalism effectively supports model consistency and translation.

The approach enhances the formalization of the four-layer metamodeling stack.

Abstract

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 a generic formalism based on typed first-order logic and provides a perspective on the potential and benefits arising for a variety of research issues in conceptual modeling. We define modeling languages as formal languages with a signature $\Sigma$ - comprising object types, relation types, and attributes through types and function symbols - and a set of constraints. Three cases studies are included to show the effectiveness of the approach. Applying the 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 three current research topics - language interleaving & consistency, operations on models, and automatic translation of formalizations to platform-specific code - and how to approach them with the proposed formalism. This shows that the rich knowledge stack on formal languages in logic offers new tools for old problems.