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 [5] and Git [24], target text-based artefacts. The underlying techniques such as merging, con ict detection and con ict resolution are based on a perline textual comparison [25]. Since the underlying structure of models is graph-based rather than text-based, these techniques are not suitable for such models [1,2].
To cope with this problem, a few prototype model versioning systems have been developed, e.g., [3,8]. However, a uniform formalisation of model merging, con ict detection and con ict resolution in MDSE is still debated in the literature. Research has lead to a number of ndings in this eld [4,7]. The interested reader may consult [9-11, 13, 35, 41, 43] for di erent approaches to model merging, con ict detection and con ict resolution. Unfortunately, these techniques consider only model elements and their conformance to the corresponding modelling language, e.g., well-formedness constraints. However, these techniques should also consider constraints added to model elements, e.g., multiplicity constraints. Therefore, an interesting challenge is to extend the current techniques by enabling versioning of constraints.
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.
The timeline of the scenario Alice creates a local copy A 1 of the model V 1 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 V 1 , 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 V 1 have been made in the repository while Alice has been modifying it. Hence, the synchronisation is completed without changing her local copy A 1 . Finally, Alice commits her local copy, which is labelled V 2 in the repository (see Fig. 2(b)). This is done in a commit step.
Afterwards, Bob checks out a local copy B 2 of the model V 2 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 B 2 . Finally, Bob commits his local copy, which is labelled V 3 in the repository (see Fig. 2(c)).
Alice continues to modify her local copy A 2 , which is now outof-date since it is a copy of the model V 2 , while the head model in the repository (containing Bob's modi cations) is V 3 . 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.
DPF is a formal diagrammatic speci cation framework founded on category theory and graph transformation. The interested reader may consult [33][34][35][36]38] for a more detailed presentation of the framework. DPF is an extension of the Generalized Sketches Framework originally developed by Diskin et al. in [14][15][16][17][18][19][20]. This section presents the basic concepts of DPF that are used in the formalisation of constraint-aware model versioning.
In DPF, a model is represented by a speci cation S. A speci cation S = (S, C S : Σ) consists of an underlying graph S together with a set of atomic constraints C S 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. In S, the nodes Student and University are interpreted as sets Student and U ni ersit , while the arrows sUnivs, uStuds are interpreted as multi-valued functions sU ni s : Student → ℘(U ni ersit ), etc., where the powerset ℘(U ni ersit ) is the set of all subsets of U ni ersit , i.e., ℘(U ni ersit
The function sU ni s 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 ni s and uStuds are inverse of each other; i.e., ∀s ∈ Student and ∀u ∈ U ni ersit : s ∈ uStuds(u) if and only if u ∈ sU ni s(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
Σ is assumed to be closed under isomorphisms. The interested reader may consult [36,38] for a more detailed discussion of the semantics of a speci cation.
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 thatas 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, C D : Σ, A D : ∆) consists of a speci cation D together with a set of annotations A D that are speci ed by means of the label signature ∆ (see, e.g., UD and D in Fig. 5).
Table 2: A subset of the signature ∆ for the annotation of atomic constraints
The underlying graph and the set of atomic constraints of a difference speci cation 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 we o er an explanation of its usage by means of the running example.
Example 4.1 (Di erence speci cation). Building on Example 2.1, recall that two (or more) developers may modify the same specications concurrently. Starting from the base speci cation V 2 (see Fig. 2(b)), Bob makes and commits his modi cations so that the head speci cation is now V 3 (see Fig. 2(c)). Concurrently, Alice makes (but does not commit) her modi cations so that her local copy is now A 2 (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 A 2 and V 2 modulo their commonality speci cation, which contains the unmodied elements from V 2 to A 2 .
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 V 3 and V 2 modulo their commonality speci cation, which contains the unmodi ed elements from V 2 to V 3 .
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 [33,36,38].
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.
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). 1 The choice of the notation MD ′′ rather than MD ′ will be clear in Section 4.4
Depending on the structure and semantics of the modi cations, some con icts may be automatically resolved. Several resolution strategies [9] may be possible for a given con ict. These strategies are speci ed by con ict resolution patterns, which are based on transformation rules. A con ict resolution pattern consists of a transformation rule, where the left-hand side L represents the conict, the right-hand side R is a speci cation where the resolution is applied, and K is their interface.
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 b L is to remove the con icting multiplicity constraints and add a constraint that is the union of the two. The second "conservative" pattern b C 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 b L , 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(m 1 , m 2 ), max(n 1 , n 2 ))], δ 1 ) ∈ C R is equal to the union of the set of valid instances of the atomic constraints ([mult(m 1 , n 1 )], δ 1 ), ([mult(m 2 , n 2 )], δ 2 ) ∈ C L . This is justi ed as follows:
Table 3: The con ict detection rules and resolution patterns for inconsistent multiplicity constraints
Similarly, in b C , the set of valid instances of the atomic constraint ([mult(max(m 1 , m 2 ), min(n 1 , n 2 ))], δ 1 ) ∈ C R is equal to the intersection of the set of valid instances of the atomic constraints ([mult(m 1 , n 1 )], δ 1 ), ([mult(m 2 , n 2 )], δ 2 ) ∈ C L . This is justi ed as follows:
Note that the con ict resolution patterns b L and b C can be applied only under the condition that the range of the multiplicity constraints overlap, i.e., if n 1 ≥ m 2 or m 1 ≤ n 2 . This could be formulated as a positive application condition [21].
The following example illustrates the application of con ict resolution patterns. 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 b L , or ([mult(1, 3)], δ 1 ), according to pattern b C (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. The application of the con ict resolution pattern b L for inconsistent multiplicity constraints (see Table 3) leads to a merge of di erences MD ′′′ that is not in normal form. In fact, the single atomic constraint ([mult(0, 4)], δ 1 ) on the arrow sUnivs expresses syntactically that the function sU ni s has cardinality between zero and four (see Fig. 7(k)), but the conjunction of all the atomic constraints ([mult(0, 4)], δ 1 ), ([inverse], δ 2 ) and ([surjective], δ 3 ) implies semantically that the function sU ni s has cardinality between one and four. This is justi ed as follows:
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 ⊢ Ri ht, where both premise (Le f t) and conclusion (Ri ht) 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.
duced by the corresponding speci cation entailment e. Fig. 9(b) shows the speci cation S ′ = (S ′ , C S ′ : Σ) 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
Figure 9: The application of the transformation rule t 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, C S : Σ) and a set of transformation rules induced by speci cation entailments, a normalisation consists of a speci cation transformation S * C Q 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. 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 b L (see Table 3) leads to a merge of di erences MD ′′′ that is in normal form. The merge of di erences MD, the merge of di erences MD ′ after the normalisation, the merge of di erences MD ′′ after the application of con ict detection rules and the merge of di erences MD ′′′ after the application of the conict resolution patterns
Model versioning has been greatly discussed in the literature. The interested reader may consult [4,7] for a survey and an introduction.
A strand of research within model versioning focuses on the problem of model merging. Di erent approaches can be found in the literature:
• In [13], the authors propose a search-based automated model merge approach where rule-based design space exploration is used to search the space of solution candidates that represent con ict-free merged models. Similar to our approach, this work takes into consideration certain structural and numeric constraints. • The work in [12] uses a repair generator to address inconsistencies that are produced while merging architectural models. The work in [11] examines the same issues more thoroughly and uses search-based techniques.
• In [31], the authors propose to use an arti cial intelligence technique of automated planning for resolving inconsistencies-be it due to model merging or due to model editionsthrough the generation of one or more resolution plans. They also implement the tool Badger in Prolog, which is a regression planner generating such plans.
• The work in [43] presents a formal approach to the threeway merging of Ecore [40] models based on set theory and predicate logic. It is based on formally de ned merge rules that can handle additions, deletions and renames of model elements as well as moves of contained model elements. Furthermore, it detects and resolves con icting modi cations of the same element and of di erent interdependent elements. Finally, the approach guarantees that the resulting merged model is well-formed. • The work in [41] proposes a formal approach to the merging of typed attributed graphs based on graph transformations and category theory. In this approach, two kinds of con icts are de ned based on the notion of graph modications: operation-based and state-based con icts. On the one hand, operation-based con icts are detected by rst extracting minimal rules from modi cations and thereafter, if possible, selecting pre-de ned operation rules. Con ict detection is then based on the parallel dependence of graph transformations and extraction of critical pairs. On the other hand, state-based con icts are detected by checking the merged graphs against graph constraints.
• In [10], the authors propose a technique for obtaining automatically generated repair plans for a given inconsistent model. Repair plans are sequences of concrete modi cations to be performed on a given model that x existing inconsistencies without introducing new ones. The technique is based on Praxis, which is a model inconsistency detection approach. In Praxis, the model is represented as the sequence of actions executed by the user in order to build it. • The work in [9] introduces a domain-speci c modelling language for the de nition of weaving models that represent patterns of con icting modi cations. Resolution criteria for these patterns can be speci ed through OCL expressions.
With the exception of [13], the approaches mentioned above do not take constraints on model elements into account. However, the approaches in [10,41,43] include checking the well-formedness of the result of merging. In future work, we may also explore this important dimension in our approach to model versioning.
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) [8] is a versioning system that can deal with arbitrary modelling languages based on Ecore. AMOR is built around Subversion to provide a centralised approach to optimistic versioning, but reuses an extended version of EMF Compare [22] for di erence calculation. AMOR provides con ict detection features that may be enhanced with user-de ned operations. Moreover, it provides collaborative con ict resolution features, which allow the implementation of con ict resolution policies. If the resolution is performed manually, it is analysed to derive resolution recommendations for similar situations that occur in future scenarios. In contrast to our approach, this tool does not provide a formal treatment of con ict detection and resolution. • Semantically enhanced Model Version Control System (SMoVer) [3] facilitates the speci cation of modelling language semantics, which is needed for accurate con ict detection. The authors exemplify how semantics can improve the accuracy of con ict detection and how these con icts can be presented to modellers. On the one hand, certain models that are in con ict syntactically may be merged without con icts based on their semantics. On the other hand, certain models that are not in con ict syntactically may not be merged without con icts based on their semantics. Similar to our approach, this tool enables the de nition of rules for con ict detection and resolution based on both syntax and semantics.
Language (EML) [30] provide a rule-based language for comparing and merging homogeneous or heterogeneous models, respectively. Rules speci ed in ECL and EML could be employed for con ict detection and resolution.
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 [39]. Moreover, the DPF modelling environment utilises Alloy [26] for consistency checking [42]. Alloy could be used to check the satis ability of the merge of di erences, which in turn could be used in the process of normalisation and con ict detection.
In this paper, we described a formal approach to model versioning based on DPF. First, we de ned the representation of di erencesi.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.