1 Introduction
1.1 A need for formalization
1.2 Goal and requirements
M2FOL
, a formal modeling language for metamodels. With M2FOL
, we are capable of modeling the syntax of a language to be specified, to be more precise, the signature of the language according to the definition. The paper at hand extends the presented definition of formal modeling languages as well as the language M2FOL
with the concept of multi-value attributes. We furthermore exemplify the potential and benefits inherent to the proposed formalism on a diverse range of research topics and demonstrate the opportunities this integrative foundation offers.M2FOL
—a formal modeling language for metamodels—and outline its self-describing character. Given a metamodel specified with M2FOL
we show how to algorithmically deduce the signature of the corresponding modeling language. After that we give in Sect. 5 an outlook to the potential and benefits of formal modeling languages. We present some ongoing research and approaches on modeling with power types, on how to interleave modeling languages, formally include operations on models into the language specification, and on the use of the formalization as a single point of specification processable by machines. In Sect. 6, we discuss the formalism with respect to the formulated goals and requirements and outline the agenda of the empirical evaluation that is currently being conducted.2 Background and related work
2.1 Formalism vs. formal syntax
2.2 Formalisms for concrete modeling languages
2.3 Formalisms for ontologies and concept spaces
2.4 Formalisms for languages
2.5 Formalisms based on logic
3 The MetaMorph formalism: defining formal modeling languages
3.1 A definition based on predicate logic
-
\({\mathcal {S}}\) is a set of types, which can be further divided into three disjoint subsets \({\mathcal {S}}_O\), \({\mathcal {S}}_R\), and \({\mathcal {S}}_D\) for object types, relation types and data types;
-
the type set \({\mathcal {S}}_O\) is strictly partially ordered with order relation \(<_O \subseteq {\mathcal {S}}_O \times {\mathcal {S}}_O\) to indicate the specialization relation between the corresponding object types;
-
the type set \({\mathcal {S}}_D\) can contain simple types \(\mathbf{T }\) for value domains of single-value attributes, or product types \(\mathbf{T }'= \mathbf{T }_1\times \mathbf{T }_2 \times \cdots \times \mathbf{T }_n\) and unions thereof for value domains of n-ary multi-value attributes \((n>1)\), where the ith value is of type \(\mathbf{T }_i \in {\mathcal {S}}_D \cup {\mathcal {S}}_O \cup {\mathcal {S}}_R \);
-
-
\({\mathcal {F}}\) is a set of typed function symbols such that:
-
for each relation type R in \({\mathcal {S}}_R\) there exist two function symbols \(F_s^{\mathbf{R }}\) and \(F_t^{\mathbf{R }}\) with domain type R \(\in {\mathcal {S}}_R\) and codomain type \(\mathbf{O }_s, \mathbf{O }_t \in {\mathcal {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 a simple type in \( {\mathcal {S}}_D\) or an element in \({\mathcal {S}}_O\) or \({\mathcal {S}}_R \) assigning the simple data type or referenced object type or relation type to the attribute;
-
for each multi-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 a product type in \( {\mathcal {S}}_D\) or unions thereof;
-
-
\({\mathcal {R}}\) is a set of typed relation symbols;
-
\({\mathcal {C}}\) is a set of typed constants to specify the possible values \(c_i\) of a simple type \(\mathbf{T }\in {\mathcal {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.
-
a universe \({\mathcal {U}}\) of typed elements respecting the type hierarchy, that is
-
for each \(\mathbf{T }\) in \({\mathcal {S}}\) there exists a set \({\mathcal {U}}_\mathbf{T } \subseteq {\mathcal {U}}\) and \({\mathcal {U}} = \bigcup _{\mathbf{T }\in {\mathcal {S}}} {\mathcal {U}}_\mathbf{T }\);
-
all sets \({\mathcal {U}}_{\mathbf{T }}\) for \(\mathbf{T }\in {\mathcal {S}}_O\cup {\mathcal {S}}_R\) have to be pairwise disjoint except for sets \({\mathcal {U}}_{\mathbf{O }_1}\) and \({\mathcal {U}}_{\mathbf{O }_2}\) with \(\mathbf{O }_1, \mathbf{O }_2 \in {\mathcal {S}}_O\) where \(\mathbf{O }_1 <_O \mathbf{O }_2\). In this case \({\mathcal {U}}_{\mathbf{O }_1}\) must be a subset of \({\mathcal {U}}_{\mathbf{O }_2}\), i.e., \({\mathcal {U}}_{\mathbf{O }_1}\subseteq {\mathcal {U}}_{\mathbf{O }_2}\);
-
all sets \({\mathcal {U}}_{\mathbf{T }}\) with \(\mathbf{T }= \mathbf{T }_1\times \mathbf{T }_2 \times \cdots \times \mathbf{T }_n\) a product type in \({\mathcal {S}}_D\) consist of tuples \((x_1,x_2, \ldots x_n)\in {\mathcal {U}}_{\mathbf{T }_1}\times {\mathcal {U}}_{\mathbf{T }_2} \times \cdots \times {\mathcal {U}}_{\mathbf{T }_n}\);
-
-
an interpretation of the function symbols in \({\mathcal {L}}\), i.e., for each function symbol \(F\in {\mathcal {F}}\) with domain type \(\mathbf{T }_1 \times \ldots \times \mathbf{T }_n\) and codomain type \(\mathbf{T }\) a function \(f:{\mathcal {U}}_{\mathbf{T }_1}\times \ldots \times {\mathcal {U}}_{\mathbf{T }_n} \rightarrow {\mathcal {U}}_\mathbf{T }\);
-
an interpretation of the relation symbols in \({\mathcal {L}}\), i.e., for each relation symbol \(R\in {\mathcal {R}}\) with domain type \(\mathbf{T }_1 \times \ldots \times \mathbf{T }_m\) a relation \(r \subseteq {\mathcal {U}}_{\mathbf{T }_1}\times \ldots \times {\mathcal {U}}_{\mathbf{T }_m}\);
-
for each simple type \(\mathbf{T }\in {\mathcal {S}}_D\) and constant \(C \in {\mathcal {C}}\) of type \(\mathbf{T }\) an interpretation \(c\in {\mathcal {U}}_{\mathbf{T }}\);
-
for each constraint \(\phi \) in C the model \({\mathcal {M}}\) satisfies \(\phi \), i.e., \({\mathcal {M}}\models \phi \).
3.2 Running example Petri Nets
4 M2FOL
: metamodel 2 first-order logic a formal modeling language for metamodels
M2FOL
, i.e., a metamodeling language to be exact. This language is capable of describing precisely the concepts explicated in Definition 1. In general, meta\(^2\)models of metamodeling languages are supposed to be self-describing, which results in a four-layer metamodeling stack as depicted in Fig. 5. We will show that the metamodel of M2FOL
, a meta\(^2\)model by nature, also partakes of this property.
4.1 Definition of M2FOL
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 instantiation 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.M2FOL
metamodel specificationM2FOL (meta)model to language-signature | Mapping | Application to the Petri Net metamodel | |
---|---|---|---|
1. | Each metamodel element o in the set \( {\mathcal {U}}_{\texttt {OT}}\) defines an object type O of the language. The specialization relation \(<_{\texttt {OT}} \subseteq {\mathcal {U}}_{\texttt {OT}} \times {\mathcal {U}}_{\texttt {OT}}\) must be adopted to the types | \(\texttt {o}\in {\mathcal {U}}_{\texttt {OT}} \rightarrowtail \mathbf{O }\in {\mathcal {S}}_O,\) \(<_\texttt {OT} \rightarrowtail <_O\) | \(\texttt {node} \in {\mathcal {U}}_{\texttt {OT}} \rightarrowtail \mathbf{Node } \in {\mathcal {S}}_O,\) \(\texttt {place} \in {\mathcal {U}}_{\texttt {OT}} \rightarrowtail \mathbf{Place} \in {\mathcal {S}}_O,\) \(\texttt {trans} \in {\mathcal {U}}_{\texttt {OT}} \rightarrowtail \mathbf{Trans} \in {\mathcal {S}}_O\) |
2. | Each metamodel element r in the set \({\mathcal {U}}_{\texttt {RT}}\) defines a relation type R of the language | \(\texttt {r}\in {\mathcal {U}}_{\texttt {RT}} \rightarrowtail \mathbf{R }\in {\mathcal {S}}_R\) | \(\texttt {arc}\in {\mathcal {U}}_{\texttt {RT}} \rightarrowtail \mathbf{Arc }\in {\mathcal {S}}_R\) |
3. | For each relation type \(\texttt {r}\in {\mathcal {U}}_{\texttt {RT}}\), there exist an element \(\texttt {s}\) of type From and an element \(\texttt {t}\) of type To and both relation elements have as source element r , \(\texttt {f}_s^{\texttt {Fr}}(\texttt {s})=\texttt {r}, \texttt {f}_s^{\texttt {Fr}}(\texttt {t})=\texttt {r}\). The assignment \(\texttt {f}_t^{\texttt {To}}(\texttt {s})=\texttt {o}_s\) indicates the source object type of \(\mathbf{R }\), \(\texttt {f}_t^{\texttt {To}}(\texttt {t})=\texttt {o}_t\) indicates the target object type of \(\mathbf{R }\) | \(\texttt {r},\texttt {s}, \texttt {o}_s \rightarrowtail \texttt {F}_s^{\text {R}}:\mathbf{R }\rightarrow \mathbf{O }_s\); \(\texttt {r},\texttt {t}, \texttt {o}_t \rightarrowtail \texttt {F}_t^{\text {R}}:\mathbf{R }\rightarrow \mathbf{O }_t\) | \(\texttt {arc},\texttt {f}_t^{\texttt {Fr}}(\texttt {a\_from})=\texttt {n} \rightarrowtail \texttt {F}_s^{\text {Arc}}:\mathbf{Arc }\rightarrow \mathbf{Node };\) \(\texttt {arc},\texttt {f}_t^{\texttt {To}}(\texttt {a\_to})=\texttt {n} \rightarrowtail \texttt {F}_t^{\text {Arc}}:\mathbf{Arc }\rightarrow \mathbf{Node }\) |
4. | Each metamodel element dt in \({\mathcal {U}}_{\texttt {DT}}\) defines a data type DT of the language. Each metamodel element d in \({\mathcal {U}}_{\texttt {D}}\) with \(\texttt {f}_{\texttt {DT}}(\texttt {d})=\texttt {dt}\) becomes a constant symbol \(C_d\) in \({\mathcal {C}}\) of type DT | \(\texttt {dt} \in {\mathcal {U}}_\texttt {DT}\rightarrowtail \mathbf{DT} \in {\mathcal {S}}_{D}\); \(\texttt {d} \in {\mathcal {U}}_\texttt {D}\rightarrowtail C_\texttt {d} \in {\mathcal {C}}\) | \({\mathbb {N}} \in {\mathcal {U}}_\texttt {DT}\rightarrowtail {\mathbb {N}} \in {\mathcal {S}}_{DT};\) \(\texttt {i} \in {\mathcal {U}}_\texttt {D}, \texttt {f}_{DT}(i)={\mathbb {N}} \rightarrowtail \text {i} \in {\mathcal {C}}\) of type \({\mathbb {N}}\) |
5. | Each metamodel element a in the set \({\mathcal {U}}_\texttt {AT}\) defines a function symbol \(\texttt {F}^\texttt {a}\) of the language. The object or relation type that a belongs to, i.e., the domain of \(\texttt {F}^\texttt {a}\), is given by the assignment \(\texttt {f}_{type}(\texttt {a})=\texttt {t}_{ty}\in {\mathcal {U}}_\texttt {OT} \cup {\mathcal {U}}_\texttt {RT} \), its value range, i.e., codomain, by \(\texttt {f}_{val}(\texttt {a})=(\texttt {t}_{v_1}, \ldots , \texttt {t}_{v_n})\in ({\mathcal {U}}_\texttt {OT} \cup {\mathcal {U}}_\texttt {RT} \cup {\mathcal {U}}_\texttt {DT})^n\) | \(\texttt {a}, \texttt {t}_{ty}, \texttt {t}_{{\bar{v}}} \rightarrowtail F^\texttt {a}:T_{ty}\rightarrow T_{{\bar{v}}}\) | \(\texttt {tok}, \texttt {f}_{type}(\texttt {tok})=\texttt {place},\) \(\texttt {f}_{val}(\texttt {tok})={\mathbb {N}}\) \(\rightarrowtail \) \(F^{Tokens}: \mathbf{Place} \rightarrow {\mathbb {N}}\) |
6. | The constraints of the language have to be added manually, because this information is not determined by the metamodel |
M2FOL
, we want to model object types and specialization 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 \({\mathcal {S}}_O\) in M2FOL
, whereas all italic concepts make up a type in \({\mathcal {S}}_R\) in M2FOL
. The types specialization, from, and to furthermore require assignment functions for source and target specification. Data types and data are necessary for defining attribute domains and their values, e.g., the domain \({\mathbb {N}}_{0\ldots 10}\) and values \(\{0,1,2,\ldots ,9,10\}\) or an enumeration list domain gender with values male, female, else. Attribute types need the assignment of owning type and value domain.M2FOL
is a modeling language with signature \(\varSigma =\{{\mathcal {S}}, {\mathcal {F}}, {\mathcal {R}}, {\mathcal {C}}\}\) with the set of types split in \({\mathcal {S}}={\mathcal {S}}_O \cup {\mathcal {S}}_R \cup {\mathcal {S}}_D\), where:-
\({\mathcal {S}}_O\) consists of the types
O
(bject)T
(ype),R
(elation)T
(ype),A
(ttribute)T
(ype),D
(ata)T
(ype), andD
(ata), furthermore two supertypes:ORT
(ype), andDORT
(ype): \( {\mathcal {S}}_O = \{\texttt {OT}, \texttt {RT}, \texttt {AT}, \texttt {DT}, \texttt {D}, \texttt {ORT}, \texttt {DORT}\}\);-
The types
OT
, andRT
, specializeORT
, the typesORT
, andDT
specializeDORT
: \(\texttt {OT}<_O \texttt {ORT}\), \(\texttt {RT}<_O \texttt {ORT}\), \(\texttt {ORT} <_O \texttt {DORT}\), \(\texttt {DT}<_O \texttt {DORT}\);
-
-
\({\mathcal {S}}_R\) consists of the types
Spec
(ialization),Fr
(om), andTo
: \({\mathcal {S}}_R = \{\texttt {Spec}, \texttt {Fr}, \texttt {To}\}\); -
\({\mathcal {S}}_D\) contains product types \(\texttt {DORT}^n\) for all \(n>1\) as well as a type \(\texttt {T}_{\texttt {DORT}}\) for the union of all \(\texttt {DORT}^n:\texttt {T}_{\texttt {DORT}}=\bigcup _i \texttt {DORT}^i\);
-
the set of function symbols consists of following elements:
-
two symbols \(\texttt {F}_{s}^{\texttt {Spec}}\) and \(\texttt {F}_{t}^{\texttt {Spec}}\) assigning source and target to
Spec
-typed relations: \(\texttt {F}_{s}^{\texttt {Spec}}:\texttt {Spec}\rightarrow \texttt {OT}\), \(\texttt {F}_{t}^{\texttt {Spec}}:\texttt {Spec}\rightarrow \texttt {OT}\); -
two symbols \(\texttt {F}_{s}^{\texttt {Fr}}\) and \(\texttt {F}_{t}^{\texttt {Fr}}\) assigning source and target to
Fr
-typed relations: \(\texttt {F}_{s}^{\texttt {Fr}}:\texttt {Fr}\rightarrow \texttt {RT},\) \(\texttt {F}_{t}^{\texttt {Fr}}:\texttt {Fr}\rightarrow \texttt {OT}\); -
two symbols \(\texttt {F}_{s}^{\texttt {To}}\) and \(\texttt {F}_{t}^{\texttt {To}}\) assigning source and target to
To
-typed relations: \(\texttt {F}_{s}^{\texttt {To}}:\texttt {To}\rightarrow \texttt {RT},\ \texttt {F}_{t}^{\texttt {To}}:\texttt {To}\rightarrow \texttt {OT}\); -
two symbols \(\texttt {F}_{val}\) and \(\texttt {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 n-valued type in \(\texttt {DORT}^n\): \(\texttt {F}_{val}: \texttt {AT} \rightarrow \bigcup _i \texttt {DORT}^i,\ \texttt {F}_{type}:\texttt {AT} \rightarrow \texttt {ORT} \);
-
a symbol \(\texttt {F}_{\texttt {DT}}\) to assign a data type to a data element: \(\texttt {F}_{\texttt {DT}}:\texttt {D}\rightarrow \texttt {DT}\);
-
-
\({\mathcal {R}}\) consists of a symbol \(<_{\texttt {OT}}\) transitively extending the specialization relation given by
Spec
to a strict partial order on the set of object types \({\mathcal {R}} = \{ <_{\texttt {OT}}\ \subseteq \texttt {OT}\times \texttt {OT}\}\).
Spec
under the assumption that all universes are finite:To
and Fr
objects of a relation (15–17), and the abstractness of the types ORT
and DORT
(18–19):4.2 Running example Petri Nets
M2FOL
-model.n
(ode), p
(lace), and tr
(ansition). The universe of relation types \({\mathcal {U}}_\texttt {RT}\) contains one element a
(rc). One element tok
(ens) is contained in the universe of attribute types \({\mathcal {U}}_{\texttt {AT}}\). The universe \({\mathcal {U}}_\texttt {Spec}\) contains the specialization relations \(\texttt {p\_n}\) between p
and n
as well as \(\texttt {tr\_n}\) between tr
and n
. \({\mathcal {U}}_{\texttt {Fr}}\) contains the relation \(\texttt {a\_from}\) of the source element assignment to the relation type a
. \({\mathcal {U}}_{\texttt {To}}\) contains the relation \(\texttt {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: \(\texttt {f}_s^{\texttt {Spec}}(\texttt {p\_n})=\texttt {p}\), \(\texttt {f}_t^{\texttt {Spec}}(\texttt {p\_n})=\texttt {n}\), \(\texttt {f}_s^{\texttt {Spec}}(\texttt {tr\_n})=\texttt {tr}\), \(\texttt {f}_t^{\texttt {Spec}}(\texttt {tr\_n})=\texttt {n}\), \(\texttt {f}_s^{\texttt {Fr}}(\texttt {a\_from})=\texttt {a}\), \(\texttt {f}_t^{\texttt {Fr}}(\texttt {a\_from})=\texttt {n}\), \(\texttt {f}_s^{\texttt {To}}(\texttt {a\_to})=\texttt {a}\), \(\texttt {f}_t^{\texttt {To}}(\texttt {a\_to})=\texttt {n}\). From Spec
the transitive order relation \(<_{\texttt {OT}}\) is deduced: \(<_{\texttt {OT}} = \{(\texttt {p},\texttt {n}), (\texttt {tr},\texttt {n})\}\). Furthermore, there are data values \(\{0,1,2,\ldots \}\) in \({\mathcal {U}}_\texttt {D}\) all of type \({\mathbb {N}}_0 \in {\mathcal {U}}_{\texttt {DT}}\), \(\texttt {f}_{DT}(i)={\mathbb {N}}_0\ \forall i \in {\mathcal {U}}_\texttt {D}\). These are needed for the value domain of the attribute type tok
, an attribute assigned to p
: \(\texttt {f}_{type}(\texttt {tok})=\texttt {p}\), \(\texttt {f}_{val}(\texttt {tok})={\mathbb {N}}_0\). In short, this can be written as follows:4.3 Meta-perspective on M2FOL
M2FOL
as M2FOL
model. The graphical metamodel is depicted in Fig. 6.M2FOL
M2FOL
metamodel contains seven objects of type OT
=\(\{\texttt {o}(\textit{bject}) \texttt {t}(\textit{ype})\), \(\texttt {r}(\textit{elation}) \texttt {t}(\textit{ype})\), \(\texttt {a}(\textit{ttribute}) \texttt {t}(\textit{ype})\), \(\texttt {d}(\textit{ata}) \texttt {t}(\textit{ype})\), \(\texttt {d}(\textit{ata})\), \(\texttt {ort}(\textit{ype})\), \(\texttt {dort}(\textit{ype})\}\), three objects of type RT
=\(\{\texttt {spec},\) \(\texttt {fr}(\textit{om}),\) \(\texttt {to}\}\), three objects of type \(\texttt {AT}\)= \(\{\texttt {val}(\textit{ue})\_\texttt {dom}(\textit{ain})\), \(\texttt {ass}(\textit{igned})\_\texttt {to}\), \(\texttt {ass}(\textit{igned})\_\) \(\texttt {d}(\textit{ata})\texttt {t}(\textit{ype})\), many objects of type \(\texttt {DT}=\{\texttt {dort}^i \forall i\), \(\bigcup _i(\texttt {dort})^i\} \) (not visible in the graphical metamodel), four relations of type Spec
=\(\{\texttt {ot}<\texttt {ort},\texttt {rt}<\texttt {ort},\texttt {ort}<\texttt {dort},\texttt {dt}<\texttt {dort}\} \), three relations of type From
=\(\{\texttt {source\_spec}\), \(\texttt {source\_to}\), \(\texttt {source\_fr}\}\), as well as three relations in To
=\(\{\texttt {target\_spec}\), \(\texttt {target\_to}\), \(\texttt {target\_fr}\}\), furthermore 26 assignments of source and target objects, attribute owning types and attribute value types.M2FOL
. On the other hand, this metamodel defines M2FOL
as a meta\(^2\)model. With the algorithm presented above, we deduce Definition 3 from Example 4. So we conclude that the proposed modeling language M2FOL
for metamodels is self-describing and thereby complete the formalization of the four-layer metamodeling stack.4.4 Pinpointing the approach in the language definition hierarchy
M2FOL
from Example 4 is an example of a meta\(^2\)modeling language representation.M2FOL
(Example 4), therefore being a representation of a metametamodel. As this representation was itself defined by means of M2FOL
, this shows that M2FOL
is a metamodel representation grammar as well as a metametamodel representation grammar and therefore suffices to complete the formalization of the four-layer metamodeling stack.5 Potential and benefits of formalized conceptual modeling languages
5.1 Modeling with power types
5.1.1 Extending MetaMorph with the power type concept
-
\({\mathcal {S}}\) is a set of types, which can be further divided into three disjoint subsets \({\mathcal {S}}_O\), \({\mathcal {S}}_R\), and \({\mathcal {S}}_D\) for object types, relation types and data types;
-
the type set \({\mathcal {S}}_O\) is strictly partially ordered with order relation \(<_O \subseteq {\mathcal {S}}_O \times {\mathcal {S}}_O\) to indicate the specialization relation between the corresponding object types;
-
the type set \({\mathcal {S}}_O\) is furthermore structured by the anti-reflexive and circle-free power type relation \(\in _O \subseteq {\mathcal {S}}_O \times {\mathcal {S}}_O\) to indicate instantiation between the base type and its power type;
-
the type set \({\mathcal {S}}_D\) can contain simple types \(\mathbf{T }\) for value domains of single-value attributes, or product types \(\mathbf{T }'= \mathbf{T }_1\times \mathbf{T }_2 \times \cdots \times \mathbf{T }_n\) and unions thereof for value domains of n-ary multi-value attributes \((n>1)\), where the ith value is of type \(\mathbf{T }_i \in {\mathcal {S}}_D \cup {\mathcal {S}}_O \cup {\mathcal {S}}_R\setminus \{\mathbf{T }_{all},\wp (\mathbf{T }_{all})\} \);
-
the type set \({\mathcal {S}}_D\) additionally contains a type \(\mathbf{T }_{all}\) and its powerset \(\wp (\mathbf{T }_{all})\) where \(\mathbf{T }_{all}\) is the union of all object types, relation types, simple and product types \(\mathbf{T }_{all}=\bigcup _{\mathbf{T }\in {\mathcal {S}}'}\mathbf{T }\), with \({\mathcal {S}}'={\mathcal {S}}_O\cup {\mathcal {S}}_R\cup {\mathcal {S}}_D \setminus \{\mathbf{T }_{all},\wp (\mathbf{T }_{all})\}\);
-
-
\({\mathcal {F}}\) is a set of typed function symbols such that:
-
for each relation type R in \({\mathcal {S}}_R\) there exist two function symbols \(F_s^{\mathbf{R }}\) and \(F_t^{\mathbf{R }}\) with domain type R \(\in {\mathcal {S}}_R\) and codomain type \(\mathbf{O }_s, \mathbf{O }_t \in {\mathcal {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 a simple type in \( {\mathcal {S}}_D\) or an element in \({\mathcal {S}}_O\) or \({\mathcal {S}}_R \) assigning the simple data type or referenced object type or relation type to the attribute;
-
for each multi-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 a product type in \( {\mathcal {S}}_D\) and unions thereof;
-
for each power type relation \(\mathbf{O }_B \in _O \mathbf{O }_P\) the set \({\mathcal {F}}\) contains a function symbol \(F_{\mathbf{O }_P}:\mathbf{O }_P\rightarrow \wp (\mathbf{T }_{all})\) assigning a set of possible values to the additional attribute added to the power type on model-level;
-
-
\({\mathcal {R}}\) is a set of typed relation symbols such that:
-
for each power type relation \(\mathbf{O }_B \in _O \mathbf{O }_P\) the set \({\mathcal {R}}\) contains a relation symbol \(\in _{BP}\subseteq \mathbf{O }_B\times \mathbf{O }_P\) to enable the check of membership of base element and power type element on model-level;
-
for each power type relation \(\mathbf{O }_B \in _O \mathbf{O }_P\) the set \({\mathcal {R}}\) contains a relation symbol \(R_{BP}\subseteq \mathbf{O }_B\times \mathbf{O }_P\times \mathbf{T }_{all}\) assigning a value to the added attribute assigned to an element in \(\mathbf{O }_B\) by its membership in \(\mathbf{O }_P\);
-
\({\mathcal {R}}\) contains a relation symbol \(\in _{val} \subseteq \mathbf{T }_{all}\times \wp (\mathbf{T }_{all})\) with the usual containment semantics of elements and sets;
-
-
\({\mathcal {C}}\) is a set of typed constants to specify the possible values \(c_i\) of a simple type \(\mathbf{T }\in {\mathcal {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. To ensure the proper behavior of the power type relation we need several constraints for each pair of related types \(\mathbf{O }_B\) base type and \(\mathbf{O }_P\) power type:
-
A language comprising a power type relation \(\mathbf{O }_B \in _O \mathbf{O }_P\) must ensure that a value is assigned to the pair (b, p) of a base type element b and power type element p iff b and p are in a power type relation:$$\begin{aligned}&\forall b\in \mathbf{O }_B, p\in \mathbf{O }_P \nonumber \\&\quad (b\in _{BP}p \Leftrightarrow \exists x\in {\mathbf {T}}_{all}\ ((b,p,x)\in {R}_{BP}) \end{aligned}$$(57)
-
To conform to the value domain of an additional attribute induced by the power type relation \(\mathbf{O }_B \in _O \mathbf{O }_P\) we furthermore need a constraint binding the type of the assigned value \(val\in \mathbf{T }_{all}\) of the relation symbol \({R}_{BP}\subset \mathbf{O }_B\times \mathbf{O }_P\times \mathbf{T }_{all}\) to \(F_{\mathbf{O }_P}(p)\):$$\begin{aligned}&\forall x \in \mathbf{T }_{all}, b\in \mathbf{O }_B, p\in \mathbf{O }_P \nonumber \\&\quad (((b,p,x)\in {R}_{BP}) \implies x\in _{val} F_{\mathbf{O }_P}(p)) \end{aligned}$$(58)
-
The assigned value \(x\in \mathbf{T }_{all}\) to the tuple of base type element and power type element must be unique:$$\begin{aligned}&\forall x,y \in \mathbf{T }_{all}\ ((\exists b\in \mathbf{O }_B, p\in \mathbf{O }_P \nonumber \\&\quad (((b,p,x)\in {R}_{BP})\wedge ((b,p,y)\in {R}_{BP}))) \nonumber \\&\quad \implies x=y) \end{aligned}$$(59)
-
-
a universe \({\mathcal {U}}\) of typed elements respecting the type hierarchy and power type relation, that is
-
for each \(\mathbf{T }\) in \({\mathcal {S}}\) there exists a set \({\mathcal {U}}_\mathbf{T } \subseteq {\mathcal {U}}\) and \({\mathcal {U}} = \bigcup _{\mathbf{T }\in {\mathcal {S}}} {\mathcal {U}}_\mathbf{T }\);
-
all sets \({\mathcal {U}}_{\mathbf{T }}\) for \(T\in {\mathcal {S}}_O\cup {\mathcal {S}}_R\) have to be pairwise disjoint except for sets \({\mathcal {U}}_{\mathbf{O }_1}\) and \({\mathcal {U}}_{\mathbf{O }_2}\) with \(\mathbf{O }_1, \mathbf{O }_2 \in {\mathcal {S}}_O\) where \(\mathbf{O }_1 <_O \mathbf{O }_2\). In this case \({\mathcal {U}}_{\mathbf{O }_1}\) must be a subset of \({\mathcal {U}}_{\mathbf{O }_2}\), i.e., \({\mathcal {U}}_{\mathbf{O }_1}\subseteq {\mathcal {U}}_{\mathbf{O }_2}\);
-
all sets \({\mathcal {U}}_{\mathbf{T }}\) with \(\mathbf{T }= \mathbf{T }_1\times \mathbf{T }_2 \times \cdots \times \mathbf{T }_n\) a product type in \({\mathcal {S}}_D\) consist of tuples \((x_1,x_2, \ldots x_n)\in {\mathcal {U}}_{\mathbf{T }_1}\times {\mathcal {U}}_{\mathbf{T }_2} \times \cdots \times {\mathcal {U}}_{\mathbf{T }_n}\);
-
all elements \({\mathcal {U}}_{\mathbf{O }_P}\) with \(\mathbf{O }_B, \mathbf{O }_P \in {\mathcal {S}}_O\) and \(\mathbf{O }_B \in _O \mathbf{O }_P\) are sets of elements of \({\mathcal {U}}_{\mathbf{O }_B}\). This means that \({\mathcal {U}}_{\mathbf{O }_P}\) is a set of sets \( \subseteq {\mathcal {U}}_{\mathbf{O }_B}\) and therefore a subset of the powerset \(\wp ({\mathcal {U}}_{\mathbf{O }_B})\).
-
-
an interpretation of the function symbols in \({\mathcal {L}}\), i.e., for each function symbol \(F\in {\mathcal {F}}\) with domain type \(\mathbf{T }_1 \times \ldots \times \mathbf{T }_n\) and codomain type \(\mathbf{T }\) a function \(f:{\mathcal {U}}_{\mathbf{T }_1}\times \ldots \times {\mathcal {U}}_{\mathbf{T }_n} \rightarrow {\mathcal {U}}_\mathbf{T }\);
-
an interpretation of the relation symbols in \({\mathcal {L}}\), i.e., for each relation symbol \(R\in {\mathcal {R}}\) with domain type \(\mathbf{T }_1 \times \ldots \times \mathbf{T }_m\) a relation \(r \subseteq {\mathcal {U}}_{\mathbf{T }_1}\times \ldots \times {\mathcal {U}}_{\mathbf{T }_m}\);
-
for each simple type \(\mathbf{T }\in {\mathcal {S}}_D\) and constant \(C \in {\mathcal {C}}\) of type \(\mathbf{T }\) an interpretation \(c\in {\mathcal {U}}_{\mathbf{T }}\);
-
for each constraint \(\phi \) in C the model \({\mathcal {M}}\) satisfies \(\phi \), i.e., \({\mathcal {M}}\models \phi \), in particular \({\mathcal {M}}\) satisfies the constraints for the proper behavior ot the power types.
5.1.2 Case study
5.2 Language interleaving and consistency
5.2.1 Top-down approach
5.2.2 Bottom-up approach
5.2.3 Case study
5.3 Operations on models
5.3.1 Structural events and domain events
M
of Example 2 of the Petri Net model depicting a barber shop. A valid domain event is the firing of the transition Serve. This event is the concatenation of the three structural events of changing the attribute values: first the value of the tokens attribute of element Busy is set to 1, the tokens attribute of Idle is set to 0, and the tokens attribute of Wait is set to 1. None of these structural events alone is semantically valid, but together they form a semantically and syntactically admissible operation. This also shows that there are many structural events (we can set the attribute tokens of each place to any number we like) but much less domain events.5.4 Translators
6 Discussion
MetaMorph
allows for a precise definition of modeling languages. The formalization of a modeling language with MetaMorph
requires a full declaration of any element possibly instantiated, i.e., any symbol in the signature of the language. The formalization process obliges the engineer to make explicit any concept and possible instances or values of the language as well as to unfold any constraint to prevent not permitted model constructs. Therefore, it results in a complete specification ready for use.MetaMorph
and to formalize their own metamodeling projects implemented for the course Metamodeling part of the masters program. After the formalization they filled in a questionnaire about adequacy and usability of MetaMorph
as well as their pre-knowledge in modeling, metamodeling, and logic. The goal of the evaluation is to measure the actual intuitivity of the formalism and satisfaction of language engineers. We are also interested in the influence of pre-knowledge on the use of the proposed formalism. Further questions to be answered are how much effort it takes to formalize a small-sized language, if the size and complexity of the language have an influence on the experienced complexity when using the formalism and if an introductory session is helpful or even required to successfully apply MetaMorph. The evaluation of the questionnaires considering the actual outcome of the students’ formalizations (correctness, extent, ...) is currently in progress.7 Conclusion
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-describing, which can be seen by applying the algorithm to its own metamodel.M2FOL
, a suitable tool for transforming graphical metamodels into formal ones will be developed.