# M2FOL: A Formal Modeling Language for Metamodels

Victoria Döller

► To cite this version:

Victoria Döller. M2FOL: A Formal Modeling Language for Metamodels. 13th IFIP WG 8.1 Working Conference on the Practice of Enterprise Modeling (PoEM 2020), Nov 2020, Riga, Latvia. pp.109-123, 10.1007/978-3-030-63479-7_8 . hal-03434665

HAL Id: hal-03434665

https://inria.hal.science/hal-03434665

Submitted on 18 Nov 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
M2FOL: A Formal Modeling Language for
Metamodels

Victoria Döller[0000-0002-5770-635X]

Research Group Knowledge Engineering,
Faculty of Computer Science,
University of Vienna, Vienna, Austria
victoria.doeller@univie.ac.at

**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. 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 $Σ$ 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 $Σ$-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.

**Keywords:** Conceptual Modeling, Metamodel, Modeling Language, Formal Language, Predicate Logic

# 1 Introduction

Enterprise modeling has proven instrumental in facing the challenges of increasing complexity and interdependences of processes and systems in the modern world. Research on enterprise modeling has enhanced modeling languages from mere instruments for pictures supporting human understanding to highly specialized tools with value adding mechanisms like information querying, simulation, and transformation [2] [14]. The nature of models has evolved from a visual representation of information to an exploitable knowledge structure [5]. Nevertheless the European enterprise modeling community experiences that the potential of enterprise modeling is currently not fully utilized in practice and modeling is
employed only by a limited group of experts, therefore in [34] and [35] a re-
search agenda is formulated to establish “modeling for the masses” (MftM) and
broadcast its benefits also to non-experts.

Although the initiators of the MftM movement mention that the formality of
model representation possibly hampers understandability, we argue that the idea
behind MftM nevertheless requires an investigation of the formal foundations of
models and languages. This is for three reasons: 1) According to the *stakeholder
dimension* of challenges in enterprise modeling research [34, S.234] computers
also have to be seen as stakeholders producing and consuming models. To make
models computer-processable they have to be formalized as computers do not un-
derstand semi-formal or unstructured models and language specifications [3]. 2)
The vision of models being not autotelic but *being a means to the operationaliza-
tion of information* [34, S.229] calls for value-adding functionality beyond mere
graphics like reasoning, verification & validation or simulation, which is formu-
lated ideally computer-understandably and implementation-independently, i.e.
formalized. 3) The vision of *local modeling practices which are globally integra-
tive* [34, S.229] calls for a common foundation of what models and modeling
languages are to enable the linking and merging of models in different domains
with different semantics [18].

Formalization is also essential in the light of the emergent importance of
domain specific modeling languages (DSMLs) [13] as well as an increasing agility
in the advancement and extension of established languages and methods [21].
The lack of a common way for formalizing DSMLs leads to divergent formal
foundations limiting the opportunities to compare or link models. Frequently
the big standards are extended for a specific domain, e.g. the extension of i*
with security concepts constituting the modeling language Secure Tropos [28]
[33]. Therefore a common way of specifying the base languages as well as the
extensions or modules is required. A silo like formalization of the big standards
is not sufficient as this impedes a mutual interconnection and integration by
divergent base concepts of models and different underlying formal structures.

Another important building block for advancing the science of conceptual
modeling is an exact and commonly applied method for specifying modeling
languages. A survey conducted by Bork et al. showed that the specification doc-
uments of the standardized languages like UML and ArchiMate diverge in the
concepts they consider as well as in the techniques they use to specify their vi-
sual metamodels [4]. Examples from recent scientific publications indicate that
also in research on domain specific languages no common practice of metamodel
specification is in use. Several contributions specify metamodels with UML class
diagrams, declaring object types as classes and relation types as classes or named
association arrows, e.g. [32] [36] [37]. Others simply define the object and rela-
tion types with box-and-line models devoid of an underlying language and rely
on the intuitive understanding of the reader, e.g. [26] [30]. This shows that al-
though metamodels are models themselves and therefore subject of interest for
enterprise modeling research no language for metamodels has been established
metamodel, itself a graph [20]. Using this formalism the authors define a self-descriptive metametamodel and deduce a domain specific language to specify metamodels. This approach puts an emphasis on the graph-like box-and-line structure of models, rather than on the linguistic aspects.

The FDMM formalism introduced by Fill et al. uses set theory to specify metamodels and models [12]. The authors explicitly aim at an formalization of metamodels realized with the metamodeling platform ADOxx [1] and do not claim to be applicable for platform-independent specifications. Neither set theory, basis of FDMM, nor graph theory, basis of KM3, provides a canonical concept for instantiation, an essential characteristic of modeling languages. Therefore the technique and semantics of this instantiation relation between model and metamodel has to be constructed ad-hoc and lacks the beneficial knowledge stack of established mathematical theories.

Formal languages as defined in mathematical logic inherently comprise the concept of instantiation as interpretation of the signature in logical terms, and they provide a rich knowledge about their properties. Therefore, in current research the notion of modeling languages as formal languages in the sense of mathematical logic is receiving increasing attention [8] [15] [29] [31] [40]. In his work on the theory of conceptual models Thalheim describes modeling languages as based on a signature $\Sigma$ comprising a set of postulates, i.e. sentences expressed with elements of $\Sigma$ [40]. Models are defined as language structures satisfying the postulates, which canonically corresponds to the concept of instantiation of a metamodel. This generic description does not restrict itself to a single type of logic. Consequently it does not provide a specification of the mapping of the formal signature to the modeling language concepts like object or relation types.

