In this chapter, we first discuss a rather informal notion of consistency and its preservation. It is supposed to describe the different dimensions in which consistency and its preservation can be considered to then discuss how correctness can be reasonably defined. After identifying the correctness notion that is relevant in the context of our work, we define a suitable formal notion of consistency. We formally define correctness of different artifacts relevant for that notion of consistency. Finally, we present a refined notion of consistency, which we do not require for the initial overview, but which we later use for several detailed considerations.

This chapter thus constitutes our contribution C 1.1, which is composed of four subordinate contributions: a discussion of consistency notions; a discussion and determination of correctness notions for consistency specifications; a formalization of a relevant correctness notion; and finally a refinement of our consistency notion for later detailed considerations. It answers the following research question:

RQ 1.1: What are relevant notions of correctness in transformation networks and how can they be formalized?

Parts of the contributions in this chapter have been published in previous work [Kla18; Kla+21; Kla+20]. We have motivated and informally derived the correctness notion that we formalize in the following and gave an overview of the goal regarding correctness of transformation networks [Kla18]. We have used a simplified version of the formalization that we introduce in this chapter and especially identified the challenge of orchestration [Kla+21], which is central for the formalization of transformation networks. Finally, we have introduced a fine-grained consistency notion [Kla+20], which is required for detailed statements on compatibility.

### **4.1. Notions of Consistency and its Preservation**

We begin with an informal discussion of different ways to consider consistency and its preservation. This involves intensional and extensional, as well monolithic and modular notions, and different execution strategies.

#### **4.1.1. Intensional and Extensional Consistency Notions**

When we consider a tuple of models, we may intuitively assume it to be consistent if it fulfills some kind of constraints. Defining these constraints to derive or check whether a given tuple of models is consistent constitutes an intensional specification of consistency, because the set that contains all consistent model tuples is intensionally represented by these constraints and can be derived from it. We can consider a set of constraints as a predicate, i.e., a Boolean-valued function , which indicates whether a model tuple ∈ fulfills the constraints : → {true, false}. Then we can say that:

consistent to :⇔ () = true

Alternatively, one can enumerate the (possibly infinite number of) consistent tuples of models. Thus, a model tuple is considered consistent if that enumeration contains it. This constitutes an extensional specification of consistency. Given such an enumeration = { | is consistent}, we can say that:

consistent to :⇔ ∈

Both kinds of specification have equal expressiveness. For each intensional specification, the extensional one can be derived by enumerating all models that fulfill the constraints:

= { | () = true}

An extensional specification can also be transferred to an intensional one by defining constraints that are fulfilled by exactly the enumerated instances:

$$P(\mathfrak{m}) \mapsto \begin{cases} \mathsf{True}, & \text{if } \mathfrak{m} \in E \\ \mathsf{False}, & \text{if } \mathfrak{m} \notin E \end{cases}$$

For us, it will only be relevant that an intensional specification can be transformed into an extensional one.

A developer who defines consistency usually wants to use an intensional specification, as tools like transformation languages allow the specification of constraints rather than enumerating consistent instances. Since there is usually an infinite number of consistent models, he or she cannot explicitly enumerate them but only define constraints that allow to derive them. From a theoretical perspective, however, we prefer to consider extensional specifications, because they allow to directly apply set theory in a concise way. Due to the fact that each intensional specification can be transformed into an extensional one, we can make theoretical statements about extensional specifications that also hold for intensional ones. In the following, we always consider extensional specifications unless otherwise stated. So we define which models are considered consistent in terms of relations, which we also call consistency relations.

#### **4.1.2. Monolithic and Modular Consistency Notions**

Consistency, be it specified intensionally or extensionally, can be considered in an either monolithic or modular way. Having a single specification of consistency for an arbitrary number of models constitutes a monolithic notion of consistency. Like discussed for intensional and extensional consistency specifications, this can be expressed by a tuple of models fulfilling constraints or being contained in a relation. A modular notion of consistency considers several relations for subsets of the relevant metamodels, which together define when models are considered consistent.

For an extensional notion of consistency between three metamodels 1, 2 and 3, a modular specification could manifest in three relations 1,2,1,3 and 2,3 defining the model pairs that are considered consistent. If two models are consistent to one of the relations, we can say that they are locally consistent to that relation. We are, however, interested in whether models are globally consistent to all these relations, so we say:

1,2,3 are consistent :⇔ ⟨1,2⟩ ∈ 1,2 ∧ ⟨1,3⟩ ∈ 1,3 ∧ ⟨2,3⟩ ∈ 2,3 Due to the assumptions of independent development and modular reuse, which we have defined in Subsection 1.3.2, we are interested in a modular notion of consistency. In the example, we have considered a modular notion based on binary relation. Such a modular notion, however, can also be based on multiple multiary relations. But even with multiary relations, modularity is necessary for reasons of independent development and reuse. For reasons of simplicity, we stick to modular notions of binary relations, although most of our considerations can be transferred to multiary ones.

#### **4.1.3. Consistency Preservation**

Consistency preservation is the process of ensuring that models stay consistent. Based on a notion of consistency relations that describe when models are considered consistent, this process ensures that models stay in that relation. If models become changed such they that are not in the relation anymore, consistency preservation updates the models such that they are in that relation again. In consequence, consistency preservation is always relative to relations defining consistency.

Consistency preservation can be considered as a function Cp that takes (potentially inconsistent) models and returns a consistent tuple of models:

Cp : → ∀ ∈ : Cp() is consistent

The definition of is consistent depends on whether we rely on a monolithic or modular notion of consistency. Thus it may require the models to be in one or multiple relations. For example, given a monolithic relation , Cp is supposed to fulfill that:

∀ ∈ : Cp() ∈

Since these functions define how consistency is preserved, we also call them consistency preservation rules.

Like for the proposed notion of consistency, we can also consider consistency preservation in an either monolithic or modular way. With a modular notion of consistency preservation, we may have multiple consistency preservation rules that preserve consistency, each of them for a consistency relation

**Figure 4.1.:** Scenarios for independently executing consistency preservation rules on input models and consecutively executing them on the results of other rules. Circles denote models, lines between models denote fulfilled (solid blue) or violated (dashed red) consistency relations, and arrows between the model states (unidirectional green) denote the conduction of user changes or consistency preservation execution.

that defines consistency for a subset of the involved models. Unlike for the relations defining consistency, which can be evaluated independently to identify whether models are consistent, the functions, i.e., consistency preservation rules, cannot be evaluated independently. If each function is executed independently, each of them returns new models that may need to be merged. This is exemplified in the following scenario, which is also depicted in Figure 4.1. Imagine two functions Cp1,2 and Cp1,3 that preserve consistency for relations 1,2 and 1,3, respectively. Consider the input models ⟨1,2,3⟩ that are not consistent to1,2 and1,3, i.e., ⟨1,2⟩ ∉ 1,2 and ⟨1,3⟩ ∉ 1,3. This can, for example, occur because 1 was changed by a user. Now if we apply the functions independently, we have Cp1,2 (⟨1,2⟩) = ⟨′ 1 ,′ 2 ⟩ ∈ 1,2 and Cp1,3 (⟨1,3⟩) = ⟨′′ 1 ,′ 3 ⟩ ∈ 1,3. It is now unclear how to unify′ 1 and′′ 1 to′′′ 1 , such that ⟨′′′ 1 ,′ 2 ⟩ ∈ 1,2 and ⟨′′′ 1 ,′ 3 ⟩ ∈ 1,3.

An intuitive approach to execute the functions is their composition, i.e., a consecutive execution that does not apply the functions for consistency preservation to the original models but to the models delivered by the previous executions of the functions, which is also exemplarily depicted in Figure 4.1. If we consecutively apply the two given functions, we know that Cp1,2 (⟨1,2⟩) = ⟨′ 1 ,′ 2 ⟩ ∈ 1,2 and Cp1,3 (⟨′ 1 ,3⟩) = ⟨′′ 1 ,′ 3 ⟩ ∈ 1,3. It is, however, unclear whether ⟨′′ 1 ,′ 2 ⟩ ∈ 1,2, so it may be necessary to execute Cp1,2 again. In fact, we need some method to decide in which order and how often the consistency preservation rules are applied to result in a consistent tuple of models. We call this an orchestration. The challenge to find an execution order of transformations without leading to execution cycles has also been identified by Kramer [Kra17, Sec. 3.9].

Even if consistency preservation rules were supposed to only modify one model instead of two, the same problems of unifying changes of their independent execution or orchestrating their consecutive execution occur as soon as there are two sequences of consistency preservation rules that change the same models.

In our work, we follow the approach of orchestrating and consecutively executing consistency preservation rules. The benefits of this approach are twofold. First, there is no additional logic required for unifying the changes performed by independently executed consistency preservation rules. Second, the unification may deliver a model that is not consistent to any of the consistency relations anymore, whereas consecutive execution at least guarantees that the models are consistent to the last applied consistency preservation rule. With this approach, the repeated execution of consistency preservation rules can be seen as a negotiation of a solution by reacting to the changes the other consistency preservation rules performed.

Remark. Finally, every monolithic notion of consistency and its preservation can be considered a special case of a modular notion. Having only one consistency relation and one function that preserves it degrades the problem by making the necessity to perform an orchestration of functions obsolete.

For now, the introduced consistency preservation rules can be any kind of functions that return consistent models. Their realization may, for example, be transformations that define how to react to certain changes for restoring consistency, or constraint solvers that find consistent models by solving

**Figure 4.2.:** Declarative and imperative specification of consistency relations and consistency preservation rules for two metamodels 1 and 2.

consistency constraints. We do not yet need to consider how these functions are realized to derive consistent models, although we later focus on transformation-based approaches.

#### **4.1.4. Declarative and Imperative Specifications**

We have discussed that consistency preservation can be considered as functions, called consistency preservation rules, that preserve consistency according to some relations. In practice, however, one will usually not specify both the consistency relation and the consistency preservation rule that preserves it. Instead, one artifact is given and the other is implied or derived. This leads to the two approaches of declarative and imperative consistency specifications, depending on whether the specification defines how consistency is achieved. The relation between the two approaches regarding a consistency relation and a consistency preservation rule is depicted in Figure 4.2.

As a first option, a developer may only define relations that specify consistency. Functions that preserve these relations can be derived from that. This is called a declarative specification, because it only declares when models are consistent but not how consistency is achieved. In general, there are multiple valid options for deriving a consistency preservation rule from a relation. It can, for example, calculate the result with minimal differences to the input according to some defined metric. Or, especially if there is an intensional specification of the relations, the approach may consider the type of input change and calculate an appropriate change according to the constraints in

the intensional specification. This approach is followed by many declarative transformation languages, such as QVT-R [QVT] or TGGs [Anj+14].

As a second option, a developer can define consistency preservation rules without explicitly specifying the consistency relations to which they preserve consistency. Instead, these functions imply the underlying consistency relations that they preserve, at least if we assume that a consistency preservation rule does not perform changes when the input models are already consistent. Given a function Cp, the relation it preserves is implied by its fixed points: = { | Cp() = }. If a function preserving consistency does not perform any changes, the models are, by definition, consistent. Usually, we will assume that such a function returns consistent models with a single application. Thus, if it does not perform changes when the input models are already consistent, the function is idempotent and then the consistency relation is given by its image, i.e., = { | ∃ ′ : Cp(′ ) = }. This is called an imperative specification, because it declares how consistency can be achieved. Such an approach is followed by many imperative transformation languages, such as QVT-O [QVT].

#### **4.1.5. Consistency Preservation Artifacts**

We have discussed that consistency can be considered in a monolithic or modular way. We have, however, also mentioned that the monolithic case can be considered as a special case of the modular one. For the general case, we thus know from the previous considerations that in a consistency preservation process at least specifications that define consistency, called consistency relations, functions that preserve consistency, called consistency preservation rules, and a function for orchestrating the functions, in the following called orchestration function, are necessary. Finally, we also need a function that applies the consistency preservation rules in the order that is determined by the orchestration function, which we call the application function. To summarize, we consider the following four artifacts necessary to handle consistency preservation.

**Figure 4.3.:** Execution process and artifacts for a modular consistency specification. Central artifacts are annotated in (green) normal font.

We explicitly distinguish the orchestration and the application to be able to make more fine-grained statements about the responsibilities for the orchestration and its actual execution. This is particularly useful to determine the behavior in cases in which no orchestration of transformations that results in consistent models can be found. The process is depicted in Figure 4.3. Given models that are consistent according to some consistency relations and changes to them that lead to inconsistencies, the orchestration function delivers an order of consistency preservation rules, which is used to parametrize the application function that executes these rules in the given order. The result is, in the best case, a model tuple that is consistent to the relations again.

