M2FOL: A Formal Modeling Language for Metamodels.

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. In this paper we build on the widely accepted approach of logic as basis for modeling languages and define them as languages in the sense of typed predicate logic comprising a signature $$\varSigma $$ and a set of constraints. We concretize how the basic concepts of a language – object and relation types, attributes, inheritance and constraints – can be expressed in logical terms. This naturally leads to the denotation of a model as $$\varSigma $$ -structure satisfying all constraints. We apply this definition also on the metalevel and propose a formal modeling language to specify metamodels called M2FOL. A thus formalized metamodel then rigorously defines the signature of a language and we provide an algorithmic derivation of the formal modeling language from the metamodel. The effectiveness of our approach is demonstrated by formalizing the Petri Net modeling language, a method frequently used for analysis and simulation in enterprise modeling.