In their investigation of formal foundations of domain-specific languages Jackson and Sztipanovits introduce typed predicate logic to handle object types in models [19]. In contrast to Thalheim, they do not adopt the concept of a language structure for model instances, but rather consider a model to be a set of valid statements about the model. This is also true for Telos [24], which builds on the premise that the concepts of entities and links are omitted and replaced by propositions constituting the knowledge base. The choice of typed first-order logic for the formalization of these propositions is natural and explained in great detail in [25]. Similar to Jackson and Sztipanovits knowledge is represented solely as a set of sentences in the formal language. In our approach on the other hand we do not adopt the transformation of models into propositions but rather directly deal with the ubiquitous concepts of objects and relations and an instantiation hierarchy between models and metamodels. This leads to a different view on models. In the attempts above a model is constituted by statements, whereas in our approach a model is any language interpretation not explicitly excluded by the statements constraining valid models.

Guizzardi builds a theory of ontologically-driven conceptual modeling based on modal logic and develops in several contributions a comprehensive formal system for conceptualizations of domains as basis for truthful modeling languages, e.g. [16] [17]. In this advanced theory, fruitful for the objective of an ontology-
based, domain-faithful grounding for modeling languages, these languages as well as models and metamodels are a-posteriori concepts implicitly obtained from ontological considerations. In the paper at hand we do not restrict to ontology-driven conceptual modeling and approach models and languages as the a-priori concepts.

Summarizing we conclude, that formal languages in logic prove to be suitable for the intended formalism, as the structure of modeling languages including its linguistic character can be grounded in concepts of formal languages. Therefore, in the work at hand we propose a formal definition of modeling languages in which we concretely point out the modeling concepts and their formal equivalent in logical terms with prospect of successive elaboration. This paper extends our prior work in [10].

## 3 Definition of Formal Modeling Languages

The intended definition shall serve as a cornerstone for a common way of specifying modeling languages, which thereby become comparable, reusable and modulizable. A formal definition for modeling languages in general enables an investigation of common features of the resulting subclass of formal languages as well as a sound mathematical foundation for their functionality. Therefore, we adopt the core concepts of modeling languages identified in [23] – object and relation types, attributes, inheritance and constraints – to be the basic constituents of formal modeling languages.

We use typed (also called sorted) predicate logic in this approach. The mathematical basics can be found in textbooks on logic or mathematics for computer science, e.g. [11] [27]. Some remarks on notation: To ease the differentiation between language and model level, we use capital letters for the symbols of the former and lowercase letters for the elements of the latter.

**Definition 1.** A (formal) modeling language $\mathcal{L}$ consists of a typed signature $\Sigma = \{S, \mathcal{F}, \mathcal{R}, \mathcal{C}\}$ and a set $\mathcal{C}$ of sentences in $\mathcal{L}$ for the constraints, where:

- $S$ is a set of types, which can be further divided into three disjoint subsets $S_O, S_R$, and $S_D$ for object types, relation types and data types;

- the type set $S_O$ is strictly partially ordered with order relation $<_O \subset S_O \times S_O$ to indicate the inheritance relation between the corresponding object types;

- $\mathcal{F}$ is a set of typed function symbols such that:

- for each relation type $\mathbf{R}$ in $S_R$ there exist two function symbols $F_s^\mathbf{R}$ and $F_t^\mathbf{R}$ with domain type $\mathbf{R} \in S_R$ and codomain type $\mathbf{O}_s, \mathbf{O}_t \in S_O$ assigning the source and target object types to a relation;

- for each single-value attribute $\mathbf{A}$ of an object or relation type $\mathbf{T}$ there exists a function symbol $F^\mathbf{A}$ with domain type $\mathbf{T}$ and codomain type an element in $S_D \cup S_O \cup S_R$ assigning the data type or referenced object type or relation type to an attribute;

- $\mathcal{R}$ is a set of typed relation symbols;
- C is a set of typed constants to specify the possible values $c_i$ of type $T \in S_D$ of the attributes;

- the set $C$ is a set of sentences in $\mathcal{L}$ constraining the possible models, also called the postulates of the language.

This definition explicates the specification of the essential modeling concepts of a language, i.e. object types and inheritance, binary directed relation types and single value attributes. Note that the definition does not prohibit the existence of additional symbols in the signature, so broader concepts like n-ary relations or multi-value attributes can optionally be included and are topic of further investigation. Also structures beyond the visual elements of a model can be included, e.g. paths as transitive relations or substructures comprising several elements.

We want to point out, that relation types are defined on the same level as object types, not subordinate to them. This highlights their significance for a model beyond mere arrows and allows for defining attributes of relations, multiple relations of the same type between the same two objects, as well as for inheritance of relation types.

With the data types and constants we can define attribute domains like integers via specifying a type called $\mathbb{N}$ and constant symbols 0,1,2,3, ... in $C$ of type $\mathbb{N}$ for the numbers, or enumeration lists like a person's gender via specifying a type called *gender* and constant symbols *male*, *female*, and *else* in $C$.

**Definition 2.** A model $\mathcal{M}$ of a language $\mathcal{L}$ with typed signature $\Sigma = \{S, \mathcal{F}, \mathcal{R}, C\}$ is an $\mathcal{L}$-structure conforming to the language constraints $C$, i.e. $\mathcal{M}$ consists of

- a universe $\mathcal{U}$ of typed elements respecting the type hierarchy, that is

- for each $T$ in $S$ there exists a set $U_T \subset \mathcal{U}$ and $\mathcal{U} = \bigcup_{T \in S} U_T$;