## **4.2. Notions of Correctness for Consistency Specifications**

Before we formally define the above introduced artifacts, such as consistency relations, consistency preservation rules, an orchestration function and an application function, we first discuss different notions of correctness for them. Since there are different dimensions of correctness, we need to clarify which of them is relevant in the context of our research questions and will be defined in the formalization.

#### **4.2.1. Relative Correctness Notions**

The overall objective regarding correctness of consistency preservation is to find models that are actually consistent. Intuitively speaking, artifacts are correct if they fulfill their intended purpose. In our case, this means that consistency relations should consider models consistent whenever they are actually supposed to be considered consistent. Consistency preservation rules should return models that are consistent according to a consistency relation to be considered correct. This also conforms to existing notions of correctness for transformations [Ste10], which realize consistency preservation rules. And finally, the orchestration and application functions should execute the consistency preservation rules such that they yield models that are consistent according to all relations afterwards.

Correctness of an artifact is usually considered with respect to some other specification, be it formally defined or only an informal notion. For example, consistency relations may be considered correct with respect to some informal notion of correctness that is collected by domain experts and requirements engineers. A consistency preservation rule should always be consistent with respect to a consistency relation. As discussed before, this relation may either be defined explicitly and the preservation rule has to be correct with respect to it, or it may be induced by the fixed points of the preservation rule. In the latter case, the consistency preservation rule will always be correct by construction.

#### **4.2.2. Correctness regarding Global Knowledge**

We previously distinguished between monolithic and modular consistency notions. In the above considerations, we have related the artifacts of a modular specification to each other. Another notion of correctness can be defined by relating a modular artifact to a corresponding monolithic artifact. For example, a set of modular consistency relations may be considered correct with respect to a monolithic relation when it considers the same model tuples consistent. For three metamodels 1, 2, 3 with three modular consistency relations 1,2,1,3,2,3 between them, as well as a ternary consistency relation 1,2,3, we could say that 1,2,1,3,2,3 are correct (with respect to 1,2,3) if, and only if,

$$\begin{aligned} \forall m\_1 \in M\_1, m\_2 \in M\_2, m\_3 \in M\_3 &: \left( \langle m\_1, m\_2, m\_3 \rangle \in CR\_{1,2,3} \\ \Leftrightarrow \langle m\_1, m\_2 \rangle \in CR\_{1,2} \land \langle m\_1, m\_3 \rangle \in CR\_{1,3} \land \langle m\_2, m\_3 \rangle \in CR\_{2,3} \right) \end{aligned}$$

We may, analogously, define correctness for consistency preservation rules, an orchestration function, and an application function with respect to a monolithic preservation rule by defining that both deliver the same results for the same inputs or at least return a consistent result in the same cases.

#### **4.2.3. Dimensions of Correctness**

The discussed correctness notions induce two dimensions: First, correctness can be considered between artifacts within a monolithic or modular specification. Second, correctness can be considered between artifacts of a modular specification and corresponding artifacts of a monolithic specification. These dimensions are depicted in Figure 4.4. The former dimension is depicted vertically. Consistency preservation rules need to be correct with respect to their consistency relations. In the modular case, in addition to each preservation rule being locally correct with respect to its relation, the combination of preservation rules by an orchestration and application function must also be globally correct with respect to the combination of all relations. The latter dimension is depicted horizontally. Each modular artifact must be consistent with respect to a corresponding monolithic artifact.

Although correctness of modular with respect to monolithic artifacts can be interesting from a theoretical perspective, its practical relevance is limited.

**Figure 4.4.:** Different notions of correctness for consistency and its preservation. Circles denote metamodels with arrows between them representing consistency relations and consistency preservation rules. Further unidirectional arrows denote different notions of correctness of one or more artifacts with respect to others.

That notion of correctness assumes that there is some kind of global truth that has to be reflected by a modular specification. This, however, has the following two essential drawbacks.

Since this conflicts with our assumption of distributed knowledge about relations and independently developed, modular specifications, we do not further consider this notion of consistency. We focus on correctness between the artifacts of a modular consistency specification. We have discussed this correctness notion as correctness between a modularization level and a global level of consistency specifications in previous work [Kla+19b].

#### **4.2.4. Correctness of Consistency Relations**

The consistency notion that we consider in the following especially requires that consistency preservation rules and the functions to orchestrate and apply them must be correct with respect to consistency relations. This notion does, however, not define when consistency relations are considered correct. One option is to only consider correctness with respect to monolithic artifacts for the case of consistency relations, as we have proposed in previous work [Kla+19b]. This, however, suffers from the discussed drawback of requiring a global notion of consistency. Another notion of correctness would be conformance of the specified relations with what developers expect to be consistent, i.e., a validation of requirements. For example, a consistency relation between UML and Java may only be considered correct if it fulfills some "natural" notion of consistency, as developers know how elements are related because they represent similar things, such as classes, or because a standard like the UML [UML] prescribes it. In this work we do not consider such a correctness notion with respect to external, maybe not formally specified artifacts, as it is part of separate research on requirements engineering and validation.

In consequence, we might say that consistency relations are simply correct by construction. Thus, relations would normatively define what is to be considered consistent. However, a consequence of not assuming a global knowledge of consistency is that different domain experts may have different and even conflicting notions of when models are to be considered consistent. Consider for three metamodel 1, 2, 3 the three modular consistency relations 1,2 = {⟨1,2⟩}, 1,3 = {⟨1,3⟩}, and 2,3 = {⟨2,′ 3 ⟩}. Then there is no triple of models that is considered consistent to all relations. Although we still do not want to assume a global knowledge about consistency to which the modular one must conform, we might say that these relations are incompatible, as we do not want to combine relations that induce an

empty set of consistent model tuples. Identifying an appropriate notion of compatibility and how to check it constitutes RQ 1.2 and will be discussed as our contribution C 1.2 in Chapter 5.

In fact, every set of modular consistency relations induces a monolithic one. The monolithic relation for metamodels 1, . . . , and pairwise relations , is defined by:

$$CR = \{ \langle m\_1, \dots, m\_n \rangle \mid \bigwedge\_{1 \le i < k \le n} \langle m\_i, m\_k \rangle \in CR\_{i,k} \} $$

At least if this induced relation is empty, we probably want to consider the modular relations incompatible, because if no models are considered consistent, we cannot describe any system consistently.

### **4.3. A Formal Notion of Transformation Networks**

We have so far discussed a general notion of consistency and its preservation with a focus on a modular way of specifying it. This notion was introduced in a rather informal way to first be able to discuss correctness notions and determine which notion is relevant for the considerations in this thesis. In the following, we define a formal notion of consistency and its preservation, based on the informal explanation given before. It extends the one we have presented in previous work [Kla+21]. We also give a precise definition of notions for correctness between the artifacts of a modular specification. Furthermore, we now focus on transformation-based approaches, i.e., we consider specifications that transform changes within one or more models into changes in one or more other models, as a specialization of the general notion for consistency preservation used before.

#### **4.3.1. Modular Consistency Specification**

As discussed informally before, an extensional specification of consistency defines a relation between models by enumerating all tuples of models that are considered consistent.

Definition 4.1 (Model-Level Consistency Relation)

Given a tuple of metamodels = ⟨1, . . . , ⟩, a model-level consistency relation is a relation for instances of the metamodels ⊆ = 1 × · · · × .

For a tuple of models ∈ , we say that:

```
 consistent to  :⇔  ∈
```
Otherwise, we call inconsistent to .

We consider a tuple of models consistent if the consistency relation contains it. This conforms to existing consistency definitions for bidirectional transformations [Ste10]. We denote this kind of consistency relation as model-level, because we later need to refine the notion of consistency relations to the level of metaclasses and distinguish them.

If a single relation describes consistency between all relevant models, consistency is defined by means of model tuples being contained in that relation. We call such a relation monolithic. If a relation only defines consistency between some of the relevant models and the global consistency relation is defined by a combination of several such relations, we need an explicit definition of such a modular notion of consistency. For the sake of simplicity, we focus on binary relations as a modular representation of consistency.

Definition 4.2 (Model-Level Consistency)

Let = ⟨1, . . . , ⟩ be metamodels and let , ⊆ × be a binary model-level consistency relation for , ∈ . We say that a model tuple = ⟨1, . . . ,⟩ ∈ is consistent to , if, and only if, the instances of and are in that relation:

 consistent to , :⇔ ⟨ , ⟩ ∈ ,

For a set of binary model-level consistency relations CR for metamodels , we say that a tuple of models ∈ is consistent to CR if, and only if, it is consistent to each consistency relation in that set:

consistent to CR :⇔ ∀ ∈ CR : consistent to

**Figure 4.5.:** A monolithic consistency relation that cannot be expressed by binary relations. Small circles denote models and blue, solid hyperedges relate tuples of consistent models.

The definition states that models are consistent to a set of model-level consistency relations if they are consistent to each relation in that set. Consider, for example, for ∈ the relations 1 = {⟨1,2⟩}, 2 = {⟨2,3⟩}, and 3 = {⟨1,3⟩}. Then the model tuple ⟨1,2,3⟩ is consistent to these relations. These consistency relations are equivalent to a monolithic relation = {⟨1,2,3⟩}, because a model tuple is consistent to exactly when it is consistent to {1,2,3}.

For reasons of simplicity, we assume only one consistency relation between each pair of metamodels. This also includes that there are no two consistency relations , and , for metamodels and , which means that the relations do not have a direction. This assumption is without loss of generality, because two relations between the same metamodels are, independent from their direction, equivalent to only considering their intersection, i.e., only the model pairs that are considered consistent by both relations.

Although in the preceding exemplary case the binary relations are equivalent to a monolithic relation, such an equivalence is not always given. In general, two interesting insights come along with the definition of consistency based on modular relations. First, expressiveness of defining consistency modularly by a set of relations is not equivalent to defining one monolithic relation. Second, a modular definition of consistency can easily contain contradictions, which can lead to an empty tuple of consistent models.

**Figure 4.6.:** Modular consistency relations, which together cannot be fulfilled (left) or which cannot be fulfilled for some of the consistent model pairs (right). Small circles denote models and (blue) lines relate consistent model pairs.

Obviously, combining binary relations has not the same expressiveness as defining a monolithic relation. For example, binary relations cannot express the monolithic relation = {⟨1,2,′ 3 ⟩, ⟨1,′ 2 ,3⟩, ⟨′ 1 ,2,3⟩}, as depicted in Figure 4.5. The binary relations necessarily need to contain ⟨1,2⟩ because ⟨1,2,′ 3 ⟩ ∈ , ⟨1,3⟩ because ⟨1,′ 2 ,3⟩ ∈ , and ⟨2,3⟩ because ⟨′ 1 ,2,3⟩ ∈ . However, this would mean that ⟨1,2,3⟩ is consistent to the binary relations although it is not consistent to the monolithic relation . Thus, using sets of binary relations in contrast to a single monolithic relation reduces expressiveness. Stevens [Ste20b] discusses the property of a multiary relation to be expressible by binary ones as binary-definable in detail. She proposes restrictions to binary relations that may be sufficient and still practical for expressing consistency, such as a notion of binary-implemented relations. We have reasoned the assumption that relations are specified independently and thus modularly, thus we have to accept these theoretic restrictions in expressiveness anyway.

Additionally, it can easily occur that multiple binary relations can be fulfilled by certain models, but no tuple of models exists that is consistent to all of them. Consider the relations 1 = {⟨1,2⟩}, 2 = {⟨2,′ 3 ⟩}, and 3 = {⟨1,3⟩}, which are also depicted at the left of Figure 4.6. Although for each of these relations a consistent pair of models exists, which is exactly the one defined in each relation, no tuple of models exists that fulfills their combination. This example illustrates the worst case, in which no consistent models exist for a set of relations. In other cases, only for some models that are

consistent according to one or some of the relations no model tuple may exist that is consistent to all relations. Consider the relations 1 = {⟨1,2⟩}, 2 = {⟨2,3⟩, ⟨2,′ 3 ⟩}, and 3 = {⟨1,3⟩}, which are also depicted at the right of Figure 4.6. In this case, the tuple ⟨1,2,3⟩ is considered consistent to the relations, but although ⟨2,′ 3 ⟩ ∈ 2 there exists no consistent model tuple containing 3, i.e., there is no ∗ 1 ∈ 1 such that ⟨∗ 1 ,2,′ 3 ⟩ is consistent to all relations.

