The era of models as executable entities rather than descriptive pictures is on the rise. Nowadays modeling languages provide a variety of additional features like transformation, simulation, or code generation and the consumers of models are persons as well as machines. This development brings about the necessity to make models machineprocessable, i.e. to formalize modeling languages. The goal of this research project is to nd a suitable formalism for this purpose. This formalism will be grounded on mathematical theories, adopting their unambiguity and expressiveness and enabling the application of established mathematical methods. Therefore the plan for this research project is to examine several promising mathematical theories regarding their possibilities and limitations. A rst result of this examination is presented in this paper: the formalization of the semantics of a metamodel based on model theory, a branch of mathematical logic. We outline the analogy between the concepts of metamodeling and model theory and describe how a metamodel can be formalized with this approach. A proof of concept is given by applying the formalism on a simple example, namely the entity-relationship modeling language.
In the past decade modeling languages have evolved from mere instruments for
pictures supporting human understanding to highly specialized tools with value
adding mechanisms like transformation, simulation or code generation. An
increasing number of models are in fact not created for human consumption but
for computational processing and execution. The most signi cant requirement
Copyright 2018 for this paper by its authors. Copying permitted for private and
academic purposes.
evolving from this fact is the inevitable need for appropriate and complete
formalization of the underlying modeling languages, as machines cannot understand
semi-formal or natural language speci cations. Yet there is no commonly used
approach or language to unambiguously de ne a modeling language much less a
formalism which su ces for these needs. Thalheim [
When talking about rigorous formalization the rst things that come to mind are concepts from mathematics as these theories are formal, complete, and unambiguous by de nition. Furthermore mathematical structures admit the exploitation of metamodels through the application of well elaborated algorithms or the discovery of hidden properties and connections by transforming them to related structures. A goal of this research project is therefore to examine appropriate theories that project concepts of metamodeling in a natural way to mathematical concepts.
RQ2: Which mathematical concepts can serve as a formal foundation for modeling methods? Which opportunities do the di erent concepts provide? What are their limitations?
Fill, Redmond and Karagiannis [
The mathematical concept that is most self-evident as a basis of a
diagrammatic model is graph theory [
Another emerging demand in metamodeling which guides us in this research
question is agility, a requirement modeling languages nowadays have to meet,
see Karagiannis [
At this quite early stage of the research project we address the speci c question of nding ways to formalize semantics, similar to established approaches like formal semantics for programming languages. The aim is to enable model checking against the metamodel as well as checking the satis ability of metamodel constraints.
RQ3: How can the semantics of a modeling language be formalized in order to enable automated processing?
Here we explicitly aim at a structurally founded formalism. In view of existing
work on formalizing semantics, e.g. ConceptBase [
The rest of this paper is structured as follows: we start with an outline of the research plan. Then we provide a summary of the results achieved so far. We give an attempt to formalize the semantics of a modeling language with tools from mathematical logic. We do so by exhibiting an analogy between metamodels, the structure and concepts of graphs and formal and logical languages. We reason the parallelism of models and graphs and how the concepts of metamodeling can be mapped to the concepts of graph theory. Then we give a short introduction to model theory so that we can show the applicability of formal languages and models to metamodeling. As a nal point we give a proof of concept by applying the approach to a simple example, namely the entity-relationship modeling language.
Phase 1: We start with a literature review to identify and study other existing
approaches in metamodeling focusing in particular on their formal foundations.
Phase 2: We study the concepts of metamodeling and abstract patterns and
structures which can be described mathematically. We will proceed iteratively,
concept by concept, component by component, and add a phase of review and
consolidation after each iterative step. For the concepts of metamodels we
follow the de nitions of Kern, Hummerl and Kuhne [
Phase 3: We examine mathematical theories standing to reason and try to match the discovered patterns from phase 2. Due to the iterative approach this phase will to some extent be executed simultaneously to the second one. We try to elaborate a formalism for the concept or component under study and moreover try to consolidate or at least link the mathematical approaches used in former iterations. For proof of concept we will implement prototypes whenever this is meaningful.
Phase 4: We nally consolidate the results from the iteration steps in a holistic approach. The aim is to establish a nal formalism comprising possibilities to formally de ne modeling languages or at least the most important components. This formalism will be a construct of structures, languages, methods and algorithms with high coherence and interoperability.
Phase 5: To validate our approach we will apply the constructed formalism on
the diverse modeling languages available at the OMiLAB platform [
In this chapter we present the preliminary results of our ongoing work on RQ3.
The goal is to nd a mathematical formalism to describe a modeling language
in a way that enables the de nition of semantic constraints of the language.
The approach is inspired by the research area of formal semantics in software
engineering [
Formal Semantics
Following the metamodeling framework of Karagiannis and Kuhn [
Nevertheless, all authors agree that semantics is a crucial but challenging
thing to deal with and many approaches have been devised to formalize
semantics for di erent areas. Especially for programming languages there are already
well elaborated theories on how to assign meaning to expressions and programs.
Historically the most important approaches are denotational semantics,
operational semantics, translational semantics, axiomatic semantics and algebraic
semantics [
In order to use the formal power of mathematical model theory in metamodeling we have to justify the analogy of the concepts on both sides, i.e. the validity of the red arrows in Figure 1. To do so we use as interim stage the concept of graphs as well as colors and labels on graphs. The procedure of creating a formal language for the structure of colored, labeled graphs is already established in model theory. The feasibility of representing models as graphs and the most important concepts of metamodeling, object types and relationship types, as concepts of colors and labels gives us the second analogy and closes the circle. The main bene t we gain by this mapping is the possibility to formally de ne the semantics of the modeling language in the unambiguous syntax of the speci cally de ned formal language L and logic, see Figure 2. The body of sentences representing the semantics of L form a so called L-theory. A valid model according to the semantics is represented by an L-structure satisfying all the sentences of the L-theory. Tellingly in model theory an L-structure with this property is called a model of the L-theory.
Once we have derived a formal language from our metamodel, de ned the semantic constraints, and expressed the models in the new language, the prerequisites for automated model checking are satis ed, see Figure 3. 3.3
Models as Graphs When looking at diagrammatic models from a mathematical point of view it is natural to interpret them as graphs. Models consist of objects and relations between objects; graphs are de ned as sets of vertices and edges i.e. ordered pairs of vertices. A mapping of subtler concepts, namely object types and relationship
Formal Language L
Graph Structure Colors & Labels
L-Structure
Colored & labeled Graph Metamodel Model
Model 2 ...
Model n types, can be achieved through the concepts of colored vertices for the former ones or labeled edges for the latter ones.
De nition 1 (Graph). A directed graph consist of a set of vertices V and a set of edges E V V .
To begin with this de nition is su cient. For more complex models with multiple edges between vertices we need the concept of multigraphs.
De nition 2 (Multigraph). A directed multigraph consist of a set of vertices V , a set of edges E and two functions s : E ! V and t : E ! V , where s assigns a source vertex to an edge and t assigns a target vertex.
De nition 3 (Colored Graph). A colored graph is a graph with an additional map p : V ! P; P a set of colors, which assigns a color to each vertex. De nition 4 (Labeled Graph). A labeled graph is a graph with an additional map l : E ! L; L a set of labels, which assigns a label to each edge. Often authors use the terms vertex-labels and edge-labels instead of colors and labels, but for emphasizing the di erence between object types and relationship types we prefer this terminology. The assigned color of a vertex symbolizes the object type of the corresponding object in the model, the assigned label of an edge the relationship type. Usually mathematicians consider graph colorings where no adjacent vertices have the same color. This is a restriction we do not follow. 3.4
Model Theory Model theory is the study of mathematical structures from the viewpoint of mathematical logic. On the one hand its aim is to de ne a formal language and to describe a given structure with axioms. The axioms or sentences are written in the well known syntax of logical expressions and represent the semantics of the structure under study. On the other hand model theory aims at the study of structures ful lling these axioms, the so called models. Model theory is a powerful tool for describing a multitude of mathematical structures such as rings, ordered groups or graphs and to de ne their semantics. In general, model theory is not con ned to a speci c type of logic. Nevertheless in the introduction and the example below we restrict ourselves to rst-order logic.
De nition 5 (Language L and L-Structure). A language L is a collection of symbols, which are divided in three groups: function symbols denoted by f , relation symbols denoted by R and constant symbols denoted by c. Each function symbol and each relation symbol has associated a number in N, which de nes the arity.
L = ffi; Rj ; ck j i 2 I; j 2 J; k 2 Kg An L-Structure M is a set M , called the universe of M, and the interpretations of fi, Rj and ck in M: { An interpretation of a function symbol f is a function f M : M n ! M where n is the arity of f . { An interpretation of a relation symbol R is a subset RM M p where p is the arity of R.
{ An interpretation of a constant symbol c is an element cM 2 M . The structure M is denoted by
M = fM; fiM; RjM; ckM j i 2 I; j 2 J; k 2 Kg Example 1 (Graphs). The language L for graphs contains only one symbol, a binary relation C representing the edge or connection between two vertices. Example 2 (Colored Graphs). The language L0 for colored graphs contains additionally several unary relations Pi, the colors of the vertices.
L = fCg
L0 = fC; Pi j i 2 Ig
Remark 1 (Formulas, Sentences and Satisfaction). We forgo a precise de nition
of the from mathematical logic well-known terms formula and sentence. The
interested reader can nd them in [
A sentence is a formula with no free variables, i.e. it is a formula with no variables or it is of the form Q1x1:::Qmxm (x1; :::; xn) with a quanti er-free formula, Qi 2 f8; 9g and m = n.
If an L-Structure M satis es a sentence we write De nition 6 (L-Theory, Model of an L-Theory). An L-Theory T is a set of sentences of the language L. A Model of an L-Theory T is an L-Structure, which satis es all sentences of T .
Example 3. Consider the language L for graphs from Example 1. Then the theory
T = f8x8y(C(x; y) ! C(y; x))g has as models all undirected graphs.
For a detailed introduction into model theory see [
M j= :
A simpli ed version of the entity-relationship modeling language will serve as an example for the de nition of the language inherent semantics with the presented approach. The simpli ed version under study comprises three concepts, namely entity, relation and attribute, only one undirected relationship type to connect any of the three types and does not admit multiple relationships between the same two objects. This example shows the simplicity and expressiveness of the presented approach. 4.1
First we de ne the language for this special case of colored graphs or the metamodel of ER-models respectively:
E R = fC; E; R; Ag where C is the binary relation of connections between the objects, E is the color or type of entities, R is the color or type of relations and A is the color or type of attributes. Now we can de ne the sentences for our Theory T for the language E R: The rst three sentences ensure that every object has exactly one type, that the relation C is bidirectional (i.e. for every directed relation, also the inverse direction is element of the relation subset) and that no element is connected to itself.
8x((E(x) _ R(x) _ A(x))^ (:(E(x) ^ R(x)) ^ :(E(x) ^ A(x)) ^ :(R(x) ^ A(x)))) 8x8y(C(x; y) ! C(y; x))
8x(:C(x; x)) The following sentences are speci c for ER-models: 8x8y((A(x) ^ C(x; y)) ! :A(y)) 8x8y((E(x) ^ C(x; y)) ! :E(y)) 8x8y((R(x) ^ C(x; y)) ! :R(y)) 8x9y9z(R(x) ! (E(y) ^ E(z) ^ C(x; y) ^ C(x; z) ^ :(y = z))) 8x8y8z((A(x) ^ C(x; y) ^ C(x; z)) ! y = z) (1) (2) (3) (4) (5) (6) (7) (8) Sentences (4) - (6) ensure that no element is connected to an element of the same type. Sentence (7) forces an element of type relation to have at least two connections to objects of type entity. Sentence (8) ensures that attributes are connected to only one other element. Example 4. The E R-Structure M1 for Figure 4 looks as follows (the elements of CM1 should be read as unordered pairs) :
M1 = fM1; CM1 ; EM1 ; RM1 ; AM1 g
M1 = fAuthor; writes; Book; N ame; T itle; ISBN g CM1 = f(Author; N ame); (Author; writes); (writes; Book); (Book; T itle); (Book; ISBN )g
EM1 = fAuthor; Bookg
RM1 = fwritesg AM1 = fN ame; T itle; ISBN g (9) (10) (11) (12) (13) (14) The E R-Structure M1 is a Model for the E R-Theory T , it ful lls all the sentences (1) - (8). (15) (16) (17) (18) (19) (20) Example 5. The ER-Structure M2 for Figure 5 is a substructure of M1: M2 = fM2; CM2 ; EM2 ; RM2 ; AM2 g
M2 = fwrites; Book; T itle; ISBN g CM2 = f(writes; Book); (Book; T itle); (Book; ISBN )g
EM2 = fBookg
RM2 = fwritesg AM2 = fT itle; ISBN g
M2 2 The ER-Structure M2 is not a Model for the ER-Theory T , because sentence (7), denoted by , does not hold for x = writes. 5
In this paper we present the research goal of this PhD thesis - a formalism for modeling methods based on mathematical concepts - and present rst results using model theory, a concept from logic. We show how a modeling language can be formalized in the notion of a formal language L, how to enrich the language with semantic constraints written in rst order logic and how models are then translated to so called L-structures, which can be checked against the constraints.
At the moment we are also working on the application of particular concepts of model theory, i.e. sorted model theory and second order logic for the axioms, on modeling language de nitions and apply them to more complex modeling methods like petri nets. With sorted model theory we can easily represent multigraphs. Furthermore, we are examining a procedure for merging modeling languages via the use of extensions and cartesian products of formal languages.
We will proceed with the literature review starting with literature on the application of graph theory in computer science, e.g. attributed graphs, type graphs, graph grammars and transformation [5{7, 18, 19, 21, 22, 26]. We expect to thereby nd techniques to supplement our formalism.
Afterwards we will start to examine possible formal structures to enrich the
semantics and achieve the necessary expressibility and conceptualization of
modeling methods [
The main challenge in this research project is the balancing act of creating
a feasible formalism. Thalheim, referencing the commandments of Bowen and
Hinchey [
This doctoral project is supervised by o. Univ.-Prof. Prof.h.c. Dr. Dimitris Karagiannis, head of the research group Knowledge Engineering at the Faculty of Computer Science, University of Vienna.