- all sets $U_T$ have to be pairwise disjoint except for sets $U_{O_1}$ and $U_{O_2}$ with $O_1, O_2 \in S_O$ where $O_1 <_O O_2$. In this case $U_{O_1}$ must be a subset of $U_{O_2}$, i.e. $U_{O_1} \subseteq U_{O_2}$;

- an interpretation of the function symbols in $\mathcal{L}$, i.e. for each function symbol $F \in \mathcal{F}$ with domain type $T_1...T_n$ and codomain type $T$ a function $f: U_{T_1} \times ... \times U_{T_n} \rightarrow U_T$;

- an interpretation of the relation symbols in $\mathcal{L}$, i.e. for each relation symbol $R \in \mathcal{R}$ with domain type $T_1...T_m$ a relation $r \subset U_{T_1} \times ... \times U_{T_m}$;

- for each $T \in S_D$ and constant $C \in C$ of type $T$ an interpretation $c \in U_T$;

- for each constraint $\phi$ in $C$ the model $\mathcal{M}$ satisfies $\phi$, i.e. $\mathcal{M} \models \phi$.

This definition of models as language structures goes beyond a visualisation and considers models as knowledge structures as described in [5]. Thereby we overcome several shortcomings of graphical representations, like the missing depiction of attributes and their domains in models or the visual mixing of the metarelation inheritance with the definition of relation types in metamodels.

We will now illustrate the definition on the example of the Petri Net modeling language. For the visualization of the metamodel we use the notation of CoChaCo, a method to support the creative process of modeling method design
<figure><img src="image_2.png" /><figcaption>Fig. 1. Notation excerpt of the CoChaCo Method [22]</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2. A metamodel of Petri Nets</figcaption></figure>

[22]. This method comprises concrete syntax for most of the concepts contained in M2FOL with a slightly different naming, see Figure 1.

Example 1. The Petri Net Modeling Language PN

The Petri Net metamodel depicted in Figure 2 comprises three object types **Node**, **Place** and **Transition** constituting $S_O$. Thereby **Place** and **Transition** inherit from **Node**, i.e. **Place** `<_O** **Node**` and **Transition** `<_O** **Node**`. Furthermore, the language comprises only one relation type **Arc** element of $S_R$. For the attribute **Tokens** of object type **Place** we need a type $\mathbb{N}$ with the usual addition + and order relation `<_N` as well as constants in $C = \{0, 1, 2, ...\}$ all of type $\mathbb{N}$. The set $S$ of types is then the union $S = S_O \cup S_R \cup S_D = \{\mathbf{Node}, \mathbf{Place}, \mathbf{Transition}, \mathbf{Arc}, \mathbb{N}\}$. For the relation **Arc** we have to specify the source and target object types by introducing two function symbols $F_s^{\text{Arc}}$ and $F_t^{\text{Arc}}$ both with domain **Arc** and codomain **Node**. For the attribute **Tokens** we introduce a function symbol $F^{\text{Tokens}}$ with domain **Place** and codomain $\mathbb{N}$ assigning each place instance a number of tokens. Finally we have to define the constraints of the language. These rules are not contained in a graphical metamodel, but usually specified in an additional source like OCL or simply stated in natural language. In the predicative formalization they are an integral part of the language. Following four sentences written in the alphabet of $PN$ ensure **Node** to be abstract, i.e. any element in **Node** lies either in **Place** or in **Transition** (1), as well as the alternation of types of the elements connected by an arc (2, 3) and the prohibition of multiple arcs between the same two elements (4). For ease of readability we abuse the notation $\forall x \in \mathbf{T}$ for $x$ being of type $\mathbf{T}$ instead of using the type specific quantifier $\forall_{\mathbf{T}} x$.

$$ \forall x \in \mathbf{Node} \ \exists y \in \mathbf{Place}, z \in \mathbf{Transition} \ (x = y \lor x = z) \quad (1) $$

$$ \exists x, y \in \mathbf{Place}, u \in \mathbf{Arc} \ (F_s^{\text{Arc}}(u) = x \land F_t^{\text{Arc}}(u) = y) \quad (2) $$

$$ \exists x, y \in \mathbf{Transition}, u \in \mathbf{Arc} \ (F_s^{\text{Arc}}(u) = x \land F_t^{\text{Arc}}(u) = y) \quad (3) $$

$$ \forall u, v \in \mathbf{Arc} \ (F_s^{\text{Arc}}(u) = F_s^{\text{Arc}}(v) \land F_t^{\text{Arc}}(u) = F_t^{\text{Arc}}(v) \implies u = v) \quad (4) $$
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** A Petri Net model depicting a simple barber shop scenario</figcaption></figure>

*Example 2.* A Petri Net Model