It is easy to see that one monolithic relation can be equally represented by an arbitrary number of sets of binary relations by simply adding model pairs to these binary relations that are never consistent to the other relations, like we have seen for the pair ⟨2,′ 3 ⟩ in the previous example. This means that the combination of relations can lead to the situation that some models are actually forbidden (like ′ 3 in the example before) due to the combination of consistency relations. Whether such a situation is intended can eventually depend on the semantics of the models and relations, but we will discuss which situations are unintended in general. We have informally discussed this as a notion of compatibility, for which we investigate in Chapter 5 how far this behavior should be expected.

#### **4.3.2. Incremental Consistency Preservation**

While the previous discussion only concerned when models are considered consistent, it is of particular interest to ensure that consistency of models is preserved. We informally introduced such specifications as consistency preservation rules. In the following, we will restrict ourselves to incremental and inductive consistency preservation and give a precise definition for that. This means that we make the following assumptions to the process.

Incrementality is an essential requirement whenever consistency shall be preserved to avoid information loss. Otherwise, if for example Java code is always generated anew after changes to a UML model instead of adapting it incrementally, all implementations of methods in Java get lost every time the UML model is changed. Inductivity, on the other hand, may not be necessary, as consistency preservation rules could also be defined to restore consistency from arbitrarily inconsistent states. We, however, make this assumption to avoid requiring from the consistency preservation rules that they need to be able to process an inconsistent state without knowing which changes introduced it. From a theoretical point of view, we could omit that requirement, but this would make the specification of consistency preservation rules impractically complicated, such that omitting that requirement is not practically relevant anyway.

Like we have discussed for consistency preservation rules in general, incremental preservation rules can be realized in an either monolithic or modular way. A monolithic consistency preservation rule takes a tuple of models that is consistent to a consistency relation and a change to these models, and it returns a tuple of models that is consistent again. In a modular specification of consistency preservation rules, a set of such rules is given of which each preserves consistency of a subset of the given models according to a modular consistency relation. In our case, we consider such rules for two models, each of them restoring consistency according to a binary consistency relation.

In existing terminology for transformations, a consistency preservation rule that restores consistency of models according to a consistency relation in one direction is called directional transformation [Ste10] or consistency restorer [Ste20b]. That terminology usually considers model states instead of changes and defines a consistency preservation rule Cpr for metamodels 1 and 2 to modify the instance of 2 for restoring consistency as:

Cpr : 1 × 2 → 2

This notion, however, has two properties that imply essential drawbacks:

**Figure 4.7.:** Execution of consistency preservation rules of which at least one cannot be unidirectional, because both involved models (circles) have been modified by a user or other consistency preservation rules.

State-based transformations suffer from not knowing which changes were made that led to an inconsistent state, and reconstructing them from the difference between two states is only a heuristic approximation [Dis+11]. This, for example, includes that information about elements that were moved or renamed can potentially not be reconstructed, leading to elements that are deleted and created anew and losing all information that was potentially added to them. Unidirectionality may be reasonable when assuming that only one of the models was modified. In that case, it is sufficient to update the other model to restore consistency. With a modular specification of consistency preservation, however, several consistency preservation rules modifying the same models may need to be executed.

Figure 4.7 depicts an example in which unidirectional consistency preservation rules cannot be applied when used in combination with other such rules. If the depicted consistency preservation rules Cpr1 and Cpr2 are executed first, Cpr3 cannot be unidirectional, because both involved models 1 and 3 have been modified by either the user or another consistency preservation rule. Thus, it is, in general, not possible to only consider changes in one model and unidirectionally propagate them to the other model. In consequence, the preservation rules need to be able to deal with changes performed in both models and, consequentially, need to update both models to reflect the changes in each other.

To be able to combine several consistency preservation rules without the discussed drawbacks, we define a synchronizing rather than a unidirectional notion of them. Those rules can react to changes in both models and produce changes in both models again. This is sometimes also called the capability of handling concurrent modifications (e.g. [Leb+14]). To precisely define this behavior, we introduce a notion of changes and consistency preservation rules, which we also refer to as synchronizing consistency preservation rules.

As motivated before, we base our notion of consistency preservation on changes to explicitly express how an inconsistent state was derived from a previously consistent one. We consider these changes as functions that take a model and return a new one. They are not restricted to a specific model but defined for all instances of a metamodel, because a change is supposed to represent how specific elements are modified, such as adding, removing or modifying them. Thus, they can be applied to any models containing these affected elements. This is also how actual implementations, such as the one in the EMF behave. When elements affected by a change are not present in a model, applying the change may fail. For that reason, we consider the function describing a change to be partial. We denote partiality by returning ⊥ for inputs the function is undefined for.

#### Definition 4.3 (Change)

Given a metamodel , a change is a partial function that takes an instance of that metamodel and returns another one or ⊥:

: → ∪ {⊥}

We denote the identity change, i.e., the one always returning the input model, as id :

id () ≔

We denote the universe of all changes in , i.e., all injective subsets of × , as:

$$\Delta\_M := \{ \delta\_M \subseteq I\_M \times I\_M \mid \forall \langle m\_1, m\_2 \rangle, \langle m\_1, m\_2' \rangle \in \delta\_M : m\_2 = m\_2' \} $$

#### Definition 4.4 (Change Tuple)

For a given metamodel tuple = ⟨1, . . . , ⟩, we denote a tuple of changes to an instance of each metamodel as:

$$
\delta\_{\mathfrak{M}} = \langle \delta\_{M\_1}, \dots, \delta\_{M\_n} \rangle \in \Delta\_{M\_1} \times \dots \times \Delta\_{M\_n}
$$

We define the universe of change tuples in instance tuples of as:

Δ ≔ Δ1 × · · · × Δ

We define the application of a change tuple = ⟨1 , . . . , ⟩ to a model tuple = ⟨1, . . . ,⟩ ∈ as the element-wise application:

 () ≔ ⟨1 (1), . . . , ()⟩

For us, it does not matter how the function behaves in cases in which the encoded change cannot be applied, e.g., because the changed or removed element does not exist. The function may do nothing, i.e., return the identical model, or even be undefined for those models, i.e., be partial and return ⊥. In fact, we do not restrict the actual behavior of a change in any way. It may return an empty model regardless of the input, or it may perform arbitrary changes to different models instead of affecting only specific elements. Since we do not need such restrictions, they are not reflected in the formalism.

With that notion of changes, we can define consistency preservation rules as functions that receive two models and changes to them, and that return new changes to both models. While the general definition does not prescribe this, we assume the resulting changes to include the input changes such that not both of them have to be executed consecutively. This will also be reflected by a correctness notion for such rules.

#### Definition 4.5 (Consistency Preservation Rule)

Let ⊆ 1 ×2 be a binary model-level consistency relation between metamodels 1 and 2. A consistency preservation rule Cpr for the relation is a function:

Cpr : (1 , 2 , Δ1 , Δ2 ) → (Δ1 , Δ2 ) ∪ {⊥} For reasons of practical applicability, the rules need to be partial, as we may not want to require them to be able to process arbitrary models and changes. Like for changes, we denote this partiality by allowing the function to return ⊥. First, this is because we do not require it to produce changes when the input models were not consistent. Second, even if the input models are consistent, it may not be possible to preserve consistency for the given changes. For example, if conflicting changes in both changes are made, i.e., changes that require one of them to be reverted, it may be desired that the consistency preservation rule does not return an unexpected result but to indicate a failure by returning ⊥. Our formalism does not restrict such a behavior, in fact it even allows to always return the same changes or to return changes that always deliver empty models. Finally, it is up to the developer to define reasonable consistency preservation rules and to define in which cases the function does not return a result.

This notion of synchronizing consistency preservation conforms to the definition of synchronizers given by Xiong et al. [Xio+13], which also reflect the case that both models have been modified and can be updated by the consistency preservation rule. They do, however, encode the changes in terms of new model states rather than explicit changes.

To consider a consistency preservation rule correct, it has to return changes that, when applied to the input models, result in models that are consistent according to the model-level consistency relation for which the preservation rule is defined. This conforms to the notion of correctness defined for bidirectional transformations [Ste10] and the notion of consistency given for synchronizers by Xiong et al. [Xio+13].

Definition 4.6 (Consistency Preservation Rule Correctness)

We call a consistency preservation rule Cpr correct if, and only if, it either returns ⊥ or changes that applied to the input models yield models that are consistent to :

$$\begin{aligned} \mathsf{CPn}\_{CR} \text{ correct } & \iff \forall \, m\_1 \in I\_{M\_1}, m\_2 \in I\_{M\_2}, \delta\_{M\_1} \in \Delta\_{M\_1}, \delta\_{M\_2} \in \Delta\_{M\_2}: \\ \forall \, \delta'\_{M\_1} \in \Delta\_{M\_1}, \delta'\_{M\_2} \in \Delta\_{M\_2}: \left(\mathsf{CPn}\_{CR}(m\_1, m\_2, \delta\_{M\_1}, \delta\_{M\_2}) = (\delta'\_{M\_1}, \delta'\_{M\_2})\right) \\ \implies \left(\delta'\_{M\_1}(m\_1), \delta'\_{M\_2}(m\_2)\right) \text{ consistent to CR} \end{aligned}$$

This definition does not restrict how the input and output changes are related. In fact, a valid (and especially correct) consistency preservation rule could always return identity changes. In consequence, the rule would simply revert all input changes to achieve a consistent state. Although this may not be the expected behavior, there is no reason to restrict this behavior by definition. Actually, the developer should specify a preservation rule in a reasonable way, such that it defines an expected behavior.

We have discussed that consistency preservation rules can be derived from consistency relations and that consistency preservation rules can imply the consistency relations by their image, i.e., the set of all models that can be derived by applying the consistency preservation rule to any models and changes for which it is defined. In practice there will only be one of these specifications and the other is implied or derived. We thus define a synchronizing transformation, in extension to bidirectional transformations [Ste10], as an artifact that encapsulates a model-level consistency relation together with a consistency preservation rule, no matter which of them is defined and which is derived or implied.

Definition 4.7 (Synchronizing Transformation)

Let be a model-level consistency relation and Cpr a consistency preservation rule that restores consistency according to that relation. A synchronizing transformation is a pair = ⟨, Cpr ⟩.

We also use the short term transformation for a synchronizing transformation. Correctness of a transformation is then given by correctness of its consistency preservation rule.

Definition 4.8 (Synchronizing Transformation Correctness)

Let = ⟨, Cpr ⟩ be a synchronizing transformation. We say that is correct if, and only if, Cpr is correct according to Definition 4.6:

correct :⇔ Cpr correct

Transformations are usually expected to by hippocratic [Ste10]. This means that a transformation, or more precisely its consistency preservation rule, does not perform any changes if the input changes applied to the input models already yield consistent models. We define the application of hippocraticness to synchronizing transformations as follows.

Definition 4.9 (Hippocratic Synchronizing Transformation)

Let = ⟨, Cpr ⟩ be a transformation for metamodels 1 and 2. We say that is hippocratic if, and only if, it returns the input changes if their application to the input models yields consistent models:

 hippocratic :⇔ ∀1 ∈ 1 ,2 ∈ 2 , 1 ∈ Δ2 , 2 ∈ Δ2 : ( ⟨1 (1), 2 (2)⟩ ∈ ⇒ Cpr (1,2, 1 , 2 ) = (1 , 2 ) )

Although hippocraticness is not a necessary requirement for our considerations in most cases, it is usually a desired property in practice [Ste10]. One benefit of hippocraticness with regards to transformations is given if a transformation is only defined by its consistency preservation rule and thus implies the underlying consistency relation as its fixed points, as discussed in Subsection 4.1.4. Actually, a consistency preservation rule according to our definition does not have fixed points, because the signatures of definition and value set of the function are different due to the models only occurring in the definition set. Transferred to our definition, the consistency relation is implied by iteratively applying the function to each pair of models and changes with the changes delivered by the function until they are not modified by the function anymore. In case that the transformation is correct and hippocratic, it does always deliver changes that yield consistent models already upon its first execution and does not modify them upon further applications, thus the consistency relation is implied by applying the function to each pair of models and changes only once.

In the following, we only refer to transformations rather than consistency relations and consistency preservation rules if the distinction is not necessary. We thus also say that models are consistent to a transformation, which is supposed to mean that they are consistent to the consistency relation encapsulated by that transformation.

Definition 4.10 (Consistency to Transformation)

