In model-driven software engineering (MDSE), models are rstclass entities of software development and undergo a complex evolution during their life-cycles. As a consequence, there is a growing need for techniques and tools to support model management activities such as versioning. Traditional versioning systems target text-based artefacts and are not suitable for graph-based structures such as software models. To cope with this problem, a few prototype model versioning systems have been developed. However, a uniform formalisation of model merging, con ict detection and con ict resolution in MDSE is still debated in the literature. In this paper, we propose an approach to constraint-aware model versioning; i.e., an approach that handles constraints in model merging, con ict detection and con ict resolution. The proposed approach is based on the Diagram Predicate Framework (DPF), which is founded on category theory and graph transformation.
Since the beginning of computer science, raising the abstraction level of software systems has been a continuous process. One of the latest steps in this direction has led to the use of modelling languages in software development processes. Software models are abstract representations of software systems that are used to tackle the complexity of present-day software by enabling developers to reason at a higher level of abstraction.
In model-driven software engineering (MDSE), models are rstclass entities of software development and undergo a complex evolution during their life-cycles. As a consequence, there is a growing need for techniques and tools to support model management activities such as versioning.
In optimistic versioning, each developer has a local (or working) copy of a software artefact. These local copies are modi ed independently and in parallel. From time to time, local modi cations are merged. In the centralised approach to optimistic versioning, local modi cations from each developer are merged into a central repository. In the distributed approach, in contrast, local modi cations from each developer are merged into other developers’ local 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 which both versions originated. This technique facilitates con ict detection. In general, con icts may arise when the modi cations are contradictory. They are resolved either manually or—where applicable—automatically.
Mainstream versioning systems, e.g., Subversion [
To cope with this problem, a few prototype model versioning
systems have been developed, e.g., [
In this paper, we describe a formal approach to constraint-aware model versioning based on the Diagram Predicate Framework (DPF) [33, 36]; i.e., a formal approach to model versioning that handles constraints in model merging, con ict detection and conict resolution. In particular, the proposed approach enables the detection, and—where applicable—resolution of syntactic and semantic con icts on constraints. This paper further develops the formalisation of model versioning published in [35, 37]. Compared to the previous work, the theoretical foundation and the underlying techniques are updated to handle constraints. Moreover, new examples are added to illustrate how model merging, con ict detection and con ict resolution are adapted to handle constraints.
The remainder of the paper is structured as follows. Section 2 introduces constraint-aware model versioning through a running example. Section 3 outlines DPF. Section 4 discusses the proposed approach to constraint-aware model versioning, with a particular focus on model merging, con ict detection and con ict resolution for constraints in DPF. In Section 5, the current research in model versioning is summarised. Finally, in Section 6, some concluding remarks and ideas for future work are presented.
This section introduces constraint-aware model versioning. The following example illustrates a common scenario of concurrent development in MDSE. The example is kept simple intentionally, retaining only the details that are relevant for the discussion.
Example 2.1 (Model versioning and con ict detection scenario). Suppose that two developers, Alice and Bob, adopt an optimistic, centralised versioning system to develop an information system for the management of students and universities. Fig. 1 illustrates the interaction between Alice, Bob, and the repository. Fig. 2 shows the di erent versions of the model being developed.
s y n c
V2 t i m m o c
V3 A1
A1 A2 A2
Alice creates a local copy A1 of the model V1 in the repository (see Fig. 2(a)). This is done in a check-out step. She modi es her local copy by adding the node University together with the arrows sUnivs and uStuds. These modi cations take place in an evolution step. Since other developers may have updated the model V1, she needs to synchronise her local copy with the repository to merge other developers’ modi cations. This is done in a synchronisation step. However, no modi cations of the model V1 have been made in the repository while Alice has been modifying it. Hence, the synchronisation is completed without changing her local copy A1. Finally, Alice commits her local copy, which is labelled V2 in the repository (see Fig. 2(b)). This is done in a commit step.
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 repository. This synchronisation is also completed without changing 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 outof-date since it is a copy of the model V2, while the head model in the repository (containing Bob’s modi cations) is V3. She adds the multiplicity constraint [1..4] on the same arrow sUnivs. Then, she synchronises her local copy with the repository. The synchronisation procedure detects con icting modi cations. This is because Alice has added a multiplicity constraint that contradicts the one added by Bob. 3
DPF is a formal diagrammatic speci cation framework founded on
category theory and graph transformation. The interested reader
may consult [
In DPF, a model is represented by a speci cation S. A speci cation S = (S , CS : Σ) consists of an underlying graph S together with a set of atomic constraints CS that are speci ed by means of a predicate signature Σ. A predicate signature Σ = (ΠΣ , α Σ ) consists of a collection of predicates π ∈ ΠΣ , each having an arity (or shape graph) α Σ (π ). An atomic constraint (π , δ ) consists of a predicate π ∈ ΠΣ together with a graph homomorphism δ : α Σ (π ) → S from the arity of the predicate to the underlying graph of a speci cation.
Example 3.1 (Signature and speci cation). Building on Example 2.1, Table 1 shows a signature Σ = (ΠΣ , α Σ ) suitable for objectoriented structural modelling. The rst column of the table shows the predicate symbols. The second and the third columns show the arities of predicates and a proposed visualisation of the corresponding atomic constraints, respectively. Finally, the fourth column presents the semantic interpretation of each predicate.
Proposed vis.
X
f [m..n]
/ Y X [sufrj] / Y
f X i [inv] ) Y g
Semantic interpretation ∀x ∈ X : m ≤ |f (x)| ≤ n, with 0 ≤ m ≤ n and n ≥ 1 ∀y ∈ Y ∃x ∈ X : y ∈ f (x) ∀x ∈ X , ∀y ∈ Y : y ∈ f (x) if and only if x ∈ g(y)
Fig. 3(a) shows a speci cation S = (S , CS : Σ) representing an object-oriented structural model. Fig. 3(b) shows the underlying graph S of the speci cation S, i.e., the graph of S without any atomic constraints.
In S, the nodes Student and University are interpreted as sets Student and U niversity, while the arrows sUnivs, uStuds are interpreted as multi-valued functions sU nivs : Student → ℘(U niversity), etc., where the powerset ℘(U niversity) is the set of all subsets of U niversity, i.e., ℘(U niversity) = {A | A ⊆ U niversity}.
The function sU nivs has cardinality between one and four. In S, this is enforced by the atomic constraint ([mult(1, 4)], δ1) on the arrow sUnivs. This atomic constraint is formulated by the predicate [mult(m, n)] from the signature Σ (see Table 1). Moreover, the function uStuds is surjective. In S, this is enforced by the atomic constraint ([surjective], δ3) on the arrow uStuds. Furthermore, the functions sU nivs and uStuds are inverse of each other; i.e., ∀s ∈ Student and ∀u ∈ U niversity : s ∈ uStuds(u) if and only if u ∈ sU nivs(s). In S, this is enforced by the atomic constraint ([inverse], δ2) on the arrows sUnivs and uStuds.
The semantics of predicates of the signature Σ (see Table 1) is described using the mathematical language of set theory. In an implementation, the semantics of a predicate is typically given by the code of a corresponding validator such that the mathematical and the validator semantics coincide [28].
A semantic interpretation [[..]]Σ of a signature Σ consists of a
mapping that assigns to each predicate symbol π ∈ ΠΣ a set [[π ]]Σ
of graph homomorphisms ι : O → α Σ (π ), called valid instances of
π , where O may vary over all graphs. [[π ]]Σ is assumed to be closed
under isomorphisms. The interested reader may consult [
Example 3.2 (Instance of a speci cation). Building on Example 3.1, Fig. 4(a) shows a valid instance of S, while Fig. 4(b) shows an invalid 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.
UnivAQ : ✈✈✈❥✈❥✈❥✈5 UiB Alessandro rk
X ●●❙●❙❙) ●UniMarburg ●●#
UAM (a)
< UiB ②②②6HVL Adrian②②❧❧❧ ❉❉◗❉◗( ❉UniMarburg ❉ ❉
A!UC (b)
This section introduces the underlying techniques of the proposed approach to constraint-aware model versioning, with a particular focus on model merging, con ict detection and con ict resolution for atomic constraints. The interested reader may consult [33, 35] for a more detailed discussion of model versioning in DPF. In this paper, the di erence between two versions of a speci cation is represented by a di erence speci cation; i.e., a speci cation that contains all common, added, deleted and renamed elements. The motivation behind adopting di erence speci cations is that— as will be clear later—gathering all these elements in one speci cation facilitates the application of transformation rules to detect and resolve con icts.
Due to the diagrammatic nature of speci cations, the representation of di erences such as added, deleted and renamed is expressed by a diagrammatic language. The diagrammatic language for the representation of di erences is given by a label signature Δ, which has the same structure of a signature but no semantic counterpart (see Table 2). A label signature Δ = (ΘΔ , α Δ ) consists of a set of labels θ ∈ ΘΔ , each having an arity α Δ (θ ). Hence, a di erence speci cation D = (D , CD : Σ, AD : Δ) consists of a speci cation D together with a set of annotations AD that are speci ed by means of the label signature Δ (see, e.g., UD and D in Fig. 5).
The underlying graph and the set of atomic constraints of a
difference speci cation are obtained by the pushout construction [
Example 4.1 (Di erence speci cation). Building on Example 2.1, recall that two (or more) developers may modify the same speci cations concurrently. Starting from the base speci cation V2 (see Fig. 2(b)), Bob makes and commits his modi cations so that the head speci cation is now V3 (see Fig. 2(c)). Concurrently, Alice makes (but does not commit) her modi cations so that her local copy is now A2 (see Fig. 2(d)). Next, Alice synchronises her local copy with the head speci cation.
The speci cation UD (see Fig. 5(g)) represents the di erence between Alice’s local copy and the base speci cation. It is calculated using the pushout construction by merging A2 and V2 modulo their commonality speci cation, which contains the unmodied elements from V2 to A2.
Similarly, the speci cation D (see Fig. 5(d)) represents the di
erence between the head speci cation and the base speci cation. It
is calculated using the same pushout construction by merging V3
and V2 modulo their commonality speci cation, which contains
the unmodi ed elements from V2 to V3.
Student
The merge of di erences MD is a speci cation that represents the
concurrent modi cations of two (or more) developers and that is
processed to detect con icts. Con icts are speci ed by con ict
detection rules, which are based on constraint-aware transformation
rules [
A transformation rule t = L o l K r / R consists of three speci cations L, K and R. L and R are the left-hand side and righthand side of the transformation rule, respectively, while K is their interface. L \ l (K) describes the part of a speci cation 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 modi cations are possible. Note that the speci cation morphism l : K → L is injective—not an inclusion—to allow for renaming [33].
An application of transformation rule consists of nding a match for the left-hand side L in a source speci cation S and replacing L with R, leading to a target speci cation S′.
A con ict detection rule consists of a non-deleting transformation rule, where the left-hand side L represents the con ict and the right-hand side R is a speci cation where the con icting elements are annotated. The interface K is equal to L since non-deleting transformation rules do not delete any elements.
Detecting a con ict consists of applying a con ict detection rule by nding a match for the left-hand side L in the merge of di erences MD, leading to a target merge of di erences MD′′ where the con icting elements are annotated.1 Hence, MD is processed by applying all applicable con ict detection rules.
Applying these rules provides a classi cation of the con icts into two kinds, namely traditional con ict and custom con ict. A traditional con ict occurs when concurrent modi cations compete over the same elements of a speci cation; e.g., a part of the underlying graph is deleted while an atomic constraint having the same part as the target is added (dangling atomic constraints). Table 3 (rule g) shows a traditional con ict detection rule for dangling multiplicity constraints. In contrast, a custom con ict occurs when concurrent modi cations lead to contradicting constraints; e.g., two (di erent) multiplicity constraints are added to the same arrow. Table 3 (rule l) shows a custom con ict detection rule for inconsistent multiplicity constraints. Note that these kinds of con icts may include domain-speci c con icts. The proposed approach enables the speci cation of custom con ict detection rules on demand.
The following example illustrates the application of custom conict detection rules.
Example 4.2 (Merge of di erences and custom con ict detection). Building on Example 2.1, Fig. 5(h) shows the merge of di erences MD. It is calculated using the pushout construction on UD, D and their commonality speci cation. Fig. 5(i) shows the merge of differences MD′′ after the application of con ict detection rules.
In MD the atomic constraints ([mult(0, 3)], δ1) and
([mult(1, 4)], δ1) are annotated with <add>[mult(m,n)], which is
visualised by a ++ and green colouring. In MD′′ these atomic
constraints are additionally annotated with <conflict>[mult(m,n)],
which is visualised by a dotted box, according to rule l (see Table 3).
1The choice of the notation MD′′ rather than MD′ will be clear in Section 4.4
(a)V2
Depending on the structure and semantics of the modi cations,
some con icts may be automatically resolved. Several resolution
strategies [
In the merge of di erences MD, we could annotate modi cations from di erent developers with di erent labels so that a conict resolution with priorities could take this information into account. However, in this paper, we abstract from these details and consider resolution patterns without priorities.
Resolving a con ict consists of applying a con ict resolution pattern by nding a match for the left-hand side L in the merge of di erences MD′′ , leading to a target merge of di erences MD′′′ . Hence, in addition to con ict detection rules, the merge of di erences MD is processed by applying all applicable con ict resolution patterns.
To resolve con icts of inconsistent multiplicity constraints, two con ict resolution patterns are de ned. The rst “liberal” pattern bL is to remove the con icting multiplicity constraints and add a constraint that is the union of the two. The second “conservative” pattern bC is to remove the con icting multiplicity constraints and add a constraint that is the intersection of the two. Table 3 shows these con ict resolution patterns.
In bL , according to the semantic interpretation [[[mult(m, n)]]]Σ of the signature Σ (see Table 1), the set of valid instances of the atomic constraint ([mult(min(m1, m2), max (n1, n2))], δ1) ∈ CR is equal to the union of the set of valid instances of the atomic constraints ([mult(m1, n1)], δ1), ([mult(m2, n2)], δ2) ∈ CL . This is justi ed as follows:
([mult(m1, n1)], δ ) ∧ ([mult(m2, n2)], δ ) ≡ ([mult(m2, n2)], δ ) ≡ ([mult(m1, n1)], δ ) ([mult(m2, n1)], δ ) ([mult(m1, n2)], δ ) if if if if m1 ≤ m2 ≤ n2 ≤ n1 m2 ≤ m1 ≤ n1 ≤ n2 m1 ≤ m2 ≤ n1 ≤ n2 m2 ≤ m1 ≤ n2 ≤ n1 ✤❴ ❴ ❴ ❴ ❴++[❴m1.❴.n1]❴ ++❴[m❴2..n❴2] ❴ ❴ ❴✤ ✤❴ X❴ ❴ ❴ ❴ ❴ ❴ f ❴ ❴ ❴ ❴ ❴ / ❴Y ❴✤ ✤❴ ❴ ❴ ❴ ❴++[❴m1.❴.n1]❴ ++❴[m❴2..n❴2] ❴ ❴ ❴✤ ✤❴ X❴ ❴ ❴ ❴ ❴ ❴ f ❴ ❴ ❴ ❴ ❴ / ❴Y ❴✤ X X
K f f / Y / Y
X X
R f ✤❴ ❴ ❴ ❴ ❴ ❴ +❴+[m❴..n]❴ ❴ ❴✤ ✤❴ X❴ ❴ ❴ ❴ -❴-f ❴ ❴ ❴ / ❴Y ❴✤ ✤❴ ❴ ❴ ❴ ❴++[❴m1.❴.n1]❴ ++❴[m❴2..n❴2] ❴ ❴ ❴✤ ✤❴ X❴ ❴ ❴ ❴ ❴ ❴ f ❴ ❴ ❴ ❴ ❴ / ❴Y ❴✤ ++[min(m1,m2)..max(n1,n2)]
f ++[max(m1,m2)..min(n1,n2)] / Y / Y
Similarly, in bC , the set of valid instances of the atomic constraint ([mult(max (m1, m2), min(n1, n2))], δ1) ∈ CR is equal to the intersection of the set of valid instances of the atomic constraints ([mult(m1, n1)], δ1), ([mult(m2, n2)], δ2) ∈ CL . This is justi ed as follows:
([mult(m1, n1)], δ ) ∨ ([mult(m2, n2)], δ ) ≡ ([mult(m1, n1)], δ ) if m1 ≤ m2 ≤ n2 ≤ n1 ≡ ([mult(m2, n2)], δ ) if m2 ≤ m1 ≤ n1 ≤ n2 ([mult(m1, n2)], δ ) if m1 ≤ m2 ≤ n1 ≤ n2 ([mult(m2, n1)], δ ) if m2 ≤ m1 ≤ n2 ≤ n1
Note that the con ict resolution patterns bL and bC can be applied only under the condition that the range of the multiplicity constraints overlap, i.e., if n1 ≥ m2 or m1 ≤ n2. This could be formulated as a positive application condition [21].
The following example illustrates the application of con ict resolution patterns.
Example 4.3 (Con ict resolution). Building on Example 2.1, Fig. 6(i) shows the merge of di erences MD′′ , while Fig.s 6(j) and 6(k) show the merge of di erences MD′′′ after the application of the liberal and conservative con ict resolution patterns, respectively.
In MD′′ the atomic constraints ([mult(0, 3)], δ1) and ([mult(1, 4)], δ1) are annotated with <add>[mult(m,n)] and <conflict>[mult(m,n)]. In MD′′′ these atomic constraints are replaced with a new atomic constraint ([mult(0, 4)], δ1), according to pattern bL , or ([mult(1, 3)], δ1), according to pattern bC (see Table 3). In general, the merge of di erences MD is a valid speci cation by construction, but it may not be in normal form; i.e., single atomic constraints of the speci cation may not express syntactically the constraints that the conjunction of all the atomic constraints implies semantically. Performing con ict detection on a merge of differences that is not in normal form may lead to a speci cation containing false negatives [29]; i.e., containing actual con icts that are not annotated with conflict. Moreover, performing con ict resolution on the merge of di erences that is not in normal form may lead to a speci cation that is also not in normal form.
Intuitively, the normal form is a speci cation N where there exist speci cation morphisms ϕ : N → {MD′′ } to all other possible ways of applying resolution patterns to MD. This speci cation may not always be unique. Therefore, we consider the scenario where we obtain a reasonable normal form, which contains the minimal set of constraints that give the same semantics. The interested reader may refer to [33] for a formal de nition of the normal form.
The following example illustrates an alternative scenario of concurrent development in MDSE, which leads to a merge of di erences MD that is not in normal form.
Example 4.4 (Alternative custom con ict detection). Let us consider a variant of the scenario in Example 2.1. Fig. 7 shows the di erent versions of the speci cation being developed.
In addition to the atomic constraint ([mult(1, 4)], δ1) on the arrow sUnivs, Alice adds the atomic constraints ([surjective], δ3) on the arrows uStuds and ([inverse], δ2) on the arrows sUnivs and uStuds.
Fig. 7(h) shows the merge of di erences MD, Fig. 7(j) shows the merge of di erences MD′′ after the application of con ict detection rules, while Fig.s 7(k) and 7(l) show the merge of di erences MD′′′ after the application of the liberal and conservative con ict resolution patterns, respectively. α([inverse])
a 1
2 b α([mult(0, n)]) 1 a 2
In this paper, the properties of conjunctively connected sets of atomic constraints are described by means of speci cation entailments. A speci cation entailment has the structure Le f t ⊢ Right , where both premise (Le f t ) and conclusion (Right ) are speci cations with the same underlying graph. From a speci cation entailment, one may induce a transformation rule that can be applied to existing speci cations. The interested reader may consult [33, 36] for a more detailed discussion of speci cation entailments.
The following example illustrates the usage of speci cation entailments.
Example 4.5 (Speci cation entailment). Fig. 8 shows a speci cation entailment e = L ⊢ R that expresses the relation between multiplicity and surjectivity constraints.
Table 4 shows the transformation rule t = L o l K r / R induced by the corresponding speci cation entailment e. Fig. 9(b) shows the speci cation S′ = (S ′, CS′ : Σ) after the application of the transformation rule t .
Performing con ict detection on a merge of di erences MD that is not in normal form may lead to a merge of di erences MD′′ containing false negatives or false positives [29]. To ensure that con ict detection and con ict resolution behave as expected, they are performed on a merge of di erences MD in normal form.
In this paper, normalisation consists of a sequence of applications of transformation rules induced by speci cation entailments. More precisely, given a speci cation S = (S , CS : Σ) and a set of transformation rules induced by speci cation entailments, a normalisation consists of a speci cation transformation S ∗ +3 S′ , leading to a normal form S′. Note that the normalisation is assumed to be terminating and con uent; i.e., each speci cation can be transformed to a unique normal form by speci cation transformation. The identi cation of the conditions under which a set of speci cation entailments guarantees termination and con uence of the normalisation is outside the scope of this work (see Section 6).
The following example illustrates the application of normalisation.
Example 4.6 (Normalisation, con ict detection and con ict resolution). Building on Example 4.4, Fig. 10(i) shows the merge of di erences MD′ after the normalisation, Fig. 10(j) shows the merge of di erences MD′′ after the application of con ict detection rules, while Fig.s 10(k) and 10(l) show the merge of di erences MD′′′ after the application of the liberal and conservative con ict resolution patterns, respectively.
The normalisation replaces the atomic constraint ([mult(0, 3)], δ1) in MD with ([mult(1, 3)], δ1) in MD′ . As a consequence, the application of the con ict resolution pattern bL (see Table 3) leads to a merge of di erences MD′′′ that is in normal form.
Model versioning has been greatly discussed in the literature. The
interested reader may consult [
A strand of research within model versioning focuses on the
problem of model merging. Di erent approaches can be found in
the literature:
• In [
With the exception of [
Research has also lead to a number of prototype tools that
support model versioning:
• EMFStore [27] provides a dedicated framework for version
control of EMF models. It is an operation- and graph-based
approach that supports the detection of composite modi
cations.
• Adaptable Model Versioning (AMOR) [
An Eclipse-based modelling environment for DPF is described in [28], while a web-based modelling environment for DPF is presented in [32]. In future work, we may implement prototype support for our approach to model versioning and perform case studies to compare the existing tools with our tool.
An initial attempt in this direction—based on Resource
Description Format (RDF)—is described in [
In this paper, we described a formal approach to model versioning based on DPF. First, we de ned the representation of di erences— i.e., the information added, deleted and renamed—as a set of annotations that are speci ed by means of a label signature. Second, we introduced a synchronisation procedure that includes normalisation, con ict detection and con ict resolution. Transformation rules are used to represent con icts and—where applicable—their resolution patterns. The con ict detection and resolution are then formalised as the application of these transformation rules. Moreover, speci cation entailments are adopted to describe properties of conjunctively connected sets of atomic constraints. The normalisation of a speci cation is then formalised as the embedding of these speci cation entailments to obtain the normal form of a speci cation.
Note that the proposed approach handles constraints in all the steps of the synchronisation, including normalisation, con ict detection and con ict resolution. To the best of our knowledge, this work constitutes the rst attempt to formalise constraint-awareness in model versioning.
Speci cation transformations constitute the basis for normalisation, con ict detection and con ict resolution. In future work, we will analyse termination and con uence in DPF. This will facilitate the identi cation of the conditions under which a set of con ict resolution patterns guarantees that no new con icts are introduced. [15] Zinovy Diskin. 2003. Practical foundations of business system speci cations.
Springer, Chapter Mathematics of UML: Making the Odysseys of UML less dramatic, 145–178. [16] Zinovy Diskin. 2005. Encyclopedia of Database Technologies and Applications.
Information Science Reference, Chapter Mathematics of Generic Speci cations for Model Management I and II, 351–366. [17] Zinovy Diskin and Boris Kadish. 2003. Variable set semantics for keyed generalized sketches: formal semantics for object identity and abstract syntax for conceptual modeling. Data & Knowledge Engineering 47, 1 (2003), 1–59. https://doi.org/10.1016/S0169-023X(03)00047-8 [18] Zinovy Diskin and Boris Kadish. 2005. Encyclopedia of Database Technologies and Applications. Information Science Reference, Chapter Generic Model Management, 258–265. [19] Zinovy Diskin, Boris Kadish, Frank Piessens, and Michael Johnson. 2000. Universal Arrow Foundations for Visual Modeling. In Diagrams 2000: 1st International Conference on Diagrammatic Representation and Inference (Lecture Notes in Computer Science), Michael Anderson, Peter Cheng, and Volker Haarslev (Eds.), Vol. 1889. Springer, 345–360. https://doi.org/10.1007/3-540-44590-0_30 [20] Zinovy Diskin and Uwe Wolter. 2008. A Diagrammatic Logic for ObjectOriented Visual Modeling. In ACCAT 2007: 2nd Workshop on Applied and Computational Category Theory (Electronic Notes in Theoretical Computer Science), Vol. 203/6. Elsevier, 19–41. https://doi.org/10.1016/j.entcs.2008.10.041 [21] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. 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 Di erential File Comparison. 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, Je 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 Speci c (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 Merging. 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 regression 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 Transformation 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, University 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 Control 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