A Petri Net model depicting a simple barber shop scenario is shown in Figure 3. Its formalization, i.e. the corresponding *PN*-structure, looks as follows: The universe of places $\mathcal{U}_P$ contains three elements $\mathcal{U}_P = \{\mathbf{w}(ait), \mathbf{b}(usy), \mathbf{i}(dle)\}$. The universe of transitions $\mathcal{U}_T$ comprises three elements $\mathcal{U}_T = \{\mathbf{e}(nter), \mathbf{s}(erve), \mathbf{d}(one)\}$. Six arc elements exist in $\mathcal{U}_A = \{\mathbf{a}_1, \mathbf{a}_2, \mathbf{a}_3, \mathbf{a}_4, \mathbf{a}_5, \mathbf{a}_6\}$ with source and target $f_s^{Arc}(\mathbf{a}_1) = \mathbf{e}, f_t^{Arc}(\mathbf{a}_1) = \mathbf{w}, f_s^{Arc}(\mathbf{a}_2) = \mathbf{w}, f_t^{Arc}(\mathbf{a}_2) = \mathbf{s}, f_s^{Arc}(\mathbf{a}_3) = \mathbf{s}, f_t^{Arc}(\mathbf{a}_3) = \mathbf{b}, f_s^{Arc}(\mathbf{a}_4) = \mathbf{b}, f_t^{Arc}(\mathbf{a}_4) = \mathbf{d}, f_s^{Arc}(\mathbf{a}_5) = \mathbf{d}, f_t^{Arc}(\mathbf{a}_5) = \mathbf{i}, f_s^{Arc}(\mathbf{a}_6) = \mathbf{i}, \text{ and } f_t^{Arc}(\mathbf{a}_6) = \mathbf{s}$. For the attribute type and values the natural numbers $\mathbb{N}$ are included in the model, $\mathcal{U}_{\mathbb{N}} = \{0, 1, 2, ...\}$. The instantiation of the attribute *Tokens* looks as follows: $f^{Tokens}(\mathbf{w}) = 2, f^{Tokens}(\mathbf{b}) = 0$ and $f^{Tokens}(\mathbf{i}) = 1$. We can easily check that the formalized model satisfies all pos- tulates 1–4 of the language *PN*.

# 4 M2FOL – MetaModel 2 First Order Logic
## A Formal Modeling Language for Metamodels

According to the principle of metaization [38] metamodels are models themselves conforming to a metamodeling language which is itself a modeling language, see Figure 4. We propose a formal modeling language in the sense of Definition 1 for metamodels. This language is capable of describing exactly the concepts explicated in Definition 1.

We stick to the notational convention of capital letters for elements on the language level and lowercase letters for elements on the model level. To indicate the metalevel of M2FOL and metamodels we use the typewriter font for meta symbols and elements. For ease of readability we write $F: X \rightarrow Y$ when F is a function with domain type X and codomain type Y. Nevertheless, the instanti- ation is then a function $f: \mathcal{U}_X \rightarrow \mathcal{U}_Y$ defined on universes of typed elements.
To be consistent in the naming of the symbols in M2FOL we distinguish between an attribute type on meta level and an attribute as the concrete assignment of a value to an element on model level.

With M2FOL we want to model **object types** and **inheritance relations** between them, **relation types** connected to their *from* and *to* object types, **attribute types** and their **data types** and possible **data**. According to Definition 1 all the bold concepts constitute a type in $S_O$ in M2FOL, whereas all italic concepts make up a type in $S_R$ in M2FOL. The types *inheritance*, *from*, and *to*, furthermore require assignment functions for source and target specification. Data types and data are necessary for defining attribute domains and its values, e.g. the domain $N_{0..10}$ and values $\{0, 1, 2, ..., 9, 10\}$ or an enumeration list domain *gender* with values *male*, *female*, *else*. Attribute types need the assignment of owning type and value domain.

**Fig. 4.** The metamodeling hierarchy according to Strahringer [38]

<figure><img src="image_5.png" /></figure>

**Definition 3.** The metalanguage M2FOL is a modeling language with signature $\Sigma = \{S, \mathcal{F}, \mathcal{R}, C\}$ with the set of types split in $S = S_O \cup S_R \cup S_D$, where:

- $S_O$ consists of the types *O(object)* *T(type)*, *R(elation)* *T(type)*, *A(ttribute)* *T(type)*, *D(ata)* *T(type)*, and *D(ata)*: $S_O = \{OT, RT, AT, DT, D\}$;

- $S_R$ consists of the types *Inh(eritance)*, *Fr(om)*, and *To*: $S_R = \{Inh, Fr, To\}$;

- $S_D$ is empty;

- the set of function symbols consists of following nine elements:

- two symbols $F_s^{Inh}$ and $F_t^{Inh}$ assigning source and target to *Inh*-typed relations: $F_s^{Inh}: Inh \to OT, F_t^{Inh}: Inh \to OT$;

- two symbols $F_s^{Fr}$ and $F_t^{Fr}$ assigning source and target to *Fr*-typed relations: $F_s^{Fr}: Fr \to RT, F_t^{Fr}: Fr \to OT$;

- two symbols $F_s^{To}$ and $F_t^{To}$ assigning source and target to *To*-typed relations: $F_s^{To}: To \to RT, F_t^{To}: To \to OT$;

- two symbols $F_{val}$ and $F_{type}$ assigning to an attribute type its value domain and the object or relation type it belongs to. The value assignment can be a reference or a simple value: $F_{val}: AT \to DT \cup OT \cup RT, F_{type}: AT \to OT \cup RT$;

- a symbol $F_{DT}$ to assign a data type to a data element: $F_{DT}: D \to DT$;

- $\mathcal{R}$ consists of a symbol $<_{OT}$ transitively extending the inheritance relation given by *Inh* to a strict partial order on the set of object types: $\mathcal{R} = \{<_{OT} \subset OT \times OT\}$.
The postulates of the language (for brevity we mostly use the abbreviation xry for relation r of type T, x being $F_s^T(r)$ and y being $F_t^T(r)$):

$$ \forall x, y, z \in OT, v, w \in \mathbf{Inh} \ (xvy, xwz \implies y = z \land v = w) \quad (5) $$

$$ \forall x, y \in OT, u \in \mathbf{Inh} \ (xuy \implies x <_{OT} y) \quad (6) $$

