=Paper=
{{Paper
|id=Vol-2245/commitmde_paper_3
|storemode=property
|title=Handling Constraints in Model Versioning
|pdfUrl=https://ceur-ws.org/Vol-2245/commitmde_paper_3.pdf
|volume=Vol-2245
|authors=Alessandro Rossini,Adrian Rutle,Yngve Lamo,Uwe Wolter
|dblpUrl=https://dblp.org/rec/conf/models/RossiniRLW18
}}
==Handling Constraints in Model Versioning==
https://ceur-ws.org/Vol-2245/commitmde_paper_3.pdf
Handling constraints in model versioning
Alessandro Rossini Adrian Rutle
PwC Norway Western Norway University of Applied Sciences
alessandro.rossini@pwc.com aru@hvl.no
Yngve Lamo Uwe Wolter
Western Norway University of Applied Sciences University of Bergen, Norway
yla@hvl.no wolter@ii.uib.no
ABSTRACT which both versions originated. This technique facilitates conflict
In model-driven software engineering (MDSE), models are first- detection. In general, conflicts may arise when the modifications
class entities of software development and undergo a complex evol- are contradictory. They are resolved either manually or—where
ution during their life-cycles. As a consequence, there is a grow- applicable—automatically.
ing need for techniques and tools to support model management Mainstream versioning systems, e.g., Subversion [5] and Git [24],
activities such as versioning. Traditional versioning systems target target text-based artefacts. The underlying techniques such as mer-
text-based artefacts and are not suitable for graph-based structures ging, conflict detection and conflict resolution are based on a per-
such as software models. To cope with this problem, a few pro- line textual comparison [25]. Since the underlying structure of mod-
totype model versioning systems have been developed. However, els is graph-based rather than text-based, these techniques are not
a uniform formalisation of model merging, conflict detection and suitable for such models [1, 2].
conflict resolution in MDSE is still debated in the literature. In this To cope with this problem, a few prototype model versioning
paper, we propose an approach to constraint-aware model version- systems have been developed, e.g., [3, 8]. However, a uniform form-
ing; i.e., an approach that handles constraints in model merging, alisation of model merging, conflict detection and conflict resolu-
conflict detection and conflict resolution. The proposed approach tion in MDSE is still debated in the literature. Research has lead
is based on the Diagram Predicate Framework (DPF), which is foun- to a number of findings in this field [4, 7]. The interested reader
ded on category theory and graph transformation. may consult [9–11, 13, 35, 41, 43] for different approaches to model
merging, conflict detection and conflict resolution. Unfortunately,
KEYWORDS these techniques consider only model elements and their conform-
ance to the corresponding modelling language, e.g., well-formed-
Model-Driven Software Engineering, Model Versioning, Constraints,
ness constraints. However, these techniques should also consider
Category Theory, Graph Transformation, Diagram Predicate Frame-
constraints added to model elements, e.g., multiplicity constraints.
work
Therefore, an interesting challenge is to extend the current tech-
niques by enabling versioning of constraints.
1 INTRODUCTION In this paper, we describe a formal approach to constraint-aware
Since the beginning of computer science, raising the abstraction model versioning based on the Diagram Predicate Framework
level of software systems has been a continuous process. One of (DPF) [33, 36]; i.e., a formal approach to model versioning that
the latest steps in this direction has led to the use of modelling handles constraints in model merging, conflict detection and con-
languages in software development processes. Software models are flict resolution. In particular, the proposed approach enables the
abstract representations of software systems that are used to tackle detection, and—where applicable—resolution of syntactic and se-
the complexity of present-day software by enabling developers to mantic conflicts on constraints. This paper further develops the
reason at a higher level of abstraction. formalisation of model versioning published in [35, 37]. Compared
In model-driven software engineering (MDSE), models are first- to the previous work, the theoretical foundation and the underly-
class entities of software development and undergo a complex evol- ing techniques are updated to handle constraints. Moreover, new
ution during their life-cycles. As a consequence, there is a growing examples are added to illustrate how model merging, conflict de-
need for techniques and tools to support model management activ- tection and conflict resolution are adapted to handle constraints.
ities such as versioning. The remainder of the paper is structured as follows. Section 2
In optimistic versioning, each developer has a local (or working) introduces constraint-aware model versioning through a running
copy of a software artefact. These local copies are modified inde- example. Section 3 outlines DPF. Section 4 discusses the proposed
pendently and in parallel. From time to time, local modifications approach to constraint-aware model versioning, with a particular
are merged. In the centralised approach to optimistic versioning, focus on model merging, conflict detection and conflict resolution
local modifications from each developer are merged into a central for constraints in DPF. In Section 5, the current research in model
repository. In the distributed approach, in contrast, local modifica- versioning is summarised. Finally, in Section 6, some concluding
tions from each developer are merged into other developers’ local remarks and ideas for future work are presented.
copies. In both cases, the merge is performed using a three-way
merging technique [29], which attempts to merge two versions of
a software artefact relying on the common ancestor version from
2 MODEL VERSIONING the repository (containing Bob’s modifications) is V3 . She adds the
This section introduces constraint-aware model versioning. The multiplicity constraint [1..4] on the same arrow sUnivs. Then, she
following example illustrates a common scenario of concurrent de- synchronises her local copy with the repository. The synchronisa-
velopment in MDSE. The example is kept simple intentionally, re- tion procedure detects conflicting modifications. This is because
taining only the details that are relevant for the discussion. Alice has added a multiplicity constraint that contradicts the one
added by Bob.
Example 2.1 (Model versioning and conflict detection scenario).
Suppose that two developers, Alice and Bob, adopt an optimistic, 3 DIAGRAM PREDICATE FRAMEWORK
centralised versioning system to develop an information system
DPF is a formal diagrammatic specification framework founded on
for the management of students and universities. Fig. 1 illustrates
category theory and graph transformation. The interested reader
the interaction between Alice, Bob, and the repository. Fig. 2 shows
may consult [33–36, 38] for a more detailed presentation of the
the different versions of the model being developed.
framework. DPF is an extension of the Generalized Sketches Frame-
V1 V2 V3
work originally developed by Diskin et al. in [14–20]. This section
Repository presents the basic concepts of DPF that are used in the formalisa-
check-out
tion of constraint-aware model versioning.
commit
sync
In DPF, a model is represented by a specification S. A specific-
ation S = (S, C S : Σ) consists of an underlying graph S together
Alice
A1 A1 A2 A2 with a set of atomic constraints C S that are specified by means of a
predicate signature Σ. A predicate signature Σ = (Π Σ , α Σ ) consists
of a collection of predicates π ∈ Π Σ , each having an arity (or shape
Bob graph) α Σ (π ). An atomic constraint (π , δ ) consists of a predicate
B2 B2B3
π ∈ Π Σ together with a graph homomorphism δ : α Σ (π ) → S
from the arity of the predicate to the underlying graph of a spe-
Figure 1: The timeline of the scenario cification.
Example 3.1 (Signature and specification). Building on Example
Alice creates a local copy A1 of the model V1 in the repository 2.1, Table 1 shows a signature Σ = (Π Σ , α Σ ) suitable for object-
(see Fig. 2(a)). This is done in a check-out step. She modifies her oriented structural modelling. The first column of the table shows
local copy by adding the node University together with the arrows the predicate symbols. The second and the third columns show the
sUnivs and uStuds. These modifications take place in an evolution arities of predicates and a proposed visualisation of the correspond-
step. Since other developers may have updated the model V1 , she ing atomic constraints, respectively. Finally, the fourth column pre-
needs to synchronise her local copy with the repository to merge sents the semantic interpretation of each predicate.
other developers’ modifications. This is done in a synchronisation
step. However, no modifications of the model V1 have been made Table 1: The signature Σ
in the repository while Alice has been modifying it. Hence, the
synchronisation is completed without changing her local copy A1 . π ∈ ΠΣ α Σ (π ) Proposed vis. Semantic interpreta-
Finally, Alice commits her local copy, which is labelled V2 in the tion
a f
repository (see Fig. 2(b)). This is done in a commit step. [mult(m, n )] 1 /2 X / Y ∀x ∈ X : m ≤
[m..n] |f (x ) | ≤ n , with 0 ≤
m ≤ n and n ≥ 1
a f
sUnivs [surjective] 1 /2 X / Y ∀y ∈ Y ∃x ∈ X : y ∈
Student Student University [surj]
uStuds
f (x )
(a) V1 (b) V2 a f
&2 )
[inverse] 1 f X i [inv] Y ∀x ∈ X , ∀y ∈ Y : y ∈
g f (x ) if and only if x ∈
b
sUnivs [1..4] sUnivs [0..3] д(y)
Student University Student University
uStuds uStuds
(d) A2 (c) V3
Fig. 3(a) shows a specification S = (S, C S : Σ) representing an
Figure 2: The models V1 , V2 , V3 and A2 object-oriented structural model. Fig. 3(b) shows the underlying
graph S of the specification S, i.e., the graph of S without any
atomic constraints.
Afterwards, Bob checks out a local copy B2 of the model V2
from the same repository. He adds the multiplicity constraint [0..3]
on the arrow sUnivs. Then, he synchronises his local copy with the sUnivs [1..4] sUnivs
Student [inv] University Student University
repository. This synchronisation is also completed without chan- [surj] uStuds uStuds
(a) S (b) S
ging his local copy B2 . Finally, Bob commits his local copy, which
is labelled V3 in the repository (see Fig. 2(c)).
Alice continues to modify her local copy A2 , which is now out- Figure 3: A specification S = (S, C S : Σ) and its underlying
of-date since it is a copy of the model V2 , while the head model in graph S
In S, the nodes Student and University are interpreted as sets 4.1 Representation of differences
Student and U niversity, while the arrows sUnivs, uStuds are inter- In this paper, the difference between two versions of a specifica-
preted as multi-valued functions sU nivs : Student → ℘(U niversi- tion is represented by a difference specification; i.e., a specification
ty), etc., where the powerset ℘(U niversity) is the set of all subsets that contains all common, added, deleted and renamed elements.
of U niversity, i.e., ℘(U niversity) = {A | A ⊆ U niversity}. The motivation behind adopting difference specifications is that—
The function sU nivs has cardinality between one and four. In S, as will be clear later—gathering all these elements in one specific-
this is enforced by the atomic constraint ([mult(1, 4)], δ 1 ) on the ation facilitates the application of transformation rules to detect
arrow sUnivs. This atomic constraint is formulated by the predic- and resolve conflicts.
ate [mult(m, n)] from the signature Σ (see Table 1). Moreover, the Due to the diagrammatic nature of specifications, the representa-
function uStuds is surjective. In S, this is enforced by the atomic tion of differences such as added, deleted and renamed is expressed
constraint ([surjective], δ 3 ) on the arrow uStuds. Furthermore, by a diagrammatic language. The diagrammatic language for the
the functions sU nivs and uStuds are inverse of each other; i.e., representation of differences is given by a label signature ∆, which
∀s ∈ Student and ∀u ∈ U niversity : s ∈ uStuds(u) if and only has the same structure of a signature but no semantic counterpart
if u ∈ sU nivs(s). In S, this is enforced by the atomic constraint (see Table 2). A label signature ∆ = (Θ∆ , α ∆ ) consists of a set of
([inverse], δ 2 ) on the arrows sUnivs and uStuds. labels θ ∈ Θ∆ , each having an arity α ∆ (θ ). Hence, a difference
The semantics of predicates of the signature Σ (see Table 1) is specification D = (D, C D : Σ, AD : ∆) consists of a specification D
described using the mathematical language of set theory. In an im- together with a set of annotations AD that are specified by means
plementation, the semantics of a predicate is typically given by the of the label signature ∆ (see, e.g., UD and D in Fig. 5).
code of a corresponding validator such that the mathematical and
the validator semantics coincide [28].
Table 2: A subset of the signature ∆ for the annotation of
A semantic interpretation [[..]]Σ of a signature Σ consists of a
atomic constraints
mapping that assigns to each predicate symbol π ∈ Π Σ a set [[π ]]Σ
of graph homomorphisms ι : O → α Σ (π ), called valid instances of
θ ∈ ΘΣ α ∆ (θ ) Proposed visual.
π , where O may vary over all graphs. [[π ]]Σ is assumed to be closed
a f
under isomorphisms. The interested reader may consult [36, 38] for [mult(m, n)] 1 /2 X / Y
++[m..n]
a more detailed discussion of the semantics of a specification. a f
[mult(m, n)] 1 /2 X / Y
- -[m..n]
Example 3.2 (Instance of a specification). Building on Example 3.1, ✤❴ ❴ ❴ ❴ ❴ ❴ ✤
a f
Fig. 4(a) shows a valid instance of S, while Fig. 4(b) shows an in- [mult(m, n)] 1 /2 ✤ X [m..n] / Y ✤
❴ ❴ ❴ ❴ ❴ ❴
valid instance of S that violates the atomic constraints
([surjective], δ 3 ) and ([inverse], δ 2 ) since Adrian is associated
with four universities but none of these universities are associated
with Adrian. The underlying graph and the set of atomic constraints of a dif-
ference specification are obtained by the pushout construction [6,
23, 33], which can be regarded as a generalisation of union. In this
paper, we do not provide details of the pushout construction, but
UnivAQ < UiB
✈ ✈: ②②HVL we offer an explanation of its usage by means of the running ex-
✈ UiB ②
✈✈✈❥❥❥5 ②②❧❧❧6 ample.
X ●●❙❙rk ❙)
Alessandro Adrian
❉❉◗◗(
●●UniMarburg
●●
❉❉
UniMarburg
❉❉ Example 4.1 (Difference specification). Building on Example 2.1,
# ! recall that two (or more) developers may modify the same specifi-
UAM AUC
cations concurrently. Starting from the base specification V2 (see
(a) (b)
Fig. 2(b)), Bob makes and commits his modifications so that the
head specification is now V3 (see Fig. 2(c)). Concurrently, Alice
Figure 4: (a) A valid instance of S; (b) An invalid instance of makes (but does not commit) her modifications so that her local
S violating ([surjective], δ 3 ) and ([inverse], δ 2 ) copy is now A2 (see Fig. 2(d)). Next, Alice synchronises her local
copy with the head specification.
The specification UD (see Fig. 5(g)) represents the difference
between Alice’s local copy and the base specification. It is calcu-
4 CONSTRAINT-AWARE MODEL lated using the pushout construction by merging A2 and V2 mod-
VERSIONING ulo their commonality specification, which contains the unmodi-
fied elements from V2 to A2 .
This section introduces the underlying techniques of the pro- Similarly, the specification D (see Fig. 5(d)) represents the differ-
posed approach to constraint-aware model versioning, with a par- ence between the head specification and the base specification. It
ticular focus on model merging, conflict detection and conflict res- is calculated using the same pushout construction by merging V3
olution for atomic constraints. The interested reader may consult and V2 modulo their commonality specification, which contains
[33, 35] for a more detailed discussion of model versioning in DPF. the unmodified elements from V2 to V3 .
4.2 Conflict detection sUnivs
Student University
The merge of differences MD is a specification that represents the uStuds
(a) V2
concurrent modifications of two (or more) developers and that is
processed to detect conflicts. Conflicts are specified by conflict de-
tection rules, which are based on constraint-aware transformation Student
sUnivs ++[1..4]
University Student
sUnivs ++[0..3]
University
rules [33, 36, 38]. uStuds
(g) UD
uStuds
(d) D
l r
A transformation rule t = L o K / R consists of three merge of differences
specifications L, K and R. L and R are the left-hand side and right- ++[0..3]
sUnivs ++[1..4]
conflict
detection
++[0..3]
sUnivs ++[1..4]
hand side of the transformation rule, respectively, while K is their Student
uStuds
University Student
uStuds
University
(h) MD (i) MD''
interface. L \ l(K) describes the part of a specification that is to
be deleted, R \ K describes the part to be added, and K describes
the part that has to exist to apply the rule, in which only renaming Figure 5: The merge of differences MD and the merge of
modifications are possible. Note that the specification morphism l : differences MD ′′ after the application of conflict detection
K → L is injective—not an inclusion—to allow for renaming [33]. rules
An application of transformation rule consists of finding a match
for the left-hand side L in a source specification S and replacing
L with R, leading to a target specification S ′ .
A conflict detection rule consists of a non-deleting transforma- 4.3 Conflict resolution
tion rule, where the left-hand side L represents the conflict and the Depending on the structure and semantics of the modifications,
right-hand side R is a specification where the conflicting elements some conflicts may be automatically resolved. Several resolution
are annotated. The interface K is equal to L since non-deleting strategies [9] may be possible for a given conflict. These strategies
transformation rules do not delete any elements. are specified by conflict resolution patterns, which are based on
Detecting a conflict consists of applying a conflict detection rule transformation rules. A conflict resolution pattern consists of a
by finding a match for the left-hand side L in the merge of differ- transformation rule, where the left-hand side L represents the con-
ences MD, leading to a target merge of differences MD ′′ where flict, the right-hand side R is a specification where the resolution
the conflicting elements are annotated.1 Hence, MD is processed is applied, and K is their interface.
by applying all applicable conflict detection rules. In the merge of differences MD, we could annotate modifica-
Applying these rules provides a classification of the conflicts tions from different developers with different labels so that a con-
into two kinds, namely traditional conflict and custom conflict. A flict resolution with priorities could take this information into ac-
traditional conflict occurs when concurrent modifications compete count. However, in this paper, we abstract from these details and
over the same elements of a specification; e.g., a part of the under- consider resolution patterns without priorities.
lying graph is deleted while an atomic constraint having the same Resolving a conflict consists of applying a conflict resolution
part as the target is added (dangling atomic constraints). Table 3 pattern by finding a match for the left-hand side L in the merge of
(rule g) shows a traditional conflict detection rule for dangling differences MD ′′ , leading to a target merge of differences MD ′′′ .
multiplicity constraints. In contrast, a custom conflict occurs when Hence, in addition to conflict detection rules, the merge of differ-
concurrent modifications lead to contradicting constraints; e.g., two ences MD is processed by applying all applicable conflict resolu-
(different) multiplicity constraints are added to the same arrow. tion patterns.
Table 3 (rule l) shows a custom conflict detection rule for inconsist- To resolve conflicts of inconsistent multiplicity constraints, two
ent multiplicity constraints. Note that these kinds of conflicts may conflict resolution patterns are defined. The first “liberal” pattern
include domain-specific conflicts. The proposed approach enables b L is to remove the conflicting multiplicity constraints and add a
the specification of custom conflict detection rules on demand. constraint that is the union of the two. The second “conservative”
The following example illustrates the application of custom con- pattern bC is to remove the conflicting multiplicity constraints and
flict detection rules. add a constraint that is the intersection of the two. Table 3 shows
these conflict resolution patterns.
Example 4.2 (Merge of differences and custom conflict detection). In b L , according to the semantic interpretation [[[mult(m, n)]]]Σ
Building on Example 2.1, Fig. 5(h) shows the merge of differences of the signature Σ (see Table 1), the set of valid instances of the
MD. It is calculated using the pushout construction on UD, D and atomic constraint ([mult(min(m 1 , m 2 ), max(n 1 , n 2 ))], δ 1 ) ∈ C R is
their commonality specification. Fig. 5(i) shows the merge of dif- equal to the union of the set of valid instances of the atomic con-
ferences MD ′′ after the application of conflict detection rules. straints ([mult(m 1 , n 1 )], δ 1 ), ([mult(m 2 , n 2 )], δ 2 ) ∈ C L . This is
In MD the atomic constraints ([mult(0, 3)], δ 1 ) and justified as follows:
([mult(1, 4)], δ 1 ) are annotated with [mult(m,n)] , which is
visualised by a ++ and green colouring. In MD ′′ these atomic con- ([mult(m 1 , n 1 )], δ ) ∧ ([mult(m 2 , n 2 )], δ ) ≡
straints are additionally annotated with [mult(m,n)] ,
([mult(m 2 , n 2 )], δ ) if m1 ≤ m2 ≤ n2 ≤ n1
which is visualised by a dotted box, according to rule l (see Table 3).
([mult(m 1 , n 1 )], δ )
if m2 ≤ m1 ≤ n1 ≤ n2
≡
([mult(m 2 , n 1 )], δ ) if m1 ≤ m2 ≤ n1 ≤ n2
1 The choice of the notation MD′′ rather than MD′ will be clear in Section 4.4
([mult(m 1 , n 2 )], δ )
if m2 ≤ m1 ≤ n2 ≤ n1
Table 3: The conflict detection rules and resolution patterns for inconsistent multiplicity constraints
Rule L K R
++[m..n] ✤❴ ❴ ❴ ❴ ❴ ❴ ++[m..n]
❴ ❴ ❴ ❴ ❴✤
д X / Y ✤ X / Y ✤
- -f ❴ ❴ ❴ ❴ ❴ -❴-f ❴ ❴ ❴ ❴ ❴
++[m1 ..n1 ] ++[m2 ..n2 ] ✤❴ ❴ ❴ ❴ ❴++[m
❴ 1 ..n
❴ 1 ]❴ ++[m
❴ ❴2 ..n❴2 ] ❴ ❴ ❴ ✤
l X / Y ✤ X / Y ✤
f ❴ ❴ ❴ ❴ ❴ ❴ ❴f❴ ❴ ❴ ❴ ❴ ❴ ❴
✤❴ ❴ ❴ ❴ ❴++[m
❴ 1 ..n
❴ 1 ]❴ ++[m
❴ ❴2 ..n❴2 ] ❴ ❴ ❴ ✤ f ++[min(m1 ,m2 )..max(n1 ,n2 )]
bL ✤ X / Y ✤ X / Y X / Y
❴ ❴ ❴ ❴ ❴ ❴ ❴f❴ ❴ ❴ ❴ ❴ ❴ ❴ f
✤❴ ❴ ❴ ❴ ❴++[m
❴ 1 ..n
❴ 1 ]❴ ++[m
❴ ❴2 ..n❴2 ] ❴ ❴ ❴ ✤ f ++[max(m1 ,m2 )..min(n1 ,n2 )]
bC ✤ X / Y ✤ X / Y X / Y
❴ ❴ ❴ ❴ ❴ ❴ ❴f❴ ❴ ❴ ❴ ❴ ❴ ❴ f
Similarly, in bC , the set of valid instances of the atomic con- 4.4 Normalisation, conflict detection and
straint ([mult(max(m 1 , m 2 ), min(n 1 , n 2 ))], δ 1 ) ∈ C R is equal to conflict resolution
the intersection of the set of valid instances of the atomic con- In general, the merge of differences MD is a valid specification by
straints ([mult(m 1 , n 1 )], δ 1 ), ([mult(m 2 , n 2 )], δ 2 ) ∈ C L . This is construction, but it may not be in normal form; i.e., single atomic
justified as follows: constraints of the specification may not express syntactically the
([mult(m 1 , n 1 )], δ ) ∨ ([mult(m 2 , n 2 )], δ ) ≡ constraints that the conjunction of all the atomic constraints im-
plies semantically. Performing conflict detection on a merge of dif-
([mult(m 1 , n 1 )], δ ) if m1 ≤ m2 ≤ n2 ≤ n1 ferences that is not in normal form may lead to a specification con-
([mult(m 2 , n 2 )], δ )
if m2 ≤ m1 ≤ n1 ≤ n2 taining false negatives [29]; i.e., containing actual conflicts that are
≡
([mult(m 1 , n 2 )], δ ) if m1 ≤ m2 ≤ n1 ≤ n2 not annotated with conflict. Moreover, performing conflict res-
([mult(m 2 , n 1 )], δ )
if m2 ≤ m1 ≤ n2 ≤ n1 olution on the merge of differences that is not in normal form may
Note that the conflict resolution patterns b L and bC can be ap- lead to a specification that is also not in normal form.
plied only under the condition that the range of the multiplicity Intuitively, the normal form is a specification N where there ex-
constraints overlap, i.e., if n 1 ≥ m 2 or m 1 ≤ n 2 . This could be ist specification morphisms ϕ : N → {MD ′′ } to all other pos-
formulated as a positive application condition [21]. sible ways of applying resolution patterns to MD. This specifica-
The following example illustrates the application of conflict res- tion may not always be unique. Therefore, we consider the scen-
olution patterns. ario where we obtain a reasonable normal form, which contains
the minimal set of constraints that give the same semantics. The
Example 4.3 (Conflict resolution). Building on Example 2.1, Fig. 6(i) interested reader may refer to [33] for a formal definition of the
shows the merge of differences MD ′′ , while Fig.s 6(j) and 6(k) normal form.
show the merge of differences MD ′′′ after the application of the The following example illustrates an alternative scenario of con-
liberal and conservative conflict resolution patterns, respectively. current development in MDSE, which leads to a merge of differ-
In MD ′′ the atomic constraints ([mult(0, 3)], δ 1 ) and ences MD that is not in normal form.
([mult(1, 4)], δ 1 ) are annotated with [mult(m,n)] and Example 4.4 (Alternative custom conflict detection). Let us con-
[mult(m,n)] . In MD ′′′ these atomic constraints are re- sider a variant of the scenario in Example 2.1. Fig. 7 shows the
placed with a new atomic constraint ([mult(0, 4)], δ 1 ), according different versions of the specification being developed.
to pattern b L , or ([mult(1, 3)], δ 1 ), according to pattern bC (see In addition to the atomic constraint ([mult(1, 4)], δ 1 ) on the ar-
Table 3). row sUnivs, Alice adds the atomic constraints ([surjective], δ 3 )
on the arrows uStuds and ([inverse], δ 2 ) on the arrows sUnivs
and uStuds.
++[0..3]
sUnivs ++[1..4]
conflict
detection
++[0..3]
sUnivs ++[1..4]
Fig. 7(h) shows the merge of differences MD, Fig. 7(j) shows the
Student
uStuds
University Student
uStuds
University merge of differences MD ′′ after the application of conflict detec-
(h) MD (i) MD''
tion rules, while Fig.s 7(k) and 7(l) show the merge of differences
liberal conflict resolution conservative conflict resolution
MD ′′′ after the application of the liberal and conservative conflict
sUnivs ++[0..4]
University
sUnivs ++[1..3]
University
resolution patterns, respectively.
Student Student
uStuds uStuds
(j) MD''' (k) MD'''
Figure 6: The merge of differences MD ′′ and the merge of
differences MD ′′′ after the application of the conflict resol-
ution patterns
L ⊢ R
sUnivs
Student University α ([mult(0, n)]) α ([mult(1, n)])
uStuds a a
1 2 1 2
(a) V2
α ([inverse]) α ([inverse])
a a
1 2 ⊢ 1 2
sUnivs ++[1..4] sUnivs ++[0..3] b b
Student ++[inv] University Student University
++[surj] uStuds uStuds α ([surjective]) α ([surjective])
a a
(g) UD (d) D 2 1 2 1
merge of differences
δ1 ε1
++[0..3] conflict ++[0..3]
sUnivs ++[1..4] detection sUnivs ++[1..4] δ2 ε2
Student ++[inv] University Student ++[inv] University ε3
δ3
++[surj] uStuds ++[surj] uStuds
(h) MD (j) MD''
liberal conflict resolution conservative conflict resolution
f
sUnivs ++[0..4] sUnivs ++[1..3] X Y
Student ++[inv] University Student ++[inv] University g
++[surj] uStuds ++[surj] uStuds
(k) MD''' (l) MD''' L=R
Figure 8: A specification entailment e = L ⊢ R
Figure 7: The merge of differences MD, the merge of differ-
ences MD ′′ after the application of conflict detection rules
and the merge of differences MD ′′′ after the application of sUnivs [0..4] sUnivs [1..4]
Student [inv] University Student [inv] University
the conflict resolution patterns [surj] uStuds [surj] uStuds
(a) S (b) S'
The application of the conflict resolution pattern b L for incon- Figure 9: The application of the transformation rule t
sistent multiplicity constraints (see Table 3) leads to a merge of
differences MD ′′′ that is not in normal form. In fact, the single
atomic constraint ([mult(0, 4)], δ 1 ) on the arrow sUnivs expresses conflict detection and conflict resolution behave as expected, they
syntactically that the function sU nivs has cardinality between zero are performed on a merge of differences MD in normal form.
and four (see Fig. 7(k)), but the conjunction of all the atomic con- In this paper, normalisation consists of a sequence of applica-
straints ([mult(0, 4)], δ 1 ), ([inverse], δ 2 ) and ([surjective], δ 3 ) tions of transformation rules induced by specification entailments.
implies semantically that the function sU nivs has cardinality be- More precisely, given a specification S = (S, C S : Σ) and a set of
tween one and four. This is justified as follows: transformation rules induced by specification entailments, a nor-
+3 S ′ , ∗
uStuds surjective ⇒ ∀s ∈ Student ∃u ∈ U niversity malisation consists of a specification transformation S
where x ∈ uStuds(y) ′
leading to a normal form S . Note that the normalisation is as-
sU nivs, uStuds inverse ⇒ ∀s ∈ Student ∃u ∈ U niversity sumed to be terminating and confluent; i.e., each specification can
where y ∈ sU nivs(x) be transformed to a unique normal form by specification trans-
sU nivs total ⇒ ∀s ∈ Student : |sU nivs(x)| ≥ 1 formation. The identification of the conditions under which a set of
In this paper, the properties of conjunctively connected sets of specification entailments guarantees termination and confluence
atomic constraints are described by means of specification entail- of the normalisation is outside the scope of this work (see Sec-
ments. A specification entailment has the structure Le f t ⊢ Riдht, tion 6).
where both premise (Le f t) and conclusion (Riдht) are specifica- The following example illustrates the application of normalisa-
tions with the same underlying graph. From a specification entail- tion.
ment, one may induce a transformation rule that can be applied to Example 4.6 (Normalisation, conflict detection and conflict resolu-
existing specifications. The interested reader may consult [33, 36] tion). Building on Example 4.4, Fig. 10(i) shows the merge of differ-
for a more detailed discussion of specification entailments. ences MD ′ after the normalisation, Fig. 10(j) shows the merge of
The following example illustrates the usage of specification en- differences MD ′′ after the application of conflict detection rules,
tailments. while Fig.s 10(k) and 10(l) show the merge of differences MD ′′′
Example 4.5 (Specification entailment). Fig. 8 shows a specific- after the application of the liberal and conservative conflict resol-
ation entailment e = L ⊢ R that expresses the relation between ution patterns, respectively.
multiplicity and surjectivity constraints. The normalisation replaces the atomic constraint ([mult(0, 3)],
l r δ 1 ) in MD with ([mult(1, 3)], δ 1 ) in MD ′ . As a consequence, the
Table 4 shows the transformation rule t = L o K / R in- application of the conflict resolution pattern b L (see Table 3) leads
duced by the corresponding specification entailment e. Fig. 9(b)
′
to a merge of differences MD ′′′ that is in normal form.
shows the specification S ′ = (S ′, C S : Σ) after the application of
the transformation rule t.
Performing conflict detection on a merge of differences MD that
is not in normal form may lead to a merge of differences MD ′′
containing false negatives or false positives [29]. To ensure that
Table 4: The transformation rule t = L ← K ֒→ R induced by the corresponding specification entailment e
Rule L K R
f [0..n] f f [1..n]
) ) )
t X i [inv] Y X i [inv] Y X i [inv] Y
[surj] g [surj] g [surj] g
sUnivs
• The work in [43] presents a formal approach to the three-
University
Student
uStuds
way merging of Ecore [40] models based on set theory and
(a) V2 predicate logic. It is based on formally defined merge rules
that can handle additions, deletions and renames of model
sUnivs ++[1..4] sUnivs ++[0..3] elements as well as moves of contained model elements. Fur-
Student ++[inv] University Student University
++[surj] uStuds uStuds thermore, it detects and resolves conflicting modifications
(g) UD (d) D
merge of differences
of the same element and of different interdependent elements.
Finally, the approach guarantees that the resulting merged
++[0..3]
sUnivs ++[1..4] model is well-formed.
Student ++[inv] University
++[surj] uStuds
(h) MD
• The work in [41] proposes a formal approach to the mer-
normalisation ging of typed attributed graphs based on graph transforma-
++[1..3] conflict ++[1..3]
tions and category theory. In this approach, two kinds of
Student
sUnivs ++[1..4]
++[inv] University
detection
Student
sUnivs ++[1..4]
++[inv] University
conflicts are defined based on the notion of graph modi-
++[surj] uStuds
(i) MD'
++[surj] uStuds
(j) MD'' fications: operation-based and state-based conflicts. On the
liberal conflict resolution conservative conflict resolution one hand, operation-based conflicts are detected by first ex-
sUnivs ++[1..4] sUnivs ++[1..3]
tracting minimal rules from modifications and thereafter, if
Student ++[inv]
++[surj] uStuds
University Student ++[inv]
++[surj] uStuds
University
possible, selecting pre-defined operation rules. Conflict de-
(k) MD''' (l) MD''' tection is then based on the parallel dependence of graph
transformations and extraction of critical pairs. On the other
Figure 10: The merge of differences MD, the merge of differ- hand, state-based conflicts are detected by checking the
ences MD ′ after the normalisation, the merge of differences merged graphs against graph constraints.
MD ′′ after the application of conflict detection rules and the • In [10], the authors propose a technique for obtaining auto-
merge of differences MD ′′′ after the application of the con- matically generated repair plans for a given inconsistent
flict resolution patterns model. Repair plans are sequences of concrete modifications
to be performed on a given model that fix existing incon-
sistencies without introducing new ones. The technique is
5 RELATED WORK based on Praxis, which is a model inconsistency detection
Model versioning has been greatly discussed in the literature. The approach. In Praxis, the model is represented as the sequence
interested reader may consult [4, 7] for a survey and an introduc- of actions executed by the user in order to build it.
tion. • The work in [9] introduces a domain-specific modelling lan-
A strand of research within model versioning focuses on the guage for the definition of weaving models that represent
problem of model merging. Different approaches can be found in patterns of conflicting modifications. Resolution criteria for
the literature: these patterns can be specified through OCL expressions.
• In [13], the authors propose a search-based automated model With the exception of [13], the approaches mentioned above do
merge approach where rule-based design space exploration not take constraints on model elements into account. However, the
is used to search the space of solution candidates that rep- approaches in [10, 41, 43] include checking the well-formedness of
resent conflict-free merged models. Similar to our approach, the result of merging. In future work, we may also explore this
this work takes into consideration certain structural and nu- important dimension in our approach to model versioning.
meric constraints. Research has also lead to a number of prototype tools that sup-
• The work in [12] uses a repair generator to address incon- port model versioning:
sistencies that are produced while merging architectural mod-
els. The work in [11] examines the same issues more thor- • EMFStore [27] provides a dedicated framework for version
oughly and uses search-based techniques. control of EMF models. It is an operation- and graph-based
• In [31], the authors propose to use an artificial intelligence approach that supports the detection of composite modific-
technique of automated planning for resolving inconsisten- ations.
cies—be it due to model merging or due to model editions— • Adaptable Model Versioning (AMOR) [8] is a versioning sys-
through the generation of one or more resolution plans. They tem that can deal with arbitrary modelling languages based
also implement the tool Badger in Prolog, which is a regres- on Ecore. AMOR is built around Subversion to provide a
sion planner generating such plans. centralised approach to optimistic versioning, but reuses an
extended version of EMF Compare [22] for difference calcu- Note that the proposed approach handles constraints in all the
lation. AMOR provides conflict detection features that may steps of the synchronisation, including normalisation, conflict de-
be enhanced with user-defined operations. Moreover, it pro- tection and conflict resolution. To the best of our knowledge, this
vides collaborative conflict resolution features, which allow work constitutes the first attempt to formalise constraint-awareness
the implementation of conflict resolution policies. If the res- in model versioning.
olution is performed manually, it is analysed to derive resol- Specification transformations constitute the basis for normalisa-
ution recommendations for similar situations that occur in tion, conflict detection and conflict resolution. In future work, we
future scenarios. In contrast to our approach, this tool does will analyse termination and confluence in DPF. This will facilitate
not provide a formal treatment of conflict detection and res- the identification of the conditions under which a set of conflict res-
olution. olution patterns guarantees that no new conflicts are introduced.
• Semantically enhanced Model Version Control System
(SMoVer) [3] facilitates the specification of modelling lan-
guage semantics, which is needed for accurate conflict de- REFERENCES
tection. The authors exemplify how semantics can improve [1] Kerstin Altmanninger. 2009. Issues and challenges in model versioning. In iiWAS
the accuracy of conflict detection and how these conflicts 2009: 11th International Conference on Information Integration and Web-based Ap-
plications and Services, Gabriele Kotsis, David Taniar, Eric Pardede, and Ismail
can be presented to modellers. On the one hand, certain Khalil (Eds.). ACM, 8. https://doi.org/10.1145/1806338.1806344
models that are in conflict syntactically may be merged with- [2] Kerstin Altmanninger, Petra Brosch, Philip Langer, Martina Seidl, Konrad Wiel,
out conflicts based on their semantics. On the other hand, and Manuel Wimmer. 2009. Why Model Versioning Research is Needed!? An Ex-
perience Report. In Models and Evolution: Joint MoDSE-MCCM 2010 Workshop on
certain models that are not in conflict syntactically may not Model-Driven Software Evolution and Model Co-Evolution and Consistency Man-
be merged without conflicts based on their semantics. Sim- agement. 1–12.
[3] Kerstin Altmanninger, Wieland Schwinger, and Gabriele Kotsis. 2010. Semantics
ilar to our approach, this tool enables the definition of rules for Accurate Conflict Detection in SMoVer: Specification, Detection and Present-
for conflict detection and resolution based on both syntax ation by Example. International Journal of Enterprise Information Systems 6, 1
and semantics. (2010), 68–84. https://doi.org/10.4018/jeis.2010120206
[4] Kerstin Altmanninger, Martina Seidl, and Manuel Wimmer. 2009. A Survey on
• Epsilon Comparison Language (ECL) and Epsilon Merging Model Versioning Approaches. International Journal of Web Information Systems
Language (EML) [30] provide a rule-based language for com- 5, 3 (2009), 271–304. https://doi.org/10.1108/17440080910983556
paring and merging homogeneous or heterogeneous mod- [5] Apache Subversion. Accessed 2018-08-20. https://subversion.apache.org/
[6] Michael Barr and Charles Wells. 1995. Category Theory for Computing Science
els, respectively. Rules specified in ECL and EML could be (2nd Edition). Prentice Hall.
employed for conflict detection and resolution. [7] Petra Brosch, Gerti Kappel, Philip Langer, Martina Seidl, Konrad Wieland,
and Manuel Wimmer. 2012. An Introduction to Model Versioning. In
SFM 2012: Formal Methods for Model-Driven Engineering—12th International
An Eclipse-based modelling environment for DPF is described School on Formal Methods for the Design of Computer, Communication, and
in [28], while a web-based modelling environment for DPF is presen- Software Systems (Lecture Notes in Computer Science), Marco Bernardo, Vit-
ted in [32]. In future work, we may implement prototype support torio Cortellessa, and Alfonso Pierantonio (Eds.), Vol. 7320. Springer, 336–398.
https://doi.org/10.1007/978-3-642-30982-3_10
for our approach to model versioning and perform case studies to [8] Petra Brosch, Gerti Kappel, Martina Seidl, Konrad Wieland, Manuel Wimmer,
compare the existing tools with our tool. Horst Kargl, and Philip Langer. 2010. Adaptable Model Versioning in Action. In
An initial attempt in this direction—based on Resource Descrip- Modellierung 2010 (Lecture Notes in Informatics), Gregor Engels, Dimitris Karagi-
annis, and Heinrich C. Mayr (Eds.), Vol. 161. GI, 221–236.
tion Format (RDF)—is described in [39]. Moreover, the DPF model- [9] Antonio Cicchetti, Davide Di Ruscio, and Alfonso Pierantonio. 2008. Man-
ling environment utilises Alloy [26] for consistency checking [42]. aging Model Conflicts in Distributed Development. In MoDELS 2008: 11th In-
ternational Conference on Model Driven Engineering Languages and Systems
Alloy could be used to check the satisfiability of the merge of differ- (Lecture Notes in Computer Science), Krzysztof Czarnecki, Ileana Ober, Jean-
ences, which in turn could be used in the process of normalisation Michel Bruel, Axel Uhl, and Markus Völter (Eds.), Vol. 5301. Springer, 311–325.
and conflict detection. https://doi.org/10.1007/978-3-540-87875-9_23
[10] Marcos Aurélio Almeida da Silva, Alix Mougenot, Xavier Blanc, and Reda
Bendraou. 2010. Towards Automated Inconsistency Handling in Design Models.
In CAiSE 2010: 22nd International Conference on Advanced Information Systems
6 CONCLUSION AND FUTURE WORK Engineering (Lecture Notes in Computer Science), Barbara Pernici (Ed.), Vol. 6051.
Springer, 348–362. https://doi.org/10.1007/978-3-642-13094-6_28
In this paper, we described a formal approach to model versioning [11] Hoa Khanh Dam, Alexander Egyed, Michael Winikoff, Alexander Re-
based on DPF. First, we defined the representation of differences— der, and Roberto E. Lopez-Herrejon. 2016. Consistent merging of
i.e., the information added, deleted and renamed—as a set of an- model versions. Journal of Systems and Software 112 (2016), 137–155.
https://doi.org/10.1016/j.jss.2015.06.044
notations that are specified by means of a label signature. Second, [12] Hoa Khanh Dam, Alexander Reder, and Alexander Egyed. 2014. Inconsistency
we introduced a synchronisation procedure that includes normal- Resolution in Merging Versions of Architectural Models. In WICSA 2014: 2014
isation, conflict detection and conflict resolution. Transformation IEEE/IFIP Conference on Software Architecture. IEEE Computer Society, 153–162.
https://doi.org/10.1109/WICSA.2014.31
rules are used to represent conflicts and—where applicable—their [13] Csaba Debreceni, István Ráth, Dániel Varró, Xabier De Carlos, Xabier Mendi-
resolution patterns. The conflict detection and resolution are then aldua, and Salvador Trujillo. 2016. Automated Model Merge by Design Space
Exploration. In FASE 2016: 19th International Conference (Lecture Notes in Com-
formalised as the application of these transformation rules. More- puter Science), Perdita Stevens and Andrzej Wasowski (Eds.), Vol. 9633. Springer,
over, specification entailments are adopted to describe properties 104–121. https://doi.org/10.1007/978-3-662-49665-7_7
of conjunctively connected sets of atomic constraints. The norm- [14] Zinovy Diskin. 2002. Visualization vs. Specification in Diagrammatic Notations:
A Case Study with the UML. In Diagrams 2002: 2nd International Conference
alisation of a specification is then formalised as the embedding of on Diagrammatic Representation and Inference (Lecture Notes in Computer Sci-
these specification entailments to obtain the normal form of a spe- ence), Mary Hegarty, Bertrand Meyer, and N. Hari Narayanan (Eds.), Vol. 2317.
cification. Springer, 112–115. https://doi.org/10.1007/3-540-46037-3_15
[15] Zinovy Diskin. 2003. Practical foundations of business system specifications. [38] Adrian Rutle, Alessandro Rossini, Yngve Lamo, and Uwe Wolter. 2012. A
Springer, Chapter Mathematics of UML: Making the Odysseys of UML less dra- formal approach to the specification and transformation of constraints in
matic, 145–178. MDE. Journal of Logic and Algebraic Programming 81, 4 (2012), 422–457.
[16] Zinovy Diskin. 2005. Encyclopedia of Database Technologies and Applications. https://doi.org/10.1016/j.jlap.2012.03.006
Information Science Reference, Chapter Mathematics of Generic Specifications [39] Hans Georg Schaathun and Adrian Rutle. 2018, to appear. Model-Driven Soft-
for Model Management I and II, 351–366. ware Engineering in the Resource Description Framework: a way to version con-
[17] Zinovy Diskin and Boris Kadish. 2003. Variable set semantics for keyed gen- trol. In NIK 2018: 31st Norsk Informatikkonferanse. BIBSYS Open Journal System.
eralized sketches: formal semantics for object identity and abstract syntax [40] Dave Steinberg, Frank Budinsky, Marcelo Paternostro, and Ed Merks. 2008. EMF:
for conceptual modeling. Data & Knowledge Engineering 47, 1 (2003), 1–59. Eclipse Modeling Framework 2.0 (2nd Edition). Addison-Wesley Professional.
https://doi.org/10.1016/S0169-023X(03)00047-8 [41] Gabriele Taentzer, Claudia Ermel, Philip Langer, and Manuel Wimmer.
[18] Zinovy Diskin and Boris Kadish. 2005. Encyclopedia of Database Technologies 2010. Conflict Detection for Model Versioning Based on Graph Modi-
and Applications. Information Science Reference, Chapter Generic Model Man- fications. In ICGT 2010: 5th International Conference on Graph Transforma-
agement, 258–265. tions (Lecture Notes in Computer Science), Hartmut Ehrig, Arend Rensink,
[19] Zinovy Diskin, Boris Kadish, Frank Piessens, and Michael Johnson. 2000. Uni- Grzegorz Rozenberg, and Andy Schürr (Eds.), Vol. 6372. Springer, 171–186.
versal Arrow Foundations for Visual Modeling. In Diagrams 2000: 1st Interna- https://doi.org/10.1007/978-3-642-15928-2_12
tional Conference on Diagrammatic Representation and Inference (Lecture Notes in [42] Xiaoliang Wang, Adrian Rutle, and Yngve Lamo. 2015. Towards User-Friendly
Computer Science), Michael Anderson, Peter Cheng, and Volker Haarslev (Eds.), and Efficient Analysis with Alloy. In MoDeVVa@MoDELS 2015: 12th Workshop
Vol. 1889. Springer, 345–360. https://doi.org/10.1007/3-540-44590-0_30 on Model-Driven Engineering, Verification and Validation (CEUR Workshop Pro-
[20] Zinovy Diskin and Uwe Wolter. 2008. A Diagrammatic Logic for Object- ceedings), Michalis Famelis, Daniel Ratiu, Martina Seidl, and Gehan M. K. Selim
Oriented Visual Modeling. In ACCAT 2007: 2nd Workshop on Applied and Com- (Eds.), Vol. 1514. CEUR-WS.org, 28–37. http://ceur-ws.org/Vol-1514
putational Category Theory (Electronic Notes in Theoretical Computer Science), [43] Bernhard Westfechtel. 2010. A Formal Approach to Three-Way Merging of EMF
Vol. 203/6. Elsevier, 19–41. https://doi.org/10.1016/j.entcs.2008.10.041 Models. In IWMCP 2010: 1st International Workshop on Model Comparison in Prac-
[21] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. tice. ACM, 31–41. https://doi.org/10.1145/1826147.1826155
2006. Fundamentals of Algebraic Graph Transformation. Springer.
https://doi.org/10.1007/3-540-31188-2
[22] EMF Compare. Accessed 2018-08-20. https://www.eclipse.org/emf/compare/
[23] José Luiz Fiadeiro. 2004. Categories for Software Engineering. Springer.
[24] Git. Accessed 2018-08-20. https://git-scm.com
[25] James W. Hunt and M. D. McIlroy. 1976. An Algorithm for Differential File Com-
parison. Technical Report 41. Bell Laboratories.
[26] Daniel Jackson. 2012. Software abstractions: logic, language, and analysis. MIT
Press.
[27] Maximilian Koegel and Jonas Helming. 2010. EMFStore: a model repository for
EMF models. In ICSE 2010: 32nd ACM/IEEE International Conference on Software
Engineering, Jeff Kramer, Judith Bishop, Premkumar T. Devanbu, and Sebastián
Uchitel (Eds.). ACM, 307–308. https://doi.org/10.1145/1810295.1810364
[28] Yngve Lamo, Xiaoliang Wang, Florian Mantz, Wendy MacCaull, and Adrian
Rutle. 2012. DPF Workbench: A Diagrammatic Multi-Layer Domain Spe-
cific (Meta-)Modelling Environment. In Computer and Information Science,
Roger Lee (Ed.). Studies in Computer Intelligence, Vol. 429. Springer, 37–52.
https://doi.org/10.1007/978-3-642-30454-5_3
[29] Tom Mens. 2002. A State-of-the-Art Survey on Software Mer-
ging. IEEE Transactions on Software Engineering 28, 5 (2002), 449–462.
https://doi.org/10.1109/TSE.2002.1000449
[30] Richard F. Paige, Dimitrios S. Kolovos, Louis M. Rose, Nikolaos Drivalos, and
Fiona A. C. Polack. 2009. The Design of a Conceptual Framework and Technical
Infrastructure for Model Management Language Engineering. In ICECCS 2009:
14th IEEE International Conference on Engineering of Complex Computer Systems.
IEEE Computer Society, 162–171. https://doi.org/10.1109/ICECCS.2009.14
[31] Jorge Pinna Puissant, Ragnhild Van Der Straeten, and Tom Mens.
2015. Resolving model inconsistencies using automated regres-
sion planning. Software and System Modeling 14, 1 (2015), 461–481.
https://doi.org/10.1007/s10270-013-0317-9
[32] Fazle Rabbi, Yngve Lamo, Ingrid Chieh Yu, and Lars Michael Kristensen.
2016. WebDPF: A Web-based Metamodelling and Model Transforma-
tion Environment. In MODELSWARD 2016: 4th International Conference on
Model-Driven Engineering and Software Development, Slimane Hammoudi,
Luís Ferreira Pires, Bran Selic, and Philippe Desfray (Eds.). SciTePress, 87–98.
https://doi.org/10.5220/0005686900870098
[33] Alessandro Rossini. 2011. Diagram Predicate Framework meets Model Versioning
and Deep Metamodelling. Ph.D. Dissertation. Department of Informatics, Univer-
sity of Bergen, Norway.
[34] Alessandro Rossini, Juan de Lara, Esther Guerra, Adrian Rutle, and Uwe Wolter.
2014. A formalisation of deep metamodelling. Formal Aspects of Computing 26,
6 (2014), 1115–1152. https://doi.org/10.1007/s00165-014-0307-x
[35] Alessandro Rossini, Adrian Rutle, Yngve Lamo, and Uwe Wolter. 2010. A
formalisation of the copy-modify-merge approach to version control in
MDE. Journal of Logic and Algebraic Programming 79, 7 (2010), 636–658.
https://doi.org/10.1016/j.jlap.2009.10.003
[36] Adrian Rutle. 2010. Diagram Predicate Framework: A Formal Approach to MDE.
Ph.D. Dissertation. Department of Informatics, University of Bergen, Norway.
[37] Adrian Rutle, Alessandro Rossini, Yngve Lamo, and Uwe Wolter. 2009.
A Category-Theoretical Approach to the Formalisation of Version Con-
trol in MDE. In FASE 2009: 12th International Conference on Fundamental
Approaches to Software Engineering (Lecture Notes in Computer Science),
Marsha Chechik and Martin Wirsing (Eds.), Vol. 5503. Springer, 64–78.
https://doi.org/10.1007/978-3-642-00593-0_5