Forschungsberichte
der Fakultät IV – Elektrotechnik und Informatik
Conflict Detection for Model Versioning
Based on Graph Modifications:
Long Version
Gabriele Taentzer1, Claudia Ermel2,
Philip Langer3 and Manuel Wimmer4
1Philipps-Universität Marburg, Germany
taentzer@mathematik.uni-marburg.de
2Technische Universität Berlin, Germany
claudia.ermel@tu-berlin.de
3Johannes-Kepler-Universität Linz, Austria
philip.lan[email protected]
4Technische Universität Wien, Austria
wimmer@big.tuwien.ac.at
Bericht-Nr. 2010-09
ISSN 1436-9915
Conflict Detection for Model Versioning
Based on Graph Modifications: Long Version
Gabriele Taentzer1, Claudia Ermel2,
Philip Langer3, and Manuel Wimmer4
1Philipps-Universit¨at Marburg, Germany, [email protected]
2Technische Universit¨at Berlin, Germany, claudia.ermel@tu-berlin.de
3Johannes-Kepler-Universit¨at Linz, Austria, [email protected]
4Technische Universit¨at Wien, Austria, [email protected]
Abstract. In model-driven engineering, models are primary artifacts and can evolve
heavily during their life cycle. Therefore, versioning of models is a key technique which
has to be offered by an integrated development environment for model-driven engi-
neering. In contrast to text-based versioning systems we present an approach which
takes abstract syntax structures in model states and operational features into account.
Considering the abstract syntax of models as graphs, we define model revisions as
graph modifications which are not necessarily rule-based. Building up on the DPO
approach to graph transformations, we define two different kinds of conflict detection:
(1) the check for operation-based conflicts, and (2) the check for state-based conflicts
on results of merged graph modifications.
1 Introduction
A key benefit of model-driven engineering is the management of the complexity
of modern systems by abstracting its compelling details using models. Like
source code, models may heavily evolve during their life cycle and, therefore,
they have to be put under version control. Especially optimistic versioning is
of particular importance because it allows for concurrent modifications of one
and the same artifact performed by multiple modelers at the same time. When
concurrent modifications are endorsed, contradicting and inconsistent changes,
and therewith versioning conflicts, might occur. Traditional version control
systems for code usually work on file-level and perform conflict detection by
line-oriented text comparison. When applied to the textual serialization of
models, the result is unsatisfactory because the information stemming from
the graph-based structure is destroyed and associated syntactic and semantic
information is lost.
To tackle this problem, dedicated model versioning systems have been pro-
posed [1,2,3,4]. However, a uniform and effective approach for precise conflict
detection and supportive conflict resolution in model versioning still remains
1
an open problem. For the successful establishment of dedicated model ver-
sioning systems, a profound understanding by means of formal definitions of
potentially occurring kinds of conflicts is indispensable, but yet missing.
Therefore, we present a formalization of two different kinds of conflicts
based on graph modifications. We introduce this new notion of graph mod-
ifications to generalize graph transformations. Graph modifications are not
necessarily rule-based, but just describe changes in graphs. Two kinds of con-
flict detection are defined based on graph modifications: (1) operation-based
conflicts and (2) state-based conflicts. The specification of operations is based
on rules. Therefore, we extract minimal rules from graph modifications and/or
select suitable pre-defined operations and construct graph transformations in
that way. Conflict detection is then based on parallel dependence of graph
transformations and the extraction of critical pairs as presented in [5]. State-
based conflicts are concerned with the well-formedness of the result after merg-
ing graph modifications. To detect state-based conflicts, two graph modifica-
tions are merged and the result is checked against pre-defined constraints.
The proposed critical pair extraction is not complex and corresponds to the
procedure of textual versioning systems, i.e. they are applied whenever graph
modifications have occurred and are being checked in. For each check-in, all
those modifications (check-ins) are checked for conflicts that have taken place
since the check-out of the model performed by the user who is performing the
current check-in.
The paper is structured as follows: In Section 2, we introduce the concept
of graph modification and recall the notion of graph transformation. While
Section 3 is concerned with the detection of operation-based conflicts, Sec-
tion 4 presents the detection of state-based conflicts. Sections 5 and 6 discuss
implementation issues and related work and finally, Section 7 concludes this
paper.
2 Graph Modifications and Graph Transformations
Throughout this paper, we describe the underlying structure of a model by a
graph. To capture all important information, we use typed, attributed graphs
and graph morphisms as presented in [5]. In the following, we omit the terms
“typed” and “attributed” when mentioning graphs and graph morphisms.
All model modifications are considered on the level of the abstract syntax
where we deal with graphs. We introduce graph modifications generalizing the
concept of graph transformation to graph changes which are not necessarily
2
rule-based. A graph modification is a partial injective graph mapping being
defined by a span of injective graph morphisms.
Definition 1 (Graph modification). Given two graphs Gand H, a direct
graph modification G=⇒His a span of injective morphisms Gg
←− Dh
−→ H.
A sequence G=G0=⇒G1=⇒. . . =⇒Gn=Hof direct graph modifications
is called graph modification and is denoted by G∗
=⇒H.
Graph Dcharacterizes an intermediate graph where all deletion actions
have been performed but nothing has been added yet.
Example 1 (Graph and graph revision). Consider the following model version-
ing scenario for statecharts. The abstract syntax of a statechart can be defined
by a typed, attributed graph, as e.g. shown in Fig. 1 (a). The node type is given
in the top compartment of a node. The name of each node of type State is writ-
ten in the attribute compartment below the type name. We model hierarchical
statecharts by using containment edges. For instance, in Fig. 1 (a), state S0
contains S1 and S2 as substates. (In contrast to UML state machines, we distin-
guish these edges which present containment links by composition decorators.)
Note that we abstract from transition events, guards and actions, as well as
from other statechart features. Furthermore, from now on we use a compact
notation of the abstract syntax of statecharts, where we draw states as nodes
(rounded rectangles with their names inside) and transitions as directed arcs
between state nodes. The compact notation of the statechart in Fig. 1 (a) is
shown in Fig. 1 (b). Fig. 1 (c) shows the statechart in the well-known concrete
syntax.
Fig. 1. Sample statechart: abstract syntax graph (a), compact notation (b) and concrete syntax (c)
In our scenario for model versioning, three users check out the current
statechart shown in Fig. 1 and change it in three different ways. User Aintends
3
to perform a refactoring operation on it. She moves state S3 up in the state
hierarchy (cf. Fig. 2).
Fig. 2. Refactoring step as graph modification gmA
User Brefines the statechart by adding a new state S5 inside superstate S0
and connects this newly added state S5 to state S2 in the same superstate by
drawing a new transition between them. Moreover, the transition connecting
S2 to S4 is deleted in this refinement step. This graph modification is shown in
Fig. 3. Finally, user Cdeletes state S3 together with its adjacent transition to
state S4 (cf. Fig. 4).
Fig. 3. Refinement step as graph modification gmB
Fig. 4. Deletion step as graph modification gmC
Obviously, conflicts occur when these users try to check in their changes:
state S3 is deleted by user Cbut is moved to another container by user A.
4
Furthermore, user Band user Cdelete different transitions adjacent to state
S4. This may lead to a problem if the statechart language forbids isolated states
(not adjacent to any transition), although each single change does not create
a forbidden situation.
Since we will use rules to detect conflicts between graph modifications, we
recall the notions of graph rule and transformation here. We use the DPO
approach for our work, since its comprehensive theory as presented in [5] is
especially useful to formalize conflict detection in model versioning.
Definition 2 (Graph rule and transformation). Agraph rule p=Ll
←−
Kr
−→ Rconsists of graphs L, K and Rand injective graph morphisms land r.
Given a match m:L→G, graph rule pcan be applied to Gif a double-pushout
(DPO) exists as shown in the diagram below with pushouts (P O1)and (PO2)
in the category of typed, attributed graphs. Graph D
is the intermediate graph after removing m(L), and
His constructed as gluing of Dand Ralong K(see
[5]). Gp,m
=⇒His called graph transformation.
L
m
(P O1)
K
k
l
oor//
(P O2)
R
m0
G D
g
ooh//H
Obviously, each graph transformation can be considered as graph modifi-
cation by forgetting about the rule and its match. If the rule and its match
are given, the pushout (P O1) has to be constructed as pushout complement.
We recall the definition of a pushout complement as presented in [5]. From an
operational point of view, a pushout complement determines the part in graph
Gthat does not come from L, but includes K.
Definition 3 (PO complement). Given morphisms l:K→Land m:L→
G, then k:K→Dand g:D→Gis the pushout complement (POC) of land
m, if (PO1)in Def. 2 is a pushout.
3 Detection of Operation-Based Conflicts
For the detection of operation-based conflicts, we have to find out the oper-
ation resulting in a particular graph modification. Thus, we have to find a
corresponding rule and match, i.e. a corresponding graph transformation to
the given graph modification. An approach which is always possible is to ex-
tract a minimal rule [6], i.e. a minimal operation which contains all atomic
actions (i.e. creation and deletion of nodes, edges, and attribute values) that
are performed by the given graph modification. Thus, the extraction of a min-
imal rule together with its match leads to a minimal graph transformation
performing a given graph modification.
5
If the operation which led to a graph modification is not known but can
be specified by a graph rule, a suitable method to identify the right operation
is to extract again the minimal rule and to find the corresponding operation
(out of a set of pre-defined operations) by comparing it with the minimal rule.
After having specified graph modifications by graph transformations, the
parallel independence of transformations can be checked and critical situations
are identified as conflicts. These conflicts can be specified as critical pairs [5].
3.1 Extraction of a minimal rule
As first step, we use the construction of minimal rules by Bisztray et al. [6].
This construction yields in a natural way a minimal DPO rule for a graph
modification. Minimal rules contain the proper atomic actions on graphs with
minimal contexts. Bisztray et al. have shown that this construction is unique,
i.e. no smaller rule than the minimal rule can be constructed for a given graph
modification.
Definition 4 (Minimal graph rule and transformation). Rule p= (Ll
←−
Kr
−→ Ris minimal over direct graph modification Gg
←− Dh
−→ Hif the outer
DPO exists and for each
rule L0l0
←− K0r0
−→ R0with injective
morphism K0→Dand pushouts (3)
and (4), there are unique morphisms
L→L0,K→K0, and R→R0such
that the following diagram commutes
and (1), (2), (1) + (3), and (2) +
(4) are pushouts. Graph transforma-
tion Gp
=⇒His also called minimal.
L
(1)
K
l
oor//
(2)
R
L0
(3)
K0
l0
oor0
//
(4)
R0
G D
g
ooh//H
The following minimal rule construction extracts all deletion and creation
actions from a given transformation in graphs L1and R1by constructing so-
called initial pushouts. In a nutshell, an initial pushout extracts a graph mor-
phism consisting of the changing part of the given graph morphism, i.e. the
non-injective mapping part as well as the codomain part that is not in the
image of the morphism (see [5]). This is done for both sides of a graph modifi-
cation, leading to the left and the right-hand sides of the minimal rule. In the
middle, two gluing graphs are constructed which have to be glued together, and
the left and the right-hand sides are potentially extended by further necessary
context.
6
Definition 5 (Initial pushout). Let g:D→Gbe a graph morphism, an
initial pushout over gconsists of graph morphisms c1:C1→G,b1:B1→C1,
and d1:B1→D(cf. diagram below) such that gand c1are a pushout over b1
and d1. For every other pushout over gconsisting of c0
1:C0
1→G,b0
1:B0
1→C0
1,
and injective d0
1:B0
1→D, there are unique graph morphisms b:B1→B0
1and
c:C1→C0
1such that c0
1◦c=c1and b0
1◦b=b1. Moreover, (c, b0
1)is a pushout
over (b1, b).
Note that for graph morphisms, initial pushouts do always exist [5].
Definition 6 (Construction of Minimal Rules from Graph Modifica-
tions). Given a graph modification G←D→H, the minimal rule L←K→
Ris constructed as follows:
1. Construct the initial pushouts (1) of D→Gand (2) of D→H
C1
(1)
B1
!!
C
C
C
C
C
b1
ooB2
}}{
{
{
{
{
//C2
(2)
G D
g
ooh//H
2. Construct the pullback B1←P→B2of B1→D←B2, and then the
pushout B1→K←B2of B1←P→B2, leading to unique injective
morphism K→Dsuch that (3),(4) commute.
P
{{w
w
w
w
w
##
G
G
G
G
G
C1
(1)
B1
##
G
G
G
G
G
b1
oo
(3)
''
B2
{{w
w
w
w
w
//
(4)
ww
C2
(2)
K
G D
g
ooh//H
3. Finally split initial pushouts (1) and (2) by (3) and (4), i.e. construct
pushouts (5) of C1←B1→Kand (6) of K←B2→C2, leading
to pushouts (7) and (8) by pushout decomposition, and the minimal rule
L←K→R.
C1
(5)
B1
##
G
G
G
G
G
b1
ooB2
{{w
w
w
w
w
//C2
(6)
L
(7)
K
oo//
(8)
R
G D
oo//H
The DPO (7),(8) is called minimal transformation of G←D→Hvia the
minimal rule L←K→R.
Proposition 1 (Minimal rule). Given any rule L0←K0→R0which gen-
erates G←D→Hwith injective match via pushouts (1) and (2) below, and
7
the outer diagram is a DPO with minimal rule and minimal transformation.
Then, there are unique injective morphisms L→L0,K→K0and R→R0
such that (3) −(5) commute and (6),(7) are pushouts.
L
A
A
A
A
A
(3)
(6)
K
!!
C
C
C
C
C
oo//
(7)
R
B
B
B
B
B
L0
~~}
}
}
}
}(1)
K0
}}|
|
|
|
|
(4)
oo(5) //
(2)
R0
~~|
|
|
|
|
G D
oo//H
Proof. The proof of Prop. 1 is given in [6]. Note that after Step 1, the minimal
rule extraction may also be considered as E-concurrent rule constructed from
a deletion rule on the left and a creation rule on the right.
Example 2 (Minimal rule construction). The construction of the minimal rule
pAfor graph modification gmA(the refactoring performed by user A in Fig. 2) is
depicted in Fig. 5. Note that the minimal rule does not contain any attributes,
since they are not changed within the graph modification. The minimal rules
Fig. 5. Construction of minimal rule pA= (LA←KA→RA) for gmA
pBfor gmB(the refinement performed by user B in Fig. 3) and pCfor gmC
(the deletion by user C in Fig. 4) are constructed analogously. The results are
8
depicted in Figs. 6 and 7. Note that the initial pushout construction leads to
variables as attribute values of deleted and newly created nodes.
Fig. 6. Minimal rule pBfor graph modification gmB
Fig. 7. Minimal rule pCfor graph modification gmC
Comparing the applications of minimal rules pAand pC, we see that min-
imal rule pCdeletes state S3 that is used by minimal rule pAto perform its
refactoring. Such conflicts are called Delete/Use-conflicts and are defined be-
low. They can be automatically detected using the graph transformation tool
AGG [7].
3.2 Identification of operations
Up to now, we investigated the actual actions performed by different users
which we extracted in minimal rules. This approach does not take any pre-
defined operations into account. Given a set of change operations defined by
graph rules, we can identify the right operation that has been performed for a
graph modification gm by the following method: we extract again the minimal
rule for gm and find the corresponding operation (out of a set of pre-defined
operations) by comparing with the minimal rule. An operation ois executable
wrt. a given graph modification G←− D−→ Hif the extracted minimal rule
is a subrule of operation oand ois applicable to the original graph Gin a
compatible way.
Definition 7 (Subrule). A rule Ls
ls
←− Ks
rs
−→ Rsis a subrule of rule
Ll
←− Kr
−→ Rif morphisms il:Ls→L,ik:Ks→K, and ir:Rs→Rexist
and the diagram on the right commutes and (P O1)and (PO2)are pushouts.
9
Ls
il
(P O1)
Ks
ik
ls
oors//
(P O2)
Rs
ir
L K
l
oor//R
Definition 8 (Minimal rule-related operation execution). Given a min-
imal rule s=Ls
ls
←− Ks
rs
−→ Rsapplicable to graph Gby match ms:Ls→G,
an operation given by rule o=Ll
←− Kr
−→ Ris executable on graph Gwrt.
rule sif sis a subrule of o(as defined in Def. 7) and if ois applicable to G
by a match m:L→Gsuch that m◦il=mswith il:Ls→L.
Note that Def. 8 is useful for identifying single operations per minimal
rule. It cannot be used to identify sequences of operations which relate to one
minimal rule. This problem is left to future work.
Example 3. We define an operation enabling the user to move a state sto an-
other container only if the new container state contains the previous container
state of s. This avoids producing cyclic containments. The operation rule oA
used for graph modification gmAhas more context than its minimal rule (cf.
Fig. 8 for the relation between these two rules where the minimal rule pAis
shown in the upper half and the operation rule oAin the lower half).
Fig. 8. MoveState operation
Once the executed operations have been identified, we can start the conflict
detection also for these rules. Since they can come with more context, more
conflicts might occur compared to the conflict detection based on minimal
rules.
10
3.3 Detection of operation-based conflicts
After having constructed graph transformations from graph modifications by
minimal rule extraction and/or operation rule selection, we can use critical
pairs as presented in [5] to define operation-based conflicts.
First we check if two graph transformations are parallel independent which
means that rule matches overlap in preserved items only.
Definition 9 (Parallel independent transformations). Two direct graph
transformations Gp1,m1
=⇒H1and Gp2,m2
=⇒H2being applications of rules p1=
(L1
l1
←− K1
r1
−→ R1)and p2= (L2
l2
←− K2
r2
−→ R2)at matches m1:L1→G
and m2:L2→Gare parallel independent if the transformations preserve all
items in the intersection of both matches, i.e. m1(L1)∩m2(L2)⊆m1(l1(K1))∩
m2(l2(K2)).
To concentrate on the proper conflict, we abstract from unnecessary context
of identified parallel dependent transformations. This leads to the notion of
acritical pair which is defined below. A critical pair consists of two parallel
dependent transformations starting from a smaller graph Know. Kcan be
considered as a suitable gluing of left-hand sides L1and L2of corresponding
rules. For each two parallel dependent transformations Gp1,m1
=⇒H1and Gp2,m2
=⇒
H2a corresponding critical pair can be found. We consider critical pairs as
operation-based conflicts.
Definition 10 (Critical pair). Acritical pair consists of two parallel depen-
dent graph transformations Kp1,o1
=⇒P1and Kp2,o2
=⇒P2with matches o1:L1→K
and o2:L2→Kbeing jointly surjective.
Proposition 2 (Completeness of critical pairs). Given two direct graph
transformations Gp1,m1
=⇒H1and Gp2,m2
=⇒H2which are parallel dependent, there
is a critical pair Kp1,o1
=⇒P1and Kp2,o2
=⇒P2such that there is a graph morphism
o:K→Gwith o◦o1=m1and o◦o2=m2.
The proof can be found in [5]. Note that this proposition is very useful
to find operation-based conflicts. If the pair of transformations considered is
parallel dependent, we get a critical pair, i.e. an operation-based conflict. By
proposition 2 we know that we get all operation-based conflicts that way.
This formalization enables us to detect so-called Delete/Use conflicts: one
transformation deletes a graph item while the other one reads it. Note that a
particular kind of delete/use conflicts are sometimes called Change/Use con-
flicts. Here, the first transformation changes the value of an attribute, while the
11
second one either changes it too, or just checks its value. Since attribute value
bindings are modeled by edges, attribute value changes involve the deletion of
edges (cf. [5]).
In case we find critical pairs, we can identify the conflict in form of the
minimal context of the critical match overlappings. Note that since we have
given the overlapping of the left-hand sides of the minimal rules already, we
need to check only this overlapping situation for a conflict. This procedure
needs much less effort than the normal critical pair analysis in AGG which
computes all possible contexts.
Example 4. Considering the minimal rules pAand pCin Figs. 5 and 7 applied
to graph Gin Figs. 2 - 4 with the obvious matches, we get a Delete/Use-conflict
based on deletion and usage of state S3.
4 Detection of state-based conflicts
Besides operation-based conflicts, we want to detect state-based conflicts which
can occur in merged modification results. These conflicts occur if a merged
modification result shows some abnormality not present in the modification
results before merging. Detection of state-based conflicts is done by constraint
checking. The constraints may be language-specific, i.e. potentially induced by
the corresponding graph language definition.
In the following, we present a procedure to merge two different graph mod-
ifications to find state-based conflicts. We show that this merge procedure
yields the expected result if there are no operation-based conflicts. Otherwise,
the procedure cannot be performed. Thus, a natural ordering of conflict detec-
tion is
1. to extract minimal rules and analyze minimal transformations for operation-
based conflicts,
2. to find further operation-based conflicts by analyzing operations,
3. to check for state-based conflicts after all operation-based conflicts have
been resolved.
4.1 Merging of graph modifications
To determine the merge graph of two graph modifications, the “least com-
mon denominator” of both modifications is determined. It is called Din the
construction below. Considering both modifications, the least common denom-
inator is extended by all the changes of modifications 1 and 2, first separately
12
in C1and C2, and finally glued together in graph X. (Compare the diagram
in Def. 11.)
Definition 11 (Merging of graph modifications). Given two modifications
Gg1
←− D1
h1
−→ H1and Gg2
←− D2
h2
−→ H2, the merged graph Xand the merged
graph modification G←− D−→ Xcan be constructed as follows:
1. Construct D1
d1
←− Dd2
−→ D2as
pullback of D1
g1
−→ Gg2
←− D2.
2. Construct PO-complements
d0
i:D→Ciand ci:Ci→Hi
from morphisms di:D→Di
and hi:Di→Hifor i= 1,2.
3. Construct C1
x1
−→ Xx2
←− C2
as pushout of C1
d0
1
←− Dd0
2
−→ C2.
4. The merged graph modification
is Gg1◦d1
←− Dx1◦d0
1
−→ X.
G
D1
g199
s
s
s
s
s
s
s
h1
||y
y
y
y
y
(PB)D2
g2
eeK
K
K
K
K
K
K
h2
""
E
E
E
E
E
H1(PO1)D
d1J
J
J
ddJ
Jd2
t
t
t
::
t
t
d0
1t
t
t
zzt
t
td0
2
J
J
J
$$
J
J
J
(PO2)H2
C1
c1
bbE
E
E
E
E
x1%%
K
K
K
K
K
K
K(PO3)C2
c2
<<
y
y
y
y
y
x2
yys
s
s
s
s
s
s
X
Proposition 3 (Existence and uniqueness of merging). The construc-
tion in Def. 11 leads to a unique graph Xand furthermore, unique graph
modification Gg1◦d1
←− Dx1◦d0
1
−→ Xup to isomorphism, if graph transformations
Gp1,m1
=⇒H1and Gp2,m2
=⇒H2with minimal rules p1=L1
l1
←− K1
r2
−→ R1
and p2=L2
l2
←− K2
r2
−→ R2uniquely extracted from graph modifications
Gg1
←− D1
h1
−→ H1and Gg2
←− D2
h2
−→ H2are parallel independent.
Proof. 1. Existence: While pullback and pushouts always exist in the category
of graph and graph morphisms, this is not the case for pushout comple-
ments. We show the existence of pushout complements in P O1and PO2
by contraposition: If the complements P OC1of P O1or P OC2of P O2do
not exist, there is not a morphism L1→D2or a morphism L2→D1.
If POC1does not exist, the gluing condition is not satisfied for d1and h1
(compare Fact 3.11 in [5]). Since h1and d1are injective, this means that the
dangling condition is not satisfied. Thus, there is an edge e∈H1Ewithout
origin in D1but with an adjacent node h1(x) with x∈D1Nand xhas not
an origin in D. Of course, there is g1(x) = y∈G. Since Dis a PB-object,
there does not exist a node in D2being mapped to yby g2.
Since there is an edge e∈H1without origin in D1, it must have an origin in
R1without origin in K1, since a minimal graph transformation is a double
pushout. Moreover, x∈D1has an origin in K1which has an image l∈L1
mapped to y∈G. However, l∈L1cannot be mapped to some node in D2
13
such that it would be mapped to y∈G. Thus, there is not a morphism
n1:L1→D2such that g2◦n1=m1.
Analogously, we can show that there is not a morphism L2→D1, if P OC2
does not exist.
2. Uniqueness: Pullback and pushout constructions are unique up to isomor-
phism. Moreover, POC constructions are unique up to isomorphism, if the
gluing condition is satisfied (compare again Fact 3.11 in [5]).
Example 5 (Merging of graph modifications). The merging construction ap-
plied to gmBand gmC(the refinement and deletion modifications by users B
and C) is depicted in Fig. 9. We see that the merged graph Xat the bottom of
Fig. 9 contains a forbidden situation: state S4 is isolated, i.e. it is not adjacent
to a transition anymore. We want to find such a situation automatically by
checking a graph constraint forbidding any situation where a state is isolated.
Fig. 9. Merging of graph modifications gmBand gmC
14
4.2 Detection of state-based conflicts
Using graph conditions as defined in [8], we can specify well-formedness con-
straints to be checked on the merged graph.
Definition 12 (Graph condition and graph constraint). Agraph con-
dition over graph Gis of the form true or ∃(a, c)where a:P→Cis a graph
morphism and cis a condition over C. Moreover, Boolean formulas over con-
ditions over Pyield conditions over P, i.e. ¬cand ∧j∈Jcjare (Boolean) con-
ditions over Pwhere Jis a finite index set and c,(cj)j∈Jare conditions over
P. Additionally, ∃aabbreviates ∃(a, true),∀(a, c)abbreviates ¬∃(a, ¬c),false
abbreviates ¬true,∨j∈Jcjabbreviates ¬ ∧j∈J¬cj, and c=⇒dabbreviates
¬c∨d.
Every graph morphism satisfies true. A morphism p:P→Gsatisfies
condition ∃(a, c)if there is an injective graph morphism q:C→Gsuch
that q◦a=pand qsatisfies c. A graph Gsatisfies a condition ∃(a, c)if this
condition is satisfied by graph morphism ∅ → G. In the context of graphs,
graph conditions are called graph constraints. The satisfaction of conditions
by graphs and morphisms is extended to Boolean conditions in the usual way.
The notation of graph constraints of the form ∃(a:∅ → G, c) can be
shortened to ∃(G, c) without loss of information. A rule application condition
of the form ¬∃ais usually called negative application condition (see [8]).
Definition 13 (State-based conflict). Given a merged graph modification
as in Def. 11, a state-based conflict (C, H1=⇒X, H2=⇒X)consists of a
graph constraint C, and graph modifications H1=⇒Xand H2=⇒Xsuch
that Cis satisfied by graphs H1and H2but not by X.
Example 6. Fig. 9 shows a merged graph Xthat contains an isolated state
which should not be allowed. This situation can be formalized by a graph
constraint C=∀G0((∃a:G0→G1)∨(∃a:G0→G2)) where G0consists
of a state contained in some other state, and G1and G2show the alternative
required contexts for G0in Fig. 10. Cis satisfied by graphs HBand HCin
Fig. 9, but not by graph X.
Further typical state-based conflicts can occur w.r.t. well-formedness con-
straints in meta models. Consider e.g. the constraint that a transition may
have at most one event. If two graph modifications add an event to the same
transition, then this leads to a state-based conflict after merging.
15
Fig. 10. Graph constraint forbidding isolated states
5 Implementation issues
5.1 AGG
AGG [5] is an integrated development environment for algebraic graph trans-
formation systems. It implements basic concepts and constructions such as
graphs, graph morphisms, matching, and pushouts. On top of these, graph
transformation, a restricted form of graph constraint checking as well as paral-
lel dependency checking of rule applications are supported. This is a solid basis
to implement initial pushouts, pullbacks, and pushout complements as basis
for minimal rule extraction, merging and conflict detection with a convenient
user interface in the near future.
5.2 AMOR.
We now compare the model versioning system AMOR [1] with the formal
definitions presented in this paper.
Model differencing. Before conflicts are detected, the concurrently per-
formed changes have to be determined. In this paper, the modifications are
extracted applying the construction of minimal rules (cf. Def. ??). To identify
executions of predefined operations, it is checked whether the extracted mini-
mal rule is a subrule of a specific predefined operation. In AMOR, all applied
changes are derived by conducting EMF Compare [9]. The resulting difference
model is conceptually equivalent to a minimal graph rule, because it consists
of a match model explicating common elements (cf. Din a graph modification)
and a set of atomic changes describing the differences between Gand H. Exe-
cutions of predefined operations are detected in AMOR by searching for their
specific change patterns in the derived difference model and, subsequently for
each match, by evaluating their pre- and postconditions. Again, this technique
is compliant to the operation identification presented in this paper.
Operation-based conflicts. As proposed in Sect. 3, we check minimal rules
and operations for critical pairs which are considered as operation-based con-
flicts. In AMOR, operation-based conflicts are detected by comparing each
change applied by one user to each change applied by another. If two changes
16
are contradicting, a conflict explicating the contradicting changes is reported.
If further operation executions have been identified before, the preconditions
of this operation are evaluated after all atomic changes of the opposite side are
executed. With this it is checked whether the operation may still be executed
(according to its preconditions) to a model incorporating the opposite changes.
State-based conflicts. These conflicts occur if a merged model bears prohib-
ited conditions. In this paper, such conditions are defined by graph constraints
which are evaluated on the merged graph (cf. Sec. 4.1). According to Propo-
sition 3, this is possible only, if there are no parallel dependent modifications.
In AMOR, the merged model is validated against the metamodel and its OCL
constraints to find state-based conflicts as well. However, the applied merge
differs slightly from the merge presented in this paper, since a merged model
is also created, if parallel dependent changes exist. In such cases, only those
changes are propagated to the merged model which are not parallel dependent
and the user has to manually resolve the operation-based conflicts.
6 Related Work
The main contribution of this work is a formal definition of model versioning
conflicts as basis for automatic conflict detection by using the DPO approach
to graph transformations. Therefore, we distinguish two kinds of related work.
First, we discuss the state-of-the-art of current model versioning systems, and
second, we compare our work to other approaches aiming at the formalization
of model versioning conflicts.
Model Versioning Systems. In the last decades a lot of research has been con-
ducted in the domain of software versioning which is profoundly outlined in
[10,11]. Most of the approaches focus on source code versioning, others fo-
cus on two-way comparison of models [12], but there are also some dedicated
approaches aiming at the versioning of models by a three-way merge. For ex-
ample, Odyssey-VCS [2] supports the versioning of UML models. This system
performs the conflict detection at a very fine-grained level, hence it is able
to merge modifications concerning different model elements or even different
attributes of one model element. EMF Compare [9] is an Eclipse plug-in, for
comparing and merging models independently of the underlying meta model.
CoObRA [4] is integrated in the Fujaba tool suite and logs the changes per-
formed on a model. The modifications performed by the modeler who did the
later commit are replayed on the updated version of the repository. Conflicts
are reported if an operation may not be applied due to a violated precondition.
17
Similar to CoObRA, Unicase [3] also provides three-way merging based on edit
logs.
Although delete/use conflicts and change/use conflicts are captured by all
of these systems, they do not take predefined operations like refactorings and,
consequently, their bigger contexts into account. EMF Compare and Unicase
also miss to detect changes causing state-based conflicts. None of the four men-
tioned systems aims at providing a precise formalization of conflict detection.
Formalization of versioning conflicts. Another category-theoretical approach
which formalizes model versioning is given in [13]. Similarly to our approach,
modifications are considered as spans of morphisms to describe a partial map-
ping of models and model merging is defined by pushout constructions. More-
over, syntactic conflicts such as adding structure to an element which has been
deleted, are identified. This kind of conflicts is very close to our delete/use-
conflicts which we can identify after having extracted minimal rules. In contrast
to [13], we refer to a formal analysis of operation-based conflicts. In addition,
we consider state-based conflict detection. This has been indicated as future
work in [13], where conflict detection based on user-specified operations are
not mentioned at al.
Alanen and Porres [14] define a difference and merge operator for MOF-
based models from a set-theoretical view. Differences are represented by atomic
changes leading from a base version to the working copy. With their approach,
they are able to detect Delete/Use and Change/Use-conflicts, also incorpo-
rating advanced concepts such as ordered features. However, conflicts going
beyond atomic changes as well as state-based conflicts remain undetected.
The approach by Blanc et al. [15,16] detects state-based inconsistencies
using Prolog empowered first-order logics. Structural and methodological con-
straints are formalized in consistency rules as logic formulae over a sequence
of model construction operations. However, they do not consider to detect
operations going beyond atomic changes as it is supported by our approach.
7 Conclusion
Two different kinds of conflicts in model versioning are defined in this pa-
per based on the notion of graph modifications: operation-based and state-
based conflicts. Graph modifications are not necessarily rule-based, but just
describe changes in graphs. Operation-based conflicts are detected by extract-
ing minimal rules from modifications first and selecting pre-defined operation
rules thereafter if possible. As a consequence, we can use the well-known con-
flict characterization for graph transformations based on parallel dependence
18
checking and extraction of critical pairs. The detection of state-based conflicts
builds directly on merged graph modifications and constraint checking.
In this paper, operations are specified simply by rules without additional
application conditions. Several extensions are imaginable here: If operations are
specified by rules with negative application conditions, an additional kind of
conflict can be identified namely Produce/Forbid-conflicts. New parallel inde-
pendence results for rules with more complex application conditions and their
applications are currently elaborated by Habel et al. Moreover, the detection
of operation sequences for minimal rules is left to future work.
Throughout this paper, we concentrate on the formalization of conflict de-
tection. What can conflict resolution mean in this setting? The resolution of
an operation-based conflict means to show the confluence of the corresponding
critical pair (see [5]), while state-based conflicts might be solved by the defini-
tion of repair actions. Usually, different conflict resolutions are possible and it
is up to future work to develop adequate resolution strategies for this formal
setting.
References
1. Brosch, P., Kappel, G., Langer, P., Seidl, M., Wieland, K., Wimmer, M., Kargl, H.: Adaptable
Model Versioning in Action. In: Modellierung 2010. Volume 161 of LNI., GI (2010)
2. Murta, L., Corrˆea, C., Prudˆencio, J.G., Werner, C.: Towards Odyssey-VCS 2: Improvements
over a UML-based Version Control System. In: 2nd Int. Workshop on Comparison and Ver-
sioning of Software Models @ ICSE’08. (2008)
3. K¨ogel, M.: Towards Software Configuration Management for Unified Models. In: Workshop on
Comparison and Versioning of Software Models @ ICSE’08. (2008)
4. Schneider, C., Z¨undorf, A., Niere, J.: CoObRA - A Small Step for Development Tools to
Collaborative Environments. In: Workshop on Directions in Software Engineering Environments
@ ICSE’04. (2004)
5. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transforma-
tion. Monographs in Theoretical Computer Science. Springer (2006)
6. Bisztray, D., Heckel, R., Ehrig, H.: Verification of architectural refactorings: Rule extraction
and tool support. ECEASST 16 (2008)
7. TFS-Group, TU Berlin: AGG. (2009) http://tfs.cs.tu-berlin.de/agg.
8. Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to
nested conditions. Math. Struct. in Comp. Sci. 19(2) (2009) 245–296
9. Brun, C., Pierantonio, A.: Model Differences in the Eclipse Modeling Framework. UPGRADE,
The European Journal for the Informatics Professional (2008)
10. Conradi, R., Westfechtel, B.: Version Models for Software Configuration Management. ACM
Computing Surveys 30(2) (1998) 232–282
11. Mens, T.: A State-of-the-Art Survey on Software Merging. IEEE Transactions on Software
Engineering 28(5) (2002) 449–462
12. Kelter, U., Wehren, J., Niere, J.: A Generic Difference Algorithm for UML Models. In: Software
Engineering 2005. Volume 64 of LNI., GI (2005) 105–116
19
13. Rutle, A., Rossini, A., Lamo, Y., Wolter, U.: A Category-Theoretical Approach to the For-
malisation of Version Control in MDE. In: Fundamental Approaches to Software Engineering
(FASE’09). Volume 5503 of LNCS., Springer (2009) 64–78
14. Alanen, M., Porres, I.: Difference and union of models. In: UML 2003—The Unififed Modeling
Language. Volume 2863 of LNCS., Springer (2003) 2–17
15. Blanc, X., Mounier, I., Mougenot, A., Mens, T.: Detecting model inconsistency through
operation-based model construction. In: ICSE’08—30th Int. Conference on Software Engi-
neering. (2008)
16. Blanc, X., Mougenot, A., Mounier, I., Mens, T.: Incremental Detection of Model Inconsistencies
Based on Model Operations. In: CAiSE’09–21st Int. Conference on Advanced Information
Systems Engineering. (2009)
20