$$ \forall x, y \in OT \exists z \in OT, u \in \mathbf{Inh} \ (x <_{OT} y \implies xuy \lor (xuz \land z <_{OT} y)) \quad (7) $$

$$ \forall x \in RT \exists y, z \in OT, u \in Fr, v \in To \ (xuy \land xvz) \quad (8) $$

$$ \mathbb{1}[u, v \in Fr] (F_s^{Fr}(u) = F_s^{Fr}(v) \land u \neq v) \quad (9) $$

$$ \mathbb{1}[u, v \in To] (F_s^{To}(u) = F_s^{To}(v) \land u \neq v) \quad (10) $$

For $<_{OT}$ we furthermore require to be a strict partial order, i.e. $<_{OT}$ is transitive, irreflexive and antisymmetric.

The constraints ensure single inheritance (5), $<_{OT}$ being the transitive closure of $\mathbf{Inh}$ under the assumption that $\mathcal{U}_{\mathbf{0T}}$ is finite (6–7), and the existence and uniqueness of to and from objects of a relation (8-10). The absence of cyclic inheritance and self-inheritance follow from the properties of $<_{OT}$.

With this language we now can transfer the graphical metamodel of Figure 2 to a formal M2FOL-model.

### Example 3. The Petri Net Metamodel $M_{NP}$

The universe of object types $\mathcal{U}_{\mathbf{0T}}$ comprises three elements n(ode), p(lace), and tr(ansition). The universe of relation types $\mathcal{U}_{RT}$ contains one element a(rc). One element tok(ens) is contained in the universe of attribute types $\mathcal{U}_{AT}$. The universe $\mathcal{U}_{\mathbf{Inh}}$ contains the instantiation relations p\_n between p and n as well as tr\_n between tr and n. $\mathcal{U}_{Fr}$ contains the relation a\_from of the source element assignment to the relation type a. $\mathcal{U}_{To}$ contains the relation a\_to of the target element assignment to the relation type a. For these four elements the corresponding source and target elements have to be assigned: $f_s^{\mathbf{Inh}}(p\_n) = p$, $f_t^{\mathbf{Inh}}(p\_n) = n$, $f_s^{\mathbf{Inh}}(tr\_n) = tr$, $f_t^{\mathbf{Inh}}(tr\_n) = n$, $f_s^{\mathbf{Fr}}(a\_from) = a$, $f_t^{\mathbf{Fr}}(a\_from) = n$, $f_s^{\mathbf{To}}(a\_to) = a$, $f_t^{\mathbf{To}}(a\_to) = n$. From $\mathbf{Inh}$ the transitive order relation $<_{\mathbf{0T}}$ is deduced: $<_{\mathbf{0T}} = \{(p, n), (tr, n)\}$. Furthermore there are data values $\{0, 1, 2, ...\}$ in $\mathcal{U}_{\mathbf{D}}$ all of type $\mathbb{N} \in \mathcal{U}_{\mathbf{DT}}$, $f_{DT}(i) = \mathbb{N} \forall i \in \mathcal{U}_{\mathbf{D}}$. These are needed for the value domain of the attribute type tok, an attribute assigned to p: $f_{type}(tok) = p$, $f_{val}(tok) = \mathbb{N}$. In short this can be written as following:

$$ \mathcal{U}_{\mathbf{0T}} = \{n(ode), p(lace), tr(ansition)\}, \mathcal{U}_{RT} = \{a(rc)\}, \mathcal{U}_{AT} = \{tok(en)\}, \quad (11) $$

$$ \mathcal{U}_{\mathbf{Inh}} = \{p\_n, tr\_n\}, \mathcal{U}_{Fr} = \{a\_from\}, \mathcal{U}_{To} = \{a\_to\} \quad (12) $$

$$ \mathcal{U}_{DT} = \{\mathbb{N}\}, \mathcal{U}_{\mathbf{D}} = \{0, 1, 2, ...\}, <_{\mathbf{0T}} = \{(p, n), (tr, n)\} \quad (13) $$

$$ f_s^{\mathbf{Inh}}(p\_n) = p, f_t^{\mathbf{Inh}}(p\_n) = n, f_s^{\mathbf{Inh}}(tr\_n) = tr, f_t^{\mathbf{Inh}}(tr\_n) = n, \quad (14) $$

$$ f_s^{\mathbf{Fr}}(a\_from) = a, f_t^{\mathbf{Fr}}(a\_from) = n, f_s^{\mathbf{To}}(a\_to) = a, f_t^{\mathbf{To}}(a\_to) = n, \quad (15) $$

$$ f_{type}(tok) = p, f_{val}(tok) = \mathbb{N}, f_{DT}(i) = \mathbb{N} \forall i \in \mathcal{U}_{\mathbf{D}} \quad (16) $$

This formal metamodel $M_{NP}$ conforms to all constraints 5-10 and describes the formal language $\mathcal{NP}$ introduced in Example 1. Their subordination prompts a
generic procedure on how to deduce the latter one from the former one. In Table 1 we present this procedure as an algorithm.