Let = ⟨, Cpr ⟩ be a synchronizing transformation. We say that a tuple of models is consistent to if, and only if, it is consistent to its consistency relation:

```
 consistent to  :⇔  consistent to
```
For a set of transformations t, we say that a model tuple is consistent to t if, and only if, it is consistent to all transformations in it:

consistent to t :⇔ ∀ ∈ t : consistent to

Although Definition 4.8 precisely defines correctness of a transformation, it is unclear how to define a transformation that fulfills that property. In particular, most existing transformation languages are restricted to input changes to one model or to delivering changes to one model. We thus discuss how we can achieve a correct synchronizing transformation with such a restricted formalism. This question was introduced as RQ 1.3, and an approach for that constitutes our contribution C 1.3, which we discuss in Chapter 6.

#### **4.3.3. Transformation Orchestration**

Preserving consistency between instances of multiple metamodels after changes with multiple transformations requires their orchestration, i.e., the decision in which order to execute them. We have discussed in Subsection 4.1.3 that transformations, or more precisely their consistency preservation rules, may be executed independently, which requires their results to be unified, or to execute them consecutively. We have identified the drawbacks of concurrent execution, including the necessity to define unification operators and the missing guarantee of consistency after unification. This is why we follow the approach of consecutively executing transformations.

To consecutively execute transformations, an execution order has to be determined. While in practice a dynamic algorithm will determine that order, from a theoretical perspective that algorithm realizes a function that returns the execution order. We call this an orchestration function, as it is responsible for orchestrating the transformation execution.

Definition 4.11 (Transformation Orchestration Function)

Let t be a set of transformations for metamodels . A transformation orchestration function Orct for these transformations is a function that delivers a sequence of transformations for given models and changes:

Orct : (, Δ) → t <N

t <N denotes all finite sequences in t, i.e., t <N ≔ ⋃∞ =0 t

The orchestration function returns a sequence of transformations and determines that their consistency preservation rules need to be executed in the given order. This especially includes that transformations may occur more than once in such a sequence.

Without further restrictions to the transformations, an orchestration function may not always find an execution order that yields a consistent model tuple for given transformations, models, and changes to them. Such an order may not exist, because due to the transformations making local decisions to restore consistency for two models that are never consistent with the other transformations. Additionally, even if such an order exists, it may not be possible to find it. We discuss these problems in detail in Chapter 7 and prove that the decision problem whether an orchestration that leads to a consistent result exists is undecidable without further restrictions. For that reason, the definition does not require that an orchestration of transformations has to lead to a consistent result.

An orchestration function only determines an order of transformations. Consistency for given models and changes can be preserved by requesting an orchestration from that function and executing the transformations in that order. We make this process explicit by defining an application function that performs consistency preservation based on given transformations, an orchestration function for them and the actual models and changes.

Before defining that application function, we first need to define an auxiliary function to concatenate transformations, more precisely their contained consistency preservation rules. Consistency preservation rules according to Definition 4.5 are restricted to the two metamodels they are defined for. Additionally, they require initial models and changes as input, but only return changes. For these two reasons, the functions describing the preservation

rules cannot be easily concatenated. This, however, is necessary to compose them to formally describe their consecutive execution. We define a generalization function for transformations, which generalizes them to arbitrary metamodel tuples and a conforming signature for their input and output, which eases the description of their concatenation.

 A transformation generalization function Gen, for metamodels and transformation is a partial function:

$$(\mathsf{GENgr}, \mathfrak{t} : (I\_{\mathfrak{R}}, \Delta\_{\mathfrak{R}}) \to (I\_{\mathfrak{R}}, \Delta\_{\mathfrak{R}}) \cup \{\bot\})$$

It generalizes the consistency preservation rule Cpr of such that it can be applied to changes in instead of and , i.e., it applies the changes delivered by Cpr for the corresponding models to the given change tuple.  We define ⟨ ′ , ′ ⟩ ≔ Cpr ( ,, , ). Then we define:

Gen, (, ) ≔ { ⊥, if ⟨ ′ , ′ ⟩ = ⊥ (, ⟨1 , . . . , ′ , . . . , ′ , . . . , ⟩), otherwise

Like consistency preservation rules, a generalization function must be partial and return ⊥ for inputs it is undefined for to reflect cases in which it cannot return a result. This is a direct consequence of consistency preservation rules being partial, thus a generalization function is defined to return ⊥ in the same cases as the consistency preservation rule it generalizes. The generalization function is a universally-defined auxiliary function only necessary for formalizing the concepts. It must neither be specialized for each transformation, nor must a transformation developer specify it at all.

Finally, either the orchestration function or an application function must be able to reflect the cases in which no execution order of transformations that restores consistency can be found. In accordance to existing terminology [Ste20b], we call these cases unresolvable. From a theoretical perspective, it does not matter whether the orchestration or application function makes that decision, as the orchestration function could even be encoded into the application function. From a practical perspective, however, we may want to determine an execution order even if there is no order that results in a consistent state. This supports finding out why no such order is found, e.g., which transformation induces that problem.

We define a transformation application function that applies transformations to a given tuple of models and changes according to an order delivered by an orchestration function. This function is partial to allow it to indicate that no result with consistent models could be found, e.g., because the input models were inconsistent or because a transformation within the orchestration delivered ⊥. We indicate those cases with the result ⊥.

Definition 4.13 (Transformation Application Function)

Let t be a synchronizing transformations set for consistency relations CR on metamodels and Orct an orchestration function. A transformation application function AppOrct for them is a partial function:

AppOrct : (, Δ) → ∪ {⊥}

The function takes a consistent tuple of models and a tuple of changes that was performed on them and returns a changed tuple of models by acquiring changes from the consistency preservation rules of t. Thus, it has to fulfill the following condition:

∀ ∈ | consistent to CR : ∀ ∈ Δ : ∀ ′ ∈ : [ AppOrct (, ) = ′ ⇒ ∃ 1, . . . , ∈ t : ∃ ′ ∈ Δ : ( Orct (, ) = [1, . . . , ] ∧ Gen, ◦ . . . ◦ Gen,1 (, ) = (, ′ ) ∧ ′ () = ′ )]

While the previous definition does not restrict in which cases ⊥ and in which an actual tuple of models is returned, we define when we consider an application function correct. Correctness can be defined in several ways. For example, we might say that the function is correct if it returns a consistent tuple of models whenever there is an order of transformations that leads to

those consistent models. As we will see later, this correctness notion is, however, inappropriate, because the underlying decision problem is undecidable. In consequence, the application function needs to operate conservatively, i.e., it may return ⊥ even if there is a sequence of transformations whose application leads to consistent models. As an alternative, we might require the function to return consistent models whenever the orchestration function delivers a sequence of transformations whose application leads to a consistent tuple of models. Since we have to deal with conservativeness anyway, this, however, does not provide any benefits. In fact, the above discussed requirements encode a kind of optimality for the functions, which we will specify more precisely in Chapter 7. For now, we stick to the simple notion of correctness that the application function does never return inconsistent models, i.e., if a tuple of models is returned, it must be consistent.

Definition 4.14 (Transformation Application Function Correctness)

Let AppOrct be an application function for an orchestration function Orct for transformations t. Let CR be the set of consistency relations of transformations in t. We say that AppOrct is correct if, and only if, its result is either ⊥ or consistent to CR:

AppOrct correct :⇔ ∀ ∈ | consistent to CR : ∀ ∈ Δ : ( AppOrct (, ) = ⊥ ∨ AppOrct (, ) consistent to CR)

This is, in fact, a rather weak notion of correctness. An application function that always returns ⊥ is correct according to that definition. Because the orchestration and application function have to operate conservatively, a binary correctness notion is less relevant than a gradual one anyway. The question how to determine such an orchestration was introduced as RQ 1.4. We present and discuss a concrete approach as contribution C 1.4 in Chapter 7.

#### **4.3.4. Transformation Networks**

Based on the previous definitions of transformations, orchestration and application functions, we define what we consider a transformation network and when we consider it correct. A transformation network is composed of transformations, an orchestration and an application function. Although we

define these artifacts specifically for one transformation network, i.e., an orchestration and application function according to their definitions are specific for one set of transformations, the goal will be to find an orchestration and application function that is independent from the actual transformations.

Definition 4.15 (Transformation Network)

Let t be a transformation set, Orct an orchestration function for these transformations, and AppOrct an application function. A transformation network is a triple:

 ≔ ⟨t, Orct, AppOrct ⟩

Correctness of a transformation network is given by correctness of the individual transformations and the application function, according to Definition 4.8 and Definition 4.14.

Definition 4.16 (Transformation Network Correctness)

Let = ⟨t, Orct, AppOrct ⟩ be a transformation network. We say that is correct if, and only if, its transformations in t and the application function AppOrct are correct:

 correct :⇔ ∀ ∈ t : correct ∧ AppOrct correct

We have already discussed that we will show that the application function has to operate conservatively, which is why correctness is an essential property but not the most interesting one to achieve. Additionally, we discussed that the consistency relations of the transformations can be considered correct by definition, but that we will discuss a notion of compatibility to reflect when those relations contain unintended contradictions.

## **4.4. A Fine-Grained Notion of Consistency**

We have up to now given a common definition of consistency [Ste10] by enumerating consistent pairs of models in a relation. That notion is sufficient for

defining transformation networks, correctness of their artifacts, and also the essential considerations regarding orchestration, as presented in the preceding section. Domain experts and transformation developers, however, usually think in terms of a more fine-grained notion of consistency. They do not consider when complete models are consistent, but when specific relations between some of their elements are fulfilled, i.e., which other elements they require to exist if some elements are present in models. For example, they consider consistency between architectural components and object-oriented classes instead of complete models containing these elements.

This is also reflected by transformation languages, such as QVT-R. First, they require relations to be defined at the level of classes and their properties. They define how properties of some classes are related to properties of other classes. Second, they are defined in an intensional way, i.e., constraints specify which elements are consistent rather than enumerating all consistent instances in an extensional specification. We have already discussed that intensional and extensional specifications have equal expressiveness and can be transformed into each other, which is why we stick to extensional specifications for reasons of simplicity. However, we reuse the concept of specifying relations at the level of classes and their properties.

This reflects a natural understanding of consistency and, in particular, makes it easier to make statements about dependencies between consistency relations, which we need to make statements about compatibility of consistency relations. Thus, we introduce an appropriate, fine-grained notion of consistency relations in the following. Finally, from such a fine-grained specification, a model-level consistency relation can always be derived by enumerating all models that fulfill all the fine-grained specifications, thus it does not restrict expressiveness in any way and can be seen as a compositional approach for defining consistency, which is only a refinement of the notion of model-level consistency relations. We have presented the following definitions of a fine-grained consistency notion, partly literally, in previous work [Kla+20]. The definitions are based on those proposed in the work of Kramer [Kra17, Sec. 2.3.2, 4.1.1] and Klare et al. [Kla+21].

#### **4.4.1. Fine-Grained Consistency Relations**

The central idea of the fine-grained consistency notion is to have consistency relations that contain pairs of objects and, broadly speaking, requires that if

the objects in one side of the pair occur in a model, the others have to occur in another model as well. A condition encapsulates such objects, for which we require objects in another model to occur.

#### Definition 4.17 (Condition)

A condition c for a class tuple ℭc = ⟨c,1, . . . ,c,⟩ is a set of object tuples with:

$$\forall \langle o\_1, \dots, o\_n \rangle \in \mathfrak{a} : \forall \ i \in \{1, \dots, n\} : o\_l \in I\_{C\_{\varepsilon, l}}$$

An element ∈ c is called a condition element. For a model tuple ∈ of a metamodel tuple and a condition element , we say that:

contains :⇔ ∃ ∈ : ⊆

Conditions represent object tuples, called condition elements, that instantiate the same tuple of classes. They are supposed to occur in models that fulfill a certain condition regarding consistency and thus require elements in other models to exist, as subsequently defined by consistency relations. We say that a tuple of models contains a condition element if any of the models contains all the objects within the condition element. This implies that such a model's metamodel has to contain all the classes in the class tuple of the condition. We use conditions to define consistency relations as the co-occurrence of condition elements.

#### Definition 4.18 (Consistency Relation)

Let ℭ, and ℭ, be two class tuples. A consistency relation is a subset of pairs of condition elements in conditions c,, c, with ℭ, = ℭc, and ℭ, = ℭc, :

⊆ c, × c,

We call a pair of condition elements ⟨ ,⟩ ∈ a consistency relation pair. For a model tuple and a consistency relation pair ⟨ ,⟩, we say that:

 contains ⟨ ,⟩ :⇔ contains ∧ contains A consistency relation is a set of pairs of condition elements, which indicate the tuples of objects that are considered consistent with each other. This means that if a model contains one of the left condition elements that occurs in the relation, another model must contain one of the related right condition elements. It bases on two conditions that define relevant object tuples in instances of each of the two metamodels and defines the ones that are related to each other. Without loss of generality, we assume that each condition element of both conditions occurs in at least one consistency relation pair:

$$\begin{aligned} \forall \mathfrak{c} \in \mathfrak{c}\_{l,CR} &: \exists \langle \mathfrak{c}\_{l}, \mathfrak{c}\_{r} \rangle \in CR : \mathfrak{c} = \mathfrak{c}\_{l} \\ \land \forall \mathfrak{c} \in \mathfrak{c}\_{r,CR} &: \exists \langle \mathfrak{c}\_{l}, \mathfrak{c}\_{r} \rangle \in CR : \mathfrak{c} = \mathfrak{c}\_{r} \end{aligned}$$

Based on these consistency relations, we can define a fine-grained notion of consistency.

#### Definition 4.19 (Consistency)

Let be a consistency relation and let ∈ be a tuple of models of the metamodels in . We say that:

$$\begin{split} \mathfrak{m} \text{ consistent to } & CR : \Leftrightarrow \\ \exists \, W \subseteq \operatorname{CR} : & \left( \forall (\mathfrak{c}\_{l,1}, \mathfrak{c}\_{r,1}), \langle \mathfrak{c}\_{l,2}, \mathfrak{c}\_{r,2} \rangle \in W : \\ & \left( \langle \mathfrak{c}\_{l,1}, \mathfrak{c}\_{r,1} \rangle = \langle \mathfrak{c}\_{l,2}, \mathfrak{c}\_{r,2} \rangle \vee \left( \mathfrak{c}\_{l,1} \neq \mathfrak{c}\_{l,2} \wedge \mathfrak{c}\_{r,1} \neq \mathfrak{c}\_{r,2} \right) \right) \\ & \wedge \forall \langle \mathfrak{c}\_{l}, \mathfrak{c}\_{r} \rangle \in W : \left( \mathfrak{m} \text{ contains } \mathfrak{c}\_{l} \wedge \mathfrak{m} \text{ contains } \mathfrak{c}\_{r} \right) \\ & \wedge \forall \mathfrak{c}'\_{l} \in \mathfrak{c}\_{l,CR} : \left( \mathfrak{m} \text{ contains } \mathfrak{c}'\_{l} \implies \mathfrak{c}'\_{l} \in \mathfrak{c}\_{l,W} \right) \end{split}$$

We call such a a witness structure for consistency of to , and for all pairs ⟨ , ⟩ ∈ , we call and corresponding to each other.

For a set of consistency relations CR = {1,2, . . .}, we say that:

consistent to CR :⇔ ∀ ∈ CR : consistent to

A consistency relation relates one condition element at the left side to one or more other condition elements at the right side of the relation. The definition of consistency ensures that if one condition element ∈ c, at the left side of the relation occurs in a tuple of models, exactly one of the condition elements related to it by a consistency relation occurs in

**Figure 4.8.:** A consistency relation derived from Figure 3.3, which depicts the necessity of a witness structure to ensure that only one employee out of those with differently capitalized names is allowed to correspond to a resident with the same name.

another model to consider the tuple of models consistent. If another element that is related to occurs in the models, this one has to be, in turn, related to another condition element ′ ∈ c, of the left side of condition elements by that also occurs in the models. This ensures that a condition element contained in a model uniquely corresponds to another element to which it is considered consistent according to .

Consider the exemplary consistency relation in Figure 4.8, which is derived from the one in our running example in Figure 3.3. The relation requires for each resident an employee with an appropriate name to exist and vice versa. It assumes that resident names are stored lowercase and allows the employee name to be written in arbitrary capitalization. Thus, for example, both the employees with names "Alice" and "alice" would be considered consistent to a resident with name "alice". Without the restriction defined by the auxiliary witness structure, an employee model containing the employees with both capitalizations would be considered consistent to a resident model containing a corresponding resident with the same name written in lowercase. The witness structure, however, ensures that for each employee one corresponding resident exists, thus there can only exist one employee with one of the allowed capitalizations, as each of them is corresponding to the resident with the lowercase name. In general, the witness structure restriction ensures that if several alternatives for a corresponding element exists, only one is actually allowed to be present.

Example 4.1. The definition of consistency is exemplified in Figure 4.9, which is an alternation of an extract of Figure 3.3 only considering employees and residents. Models with employees and residents are considered consistent if for each employee exactly one resident with the same name or the name in lowercase exists. The model pairs 1–3 are obviously consistent according to the definition, because there is always a pair of objects that fulfills the consistency relation. In model pair 4, there is a consistent resident for each employee, but there is no appropriate employee for the resident with name = "Bob". However,

**Figure 4.9.:** A consistency relation between employee and resident and six example model pairs: pairs 1–4 consistent with an appropriate witness structure shown in blue, solid lines, and pairs 5 and 6 inconsistent with an inappropriate mapping structure shown in red, dashed lines. Adapted from [Kla+20, Fig. 2].

our definition of consistency only requires that for each condition element at the left side of the relation that appears in the models, an appropriate right element occurs, but not vice versa. Thus, a relation is interpreted unidirectionally, which we subsequently discuss in more detail. In model pair 5, there are two residents with names in different capitalizations, which would both be considered consistent to the employee according to the consistency relation. Comparably, in model pair 6, there is a resident that fulfills the consistency relations for both employees, each having a different but matching capitalization. However, the consistency definition requires that each model element for which consistency is defined by a consistency relation must only have one corresponding element. In this case, there are two residents or employees that could be considered consistent to the employee or resident, respectively, thus there is no witness structure with a unique mapping between the elements as required by the definition.

As mentioned in the example, the definition considers consistency in a unidirectional way, which means that a consistency relation may define that some elements are required to occur in a tuple of models if some elements occur, but not vice versa. Such a unidirectional notion can also be reasonable in our example, as it could make sense to require a resident for each employee, but not every resident might be employed and thus also represent an employee. To achieve a bijective consistency definition, for each consistency relation its transposed relation = {⟨ ,⟩ | ⟨ ,⟩ ∈ } can be considered as well. Regarding Figure 4.9, if we consider the relation between employees and residents as well as its transposed, the model pair 4 would also be considered inconsistent, because an appropriate employee for each resident is required by the transposed relation. We call sets of consistency relations that contain only bijective definitions of consistency symmetric.

Definition 4.20 (Symmetric Consistency Relation Set)

Let CR be a set of consistency relations. We say that CR is symmetric if, and only if, for each contained relation its transposed one is also contained:

CR is symmetric :⇔ ∀ ∈ CR : ∈ CR

Any description of bijective consistency relations can be defined with a symmetric consistency relation set. We have defined consistency in a unidirectional way for the two following reasons.

One might argue that consistency is usually traced by means of a trace model, which stores the pairs of element tuples in models that fulfill a consistency relation. A trace model can be seen as an explicit representation of a witness structure as specified in Definition 4.19. We do, however, not explicitly consider such an explicit trace model in this formalism for two reasons also discussed in previous work [Kla+21]. First, a trace model is only necessary in practice if no identifying information for related elements is present, or if performance is to be improved. However, we assume such identifying information to exist without loss of generality, as introduced in Subsection 3.3.3. Second, a trace model can, from a theoretical perspective, be treated as a usual model by defining consistency between one concrete and one trace model. This conforms to the fact that each multiary relation can be expressed by binary relations to an additional model (in this case the trace model), as discussed in existing work [Ste20b; Cle+19]. We discuss practical benefits of having an explicit trace model for consistency preservation in Chapter 6 to distinguish modifications of elements from their removal and addition. But this does, as discussed, not restrict applicability of our formalism.

#### **4.4.2. Expressiveness of Fine-Grained Relations**

The model-level consistency notion of Definition 4.2 is established and based on notions used by several researchers. The fine-grained consistency notion according to Definition 4.19 is based on the insight that practical approaches to describe consistency and its preservation use fine-grained rules rather than enumerating consistent model pairs. We did, however, only provide examples that justify specific decisions in the definitions, such as the witness structure for corresponding elements, but we did not argue if and why fine-grained relations are an actual refinement, such that statements about model-level consistency relations also apply to fine-grained relations.

To show that every set of fine-grained consistency relations can be expressed by a single model-level consistency relation, we can use the same constructive approach that we have used to define consistency according to multiple consistency relations, be they at the model level or fine-grained. Given finegrained consistency relations CR = {1, . . . , }, we can construct an equivalent model-level consistency relation as follows:

= { | consistent to CR}

A model-level consistency relation can, however, not necessarily be expressed by fine-grained consistency relations. The most simple construction approach would define a single fine-grained consistency relation to express a modellevel consistency relation, which contains the complete models instead of extracts of them. The definition of consistency is, however, different for the two types of relations. While at the model level consistency is defined as two (or more) models being in a relation (see Definition 4.2), fine-grained consistency relations do only describe that if an element at the left side of the relation occurs in a model, then any of the related elements at the right side has to occur in another. If two models are considered consistent by a model-level consistency relation, they are also consistent to the accordingly constructed fine-grained relation, because there is a witness structure that contains exactly the two consistent models. If there is a model that is not considered consistent to any other model in the model-level consistency relation, thus the model-level consistency relation does not contain any pair with that model, then there will also be no such pair in the fine-grained relation. According to Definition 4.19 of consistency for fine-grained relations, if there is no condition element in the relation, then consistency is not constrained for the contained model elements. In consequence, such a model would be considered consistent to every other model.

While, at first, this may seem inappropriate, it actually is appropriate for two reasons. First, the formalism can only express that for some elements other elements need to exist, but not that specific elements are not allowed

to exist if other elements exist. This is reasonable, because consistency between models is supposed to ensure that the overlap of information is represented uniformly, thus to express that information in one model needs to be represented in another one as well. Expressing that some elements are not allowed to exist because of others, e.g., being an employee in one model, the same person cannot be a student in another model, is actually not a consistency constraint for information shared between models. This is actually additional information that should be stored in a specific model representing these semantics. Thus, we do not consider this case at all.

Second, the formalism for fine-grained consistency relations can not prevent specific elements from existing at all. For example, a consistency relation may define that for a component in an architecture model a corresponding class in the object-oriented design model has to exist, but it may not restrict that only components of specific names are allowed. Such restrictions should and actually are separate specifications not related to consistency between models but restricting a model on its own. Thus, the metamodel or some additional specification for it should provide such restrictions of valid models, which we have discussed as a restriction of for a metamodel in Section 3.3.

Summarizing, we found that we can express each set of fine-grained consistency relations by a model-level consistency relation. Additionally, we know that there are specific kinds of restrictions that can be encoded in model-level consistency relations but not in fine-grained consistency relations. We have, however, discussed why they are not relevant for the designated application area of consistency preservation. In consequence, all insights made for modellevel consistency relations can also be applied to fine-grained consistency relations and, if specific restrictions are excluded, vice versa.

#### **4.4.3. Application to Consistency Preservation Rules**

As mentioned before, the fine-grained notion of consistency fits well to how transformation languages consider consistency. They allow to define rules that relate only some classes by relations, conforming to fine-grained consistency relations, from which fine-grained consistency preservation rules are derived. Alternatively, they directly allow to define rules to preserve consistency between specific classes. These rules are often called transformation rules and composed to a transformation that consists of multiple such rules, each encoding a consistency relation and a preservation rule.

It may easily happen that the execution of one transformation rule leads to the violation of the consistency relation of another, which induces dependencies between the individual transformation rules. Thus, a combination of transformation rules to a transformation has to ensure correctness, i.e., that the consecutive execution of the rules leads to a consistent state of the models. Languages such as QVT-R and QVT-O therefore specify that transformation rules may not be conflicting [QVT, Sec. 7.10.2.]. It is also a dedicated topic of research to ensure that the rules of a single transformation conform to each other, e.g. [CGL17; Cab+10], which is why we assume that transformations fulfill that property.

To avoid the necessity of specifying this conformance property for transformation rules, we stick to the existing notion of coarse-grained consistency preservation rules, as it is sufficient for our considerations. Still, consistency preservation rules were defined for model-level consistency relations in Definition 4.5. This can, however, be easily extended to fine-grained consistency relations, as we simply need to require the rule to consider consistency to a set of fine-grained relations according to Definition 4.19 rather than consistency to a single model-level consistency relation according to Definition 4.2.

A consistency preservation rule CprCR for a set of consistency relations CR according to Definition 4.18 is thus still considered correct if it only returns changes when they yield models that are consistent to all consistency relations if applied to the input models, in accordance with Definition 4.6:

$$\begin{aligned} \forall \; m\_1 &\in I\_{M\_1}, m\_2 \in I\_{M\_2}, \delta\_{M\_1} \in \Delta\_{M\_1}, \delta\_{M\_2} \in \Delta\_{M\_2}: \\ \forall \; \delta'\_{M\_1} &\in \Delta\_{M\_1}, \delta'\_{M\_2} \in \Delta\_{M\_2}: \left(\mathsf{CPR}\_{\mathbb{C}\,\mathbb{R}}\left(m\_1, m\_2, \delta\_{M\_1}, \delta\_{M\_2}\right) = \langle \delta'\_{M\_1}, \delta'\_{M\_2}\rangle\right) \\ \implies \langle \delta'\_{M\_1}(m\_1), \delta'\_{M\_2}(m\_2)\rangle &\text{ consistent to } \mathsf{CIR}\,\rangle \end{aligned}$$

Note that being consistent to all fine-grained consistency relations is equivalent to being consistent to the model-level consistency relation induced by the fine-grained relations.

Likewise, we consider a synchronizing transformation according to Definition 4.7 as a pair of fine-grained consistency relations and a consistency preservation rule for them, thus = ⟨CR, CprCR⟩. Again, in conformance with Definition 4.8, we call such a transformation correct if, and only if, its consistency preservation rule is correct.

**Figure 4.10.:** A conceptual model for the terms and artifacts introduced for transformation networks and their relations. Adapted from [Kla+21, Fig. 5].

## **4.5. Summary**

In this chapter, we have discussed notions of correctness for transformation networks and the artifacts they consist of, and we have precisely defined the notion that is relevant for the context of this thesis. We give an overview of the introduced concepts and their relations in the conceptual model in Figure 4.10. In summary, we provided the following insight in this chapter.

#### Insight II.1 (Correctness Notion)

A reasonable notion of correctness for networks of modular, independently developed transformations consists of correctness of the single transformations, which need to be synchronizing, and correctness of the application function that determines an execution order of the transformations. An application function may not be able to return a result for different reasons, such as transformations not being applicable to specific changes, the absence of an execution order of the transformations that leads to consistent models, or the inability to find such an order. Thus, in comparison to correctness, the degree of conservativeness is the more important property of an application function, which indicates how often the function does not deliver a result although there is an order of transformations that would restore consistency. Additionally, although theoretically not relevant for correctness, the relations defining when models are considered consistent must fulfill some notion of compatibility to be useful, as they can otherwise prevent transformations from finding consistent models.

In the following chapters, we thus define a notion of compatibility for consistency relations, discuss how correctness of the individual synchronizing transformations for achieving local consistency can be achieved, and finally how a correct and appropriate application function to perform the orchestration for achieving global consistency can be defined. In summary, these following contributions together allow to develop what we defined as a correct transformation network.

For visualizing examples of consistency relations, consistency preservation rules, and their execution throughout the next chapters, we use a notation according to the example depicted in Figure 4.11. We visualize consistency relations with blue arrows and a definition of the conditions for consistency relation pairs forming that relation. In the example, the consistency relation contains all pairs of employees and residents having the same name, except for those with an empty name. The arrows of such a relation indicate whether we only consider a directional consistency relation or also its transposed one. We depict consistency preservation rules with orange arrows and denote which changes it produces because of which input change. In the example, we denote that the addition of an employee (+) leads to the addition of a resident with the same name, specified by the according property assignment

**Figure 4.11.:** Example for the visualization of consistency relations, consistency preservation rules, and the execution of changes by users or consistency preservation.

(name = e.name). In addition, we annotate conditions to the consistency preservation rules, such as e.name ≠ "" in the example, which restricts the resident creation to the case in which the employee name is not empty. We usually specify only parts of a consistency preservation rule if the other cases are not relevant in the specific context. In the example, we only specify the behavior for the case of adding an element but not of modifying or removing it. Finally, we denote the execution of any changes, including consistency preservation rules, with green arrows. In the example, we visualize the addition of an employee by a user, denoted with a "+", which leads to the addition of a resident because of the execution of the above introduced consistency preservation rule.

## **5. Proving Compatibility of Consistency Relations**

Transformations, from which we construct transformation networks, are composed of consistency relations and consistency preservation rules that preserve them, as we have defined in Chapter 4. We focus on binary relations and according preservation rules, which relate two metamodels. While we have precisely defined correctness of transformations and their orchestration in a network, we found that the underlying consistency relations themselves can, from a theoretical perspective, be considered correct by construction, as there is no other artifact (be it explicit or only given implicitly) with respect to which it has to be correct. Since we assume transformations to be developed independently and reused in a modular way, we can especially not assume a monolithic consistency relation to which the modular consistency relations must be correct (see Subsection 4.2.3).

We have, however, already given examples for cases in which binary consistency relations are somehow contradictory. This is the case if the developers of individual transformations have different, conflicting notions of consistency between the metamodels. In the worst case, this can lead to the situation that no single tuple of models would be considered consistent to a set of binary consistency relations, which is obviously unwanted behavior. We have discussed an abstract example for that case already in Subsection 4.2.4.

We recapture the running example defined in Figure 3.3 and extend it with alternatives for two of the binary consistency relations in Figure 5.1. The example contains three pairwise consistency relations between persons, employees and residents. They are defined in a way such that none of them can be omitted, because each pair shares a unique overlap in their attributes. In the example, the consistency relations , and (as well as their transposed ones) are fulfilled if for each person (and each employee and resident analogously) in the models exactly one employee and one resident

 = {⟨, ⟩ | p.firstname + "␣" + p.lastname = e.name ∧ p.income = e.salary} = {⟨, ⟩ | p.firstname + "␣" + p.lastname = r.name ∧ p.address = r.address} ′ = {⟨, ⟩ | p.lastname + ", ␣" + p.firstname = r.name ∧ p.address = r.address} = {⟨, ⟩ | e.name = r.name ∧ e.socsecnumber = r.socsecnumber} ′ = {⟨, ⟩ | e.name.toLower = r.name ∧ e.socsecnumber = r.socsecnumber}

**Figure 5.1.:** Derivation of Figure 3.3: Three simple metamodels for persons, employees and residents, and three binary relations ,, for each pair of them, with ′ as an alternative for and ′ as an alternative for . Adapted from [Kla+20, Fig. 1].

exist that fulfill the defined relations for names and other attributes. According to our notion of consistency relations (Definition 4.18), it is essential that always only one such corresponding element exists. Intuitively, these consistency relations are compatible, as they lead to a reasonable set of model tuples that are considered consistent.

In contrast, considering ′ instead of , the relations can never be fulfilled, because the concatenation of firstname and lastname from person to employee conflicts with the one from person to resident. The relation between employees and persons assumes firstname and lastname in that order, whereas the relation between residents and persons assumes them to be concatenated vice versa and to be separated by a comma. Fulfilling these relations would require an infinitely large model, as the cycle of the relations requires for each person, employee, and resident the existence of the others with firstname and lastname swapped and extended with a comma.

**Figure 5.2.:** Elements required by the consistency relations , and ′ (as well as their transposed) in Figure 5.1 for a resident with the name "Alice Avid". Solid blue lines connect corresponding elements, which do not form a valid witness structure.

As finite models cannot fulfill this, the set of consistent model tuples would be empty.

In addition, considering consistency relation′ instead of, no models containing residents with a name not written in lowercase can be consistent to all relations, as depicted in the example in Figure 5.2, which, for reasons of simplicity, omits all other attributes than the names. A resident with a non-lowercase name requires a person with equally capitalized firstname and lastname to exist. This requires an employee with an equally capitalized name to exist. The relation ′ now requires a resident with the name written in lowercase to exist, which, again, requires a person with the lowercase name to exist. This, in turn, requires an employee with the lowercase name to exist as well. In consequence, the resident with the lowercase name would correspond to both the employee with the original and the lowercase name, whereas the resident with the original name does not correspond to any employee. Since there is no witness structure with a unique mapping of corresponding elements, as also reflected in Figure 4.9, such models cannot be consistent to the consistency relations. More intuitively speaking, it is impossible to find an employee that fulfills the consistency relation ′ for a resident with a non-lowercase name. This is what we call and later precisely define as an incompatibility of the consistency relations, as they define constraints that cannot be fulfilled at the same time. This can always occur if there is a cycle in the graph induced by the consistency relations.

Such incompatibilities are unwanted, as they indicate that developers have different, contradictory notions of consistency. Additionally, they can easily result in transformations that do not yield consistent models or for which finding an orchestration that yields consistent models becomes unnecessarily difficult. For that reason, we first discuss scenarios to identify an intuitive notion of compatibility, which we then transfer into a formal notion. Afterwards, we develop a formal, inductive approach to prove compatibility of relations, for which we prove correctness. It is based on the insight that consistency relations forming a specific kind of tree structure are compatible and that removing a specific kind of redundant relations preserves compatibility. We then derive a practical approach for the transformation language QVT-R. This chapter thus constitutes our contribution C 1.2, which consists of four subordinate contributions: a discussion of compatibility notions; a formal definition of one such notion; a formal approach to prove compatibility; and finally a practical realization of that approach. It answers the following research question:

RQ 1.2: When are the constraints induced by transformations contradictory and how can that be analyzed?

We will see that it is, in general, not possible to prove that transformations are incompatible if the language, in which the relations are described, is undecidable, such as QVT-R. We can, however, at least conservatively validate compatibility of transformations. Thus, if our approach proves compatibility, the transformations are actually compatible, but not vice versa. This enables transformation developers to validate compatibility of their transformations on-the-fly during transformation development, if developed for a specific scenario, or a posteriori during their combination, according to the scenarios introduced in Section 3.2. In particular, in the first scenario developers can immediately react to the introduction of incompatibilities during transformation development.

We have published central contributions of this chapter, in particular the formal and the practical approach for validating compatibility, in previous work [Kla+20]. Parts of some sections of this chapter are also literally taken from that publication, which we further indicate in the respective sections. The practical approach has been developed in the Master's thesis of Pepin [Pep19], which was supervised by the author of this thesis.

**Figure 5.3.:** Example for consistency relations that imply an empty global relation. Small circles denote models, and solid, blue lines relate consistent models.

## **5.1. Towards a Notion of Compatibility**

We start with general considerations on model-level consistency relations, no matter whether they are specified explicitly or implied by sets of fine-grained consistency relations. A set of binary model-level consistency relations induces a monolithic, multiary relation, also called global relation, as discussed in Subsection 4.2.4. A monolithic relation for metamodels 1, . . . , and pairwise consistency relations , is defined by:

$$CR = \{ \langle m\_1, \dots, m\_n \rangle \mid \bigwedge\_{1 \le i < k \le n} \langle m\_i, m\_k \rangle \in CR\_{i,k} \} $$

As discussed before, the consistency relations are correct by definition and so is the induced global relation, even if it is empty. It is, however, unclear whether the relations are reasonable in combination.

In fact, if the relations induce an empty global relation, these relations do actually not properly fit to each other, because no single tuple of models would be considered consistent, thus no system could be consistently described. One may thus consider such relations incompatible. Figure 5.3 shows an extended version of the example already given in Subsection 4.2.4, which induces an empty global relation. This is an abstraction of the concrete examples that we have already discussed for our our running example, in

which modified consistency relations lead to an empty set of consistent model tuples due to conflicting concatenations of names between persons, residents and employees.

There may, however, be more cases than empty induced global relations that we want to exclude by considering the relations incompatible. In general, the goal of finding incompatibilities and excluding them is twofold: First, we want to identify if different developers of modular relations have an incompatible notion of consistency, such that the results of preserving consistency would never be as expected. This is what we have seen in the examples with the name relations. We want to exclude these cases, because developers will not want to combine transformations based on relations that are contradicting. Second, incompatibilities may lead to transformations not being able to find consistent models, so the orchestration would not be able to execute transformations in an order that achieves a consistent state. If we, for example, encoded the relations from the running example with the inverse concatenation of firstname and lastname (′ ) into transformations, each cycle in which the transformations are executed would produce one new person, employee, and resident, or it would change each of the existing ones, such that firstname and lastname are swapped and a comma is appended to lastname. In consequence, transformations would not be able to find a consistent state and, if not stopped preemptively, be executed endlessly. Thus, we also want to exclude such cases, because they can prevent the execution of transformations in a transformation network from terminating.

#### **5.1.1. Necessity of Obsolete Relation Elements**

A first intuitive option to define incompatibility is the presence of model pairs in the consistency relations, for which no globally consistent model tuple containing them can be found. This canonically covers the case in which the modular relations induce an empty global relation, because for none of the model pairs in each relation a globally consistent model tuple containing them can be found. An example for this case is depicted in Figure 5.4, in which the relation 1,2 contains the pairs ⟨1,′ 2 ⟩ and ⟨′ 1 ,2⟩, for which neither 3 nor ′ 3 is consistent to both other consistency relations, as the induced global relation is = {⟨1,2,3⟩, ⟨′ 1 ,′ 2 ,′ 3 ⟩}. Thus, these model pairs may be denoted obsolete as they cannot occur in any globally consistent model tuple.

**Figure 5.4.:** Example for obsolete model pairs in consistency relation 1,2, which can never occur in a globally consistent model tuple. Small circles denote models, and solid, blue lines relate consistent models.

While this point of view may be reasonable when considering only the consistency relations, as we are finally just interested in results that are globally consistent, it induces problems to the process of achieving such a result by means of the execution of transformations or, more precisely, their consistency preservation rules. In fact, transformation networks need to allow intermediate states of models that are only locally consistent, although they can never occur in a globally consistent state. This is necessary, because otherwise each transformation would have to consider which model pairs are not only locally consistent but can be globally consistent as well. We, however, excluded such an alignment of the transformations by assumption of independent development and modular reuse and instead let the orchestration of transformations negotiate a consistent result.

Consider the following example, which is also exemplarily depicted in Figure 5.5. A UML class model and Java code are considered consistent when the same classes and interfaces with the same methods (in Java potentially with an empty body) are contained. Declaring the methods in a class when they are already declared in an implemented interface is optional in the UML. Then for each UML model a usually infinite number of consistent Java models exists, containing arbitrary implementations of the methods. PCM models and UML class models are consistent when components are realized as classes implementing the provided interfaces of the components. In this

**Figure 5.5.:** Example for an obsolete model pair in consistency relations between PCM, UML and Java: The Java model with the empty method is locally consistent to the UML class model specifying the interface method also in the component implementation class. But these two models can never be globally consistent, because for the PCM component providing the interface, the consistency relation requires at least a default implementation of the method. Lines relate consistent models, whereof models related by dashed, red lines are never globally consistent.

case, the classes are required to declare the methods of provided interfaces again. Every class with "Comp" in its name is considered a component. Analogously, each component is represented by a Java class implementing the provided interfaces. The consistency relation between PCM and Java may, however, require that a method within a class that realizes a method of a provided interface of a component contains at least some default implementation, be it logging or something more component-specific. If we considered model pairs that can never occur in globally consistent model tuples as incompatible and thus forbid them, a UML model could not be

considered consistent to a Java model if any method in a class with "Comp" in its name that is declared in one of its interfaces is realized by a Java method with an empty body. The transformation between UML and Java would thus not be allowed to create an empty Java method upon creation of such a UML method. This would, however, enforce the relation between UML and Java to encode information about components, which both breaks our assumption of independent development, as the developer of the transformation between UML and Java would need to know about components, and of modular reuse, because the transformation is then tied to the scenario in which the PCM is used as well.

In consequence of the given scenario and the according insight that transformations may need to produce transient states that are only locally consistent to ensure independence of the transformations and their reusability in different contexts, such obsolete consistency relations do not induce a proper notion of incompatibility.

#### **5.1.2. Prevention from Finding Consistent Solutions**

To identify a proper notion of incompatibility, we consider an exemplary transformation scenario from which we can derive such a notion. In the example depicted in Figure 5.6, we start with the models 1, 2 and 3, which are consistent to all three defined consistency relations. If a user performs a change of 2 to ′ 2 , one possible execution of transformations can be as follows: The transformation for 2,3 changes 3 to ′ 3 , the one for 1,3 changes 1 to ′ 1 and then the one for 1,2 changes ′ 2 back to 2, as that is the only model consistent to ′ 1 . Now the transformation for 2,3 changes ′ 3 back to 3, and finally the one for 1,3 restores 1. As a result, the determined execution order yields the initial models before the user change, which are actually consistent but reject the user change.

Apart from the three given models, only ′′ 1 , ′ 2 , and ′ 3 are consistent. Upon the user change of 2 to ′ 2 , we would expect the transformations to find these models as a consistent result, as otherwise, like in the exemplary execution, the original models are returned, which actually rejects the user change. The issue results from model ′ 1 being present in the consistency relations but not being consistent in any globally consistent model tuple.

**Figure 5.6.:** Example for rejecting a user change because of consistency relations containing model pairs that are never globally consistent. Small circles denote models, and solid, blue lines relate consistent models.

Nevertheless, the selection of ′ 1 is valid and appropriate for each transformation locally, as there are models to which it is locally consistent according to each consistency relation on its own.

Note that this scenario is different from the case discussed for obsolete relation elements. In the scenarios discussed for obsolete relation elements, each model in such an obsolete pair occurs in a globally consistent model tuple but not both models in that pair together do. For example, the Java class with an empty method body actually occurs in a globally consistent model tuple but not together with the UML class model in which the method is declared in the class, although they are locally consistent.

We have seen that it is problematic when consistency relations define consistency of models that do not occur in any globally consistent model tuple. This can easily lead to transformations that do not find expected solutions and unnecessarily reject user changes. We did not define a requirement that user changes may not be reverted on purpose, as that behavior may also be expected to express that certain changes are not allowed to be made. However, if there was a reasonable sequence of transformations that returns a

consistent tuple of models reflecting the user changes, it should be preferred over one that reverts the user change.

#### **5.1.3. An Informal Notion of Compatibility**

The discussed case that models do not occur in any globally consistent model tuple can be seen as a special case of obsolete relation elements, because it actually means that for each pair in a consistency relation in which a model occurs, the model pair cannot occur in a globally consistent model. In consequence, we found that in a combination of relations a model is problematic if

The model ′ 1 in Figure 5.6 is such a model, as it is locally consistent to 2 and ′ 3 , but those two are inconsistent. We can distinguish the following two cases that lead to the occurrence of such a model like ′ 1 .

In consequence, allowing such models during the process of describing a system and preserving consistency between the system models does not provide any benefits and thus should, in the best case, not occur. There is no reason to create such models, but it may prevent transformations from finding consistent states. In fact, disallowing the adaptation of the user change is even more reasonable when not concerning the complete model, like proposed with authoritative models by Stevens [Ste20b], but only the part considered by a specific rule that describes consistency. This can, for

example, be a rule specifying the relation between classes and components rather than between the complete metamodels of the PCM and the UML. This is one of the reasons why we provided the formalization of fine-grained consistency relations in Definition 4.18 that relate extracts of models rather than complete ones. We use this fine-grained notion for formalizing and analyzing compatibility.

Transferred to our fine-grained notion of consistency relations, we consider consistency relations incompatible if there is a condition element (rather than a model) which does not occur in any tuple of models that is globally consistent to all consistency relations. We can thus formulate the following, for now informal notion of compatibility:

For every condition element occurring in a consistency relation pair, a globally consistent model tuple containing it must exist.

This notion is especially reasonable when we consider the process of preserving consistency after user changes. We want to ensure that if consistency of the elements modified by the user is restricted by a consistency relation, there should at least be one consistent tuple of models that reflects the user change, i.e., contains the condition element he or she introduced or modified. If this is not the case, the transformations will not be able to produce a reasonable result, apart from reverting or adapting the user change.

Note that this notion of compatibility does only exclude combinations of relations according to the above made argumentation of being generally useless and potentially preventing transformations from finding consistency result. This does, however, not exclude further useless or unintended combinations of relations, for which the semantics of the relations would have to be known and analyzed. The already discussed example of the necessity to infinitely swap firstname and lastname and append a comma induced by the alternative consistency relation ′ in Figure 5.1 leads to the situation that no tuple of models can fulfill those constraints, thus the global induced consistency relation is empty. If we, however, relax ′ such that only firstname and lastname are swapped but no comma is appended, the relations can be fulfilled by models that contain each person twice, once with firstname and lastname assigned properly and once with them swapped. Although we might say that the relations are not intended that way, it is impossible for a generic approach to validate that without knowing about the semantics of the attributes firstname, lastname and their combination in name. In a

different context, it may be desired that two attributes are concatenated in both orders, thus we cannot disallow that case in general.

Obviously, the given notion of compatibility is a property of a set of consistency relations and not of a single consistency relation. We may say that compatibility of a single relation is context-dependent. In consequence, that property can neither be analyzed nor systematically achieved for a single consistency relation. We can, by definition, not provide a construction approach for consistency relations to be compatible in each context. Compatibility can only be achieved by construction if all consistency relations to be used together are known and developed together, such that compatibility can be analyzed on-the-fly.

#### **5.1.4. An Analysis for Compatibility of Relations**

In the following sections, we define a formal notion of compatibility and derive a formal as well as a practical approach for analyzing or, more precisely, proving it. To give a first overview of this approach, we briefly introduce the central idea based on the informal notion of compatibility, which we first introduced in previous works [Kla18; Kla+19b].

We have seen that incompatibilities can arise whenever there are cycles in the graph induced by consistency relations. This means that the same models are related across two paths of relations, which may be contradictory. Thus, to avoid incompatibilities by construction, one could define a network of transformations and thus underlying consistency relations that does not contain any cycles. This situation is given when the network forms a tree. As we have already discussed, it is, however, in general not possible to define such a tree. First, it contradicts our assumption of independent development, as transformations would need to be aligned such that the missing direct relations between metamodels are expressed across other paths. Second, like we have seen in the running example in Figure 5.1, if three metamodels all share specific information only pairwise, there needs to be a cycle of transformations to keep that information consistent.

Even if we cannot construct a tree, we can use the insight that trees of transformations consist of inherently compatible consistency relations to analyze arbitrary topologies for compatibility. This bases on the following two techniques.

**Figure 5.7.:** Example for the decomposition of independent and removal of redundant consistency relations for analyzing compatibility. Adapted from [Kla18, Fig. 4].

Finding independent subsets of relations and removing their redundancies until only trees remain proves compatibility. We call this approach decomposition, as we decompose the original relations into independent, essential relations, and we say that the resulting trees witness compatibility.

Figure 5.7 sketches the ideas for proving compatibility based on the given informal notion. We consider consistency relations 1, 2, and 3 between three metamodels, for which we know that 3 can be separated into disjoint 4 and 5, i.e., the relations are independent. Thus, one relation may relate components and classes and the other may relate different interface representations, as exemplarily explained before. Additionally, we know that the combination of 1 and 2 is a subset of 4, thus 4 is redundant as models are only considered consistent if they are consistent to 1 and 2 anyway. In other words, 1 ⊗ 2 is more restrictive regarding consistency than 4. In consequence, we can, for the scope of the analysis, remove 4 and consider 1 and 2 independently from 5. This results in two independent trees of relations, which are inherently compatible. Since redundancy and independence are compatibility-preserving, this proves compatibility of the original relations.

### **5.2. A Formal Notion of Compatibility**

In this section, we precisely define our up to now informally introduced notion of compatibility. For that, we use the fine-grained notion of consistency and its defining relations as proposed in Section 4.4. We discuss implicit relations, which are induced by a set of consistency relations, such as transitive relations, and, finally, derive a compatibility notion from the consistency formalization and its pursued perception. The contents of this and the remaining sections of this chapter are mostly, in parts literally, taken from our published article on proving compatibility [Kla+20].

#### **5.2.1. Implicit Consistency Relations**

Considering sets of consistency relations, as they are implicitly defined by the set of transformations in a transformation network, their combination is of especial interest. Each set of consistency relations defines relations between two sets of classes but also implies further transitive consistency relations. Having one relation between classes and and one between and implies an additional relation between and . We define a notion for the concatenation of relations that implies such transitive relations, which are supposed to reflect the consistency constraints introduced by the concatenated relations. Models should always be consistent to a concatenation of

consistency relations if they are consistent to each of the concatenated relations, as otherwise the concatenation would introduce additional constraints. To achieve this, the following definition makes appropriate restrictions to the derived consistency relation pairs.

Definition 5.1 (Consistency Relations Concatenation)

Let1 and2 be consistency relations. We define their concatenation 1 ⊗ 2 as:

1 ⊗ 2 ≔ {⟨ ,⟩ | ∃⟨ ,,1⟩ ∈ 1 : ∃⟨,2,⟩ ∈ 2 : ,2 ⊆ ,1 ∧ ∀⟨ , ′ ,1 ⟩ ∈ 1 : ∃⟨ ′ ,2 , ′ ,2 ⟩ ∈ 2 : ′ ,2 ⊆ ′ ,1 } with ℭ, = ℭ,1 and ℭ, = ℭ,2

The concatenation of two consistency relations contains pairs of object tuples that are related across common elements in the right respectively left side of the consistency relation pairs. Such a concatenation may be empty. Two requirements ensure that all models considered consistent to the concatenation are also consistent to the single relations: First, two consistency relation pairs of 1 and 2 are only combined if the left condition element of the consistency relation pair of 2 is a subset of the right condition element of the consistency relation pair of 1. Only in that case the existence of the right condition element of the pair of 1 in a model requires the existence of an according condition element in 2. Second, it is necessary that for all elements ′ ,1 in the right side of 1, which are considered consistent to a condition element , there must be a matching condition element, i.e., a subset of ′ ,1 , in the left condition of 2. If there was an element ′ ,1 in the right side of 1 for which the left-side condition of 2 does not contain a subset, the concatenation does not constrain consistency for the existence of . Thus, without these restrictions the occurrence of in a model tuple would not necessarily impose any consistency constraint by 2. We explain these two restrictions at an example.

Example 5.1. Figure 5.8 extends the example in Figure 5.1 with further classes in the consistency relations, such that they do not only relate single classes to each other. It defines an address for employees and, in the second example, also a

3 = {⟨, ⟩ | p.name = r.name}

4 = {⟨(,), (, )⟩ | r.name = e.name ∧ l.street = a.street}

**Figure 5.8.:** Two scenarios, each with two consistency relations: Consistency relations 1 and two options 2,′ 2 with 1 ⊗ 2 ≠ ∅ and 1 ⊗ ′ 2 = ∅, and consistency relations 3 and 4 with 3 ⊗ 4 = ∅ and 4 ⊗ 3 ≠ ∅. Taken from [Kla+20, Fig. 3].

location for the addresses of residents, which are represented in additional classes. Both examples contain consistency relations between persons and residents (1 and 3), which define that for each person a resident with the same name has to exist. The examples provide different options for the consistency relation between residents (with locations) and employees with addresses (2, ′ 2 , and 4), which exemplify the necessity for the restrictions in Definition 5.1:

results in1 ⊗ ′ 2 = ∅, because every person is consistent to a resident with an empty street name, thus not requiring a corresponding employee. This shows the necessity of the second restriction in the definition.

We can formally show that the defined notion of concatenation does not lead to any restriction of consistency regarding the single relations:

Lemma 5.1 (Concatenation Consistency)

Let 1 and 2 be two consistency relations for a metamodel tuple , and let = 1 ⊗ 2 be their concatenation. Then it holds that:

∀ ∈ : ( consistent to {1,2} ⇒ consistent to )

Proof. For any tuple of models that is consistent to 1 and 2, take a witness structure 1 that witnesses consistency of to 1 and 2 that witnesses consistency of to 2. Now consider the composed witness structure = 1 ⊗ 2. We show that is a valid witness structure for .

Let us assume there were ⟨ ,⟩, ⟨ ′ , ′ ⟩ ∈ with = ′ and ≠ ′ , such that is not a witness structure for . Per definition, only occurs in one ⟨ ,,1⟩ ∈ 1. So there must be two consistency relation pairs

⟨,2,⟩, ⟨ ′ ,2 , ′ ⟩ ∈ 2 with ,2 ⊆ ,1 and ′ ,2 ⊆ ,1. However, since ,2 and ′ ,2 contain instances of the same classes and are both subsets of the same object tuple ,1, we have ,2 = ′ ,2 . So we know that fulfills the first condition of a witness structure according to Definition 4.19 for consistency:

$$\forall \langle \mathfrak{c}\_{l,1}, \mathfrak{c}\_{r,1} \rangle, \langle \mathfrak{c}\_{l,2}, \mathfrak{c}\_{r,2} \rangle \in W : \left( \langle \mathfrak{c}\_{l,1}, \mathfrak{c}\_{r,1} \rangle = \langle \mathfrak{c}\_{l,2}, \mathfrak{c}\_{r,2} \rangle \vee \mathfrak{c}\_{l,1} \neq \mathfrak{c}\_{l,2} \wedge \mathfrak{c}\_{r,1} \neq \mathfrak{c}\_{r,2} \right)$$

Additionally, since 1 and 2 are witness structures for consistency of to 1 and 2, the model tuple contains all condition elements in 1 and 2. Consequentially, also contains the condition elements in , as those in are composed of the ones in 1 and 2. This implies that the second condition of Definition 4.19 is fulfilled:

$$\forall \langle \mathfrak{c}\_l, \mathfrak{c}\_r \rangle \in \mathcal{W} \colon \left( \mathfrak{m} \text{ contains } \mathfrak{c}\_l \wedge \mathfrak{m} \text{ contains } \mathfrak{c}\_r \right).$$

Finally, we assume the third condition of Definition 4.19 was unfulfilled, i.e.:

$$\exists \mathbf{c}'\_{l} \in \mathbb{w}\_{l,CR} : \left(\mathfrak{m} \text{ contains } \mathbf{c}'\_{l} \wedge \mathbf{c}'\_{l} \notin \mathfrak{w}\_{l,W}\right).$$

We know that c, ⊆ c,1 , because the left condition elements in are, per definition, taken from the left condition elements in 1 and thus also contained in 1. Since contains ′ , there must be a consistency relation pair ⟨ ′ , ′ ,1 ⟩ ∈ 1 that witnesses consistency of ′ according to 1. There must be at least one consistency relation pair ⟨ ′ ,2 , ′ ,2 ⟩ ∈ 2 with ′ ,2 ⊆ ′ ,1 , because otherwise ′ would, per definition, not occur in the left condition of . For all such tuples ⟨ ′ ,2 , ′ ,2 ⟩, we know that contains ′ ,2 , because contains ′ ,1 due to its containment in 1 and due to ′ ,2 ⊆ ′ ,1 . In consequence, consistency to 2 requires that for one of those ′ ,2 it holds that contains ′ ,2 and that there is ⟨ ′ ,2 , ′ ,2 ⟩ ∈ 2 that witnesses this consistency. Summarizing, due to ⟨ ′ , ′ ,1 ⟩ ∈ 1 and ⟨ ′ ,2 , ′ ,2 ⟩ ∈ 2 with ′ ,2 ⊆ ′ ,1 and due to the definition of as 1 ⊗ 2, we know that ⟨ ′ , ′ ,2 ⟩ ∈ , which breaks our assumption. So we have shown that:

$$\forall \mathbf{c}'\_{l} \in \mathbb{w}\_{l,CR} : \left(\mathfrak{m} \text{ contains } \mathbf{c}'\_{l} \Longrightarrow \mathbf{c}'\_{l} \in \mathbb{w}\_{l,W}\right).$$

Summarizing, we have shown that fulfills all three requirements for a witness structure for consistency according to Definition 4.19, so we know that consistent to .

#### **5.2.2. Transitive Closure of Consistency Relations**

Based on the introduced notion of concatenation, we can define a transitive closure for a consistency relation set, which contains all relations in that set complemented by all possible concatenations of them, i.e., implicit relations of that set. Having shown that our definition of concatenation of consistency relations is well-defined in the sense that it does not introduce further restrictions for consistency, we can show that the transitive closure does not restrict consistency in comparison to the set of consistency relations itself.

Definition 5.2 (Consistency Relations Transitive Closure)

Let CR be a set of consistency relations. We define its transitive closure CR+ as:

CR+ ≔ { | ∃1, . . . , ∈ CR : = 1 ⊗ . . . ⊗ }

The transitive closure of a set of consistency relations CR contains all consistency relations of CR and all their concatenations. Thus, the transitive closure contains consistency relations that relate all elements that are directly or indirectly related due to CR. Due to cycles in the concatenation of relations, this closure can, in general, be of infinite size.

The transitive closure of a consistency relation set does not restrict consistency in comparison to the original set, i.e., if a model tuple is consistent to a set of consistency relations, it is also consistent to their transitive closure. We show that by first extending the argument of Lemma 5.1, which shows that concatenation does not further restrict consistency, to the transitive closure, which is only a set of concatenations of consistency relations.

Lemma 5.2 (Relation Set Consistency)

Let CR be a set of consistency relations for a tuple of metamodels . Then it holds that:

∀ ∈ CR+ \ CR : ∃1, . . . , ∈ CR : ∀ ∈ : ( consistent to {1, . . . } ⇒ consistent to ) Proof. Per definition, every ∈ CR+ is a concatenation of relations in CR, i.e.:

∀ ∈ CR+ : ∃1, . . . , ∈ CR : = 1 ⊗ . . . ⊗

We know for every two consistency relations 1 and 2 and all model tuples that if consistent to {1,2}, then consistent to 1 ⊗ 2 (Lemma 5.1). Inductively applying that argument to 1, . . . , shows that consistent to whenever consistent to {1, . . . , }.

As a result of this lemma, we can show that the transitive closure of a consistency relation set considers the same tuples of models consistent as the consistency relation set itself.

Lemma 5.3 (Transitive Closure Consistency)

Let CR be a consistency relation set for a metamodel tuple . Then it holds that:

∀ ∈ : ( consistent to CR ⇔ consistent to CR+ )

Proof. Adding a consistency relation to a set of consistency relations can never relax consistency, i.e., it cannot lead to models being consistent that were not considered consistent before. Definition 4.19 for consistency defines models as consistent when they are consistent to all consistency relations in a set. Thus, only adding relations can further restrict the set of consistent model tuples. In consequence, it holds that:

```
 consistent to CR+ ⇒  consistent to CR
```
According to Lemma 5.3, a tuple of models that is consistent to CR is always consistent to all transitive relations in CR+ as well. Thus, we know that:

```
 consistent to CR ⇒  consistent to CR+
```
In consequence, the same models are consistent to CR and its transitive closure CR+ .

#### **5.2.3. Compatibility of Consistency Relations**

Based on the notion of fine-grained consistency relations and their concatenation, we can precisely formulate our initially informal notion of compatibility of consistency relations. We have stated that we consider consistency relation incompatible if they are contradictory, like the relation between names in our initial example in Figure 5.1. In that example, for residents with non-lowercase names no consistent tuple of models could be derived. We formalize this notion of non-contradictory relations by requiring that relations may not restrict that an object tuple, for which consistency is defined in any consistency relation, cannot occur in a consistent model tuple anymore.

```
Definition 5.3 (Compatibility)
```
Let CR be a set of consistency relations for a tuple of metamodels . We say that:

```
CR compatible :⇔ ∀ ∈ CR : ∀ ∈ c, : ∃  ∈  :
  (
   contains  ∧  consistent to CR)
```
We call a set of consistency relation CR incompatible if it is not compatible.

We exemplify this notion of compatibility at an extract of the initial example with different consistency relations.

Example 5.2. Figure 5.9 shows an extract of the three metamodels from Figure 5.1 and several consistency relations, of which different combinations are compatible or incompatible according to the previous definition. We always consider the actual relations together with their transposed ones to have a symmetric set of consistency relations.

{1, 1 ,2, 2 ,3, 3 }**:** These relations are obviously compatible, because they relate firstname, lastname and name in the same way. Thus, for each object with any name, and thus any condition element in all of the consistency relations, a consistent model tuple can be found by adding instances of the other classes with appropriate names.

1 = {⟨, ⟩ | r.name = p.firstname + "␣" + p.lastname} 2 = {⟨, ⟩ | e.name = p.firstname + "␣" + p.lastname} ′ 2 = {⟨, ⟩ | e.name = p.firstname + ", ␣" + p.lastname} ′′ 2 = {⟨, ⟩ | e.name = p.lastname + "␣" + p.firstname} 3 = {⟨, ⟩ | r.name = e.name} ′ 3 = {⟨, ⟩ | r.name = e.name.toLower}

**Figure 5.9.:** Three metamodels with different options for consistency relations. The relation sets {1, 1 ,2, 2 ,3, 3 } and {1, 1 ,′′ 2 ,′′ 2 ,3, 3 } are compatible, whereas the sets {1, 1 ,′ 2 ,′ 2 ,3, 3 } and {1, 1 ,2, 2 ,′ 3 ,′ 3 } are not. Taken from [Kla+20, Fig. 4].