Models undergo a variety of transformations throughout development. One of the key transformations is merge, used when developers need to combine a set of models with respect to the overlaps between them. A major question about model transformations in general, and merge in particular, is what consistency properties are preserved across the transformations and what consistency properties may need to be re-checked (and if necessary, re-established) over the result. In previous work [18], we developed a technique based on category-theoretic colimits for merging sets of inter-related models. The use of category theory leads to the preservation of the algebraic structure of the source models in the merge; however, this does not directly provide a characterization of the (in)consistency properties that carry over from the source models to the result, because consistency properties are predominantly expressed as logical formulas. Hence, an investigation of the connections between the “algebraic” and “logical” properties of model merging became necessary. In this paper, we undertake such an investigation and use techniques from finite model theory [9] to show that the use of colimits indeed leads to the preservation of certain logical properties. Our results have implications beyond the merge framework in [18] and are potentially useful for the broad range of techniques in the graph transformation and algebraic specification literature that use colimits as the basis for model manipulations.
D.2.1 [Software Engineering]: Requirements/Specifications Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.
Copyright 200X ACM X-XXXXX-XX-X/XX/XX ...$5.00.
In the past several years, we have been studying the
problem of model integration, particularly in situations where the
models are originating from distributed sources of
information. Many activities in model-based development fall under
the umbrella of integration. These include (1) merging, used
to build a global view of a set of overlapping perspectives
(e.g., [
Our position towards the integration problem has been
that the integration operators (e.g., merge, compose, weave)
must tolerate inconsistency. That is, the operators must
work for any given set of models, even when the models are
inconsistent. This position is motivated by two well-known
observations: First, immediate resolution of inconsistency
can be disruptive in projects where ambiguities and conflicts
tend to occur frequently [
In light of our position, it is important to understand how different consistency properties are affected by the integration operations. Specifically: • If all the source models are consistent with respect to a given consistency property, will the integrated model be consistent with respect to that property as well? • If there is an inconsistency in the source models, will the inconsistency necessarily carry over to the integrated model?
Answering the first question is interesting to enable compositional reasoning about consistency. Answering the second question is useful for understanding the nature of an inconsistency. In particular, inconsistencies that are due to incomplete information in the individual source models can be automatically resolved in the integrated models when the source models are complementary and address each other’s areas of incompleteness. For example, an abstract class with no descendants in a UML class diagram might be seen as inconsistent. But this class might be inherited from in other models and hence the overall view might still be consistent. In contrast, cyclic inheritance in a UML class diagram cannot be resolved in the integrated model (unless the integrated model omits information from the source models). M4 Merge
D R3
A B
E M1
R4 D B E
A B E
Since consistency rules are often described in logical languages (e.g., first order logic), we are interested in studying how different integration operators preserve the logical properties of models. In general, property preservation is a powerful tool for reasoning about model transformations. The main question that property preservation tackles is the following: If a property (formula) ϕ in some logic holds over a model M , will ϕ also hold over a model M 0 derived from M via some transformation?
In this paper, we discuss the logical property preservation
characteristics of our merge operator in [
We use techniques from finite model theory [
The remainder of this paper is structured as follows: In Section 2, we provide background information on our merge algorithm and present the logical preliminaries for our work. In Section 3, we describe our general logical preservation results for colimits; and in Section 4, we use these general results to reason about the preservation of some logical expressions that are frequently used in consistency rules. We conclude in Section 5 with a summary and directions for future work.
We first briefly review our merge operator. For more
information, see [
The third abstraction, the interconnection diagram, captures a set of models and a set of known or hypothesized mappings between them. An example interconnection diagram is shown in Figure 1. In this example, M1, . . . , M4 An equivalence class
C
B C
E R1 M2
R2
M3 are simple UML class diagrams with their overlapping parts specified through four mappings, R1, . . . , R4 (depicted using directed dashed lines). A simpler example with just two models, M1, M2, and one mapping, R, is shown in Figure 3(a). A third example is given in Figure 4(a), where the shared parts of two models, M2, M3, are captured by a third model M1 and two mappings R1, R2.
The input to the merge algorithm is an interconnection diagram D = hM1, . . . , Mi, R1, . . . , Rji. The algorithm works by unifying elements in M1, . . . , Mi that fall into the same equivalence class induced by R1, . . . , Rj. As an example, we have delineated by thin dashed lines one of the several equivalence classes in Figure 1. Note that each unmapped element in the input models falls into a distinct equivalence class of its own.
For convenience, in the example shown in Figure 1, we used a consistent vocabulary for naming the elements of M1, . . . , M4, hence defining R1, . . . , R4 based on name equalities. In general, models may not have a common vocabulary, and mappings are not necessarily based on vocabulary similarities (e.g., see the examples in Figures 3(a) and 4(a)).
The merged model has exactly one element corresponding to each equivalence class. Since mappings denote equality of mapped element pairs and hence are symmetric, the directionality of mappings is ignored in the computation of equivalence classes.
Figure 2 shows the resulting merge for the interconnection diagram of Figure 1. The merge provides interesting insights about how consistency properties can be broken across merge. For example, we may have consistency rules that check for multiple or cyclic inheritance in UML class diagrams. Obviously, these rules are satisfied over the individual source models in Figure 1, but the global view of the system (i.e., the merge) is inconsistent. In particular, in Figure 2: B has two parents; and B, C, E form a cycle. In Section 4, we provide a systematic explanation of what properties of the source models carry over to the merge and what properties do not. 2.2
First Order (FO) logic is one of the most commonly used
logical languages for expressing consistency rules [
Definition 2.1 (relational structure) A (relational) structure is an object A = (A, R1, . . . , Rm), where A is a nonempty set, m is a natural number, R1, . . . , Rm are abstract relation symbols with associated arities k1, . . . , km (nonnegative integers), and each Ri is a ki-ary relation on A.
The set A is called the universe of A. The sequence of relation symbols R1, . . . , Rm together with corresponding arities k1, . . . , km comprise the vocabulary of A. We usually denote a vocabulary by σ. Relation RiA is called the interpretation of a relation symbol Ri in A.
FO formulas in a vocabulary σ are built up from atomic formulas using negation, conjunction, disjunction, and existential and universal quantification: ϕ ::= x = y | R(x1, . . . , xn) | ¬ϕ | ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2 |
∃xϕ(x) | ∀xϕ(x)
In the above, x, y and x1 . . . , xn are variables, R is an n-ary relation symbol in σ, and ϕ1 and ϕ2 are formulas.
Given a set U , let P(U ) denote its powerset. A set X ⊆ U is said to be a fixpoint of a mapping F : P(U ) → P(U ) if F (X) = X. A set X ⊆ U is a least fixpoint of F if it is a fixpoint, and for every other fixpoint Y of F , we have X ⊆ Y . The least fixpoint of F is denoted by lfp(F ). Least fixpoints are guaranteed to exist only if F is monotone. That is,
X ⊆ Y implies F (X) ⊆ F (Y ).
We now add a least fixpoint operator to FO. Suppose we have a vocabulary σ, and an additional relation symbol R 6∈ σ of arity k. Let ϕ(R, x1, . . . , xk) be a formula with vocabulary σ ∪ {R}. For a structure A with vocabulary σ, the formula ϕ(R, ~x) yields a mapping Fϕ : P(Ak) → P(Ak) defined as follows:
Fϕ(X) = {~a | A |= ϕ(X/R, ~a)}
The notation ϕ(X/R, ~a) means that X is substituted for R in ϕ. More precisely, if A0 is a (σ ∪{R})-structure expanding A, in which R is interpreted as X, then A0 |= ϕ(~a).
To ensure that Fϕ is monotone, we impose certain restrictions. Given a formula ϕ that may contain a relation symbol R, we say that an occurrence of R is negative if it is under the scope of an odd number of negations, and positive, otherwise. We say that a formula is positive in R if there are no negative occurrences of R in it, i.e., either all occurrences of R are positive, or there are none at all.
Lemma 2.2 [
Definition 2.3 (least fixpoint logic) [
A |= [lfpR,~xϕ(R, ~x)](~a) iff ~a ∈ lfp(Fϕ).
Example 2.4 (reachability) Consider graphs whose edge relation is E, and let
ϕ(R, x, y) = E(x, y) ∨ ∃z (E(x, z) ∧ R(y, z)) .
Reachability, i.e., the transitive closure of E, is characterized by the formula
ψ(x, y) = [lfpR,x,yϕ(R, x, y)](x, y).
That is, ψ(a, b) holds over a graph G iff there is a path from a to b in G. 2.3
Our merge framework embeds each source model into the merge through a homomorphism. The existence of these homomorphisms leads to the preservation of certain consistency properties. Below, we review the theoretical results underlying our discussion of property preservation in Section 3. We begin with a definition of homomorphism: Definition 2.5 (homomorphism) Let A = (A, R1A, . . . , RmA) and B = (B, R1B, . . . , RmB) be structures in the same vocabulary. A homomorphism from A to B is a function h : A → B such that h(RiA) ⊆ RiB, i.e., if (a1, . . . , aki ) ∈ RiA then (h(a1), . . . , h(aki )) ∈ RiB for every 1 ≤ i ≤ m.
The first result about property preservation under
homomorphisms, dating back to the 1950’s, is the
Los-TarskiLyndon Theorem:
Theorem 2.6 (homomorphism preservation theorem)
(e.g., see [
The existential positive fragment of FO is denoted ∃FO+.
For our purposes, we are interested in finite structures only,
and like many classical mathematical logic results that fail
in the finite case (e.g., compactness), there is the danger
that the above result may fail as well when restricted to
finite structures. Fortunately, this is not the case.
Theorem 2.7 (h. p. t. in the finite) [
The forward direction of the if-and-only-if (i.e., sufficiency) in the above result can be extended to the existential positive fragment of LFP, denoted ∃LFP+.
Lemma 2.8 Every ∃LFP+ formula is preserved under homomorphisms on finite structures.
A proof of the above lemma is provided in the appendix. The lemma is the basis for the results we present in Section 3.
Our merge framework offers three key features [
F2 The merged model does not contain any unmapped elements, i.e., every element in the merged model is the image of some element in the source models. This feature ensures minimality, i.e., the merge does not introduce information that is not present in or implied by the source models.
F3 Merge respects the mappings in the source system, i.e., the image of each element in the merged model remains the same, no matter which path through the mappings in the source system one follows. This feature ensures non-reduandancy. More precisely, if a concept appears in more than one source model, only one copy of it appears in the merged model.
From F1 and Lemma 2.8 (in Section 2.3), it follows that the result of our merge procedure preserves the existential positive fragment of LFP.
Theorem 3.1 If an existential positive LFP formula ϕ is satisfied by some source model M , any merge in which M participates satisfies ϕ as well.
By F2 and the above theorem, we obtain the following result regarding preservation of universal properties. Theorem 3.2 Let ϕ(x) be an existential positive LFP formula with a free variable x. If the formula ψ = ∀x ϕ(x) is satisfied by all the source models, ψ is satisfied by any merge of the models as well.
Notice that Theorem 3.2 allows the introduction of only one universal quantifier. To gain intuition on what happens when additional universal quantifiers are introduced, consider the system in Figure 3(a) and let the relation E(x, y) denote the graph edge relation. Both models in Figure 3(a) are complete graphs and hence satisfy the property ∀x ∀y Node(x) ∧ Node(y) ⇒ E(x, y) 1. However, the property is violated over the resulting merge shown in Figure 3(b), 1The property uses implication and hence has negation. But the negation can be resolved, because every element in the universe that is not a node is an edge. Therefore, the property is equivalent to ∀x ∀y Edge(x) ∨ Edge(y) ∨ E(x, y). because there is no edge from node a to node d and vice versa. The general observation here is that, when there is more than one universal quantifier, universally quantified variables can be assigned values from non-shared parts of different source models. In such a case, property satisfaction over the individual source models may not extend to the merge.
Currently, we do not know whether F3 leads to further property preservation results. This is an issue that we plan to investigate in future work. 4.
In previous work [
Below, we use results of Section 3 to reason about the preservation of these expressions.
Compatibility Properties. Preservation of compatibility properties can be established directly through algebraic means, but it is interesting to see if the same can be done through logical means. For example, in a class diagram, an edge of type “implements” must relate a class to an interface; otherwise, the diagram would not be well-formed. This property can be formalized as follows:
C1 = ∀e (Edge(e) ∧ Type(e, “implements”) ⇒
Compatibleclass,interface(e)) where Edge is the set of edges of the graph representing a class diagram, Type is a binary relation between the set of edges and different types of relations between classes, and Compatibleclass,interface(e) is a constraint that verifies whether the source and target nodes of edge e are of type class and interface, respectively. The general form of this constraint can be formalized using an existential positive formula as follows:
Compatibleα,β(e) = ∃n (∃m (Source(e, n) ∧ Target(e, m) ⇒
Type(n, α) ∧ Type(m, β))) where Source and Target are binary relations, respectively giving the source and target node for a given edge.
The sub-formula Type(e, “implements”) of C1 appears in negated form, but the negation can be resolved, knowing that (1) the set of types is fixed and, (2) every element has a type. More precisely, if the set of types is {t1, . . . , tn}, the formula ¬Type(e, t`) can be replaced with Wi6=` Type(e, ti). Hence, by Theorem 3.2, C1 is preserved.
Multiplicity Properties. One can show through simple counterexamples that none of the following lift from the source models to the merge: M1 u M2 b
c R (a) a M1 b c
d (a) v
w R1 x y d M2 R2 z M3 d Merge (b)
b,c a,b,u,x,y
c,d,v,w,z Merge (b) • There exists at least c elements satisfying ϕ. • There exists exactly c elements satisfying ϕ. • There exists at most c elements satisfying ϕ.
It is easy to see why the “exactly” and “at most” cases
do not get preserved, noting that merge normally has more
information than any of the source models. To understand
why the “at least” case is not preserved, note that
homomorphisms (and functions as well) are not necessarily
oneto-one, and can therefore shrink the number of elements
satisfying a property. For example, consider the system of
models in Figure 4(a) and its merge in Figure 4(b). For
simplicity, the models are discrete graphs, i.e., sets, and their
mappings are functions. Although M1, M2, M3 all satisfy
the property “there exists at least three (distinct) nodes”,
the merge has only two nodes, hence violating the property.
It is important to mention that the flexibility to fuse
together multiple elements of the same source model is not an
undesirable feature and is indeed valuable when one needs
to perform an abstraction during merge [
Reachability Properties. An interesting consequence of Theorem 3.1 is the preservation of paths in the merge. Recall that we gave a formalization for the reachability property in Example 2.4. To see how this can be used for reasoning about consistency, consider the following consistency rule over class diagrams: “Every abstract class must have a concrete implementation”. This rule is formally expressed as follows:
C2 = ∀c ((Type(c, “class”) ∧ Abstract(c)) ⇒
∃c0(Concrete(c0) ∧ Reachableextends(c0, c))) where Reachableextends(x, y) holds iff a path from x to y made up of edges of type “extends” exists. Using the argument we gave when discussing preservation of compatibility properties, we know that the negation of Type(c1, ”class”) can be resolved. Further, ¬Abstract(c1) can be replaced with a positive property, say, Concrete(c1). It now follows from Theorem 3.2 that C2 is preserved.
Note that our results can be used for reasoning about preservation of inconsistency as well. For example, consider the following rule:
C3 =
∃c ((Type(c, “class”) ∧ Reachableextends(c, c)))
This rule holds over a class diagram M when the inheritance hierarchy in M is cyclic, i.e., M is inconsistent. By Theorem 3.1, we can conclude that any merged model that has M as a source model satisfies C3 as well, and hence is also inconsistent. 5.
In this paper, we showed that the use of algebraic colimits for model merging leads to the preservation of certain logical properties. We used our results to formally reason about the preservation of consistency properties across merge.
Based on our recent survey of existing model merging
techniques [
For future work, we would like to provide a full logical characterization of colimits. In particular, the logical implications of F 3, described in Section 3, is unknown to us at the moment and need to be revisited in the future. Further, it may be possible to trade off development flexibility in favour of a broader class of preserved properties, e.g., by using more constrained mappings for relating models, or by placing restrictions on the patterns used for interconnecting the models. We leave an elaboration of these topics to future investigation. Lastly, we would like to explore the application of our results for checking the consistency of model manipulations in graph transformation and algebraic specification approaches that are based on colimits. 6.
Let A = (A, R1A, . . . , RmA) and B = (B, R1B, . . . , RmB) be a pair of relational structures over vocabulary σ = (R1, . . . , Rm). Let h : A → B be a homomorphism. We show that for every ϕ ∈ ∃LF P + and for every ~a ∈ Ak
A |= ϕ(~a) ⇒ B |= ϕ(h(~a)) where h(~a) = (h(a1), . . . , h(ak)).
The proof for ϕ ∈ ∃F O+ ∩ ∃LF P + follows from Theorem 2.7. Below, we provide a proof for least fixpoint formulas.
Let ϕ(~x) = [lfpR,y~α(R, ~y)](~x). By the definition of lfp, for every structure A, the formula ϕ yields a mapping Fα,A : P(Ak) → P(Ak) defined as follows:
Fα,A(X) = {~a | A |= α(X/R, ~a)} By Definition 2.3 and Knaster-Tarski’s fixpoint theorem, for every ~a ∈ Ak we have:
∞ ~a ∈ [ Fαi ,A(∅) ⇔ A |= [lfpR,y~α(R, ~y)](~a)
i=0 We first prove by induction that h(Fαi ,A(∅)) ⊆ Fαi ,B(∅). Base case: Let ~a ∈ Fα,A(∅). Then, A |= α(∅, ~a). Since A is a substructure of B by h and since h(∅) = ∅, we have B |= α(∅, h(~a)). Thus, h(~a) ∈ Fα,B(∅).
Inductive step: Let ~a ∈ Fαi ,A(∅). Then, A |= α(Fαi −,A1(∅), ~a).
Since A is a substructure of B by h, we have B |= α(h(Fαi −,A1(∅)), h(~a)). Thus, h(~a) ∈ Fα,B(h(Fαi −,A1(∅))). By the inductive hypothesis and since Fα,B is monotone, h(~a) ∈ Fαi ,B(∅).
h(Si∞=0 Fαi ,A(∅)) ⊆ Si∞=0 Fαi ,B(∅)
A |= ϕ(~a) (By assumption ϕ(~a) = [lfpR,y~α(R, ~y)](~a)) A |= [lfpR,y~α(R, ~y)](~a) (By Definition 2.3 and Knaster-Tarski’s Theorem) ~a ∈ Si∞=0 Fαi ,A(∅) (Since h is homomorphism) h(~a) ∈ h(Si∞=0 Fαi ,A(∅)) (By (1)) h(~a) ∈ S∞
i=0 Fαi ,B(∅) (By Definition 2.3 and Knaster-Tarski’s Theorem) B |= [lfpR,y~α(R, ~y)](h(~a)) (By definition of lfp) B |= ϕ(h(~a)) (1) ⇔ ⇔ ⇔ ⇒ ⇔