<table><caption>**Table 1.** Algorithm to deduce a formal modeling language signature from its M2FOL metamodel specification</caption><thead><tr><th></th><th>M2FOL (Meta)Model to Language-Signature</th><th>Mapping</th></tr></thead><tbody><tr><td>1.</td><td>Each metamodel element o in the set U<sub>0T</sub> defines an object type O of the language. The inheritance relation &lt;<sub>0T</sub>&subset; U<sub>0T</sub> &times; U<sub>0T</sub> must be adopted to the types.</td><td>o &isin; U<sub>0T</sub> &mapsto; O &isin; S<sub>O</sub></td></tr><tr><td>2.</td><td>Each metamodel element r in the set U<sub>RT</sub> defines a relation type R of the language.</td><td>r &isin; U<sub>RT</sub> &mapsto; R &isin; S<sub>R</sub></td></tr><tr><td>3.</td><td>For each relation type r &isin; U<sub>RT</sub> there exist an element s of type From and an element t of type To and both relation elements have as source element r, f<sub>s</sub><sup>Fr</sup>(s) = r, f<sub>s</sub><sup>Fr</sup>(t) = r. The assignment f<sub>s</sub><sup>To</sup>(s) = o<sub>s</sub> indicates the source object type of R, f<sub>s</sub><sup>To</sup>(t) = o<sub>t</sub> indicates the target object type of R.</td><td>r, s, o<sub>s</sub> &mapsto; F<sub>s</sub><sup>RI</sup>: R &rarr; O<sub>s</sub>; r, t, o<sub>t</sub> &mapsto; F<sub>t</sub><sup>RI</sup>: R &rarr; O<sub>t</sub></td></tr><tr><td>4.</td><td>Each metamodel element dt in U<sub>DT</sub> defines a data type DT of the language. Each metamodel element d in U<sub>D</sub> with f<sub>DT</sub>(d) = dt becomes a constant symbol C<sub>d</sub> in C of type DT.</td><td>dt &isin; U<sub>DT</sub> &mapsto; DT &isin; S<sub>D</sub>; d &isin; U<sub>D</sub> &mapsto; C<sub>d</sub> &isin; C</td></tr><tr><td>5.</td><td>Each metamodel element a in the set U<sub>AT</sub> defines a function symbol F<sup>a</sup> of the language. The object or relation type a belongs to, i.e. the domain of F<sup>a</sup>, is given by the assignment f<sub>type</sub>(a) = t<sub>ty</sub> &isin; U<sub>0T</sub> &cup; U<sub>RT</sub>, its value range, i.e. codomain, by f<sub>val</sub>(a) = t<sub>v</sub> &isin; U<sub>0T</sub> &cup; U<sub>RT</sub> &cup; U<sub>DT</sub></td><td>a, t<sub>ty</sub>, t<sub>v</sub> &mapsto; F<sup>a</sup>: T<sub>ty</sub> &rarr; T<sub>v</sub></td></tr><tr><td>6.</td><td>The constraints of the language have to be added manually, because this information is not determined by the metamodel.</td><td></td></tr></tbody></table>

Finally we take the meta-perspective on M2FOL. Its graphical metamodel is depicted in Figure 5 and contains five objects of type `OT={ot, rt, at, dt, d}`, three objects of type `RT={inh, fr, to}`, three objects of type `AT={value_domain, assigned_to, assigned_domain}`, three relations of type `From={source_inh, source_to, source_fr}`, and three relations of type `To={target_inh, target_to, target_fr}`, furthermore 18 assignments of source and target objects, attribute owning types and attribute value types. On the one hand it is itself a model conforming to the language M2FOL, to be precise the graphical representation thereof. On the other hand this metamodel describes M2FOL and with the algorithm presented above we deduce Definition 3. So we conclude that the proposed modeling language for metamodels M2FOL is self-describing and thereby complete the formalization of the full modeling stack.
<figure><img src="image_6.png" /><figcaption>Fig. 5. The metamodel of M2FOL</figcaption></figure>

# 5 Conclusion and Outlook

In this paper we presented a definition of modeling languages as formal languages $\mathcal{L}$ with a signature $\Sigma$ in the sense of logic. The concept of a $\mathcal{L}$-structure canonically corresponds to the instantiation relation between model and language and led us to the definition of models as $\mathcal{L}$-structures. To illustrate the specification of formal modeling languages we demonstrated the definition on the Petri Net modeling language. We applied the definition also on the meta level and developed M2FOL – a formal modeling language for metamodels. M2FOL models are precise and complete and therefore we were able to show how to algorithmically derive a formal modeling language signature from its metamodel. M2FOL is self-descriptive, which can be seen by applying the algorithm to its own metamodel.

This work investigates the theoretical foundations of conceptual modeling. For a practical application of the formalism a suitable tool for transforming graphical metamodels into formal ones can be developed. This formal specification of a language, precise enough to be processed by a machine yet platform-independent, additionally allows us to develop platform-specific translators, transferring the single source of language specification to realizations on different platforms.

With this common practice of defining metamodels and modeling languages these languages become comparable, reusable, and open to modularization. To broaden the conceptual capabilities of our approach we will further investigate more subtle concepts to be integrated into the definition. These are for example multi-value attributes, the concepts of mixins and extenders for modular metamodels as proposed in [41], or the structural types of relations identified in [39]. Furthermore, we intend to investigate formal modeling languages $\mathcal{L}$ beyond their syntax and approach also their functionality by describing domain events on models, like firing a transition in a Petri Net, as transitions between $\mathcal{L}$-structures.

Finally, by using a sophisticated mathematical theory as grounding for the definition of modeling languages we can use this knowledge stack as resource
to further establish a formal foundation for modeling languages and approach old problems with new tools. One issue currently under research is the process of language interleaving, which is highly relevant for ensuring consistency of the same information captured in models of different languages or model types. Connecting formal languages is a well researched topic in mathematical logic and provides methods which are now also applicable to modeling languages.

## References

1. BOC: ADOxx Metamodelling Platform (2020), https://www.adoxx.org

