Formalizing Conceptual Modeling Methods with MetaMorph

Models evolved from mere pictures supporting human understanding to sophisticated knowledge structures processable by machines. This entails an inevitable need for computer-understandable models and languages and causes formalization to be a crucial part in the lifecycle of a modeling method. An appropriate formalism must be a means for providing a unique, unambiguous but implementation-independent way of specifying arbitrary modeling languages and for this purpose must be generic and open to capture any domain and any functionality. In this paper we give a pervasive description of the formalism MetaMorph based on predicate logic – an approach fulfilling these requirements. This is done with an extensive proof-of-concept case illustrating the application of the formalism concept by concept. For the case study we use the modeling language ProVis from the domain of stochastic education. The language ProVis comprises only few objects and relation types but with high interconnection and therefore appears as a interesting specimen for formalization and showing the feasibility of the demonstrated approach.