2. Bork, D., Buchmann, R.A., Karagiannis, D., Lee, M., Miron, E.T.: An Open Platform for Modeling Method Conceptualization: The OMiLAB Digital Ecosystem. Communications of the Association for Information Systems 44(1), 673–679 (2019)

3. Bork, D., Fill, H.G.: Formal Aspects of Enterprise Modeling Methods: A Comparison Framework. In: 47th Hawaii International Conference on System Sciences. pp. 3400–3409 (jan 2014)

4. Bork, D., Karagiannis, D., Pittl, B.: A survey of modeling language specification techniques. Information Systems 87, 101425 (jan 2020)

5. Buchmann, R.A., Ghiran, A.M., Döller, V., Karagiannis, D.: Conceptual Modeling Education as a “Design Problem”. Complex Systems Informatics and Modeling Quarterly (21), 21–33 (dec 2019)

6. Choe, Y., Lee, S., Lee, M.: SAVE: An Environment for Visual Specification and Verification of IoT. In: IEEE 20th International Enterprise Distributed Object Computing Workshop, EDOCW. pp. 269–276 (2016)

7. Clyde, S.W., Embley, D.W., Liddle, S.W., Woodfield, S.N.: OSM-Logic: A Fact-Oriented, Time-Dependent Formalization of Object-oriented Systems Modeling. In: Conceptual Modelling and Its Theoretical Foundations, pp. 151–172. Springer, Berlin, Heidelberg (2012)

8. Delcambre, L.M.L., Liddle, S.W., Pastor, O., Storey, V.C.: A reference framework for conceptual modeling. In: Trujillo, J.C., Davis, K.C., Du, X., Li, Z., Ling, T.W., Li, G., Lee, M.L. (eds.) Conceptual Modeling. ER 2018. Lecture Notes in Computer Science. vol. 11157 LNCS, pp. 27–42. Springer International Publishing, Cham (2018)

9. Delcambre, L.M.L., Liddle, S.W., Pastor, O., Storey, V.C.: Characterizing Conceptual Modeling Research. In: Panetto, H., Debruyne, C., Hepp, M., Lewis, D., Ardagna, C.A., Meersman, R. (eds.) On the Move to Meaningful Internet Systems: OTM 2019 Conferences. pp. 40–57. Springer International Publishing, Cham (2019)

10. Döller, V.: Formal semantics for conceptual modeling languages based on model theory. In: Proceedings of the Doctoral Consortium Papers Presented at the 11th IFIP WG 8.1 Working Conference on the Practice of Enterprise Modelling, PoEM 2018. vol. 2234, pp. 61–73. CEUR-WS (2018)

11. Enderton, H.B.: A Mathematical Introduction To Logic. Harcourt/Academic Press, San Diego, 2nd edn. (2001)

12. Fill, H.G., Redmond, T., Karagiannis, D.: FDMM: A formalism for describing ADOxx meta models and models. In: ICEIS 2012 - Proceedings of the 14th International Conference on Enterprise Information Systems. vol. 3, pp. 133–144 (2012)

13. Frank, U.: Domain-specific modeling languages: Requirements analysis and design guidelines. In: Reinhartz-Berger, I., Sturm, A., Clark, T., Cohen, S., Bettin, J. (eds.) Domain Engineering: Product Lines, Languages, and Conceptual Models, pp. 133–157. Springer Berlin Heidelberg (2013)
14. Frank, U., Strecker, S., Fettke, P., Vom Brocke, J., Becker, J., Sinz, E.: The research field "modeling business information systems": Current challenges and elements of a future research agenda. Business and Information Systems Engineering **6**, 39–43 (2014)

15. Guarino, N., Guizzardi, G., Mylopoulos, J.: On the Philosophical Foundations of Conceptual Models. In: Proceedings of the 29th International Conference on Information Modelling and Knowledge Bases, EJC 2019. Frontiers in Artificial Intelligence and Applications, vol. 321, pp. 1–15. IOS Press (2019)

16. Guizzardi, G.: On ontology, ontologies, conceptualizations, modeling languages, and (meta)models. In: Vasilecas, O., Eder, J., Caplinskas, A. (eds.) Selected Papers from the Seventh International Baltic Conference, DB&IS. pp. 18–39. IOS Press (2007)

17. Guizzardi, G.: Logical, ontological and cognitive aspects of object types and cross-world identity with applications to the theory of conceptual spaces. In: Applications Of Conceptual Spaces: The Case For Geometric Knowledge Representation, pp. 165–186. Springer International Publishing (jan 2015)

18. Herrmann, C., Krahn, H., Rumpe, B., Schindler, M., Völkel, S.: An algebraic view on the semantics of model composition. In: Model Driven Architecture-Foundations and Applications (ECMDA-FA). pp. 99–113. Springer (2007)

19. Jackson, E., Sztipanovits, J.: Towards a Formal Foundation for Domain Specific Modeling Languages. In: Proceedings of the 6th ACM & IEEE International Conference on Embedded Software. pp. 53–62. EMSOFT ’06, ACM, New York, NY, USA (2006)

20. Jouault, F., Bézivin, J.: KM3: a DSL for Metamodel Specification. In: International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2006. pp. 171–185. Springer, Berlin, Heidelberg (2006)

21. Karagiannis, D.: Conceptual modelling methods: The AMME agile engineering approach. In: Informatics in Economy. IE 2016. Lecture Notes in Business Information Processing. vol. 273, pp. 3–19. Springer Verlag (2018)

22. Karagiannis, D., Burzynski, P., Utz, W., Buchmann, R.A.: A Metamodeling Approach to Support the Engineering of Modeling Method Requirements. In: 27th IEEE International Requirements Engineering Conference. pp. 199–210 (2019)

23. Kern, H., Hummel, A., Kühne, S.: Towards a comparative analysis of metamodels. In: Proceedings of the compilation of the co-located workshops on DSM’11, TMC’11, AGERE! 2011, AOOPES’11, NEAT’11, & VMIL’11. pp. 7–12. ACM (2011)

24. Koubarakis, M., Borgida, A., Constantopoulos, P., Doerr, M., Jarke, M., Jeusfeld, M.A., Mylopoulos, J., Plexousakis, D.: A retrospective on Telos as a metamodeling language for requirements engineering. Requirements Engineering (2020)

25. Koubarakis, M., Mylopoulos, J., Stanley, M., Borgida, A.: Telos: features and formalization. Tech. rep., Technical report KRRTR-89-4, Department of Computer Science, University of Toronto (1989)

26. Lara, P., Sánchez, M., Villalobos, J.: Bridging the IT and OT worlds using an extensible modeling language. In: Conceptual Modeling. ER 2016. Lecture Notes in Computer Science. vol. 9974, pp. 122–129. Springer, Cham (nov 2016)

27. Mazzola, G., Milmeister, G., Weissmann, J.: Comprehensive mathematics for computer scientists 1: Sets and numbers, graphs and algebra, logic and machines, linear geometry (second edition). Springer Berlin Heidelberg (2006)

28. Mouratidis, H., Giorgini, P.: Secure Tropos: A security-oriented extension of the Tropos methodology. In: International Journal of Software Engineering and Knowl-
edge Engineering. vol. 17, pp. 285–309. World Scientific Publishing Company (apr 2007)

29. Olivé, A.: Conceptual modeling of information systems. Springer-Verlag, Berlin Heidelberg (2007)

30. Paczona, M., Mayr, H.C.: Model-Driven Mechatronic System Development. In: IEEE 15th International Conference on Automation Science and Engineering (CASE). pp. 1730–1736. IEEE (aug 2019)

31. Partridge, C., Gonzalez-Perez, C., Henderson-Sellers, B.: Are conceptual models concept models? In: Conceptual Modeling. ER 2013. Lecture Notes in Computer Science. vol. 8217, pp. 96–105. Springer, Berlin, Heidelberg (nov 2013)

32. Ralyté, J., Léonard, M.: Evolution Models for Information Systems Evolution Steering. In: Poels, G., Gailly, F., Serral Asensio, E., Snoeck, M. (eds.) The Practice of Enterprise Modeling, PoEM 2017. pp. 221–235. Springer International Publishing, Cham (2017)

33. Rrenja, A., Matulevičius, R.: Pattern-based security requirements derivation from secure tropos models. In: Ralyté, J., España, S., Pastor, O. (eds.) The Practice of Enterprise Modeling. PoEM 2015. vol. 235, pp. 59–74. Springer Verlag (2015)

34. Sandkuhl, K., Fill, H.G., Hoppenbrouwers, S., Krogstie, J., Leue, A., Matthes, F., Opdahl, A.L., Schwabe, G., Uludag, Ö., Winter, R.: Enterprise modelling for the masses – From elitist discipline to common practice. In: Horkoff, J., Jeusfeld, M., Persson, A. (eds.) The Practice of Enterprise Modeling. PoEM 2016. vol. 267, pp. 225–240. Springer Verlag (2016)

35. Sandkuhl, K., Fill, H.G., Hoppenbrouwers, S., Krogstie, J., Matthes, F., Opdahl, A., Schwabe, G., Uludag, Ö., Winter, R.: From Expert Discipline to Common Practice: A Vision and Research Agenda for Extending the Reach of Enterprise Modeling. Business and Information Systems Engineering **60**, 69–80 (2018)

36. Schön, H., Zdravkovic, J., Stirna, J., Strahringer, S.: A role-based capability modeling approach for adaptive information systems. In: Gordijn, J., Guédria, W., Proper, H. (eds.) The Practice of Enterprise Modeling. PoEM 2019. vol. 369, pp. 68–82. Springer (nov 2019)

37. Stirna, J., Zdravkovic, J., Grabis, J., Sandkuhl, K.: Development of Capability Driven Development Methodology: Experiences and Recommendations. In: Poels, G., Gailly, F., Serral Asensio, E., Snoeck, M. (eds.) The Practice of Enterprise Modeling, PoEM 2017. pp. 251–266. Springer International Publishing, Cham (2017)

38. Strahringer, S.: Zum Begriff des Metamodells. Schriften zur Qualitativen Betriebswirtschaftslehre, Techn. Hochsch., Inst. für Betriebswirtschaftslehre (1995)

39. Thalheim, B.: Towards a theory of conceptual modelling. In: Conceptual Modeling. ER 2009. Lecture Notes in Computer Science. vol. 5833 LNCS, pp. 45–54. Springer, Berlin, Heidelberg (2009)

40. Thalheim, B.: The Theory of Conceptual Models, the Theory of Conceptual Modelling and Foundations of Conceptual Modelling. In: Handbook of Conceptual Modelling, pp. 543–577. Springer Berlin Heidelberg (2011)

41. Zivkovic, S., Karagiannis, D.: Mixins and Extenders for Modular Metamodel Customisation. In: Proceedings of the 18th International Conference on Enterprise Information Systems. vol. 1, pp. 259–270. SCITEPRESS - Science and Technology Publications (2016)