Document [original]

Forschungsberichte

der Fakultät IV – Elektrotechnik und Informatik

Correctness, Completeness and Termination of

Pattern-Based Model-to-Model Transformation:

Long Version

Fernando Orejas, Esther Guerra,

Juan de Lara, Hartmut Ehrig

Bericht-Nr. 2009-9

ISSN 1436-9915

Correctness, Completeness and Termination of

Pattern-Based Model-to-Model Transformation

(Long Version)

Fernando Orejas1, Esther Guerra2, Juan de Lara3, and Hartmut Ehrig4

1Universitat Polit`ecnica de Catalunya (Spain), orejas@lsi.upc.edu

2Universidad Carlos III de Madrid (Spain), eguerra@inf.uc3m.es

3Universidad Aut´onoma de Madrid (Spain), jdelara@uam.es

4Technische Universit¨at Berlin (Germany), [email protected]u-berlin.de

Abstract. Model-to-model (M2M) transformation consists in transform-

ing models from a source to a target language. Many transformation

languages exist, but few of them combine a declarative and relational

style with a formal underpinning able to show properties of the transfor-

mation. Pattern-based transformation is an algebraic, bidirectional, and

relational approach to M2M transformation. Specifications are made of

patterns stating the allowed or forbidden relations between source and

target models, and then compiled into low level operational mechanisms

to perform source-to-target or target-to-source transformations. In this

paper, we study the compilation into operational triple graph grammar

rules and show: (i) correctness of the compilation of a specification with-

out negative patterns; (ii) termination of the rules, and (iii) complete-

ness, in the sense that every model considered relevant can be built by

the rules.

1 Introduction

Model-to-model (M2M) transformation is an enabling technology for recent soft-

ware development paradigms, like Model-Driven Development. It consists in

transforming models from a source to a target language and is useful, e.g. to

migrate between language versions, to transform a model into an analysis do-

main, and to refine a model. In some cases, after performing the transformation,

the source and target models can be modified separately. Therefore, it is useful to

be able to execute transformations both in the forward and backward directions

to recover consistency. Thus, an interesting property of M2M transformation

languages is to allow specifying transformations in a direction-neutral way, from

which forward and backwards transformations can be automatically derived.

In recent years, many M2M specification approaches have been proposed [1,

2, 13–17] with either operational or declarative style. The former languages ex-

plicitly describe the operations needed to create elements in the target model

from elements in the source, i.e they are unidirectional. Instead, in declarative

approaches, a description of the mappings between source and target models is

provided, from which operational mechanisms are generated to transform in the

forward and backward directions.

In this paper, we are interested in declarative, bidirectional M2M transforma-

tion languages. Even though many language proposals exist, few have a formal

basis enabling the analysis of specifications or the generated operational mech-

anisms [18]. In previous work [3], we proposed a new graphical, declarative,

bidirectional and formal approach to M2M transformation based on triple pat-

terns. Patterns specify the allowed or forbidden relations between two models

and are similar to graph constraints [6], but for triple graphs. The latter are

structures made of three graphs representing the source and target models, as

well as the correspondence relations between their elements. Thus, in pattern-

based transformation we define the set of valid pairs of source and target models

by constraints, and not by rules. Then, patterns are compiled into operational

rules working on triple graphs to perform forward and backward transformations.

In the present work, we prove certain properties of the compilation of pattern-

based specifications into rules. First, we show that our compilation mechanism

generates graph grammars that are terminating. This result is interesting as it

means that we do not need to use external control mechanisms for rule applica-

tion [11]. Second, we prove that the transformation rules are sound with respect

to the positive fragment of the specification. This means that a triple graph satis-

fies all positive patterns in a specification if and only if it is terminal with respect

to the generated rules. In other words, the operational mechanisms actually do

their job, and this corresponds to the notion of correctness in [18]. Finally, we

also prove completeness of the rules, i.e. that the rules are able to produce any

model generated by the original M2M specification. These generated graphs are

a meaningful subset of all the models satisfying the specification.

Altogether, we think that this work paves the way to using formal methods

in one of the key activities of Model-Driven Development: the specification and

execution of M2M transformations. The rest of the paper has been organized as

follows. Section 2 provides an introduction to triple graphs and to the kind of

transformation rules that we use in this paper. Section 3 introduces M2M pattern

specifications, their syntax and semantics. Section 4 is the core of the paper: first

we introduce the transformation rules associated to a pattern specification and

then we prove their termination, soundness and completeness. Then, in Section

5 we compare the approach that we follow with some other approaches to M2M

transformation. Finally, in Section 6 we draw some conclusions and we sketch

some future work. In addition, along the paper we use a small running example

describing the transformation of class diagrams into relational schemas [16]. An

appendix includes the full proofs for all the presented results.

2 Preliminaries

This section introduces the basic concepts that we use throughout the paper

about triple graphs and triple graph transformation. Triple graphs [17] model

the relation between two graphs called source and target through a correspon-

dence graph and a span of graph morphisms. In this sense, if we consider that

models are represented by graphs, triple graphs may be used to represent trans-

formations, as well as transformation information through the connection graph.

Definition 1 (Triple Graph and Morphism). A triple graph G= (GS

←

→GT)(or just G=hGS, GC, GTiif cSand cTmay be considered implicit)

consists of three graphs GS,GC, and GT, and two morphisms cSand cT. A

triple graph morphism m= (mS, mC, mT): G1→G2is made of three graph

morphisms mS,mC, and mTsuch that mS◦c1

S=c2

S◦mCand mT◦c1

T=c2

T◦mC.

Given a triple graph G, we write G|Xfor X∈ {S, T }to refer to a triple graph

whose X-component coincides with GXand the other two components are the

empty graph, e.g. G|S=hGS,∅,∅i. Similarly, given a triple graph morphism

h:G1→G2we also write h|X:G1|X→G2|Xto denote the morphism whose

X-component coincides with hXand whose other two components are the empty

morphism between empty graphs. Finally, given G, we write iX

Gto denote the

inclusion iX

G:G|X→G, where the X-component is the identity and where the

other two components are the (unique) morphism from the empty graph into

the corresponding graph component.

Triple graphs form the category TrG, which can be formed as the functor

category Graph·←·→·. In principle, we may consider that Graph is the standard

category of graphs. However, the results in this paper still apply when Graph is

a different category, as long as it is an adhesive-HLR category [12, 6] and satisfies

the additional property of n-factorization (see below). For instance, Graph could

also be the category of typed graphs or the category of attributed (typed) graphs.

Definition 2 (Jointly surjective morphisms). A family of graph morphisms

{H1

→G,...,Hn

→G}is jointly surjective if for every element e(a node or

an edge) in Gthere is an e′in Hk, with 1≤k≤nsuch that fk(e′) = e.

A property satisfied by graphs and by triple graphs, is n-factorization, a

generalization (and also a consequence) of the property of pair factorization [6]:

Proposition 1 (n-factorization). Given a family of graph morphisms {H1

→

G,...,Hn

→G}with the same codomain G, there exists a graph H, a monomor-

phism mand a jointly surjective family of morphisms {H1

→H,...,Hn

→H}

such that the diagram below commutes:



.Hm//G



It may be noticed that if a category satisfies the n-factorization property and

{f1,...,fn}in the above diagram are monomorphisms then so are {g1,...,gn}.

In this paper, a graph transformation rule is a monomorphism (Lr

→R),

possibly equipped with some Negative Application Conditions (NACs) in its

left-hand side for limiting its application. The reason is that in our approach

we just need to use non-deleting rules. Hence, rule application is defined by a

pushout. Moreover, in our case, when applying a rule to a given graph G, it is

enough to consider the case where the morphism that matches Lto Gis a mono:

Definition 3 (Non-Deleting Triple Rule, Rule Application, Terminal

Graph). A (non-deleting) triple rule p=hN, L r

→Ri, consists of a triple

monomorphism rand a finite set of negative application conditions N={Lni

→

Ni}i∈I, where each niis a triple monomorphism.

A monomorphism m:L→Gis a match for the rule p=hN, L r

→Riif m

satisfies all the NACs in N, i.e. for each NAC Lni

→Nithere is no monomor-

phism h:Ni→Gsuch that m=h◦ni. Given a match m:L→Gfor p, the

application of pto Gvia m, denoted G⇒p,m H, is defined by the pushout below:

r//



m′



Gr′//H

where m′is called the comatch of this rule application.

Given a set TR of transformation rules, a triple graph Gis terminal for TR

if no rule in TR can be applied to G.

3 Pattern-Based Model-to-Model Transformation

Triple patterns are similar to graph constraints [6, 9]. We use them to describe

the allowed and forbidden relationships between the source and target models in

a M2M transformation. In particular, we consider two kinds of patterns. Negative

patterns, which are denoted by just a triple graph, describe relationships that

should not occur between the source and target models. This means that, from a

formal point of view, negative patterns are just like negative graph constraints,

i.e. a (triple) graph Gsatisfies the negative pattern Nif Nis not a subgraph

of G(up to isomorphism). Positive patterns specify possible relationships be-

tween source and target models. Positive patterns consist of a set of negative

premises and a conclusion. As we can see below, satisfaction of P-patterns does

not coincide exactly with satisfaction of graph constraints.

Definition 4 (Patterns, M2M Specification). An N-pattern, denoted N(Q)

consists of a triple graph Q. A P-pattern S={N(Qnj

→Cj)}j∈J⇒Qconsists of

–The conclusion, given by the triple graph Q.

–The negative premises N(Qnj

→Cj), given by the inclusions Qnj

→Cj.

An M2M specification SP is a finite set of P and N-patterns. Given a specifi-

cation SP , we denote by SP +(respectively, SP −) the positive fragment of SP ,

i.e. the set of all P-patterns in SP (respectively, the set of all N-patterns in SP ).

A P-pattern is intended to describe a class of transformations denoted by

triple graphs. P-patterns describe, simultaneously, source-to-target and target-

to-source transformations. In this sense, there are two notions of satisfaction as-

sociated to P-patterns: forward satisfaction, associated to source-to-target trans-

formations and backward satisfaction, associated to target-to-source transforma-

tions. Then, a triple graph Gforward satisfies a pattern {N(Qnj

→Cj)}j∈J⇒Q

if whenever QSis embedded in the source of G(and the premises are forward

satisfied by the embedding), Q is embedded in G. And an embedding mof QSin

GSforward satisfies a premise N(Qnj

→Cj) if there is no embedding m′of (Cj)S

in GSsuch that m′extends m. Backward satisfaction is the converse notion.

Definition 5 (Pattern Satisfaction).

–A monomorphism m:Q|S→Gforward satisfies a negative premise N(Qnj

→

Cj), denoted m|=FN(Qnj

→Cj)if there does not exist a monomorphism

g: (Cj)|S→Gsuch that m=g◦(nj)|S. Similarly, m:Q|T→Gbackward

satisfies a negative premise N(Qnj

→Cj), denoted m|=BN(Qnj

→Cj)if there

does not exist a monomorphism g: (Cj)|T→Gsuch that m=g◦(nj)|T.

–A triple graph Gforward satisfies a P-pattern S={N(Qnj

→Cj)}j∈J⇒Q,

denoted G|=FS, if for every monomorphism m:Q|S→G, such that, for

every jin J,m|=FN(Qnj

→Cj), there exists a monomorphism m′:Q→G

such that m=m′◦iS

(Cj)|S

Q|S

Q//

(nj)|S



m′

~~|

–A triple graph Gbackward satisfies a P-pattern S={N(Qnj

→Cj)}j∈J⇒Q,

denoted G|=BS, if for every monomorphism m:Q|T→G, such that, for

every jin J,m|=BN(Qnj

→Cj), there exists a monomorphism m′:Q→G

such that m=m′◦iT

–Gsatisfies S, denoted G|=S, if G|=FSand G|=BS.

–A triple graph Gsatisfies an N-pattern N(Q), denoted G|=N(Q)if there is

no monomorphism h:Q→G.

Though the abuse of notation, given a monomorphism m:Q→G, we may

also say that mforward satisfies a negative premise if the monomorphism iS

G◦

m|S:Q|S→Gforward satisfies it.

Example 1. The left of Fig. 1 shows a specification describing a transformation

between class diagrams and relational schemas [16]. When considered in the

forward direction, the transformation creates a database schema to store in tables

the attributes of the classes, where classes of the same inheritance hierarchy are

mapped to the same table. The first pattern C-T states that top-level classes

(i.e., those without parents in the inheritance hierarchy) are mapped to tables.

Note that we use a notation similar to UML object diagrams (i.e. c:C represents

a node cof type Class). N(NoDup) is an N-pattern that forbids associating two

tables to the same class. A-Co and ChC-T are P-patterns with an empty set

of premises. A-Co says that attributes of a class are stored in columns of the

associated table. Finally, ChC-T specifies that children and parent classes are

mapped to the same table. The right of the same figure shows an example of

satisfaction. Graph Gsatisfies all patterns in the specification and, in particular,

the diagram shows how an occurrence of ChC-T|Sis extended to ChC-T.

:T:C

:A :Co

A-Co

N(NoDup)

:T:C

c:C t:T

C-T

t:T

c:C

N(NoParent)

:T:C

ChC-T

:T:C

:A :Co

ChC-T

ChC-T|S

Fig. 1. Example patterns (left). Triple graph satisfying the specification (right).

4 Correctness, Completeness, and Termination of

Transformations

An M2M specification Scan be used in different scenarios [11]. We can build a

target model from a source model (or vice-versa), check whether two models can

be mapped according to S, or synchronize two models that previously satisfied S

but that were modified separately. Each scenario needs a specialized operational

mechanism. Here we cover the first scenario. Starting from a specification S, we

generate a triple graph grammar to perform forward transformations. Obviously,

the same techniques could be applied for implementing backward transforma-

tions. The basic idea is to see the given P-patterns as tiles that have to “cover” a

given source model, perhaps with some overlapping. The target model obtained

by gluing the target parts of these patterns is the result of the transformation.

In addition, the N-patterns allow us to discard some possible models.

Given a source model, a pattern specification will normally have many mod-

els. In particular, there may be several non-isomorphic triple graphs sharing the

same source graph. This means that there may be several correct transforma-

tions for that source graph. Our technique will non-deterministically allow us to

obtain all the transformations satisfying the specification. We think that this is

the only reasonable approach, if a priori we cannot select any preferred model. It

should be obvious that following this kind of approach it is impossible to build

some models of the given specification. In particular, it would be impossible to

generate models whose target and connection part cannot be generated using

the given patterns as described above. For instance, models whose target part

includes some nodes of a given type not mentioned in the patterns. We think that

restricting our attention to this kind of generated models is reasonable in this

context. This is similar to the “No Junk” condition in algebraic specification.

Our approach is based on associating to a given specification SP a set of

forward transformation rules TR(SP). These rules have, in the left-hand side, a

graph including the source part of the conclusion of a positive pattern and part

of the target and the connection part. In the right-hand side they have the whole

conclusion of the pattern. The idea is that these rules may be used to build “a

piece” of the target and the connection graphs, when we discover an occurrence

of the source part of a pattern on the given source graph. Rules may include part

of the target and connection part of the pattern because this part of the pattern

may have been already built by another pattern (rule) application. In addition,

the negative premises in the given positive patterns are transformed into NACs

of the given rules. Moreover, if we want these rules to be terminating, then we

may include some additional NACs that ensure the termination of the set of

transformation rules associated to all the P-patterns of a given specification. It

should be clear that we can define a set of backward rules in a similar way.

Definition 6 (Forward Transformation Rules for Patterns). To every

P-pattern S={N(Qnj

→Cj)}j∈J⇒Q, we associate the set of forward transfor-

mation rules TR(S)consisting of all the rules r=hNAC(r), Lr

→Qi, where:

–Lris a triple graph such that Q|S⊆Lr⊂Qand iis the monomorphism

associated to the inclusion Lr⊂Q.

–NAC(r)is the set that includes a NAC n′

j:Lr→C′

jfor each premise

N(nj:Q→Cj)in S, where n′

jand C′

jare defined up to isomorphism by

the pushout depicted on the left below.

The set of terminating transformation rules associated to S, TTR(S)is the

set of all rules hNAC(r)∪TNAC(r), Lr

→Qisuch that hNAC(r), Lr

→Qi ∈

TR(S)and TNAC (r)is the set of all the termination NACs for r, i.e. all the

monomorphisms n:Lr→Twhere there is a monomorphism f2:Q→Tsuch

that nand f2are jointly surjective and the diagram on the right below commutes:

Q|S

(nj)|S



(Cj)|S



Q|S

Q//



Lrn′

//C′

jLrn//T

Notice that the first condition implies that QS= (Lr)S. Notice also that, in

the construction of the NAC associated to a premise, (iS

Lr)Sis the identity, and

so are (n′

j)Cand (n′

j)T.

Example 2. Fig. 2 shows the two forward rules generated from pattern C-T pre-

sented in Example 1. The first one uses L=Q|S, while the LHS of the second

reuses an existing table. Both rules include a NAC (named NAC1), generated

from the negative pre-condition NoParent of the pattern. The termination NACs

ensure that each class is connected to at most one table.

c:C

c:C :T

c:C

NAC1

c:C :T

TNAC1

rC-T.1:

c:C

NAC1

c:C t:T

TNAC1

c:C t:T

C-T

t:T c:C t:T

TNAC2

rC-T.2:

Fig. 2. Forward rules generated from pattern C-T.

In some related work (e.g., [6, 4]) termination is ensured by just the termina-

tion NAC Lr→Q. This NAC is enough to ensure finite termination if the set of

possible matches of the given rule does not change after applying the transfor-

mation rules, i.e. if the possible matches of the rule are always essential matches,

according to the terminology in [6, 4]. However, this is not the case in our context.

Our rules may have triple graphs in the left-hand side with non-empty target or

connection part. As a consequence, at some point, there may exist non-essential

matches, and this may cause, if we would only use that NAC, that the resulting

transformation system is not terminating, as the example below shows.

Example 3. Suppose we have the rule shown to the left of Fig. 3, which is one

of the backward rules that we would derive from pattern ChC-T if we want to

apply our technique to implement backward model transformations. And sup-

pose that we only add a termination NAC (labelled TNAC) equal to its RHS. The

rule creates a new child of a class connected to a table. Then, the sequence of

transformations that starts as shown to the right of the same figure does not

terminate. This is so, because the rule adds a new match for the LHS in each

derivation, thus being able to produce an inheritance hierarchy of any depth.

t:Tc:C

t:Tc:C :T:C

:T:C

...

L R = TNAC M0

Fig. 3. Backward rule (left). Non-terminating sequence (right).

According to Definition 6, the set of termination NACs for the rule includes

the three graphs depicted in Fig. 4. TNAC2 is isomorphic to TNAC, but it identifies

the class in Lwith the child class. Then it is clear that TNAC2 avoids applying

the rule to M1, thus ensuring termination.

t:Tc:C

L R = TNACTNAC1

t:T:C

c:C

TNAC2

c:C

t:T:C

Fig. 4. Rule with termination NACs.

Definition 7 (Forward Transformation Rules for Specifications). Given

a pattern specification SP , we define the set of forward transformation rules

associated to SP :

TR(SP) = [

S∈SP +

TR(S)

Similarly, TTR(SP)is the set of terminating transformation rules associated

to the patterns in SP +.

Our first result shows that TTR(SP) is terminating. To show this result, we

first need to notice that the transformation rules never modify the source part of

the given triple graphs. Then, the key to show this theorem is a specific property

of our termination NACs ensuring that, if we have transformed the graph G1

into the graph G2using a rule rwith match m1:Lr→G1, then we cannot apply

the same rule with match m2:Lr→G2if the source parts of the domains of m1

and m2coincide. The reason is that, if we have already applied rwith match m1

then the graph G2will already embed Lrand Q(via m2and m1, respectively).

Moreover if the source parts of the domains of m1and m2coincide, then we can

ensure the existence of embeddings n:Lr→Tand h:T→G2, where nis a

termination NAC and h◦n=m2. Implicitly, this means that the termination

NACs impose finite bounds on the number of times that an element of the given

source graph can be part of a match.

Theorem 1 (Termination). For any finite pattern specification SP , TTR(SP)

is terminating.

Our second main result shows that a triple graph is terminal for TTR(SP) if

and only if it forward satisfies the positive patterns in SP . Obviously, we cannot

ensure that if Gis terminal then Gwill also satisfy the negative patterns in SP ,

since they play no role in the construction of TTR(SP).

Theorem 2 (Correctness). For any finite pattern specification SP ,G|=F

SP +if and only if Gis terminal with respect to TTR(SP).

To prove this theorem, first, we show that a morphism forward satisfies a

premise of a pattern if and only if it satisfies the corresponding NACs in the

associated rules. Then, we can see that if Gis a forward model of SP +and h

is a match for a rule rassociated to a pattern Sthat forward satisfies all the

negative premises in S, then hwill not satisfy a termination NAC in the rule.

Conversely, we can prove that if h:Q|S→Gis a monomorphism that satisfies

all the premises in Sand hdoes not satisfy the termination NAC of the rule

Q|S→Qthen there exists an h′:Q→Gthat extends h.

With respect to completeness, as discussed above, we are only interested in

the models whose elements in the target and connection part can be considered

to be there because some pattern prescribes that they must be there. We call

these graphs SP -generated.

Definition 8 (SP-Generated Graphs). Given a pattern specification SP , a

triple graph Gis SP -generated if there is a finite family of P-patterns {Sk}k∈K,

with Sk={N(Qk

→Cjk)}j∈J⇒Qkin SP , and a family of monomorphisms

{Qk

→G}k∈Ksuch that every fkforward satisfies all the premises in Sk, and

f1,...,fn, iS

Gare jointly surjective. In this case, we also say that Gis generated

by the patterns S1,...Snand the morphisms f1,...fn.

Example 4. Fig. 5 presents three SP-generated graphs from the example spec-

ification of Fig. 1, together with the family of patterns that generates them.

It must be noted that the same pattern may occur several times in the given

family generating the graph. For instance, the pattern A-Co is used twice for

generating G3. Graph G1is generated by pattern C-T, but is not a model of the

specification as the child class and its attribute need to be translated. On the

contrary, graphs G2and G3are models of the specification.

Our next result shows that, given a source graph GSusing the rules from

TR(SP), and starting from the graph hGS,∅,∅i, we can generate exactly all

SP -generated graphs Hsuch that HS=GS. Obviously not all SP -generated

graphs need to be models of the specification (for instance hGS,∅,∅i is generated

by the empty family of patterns), but this result ensures that if Hdescribes a

{C-T}

:T:C

G1:

{C-T, ChC-T, A-Co}

:T:C

G2:

:Co

{C-T, ChC-T, A-Co, A-Co}

:T:C

G3:

:Co :Co

Fig. 5. SP-generated graphs.

valid model transformation of GSand Honly contains nodes and edges that

the patterns prescribe that must be present, then Hcan be obtained by graph

transformation.

Theorem 3 (Characterization of SP-Generated Graphs). Given a pat-

tern specification SP ,Gis an SP -generated graph if and only if G|S⇒∗Gusing

rules from TR(SP).

The proof of this theorem goes as follows. First, we prove that if Gis gener-

ated by S1,...Snand f1,...fnthen there is a series of transformations:

i1//



AL2

i2//



... Ln



in//Qn



G|Sh1

//G1h2

//G2h3

//...

hn−1

//Gn−1hn

//Gn

such that G=Gnup to isomorphism, where the rules involved in these trans-

formations are obtained by the pullback:

mk//



Gk−1hn◦···◦hk

//G

Conversely, we can prove that if Gcan be obtained by a series of transformations

as the one above then Gis generated by the patterns associated to these rules,

together with the morphisms f1,...fn, where fk=hn◦ · · · ◦ hk+1 ◦ck.

As a direct consequence of this theorem we immediately get our first com-

pleteness result:

Corollary 1 (Completeness). Given a pattern specification SP , if Gis SP -

generated and G|=FSP then G|S⇒∗Gusing rules from TR(SP).

There are two aspects in the previous completeness result which may be

considered not fully satisfactory. On one hand, we have proved completeness of

TR(SP), i.e. a non-terminating transformation system. On the other hand, the

notion of generated model may not completely follow our intuition. In particular,

according to Def. 8, a given pattern may be used several times with the same

match to generate several different parts of the target and connection graphs.

Next, we provide a more restrictive notion of SP -generated graphs, namely

strictly SP -generated graphs, and then we show that strictly SP -generated for-

ward models are the terminal graphs of our terminating transformation systems.

Definition 9 (Strictly SP-Generated Graphs). Given a pattern specifica-

tion SP , a triple graph Gis strictly SP -generated if Gis an SP -generated

graph and for every P-pattern S={N(Qnj

→Cj)}j∈J⇒Q, if f1:Q→Gand

f2:Q→Gare two monomorphisms such that (f1)S= (f2)Sand both forward

satisfy all the premises nj:Q→Cj, then f1=f2.

Notice that in the above definition it is enough to ask that either f1or f2

forward satisfy all the premises of the pattern since this depends only on the

source component of the morphisms. Therefore, since both morphisms coincide

in their source component, if one of them forward satisfies a premise so will do

the other morphism.

Example 5. In Fig. 5, graphs G1and G2are strictly generated, while G3is not,

because both occurrences of A-Co share the same source.

Theorem 4 (Completeness for strictly SP-Generated Graphs). Given

a pattern specification SP , if Gis strictly SP -generated and G|=FSP then

G|S⇒∗Gusing rules from TTR(SP)and, moreover, Gis a terminal graph.

The key to prove the above theorem is to show that if Gis a strictly SP -

generated graph and we assume that Gis generated by a minimal family of pat-

terns S1,...Snand monomorphisms f1,...fn, then the minimality of the family

ensures that all the matches in the above derivation satisfy the corresponding

termination NACs, which means that the rules may be applied.

Finally, by Theorem 2 and Theorem 4, we have:

Corollary 2 (Soundness and Completeness). Given a pattern specification

SP consisting of positive patterns, and a strictly SP -generated graph Gthen

G|=FSP if and only if G|S⇒∗Gusing rules from TTR(SP)and Gis a

terminal graph.

Remark 1. Corollary 2 tells us that, given a set of positive patterns SP and a

source graph GS, the set of all strictly SP -generated forward models of SP ,

whose S-component coincides with GS, is included in the set of terminal graphs

obtained from hGS,∅,∅i. However, if SP includes some negative patterns, then

some (or perhaps all) of these terminal graphs may fail to satisfy these additional

patterns. As said above, this is completely reasonable since negative patterns

have not played any role in the construction of TR(SP) or TTR(SP). However,

the negative patterns can be added as NACs into the transformation rules as

described, for instance, in [6]. In this case, it will be impossible to transform a

graph G1into G2if G2would violate some negative pattern. Then, the trans-

formation system could be considered more efficient since the derivation tree

associated to a given start graph would be pruned from all the graphs violating

the negative patterns. However, in this case, our soundness and completeness

results would slightly change. In particular, a terminal graph would not nec-

essarily be a model of the given positive patterns anymore. More precisely, a

graph would be terminal if it is a model of the given positive patterns or if all

its possible transformations violate a negative pattern.

Example 6. Fig. 6 shows some derivations starting from a given graph G0using

the generated terminating forward rules. All graphs in the derivations are strictly

SP-generated. Hence all graphs in Fig. 5 are reachable. Notice that G3in Fig. 5

is not reachable using the terminating rules, as the rule generated from A-Co

is not applicable to G2. Graphs G2and G5are terminal w.r.t. TTR(SP): the

former is a forward model of SP , and the latter is only a forward model of

SP +because the N-pattern N(NoDup) is not satisfied. As stated in the remark,

we could add additional NACs to the generated rules to forbid applying a rule

creating an occurrence of N-patterns. In that case, rule rA−Co.1would not be

applied to G4and therefore graph G5would not be reached.

:T:C

:A :Co

:T:C

:A :T:C

:T:C

:A :Co

rC-T.1

rChC-T.1

rC-T.2

G0:

G1:

G2:

G4:

G5:

rA-Co.2

rA-Co.1

Fig. 6. Some derivations using the generated terminating forward rules.

5 Related Work

Some declarative approaches to M2M transformation are unidirectional, e.g.

PMT [19] or Tefkat [13], while we generate both forward and backward transfor-

mations. Among the visual, declarative and bidirectional approaches, a promi-

nent example is the OMG’s standard language QVT-relational [16]. Relations

in QVT contain when and where clauses to guide the execution of the opera-

tional mechanisms. In our case, it is not necessary because the generated rules

are terminating, correct and complete. Moreover, QVT lacks a formal semantics,

complicating the analysis. On the contrary, our patterns have a formal semantics,

which makes them amenable to verification.

TGGs [17] formalize the synchronized evolution of two graphs through declar-

ative rules. From this specification, low level operational TGG rules are derived

to perform forward and backward transformations, similar to our case. However,

whereas in declarative TGG rules dependencies must be made explicit (i.e. TGG

rules must declare which elements should exist and which ones are created), in

our patterns this information is derived when generating the rules.

Completeness and correctness of forward and backward transformations was

proved for TGGs in [7]. Termination was not studied because TGGs need a

control mechanism to guide the execution of the operational rules, such as pri-

orities [10] or their coupling to editing rules [5]. This is not necessary with our

patterns, but we need to ensure finite termination of the operational mechanisms.

The conditions for information preservation of forward and backward transfor-

mations was studied in [5]. Moreover, in [8] the results in [5] are extended to

the case of triple graph grammars with NACs. A similar result can be adapted

for pattern-based specifications.

In our initial presentation of pattern-based transformation [3], we introduced

some deduction operations able to generate new patterns from existing ones.

In the present paper, we have simplified the framework by eliminating such

deduction operations, but enriching the process of generating operational rules.

The new generation process ensures completeness as it generates each possible

LHS for the rules, which however could not be guaranteed with the deduction

operations. However, such operations can be used as heuristics to generate less

rules, or to reduce the non-confluent behaviour of the transformations.

6 Conclusions and Future Work

In this paper we have demonstrated three properties of the compilation mech-

anisms of pattern-based M2M specifications into graph grammar rules: finite

termination, correctness with respect to the positive fragment of the specifica-

tion and completeness. The first result allows using the generated rules without

any external control mechanism for rule execution, as a difference from current

approaches [11, 16, 17]. The correctness result ensures soundness of the opera-

tional mechanisms, and as remarked in the article, it can be easily extended to

correctness of specifications including negative patterns. Finally, completeness

guarantees that if the M2M specification has a model, then it can be found by

the operational mechanism.

Our results provide a formal foundation for our approach to pattern-based

M2M transformations. However, from a practical point of view, we believe that

the techniques presented in this paper have to be complemented with other tech-

niques that ensure some good performance. More precisely, our results guarantee

that using our approach we can obtain all the (generated) models of given speci-

fication, which means all the possible transformations that are correct according

to the given specification. However, on one hand, this is in general an exponen-

tial number of models, which implies that computing all these models would be

not feasible. On the other hand, typically, there may be some preferred kind of

model (for instance, models that are minimal in some sense) and, as a conse-

quence, we would not be interested in computing all the models, but only the

preferred ones. In addition, in order to make pattern-based transformation useful

for Model-Driven Development, we are currently addressing further challenges:

handling attributes in M2M specifications, supporting advanced meta-modelling

concepts like inheritance and integrity constraints, and tool support. Moreover,

we believe that pattern-based transformation can be used as a formal basis for

other transformation languages, like QVT.

Acknowledgments. Work supported by the Spanish Ministry of Science

and Innovation, projects METEORIC (TIN2008-02081), MODUWEB (TIN2006-

09678) and FORMALISM (TIN2007-66523). Moreover, part of this work was

done during a sabbatical leave of the first author at TU Berlin, with finan-

cial support from the Spanish Ministry of Science and Innovation (grant ref.

PR2008-0185). We thank the referees for their useful comments.

References

1. D. H. Akehurst and S. Kent. A relational approach to defining transformations in

a metamodel. In Proc. UML’02, volume 2460 of LNCS, pages 243–258. Springer,

2002.

2. P. Braun and F. Marschall. Transforming object oriented models with BOTL.

ENTCS, 72(3), 2003.

3. J. de Lara and E. Guerra. Pattern-based model-to-model transformation. In Proc.

ICGT’08, volume 5214 of LNCS, pages 426–441. Springer, 2008.

4. H. Ehrig, K. Ehrig, J. de Lara, G. Taentzer, D. Varr´o, and S. Varr´o-Gyapay. Ter-

mination criteria for model transformation. In M. Cerioli, editor, FASE, volume

3442 of Lecture Notes in Computer Science, pages 49–63. Springer, 2005.

5. H. Ehrig, K. Ehrig, C. Ermel, F. Hermann, and G. Taentzer. Information preserving

bidirectional model transformations. In Proc. FASE’07, volume 4422 of LNCS,

pages 72–86. Springer, 2007.

6. H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of algebraic graph

transformation. Springer-Verlag, 2006.

7. H. Ehrig, C. Ermel, and F. Hermann. On the relationship of model transformations

based on triple and plain graph grammars. In Proc. GRAMOT’08, 2008.

8. H. Ehrig, F. Hermann, and C. Sartorius. Completeness and correctness of model

transformations based on triple graph grammars with negative application condi-

tions. In GT-VMT 2009, Electronic Communications of the EASST, to appear,

2009.

9. R. Heckel and A. Wagner. Ensuring consistency of conditional graph rewriting - a

constructive approach. ENTCS, 2, 1995.

10. A. K¨onigs. Model transformation with triple graph grammars. In Proc. MTiP’05,

2005.

11. A. K¨onigs and A. Sch¨urr. Tool integration with triple graph grammars - a survey.

ENTCS, 148(1):113–150, 2006.

12. S. Lack and P. Sobocinski. Adhesive categories. In Foundations of Software Sci-

ence and Computation Structures, 7th International Conference, FOSSACS 2004,

volume 2987 of Lecture Notes in Computer Science, pages 273–288. Springer, 2004.

13. M. Lawley and J. Steel. Practical declarative model transformation with Tefkat. In

MoDELS Satellite Events, volume 3844 of LNCS, pages 139–150. Springer, 2005.

14. MOLA. MOdel transformation LAnguage. http://mola.mii.lu.lv/.

15. MTF. Model Transformation Framework. http://www.alphaworks.ibm.com/tech/mtf.

16. QVT. http://www.omg.org/docs/ptc/05-11-01.pdf, 2005.

17. A. Sch¨urr. Specification of graph translators with triple graph grammars. In Proc.

WG’94, volume 903 of LNCS, pages 151–163. Springer, 1994.

18. P. Stevens. Bidirectional model transformations in QVT: Semantic issues and open

questions. In Proc. MoDELS’07, volume 4735 of LNCS, pages 1–15. Springer, 2007.

19. L. Tratt. A change propagating model transformation language. JOT, 7(3):107–

126, 2008.

Appendix: Proofs of the results

The proposition below shows a property of our termination NACs which is the

key to prove the finite termination of the set of transformation rules associated

to a given specification. In particular, the termination NACs ensure that, if we

have transformed the graph G1into the graph G2using a rule rwith match

m:Lr→G1, i.e. if there is an injective morphism m1:Q→G2such that

m1coincides with mwhen restricted to Lr, then we cannot apply the same rule

with match m2:Lr→G2if (m1)S= (m2)S:

Proposition 2. Given a rule hNAC(r)∪T NAC(r), Lr

→Qiassociated to a

positive pattern and given a graph Gsuch that there is an injective morphism

m1:Q→G. If m2:Lr→Gis a monomorphism such that (m1)S= (m2)S

then there is a termination NAC (Lr

→T)∈T NAC(r)and a monomorphism

h:T→Gsuch that h◦n=m2.

Proof. We know that m1◦iS

Q=h(m1)S,(1G)C,(1G)Ti, where 1Gis the canonical

morphism from the empty graph to G. But, since QS= (Lr)Sand by the

assumption that (m1)S= (m2)S, we have that (m1)S◦(iS

Q)S= (m2)S◦(iS

Lr)S.

This means that the diagram below commutes:



Q|S

Q!!



Then, by the n-factorization property (Prop. 1) there exists a graph T and

monomorphisms h,fand n:





Q|S

Q!!

Th//G



such that fand nare jointly surjective and the diagram above commutes.

Proof of Theorem 1 Let G0be an arbitrary triple graph and let us suppose

that there exists an infinite sequence of transformations:

G0⇒T T R(SP )G1⇒TTR(SP )· · · ⇒TTR(SP )Gk⇒TTR(SP )...

This means that there are monomorphisms:

G0→G1→ · · · → Gk→...

Let us denote by hj→kthe monomorphism from Gjto Gkinduced by the

transformations. Now, since there is a finite set of rules, there should exist a rule

r∈TTR(SP ), r=hNAC(r)∪T NAC(r), Lr

→Qi, that is applied infinitely

often in the sequence. In addition, we know that the transformation rules do not

modify the source part, i.e. for every j, k, (hj→k)Sis the identity. But, since the

source part of G0is a finite graph there should exist two matches m:Lr→Gj

and m′:Lr→Gk, with j < k, such that mS=m′

If we have applied the rule rwith match mat step j, we have that Gj+1 is

obtained by the pushout depicted in the outer square:

i//



m′

m′′



||y

Gjhj→j+1

//Gj+1

hj+1→k

bbE

This means that g=hj+1→k◦m′′ is a monomorphism from Qto Gksuch

that gS=m′

S. Then, by Prop. 2, rincludes a termination NAC n:Lr→T

such that there is a monomorphism h:T→Gkwith h◦n=m′. But this means

that this NAC would not allow the application of rwith match m′against the

hypothesis.

Before proving our soundness and completeness results, we will prove a tech-

nical proposition, that shows that a morphism forward satisfies a precondition

of a pattern if and only if it satisfies its corresponding NAC in the associated

rules.

Proposition 3. Let hNAC(r)∪T NAC(r), Lr

→Qibe a rule associated to the

pattern S=N({Qnj

→Cj}j∈J)⇒Q, where the NAC n′

j:Lr→C′

jcorresponds

to the precondition nj:Q→Cj, and let m:Lr→Gbe a monomorphism. Then

there is a monomorphism h: (Cj)|S→Gsuch that h◦(nj)|S=m◦i1if and

only if there is a monomorphism h′:C′

j→Gsuch that h′◦n′

j=m, where i1is

the monomorphism associated to the inclusion Q|S⊆Lr.

Proof. Suppose that there is a monomorphism h: (Cj)|S→Gsuch that h◦

(nj)|S=m◦i1. By the universal property of pushouts there exists a morphism

h′making the diagram below commute:

Q|S

(nj)|S//



(Cj)|S



||y

Lrn′

m>>

}

}C′

h′

bbE

Thus, we have to prove that h′is injective. But this is not difficult. It is

enough to consider each of the components of h′. In particular, by construction,

we know that C′

j=h(Cj)S,(Lr)C,(Lr)Ti, which means that (i2)S=id,n′

C=id

and n′

T=id. As a consequence, h′=hhS, mC, mTi. But, since mand hare

assumed to be injective, so should be h′.

Conversely, suppose that h′:C′

j→Gis a monomorphism such that h′◦

n′

j=m. Then, if we define h=h′◦i2(see the diagram above), we have that

h◦(nj)|S=h′◦i2◦(nj)|S=h′◦n′

j◦i1=m◦i1.

Proof of Theorem 2

–Let us suppose that G|=FSP +this means that for every pattern S=

N({Qnj

→Cj}j∈J)⇒Qin SP +,G|=FSand this means that for every

monomorphism m:Q|S→G, such that for every j∈J,m|=FQnj

→Cj,

there exist a monomorphism m′:Q→Gsuch that m=m′◦iS

Let r=hNAC(r)∪T NAC(r), Lr

→Qibe a rule in TTR(S), we will show

that if h:Lr→Gis a match for the rule then there is some NAC in NAC(r)

that forbids the application of r.

If h:Lr→Gis a monomorphism then so it is m:Q|S→G, where m=h◦i1

and i1is the monomorphism associated to the inclusion Q|S⊆Lr.Then,

since G|=FS, we have two cases:

1. mdoes not forward satisfy some negative precondition. This means,

by Prop. 3, that hdoes not satisfy its corresponding NAC and, as a

consequence, the rule rwould not be applicable with match h.

2. msatisfies all the preconditions and there is a monomorphism m′:Q→

Gsuch that m′◦iS

Q=m=h◦i1. But (i1)Sand (iS

Q)Sare the identity and

this means that m′

S=hS. Then, by proposition 2 there is a termination

NAC in rsuch that hdoes not satisfy that NAC.

–Conversely, suppose that G is a terminal graph with respect to TTR(SP ),

let us see that Gsatisfies all the positive patterns in SP. Let S=N({Qnj

→

Cj}j∈J)⇒Qbe a pattern in SP +, we have to show that if m:Q|S→G

is a monomorphism, and for every j∈J,m|=FQnj

→Cj, there exist a

monomorphism m′:Q→Gsuch that m=m′◦iS

Q. Let rbe the terminating

rule r=hNAC(r)∪T NAC(r), Q|S→Qiassociated to that pattern. Notice

that in this case Lr=Q|S. Hence, by construction, the NAC associated to

the precondition nj:Q→Cjis the monomorphism (nj)|S:Q|S→(Cj)|S

and the only termination NAC is the inclusion i:Q|S→Q. Now, if h:

Q|S→Gis a monomorphism then his a possible match for the rule r.

Moreover, if hsatisfies the precondition nj:Q→Cjthen hsatisfies the

NAC (nj)|S:Q|S→(Cj)|S. Then, if Gis a terminal graph with respect to

T R(SP ), this may only mean that Gdoes not satisfy the termination NAC

i:Q|S→Q. But this means that there exist a monomorphism f:Q→G

such that f◦i=h.

Proof of Theorem 3

We start proving that if Gis an SP -generated graph then G|S⇒∗

T R(SP )G.

Let us assume that S1,...Sn,f1,...fnare the patterns and morphisms that

generate G. We will show that there is a series of transformations:

i1//



AL2

i2//



... Ln



in//Qn



G|Sh1

//G1h2

//G2h3

//...

hn−1

//Gn−1hn

//Gn

such that G=Gnup to isomorphism. More precisely, first we will show by

induction that for every k, if Sk=N({Qk

→Cjk}j∈J)⇒Qk, then there is a

rule rk=hNAC(r), Lk

→Qkiin T R(Sk) and there is an injective morphism

h′

k:Gk→Gsuch that (h′

k)Sis the identity (up to isomorphism), fk=h′

k◦ck

and h′

k=h′

k+1 ◦hk+1. Notice that the last condition implies that h′

k=h′

n◦hn◦

· · · ◦ hk+1. Finally, we will show that h′

nis an isomorphism.

–If n= 0 then trivially the theorem holds, since this means that G=G|S.

–Let us suppose that G|S⇒∗Gkand h′

k:Gk→Gis a monomorphism such

that (h′

k)Sis an isomorphism. Let rk+1 be the rule in T R(SP ) whose right-

hand side is Qk+1 and whose left-hand side, Lk+1 ⊆Qk+1, is defined (up to

isomorphism) by the following pullback, with inclusion ik+1 without loss of

generality:

Lk+1

mk+1 //

ik+1



Qk+1

fk+1



Gkh′

//G

Notice that there is such rule in T R(Sk+1), since we know that fk+1 is a

monomorphism from Qk+1 to Gand we also know that (h′

k)Sis the identity,

which means that there is a monomorphism from (Qk+1)|Sto G, defined by

(fk+1)S, and therefore, by the pullback property of Lk+1, (Qk+1)|S⊆Lk+1.

Now, to apply this rule to Gkwith match mk+1 we must first show that

mk+1 satisfies the NACs in NAC(rk+1). But this is a consequence of Prop.

3. Therefore, we know that we can apply the rule rk+1 with match mk+1 to

Gkyielding the graph Gk+1 and, by the universal property of pushouts, we

know that there is a morphism h′

k+1 :Gk+1 →Gsuch that fk+1 =h′

k+1◦ck+1

and h′

k=h′

k+1 ◦hk+1:

Lk+1

ik+1 //

mk+1



Qk+1

ck+1



fk+1

||z

Gkhk+1

h′

zGk+1

h′

k+1

Now, since the outer square is a pushout, the inner diagram is a pull-

back, the morphisms in the diagram are monomorphisms, and triple graphs

are an adhesive category, then h′

k+1 is a monomorphism. Moreover, since

h′

k=h′

k+1 ◦hk+1, (h′

k+1)Sis a monomorphism and (h′

k)Sand (hk+1)Sare

isomorphisms we can conclude that (h′

k+1)Sis an isomorphism.

To end this part of the proof we must show that h′

nis an isomorphism. We

know that h′

nis a monomorphism and (h′

n)Sis an isomorphism, so we have

to prove that (h′

n)Tand (h′

n)Care also surjective. Let ebe an element in GT

(a node or an edge). Since the morphisms f1,...,fn, iS

Gare jointly surjective

and (G|s)Tis the empty graph then (f1)T,...,(fn)Tare jointly surjective. As

a consequence, there exists an element ek∈(Qk)Tsuch that e=fk(ek). But,

since fk=h′

k◦ck=h′

n◦hn◦ · · · ◦ hk+1 ◦ckthis means that there is an element

en∈Gn,en=hn◦ · · · ◦ hk+1 ◦ck(ek) such that h′

n(en) = fk(ek) = e. Similarly,

we could prove that (hn)Cis surjective.

Let us now prove that if G|S⇒∗

T R(SP )Gthen Gis SP -generated. So, suppose

that we have a derivation:

i1//



AL2

i2//



... Ln



in//Qn



G|Sh1

//G1h2

//G2h3

//...

hn−1

//Gn−1hn

//Gn

with Gn=G. We will prove that, if we define the morphisms f1=hn◦ · · · ◦

h2◦c1,...fk=hn◦ · · · ◦ hk+1 ◦ck,...,fn=cn, then f1,...,fn, iS

Gare jointly

surjective. Now, since Gis the result of the sequence of pushouts of the above

diagram, this means that Gis the colimit of that diagram, and this implies that

the morphisms f1,...,fn, hn◦· · ·◦h1are jointly surjective. But, (hn◦· · ·◦h1)Sis

the equality since the rules in T R(SP ) do not modify the source part of the triple

graphs. As a consequence, hn◦ · · ·◦ h1=iS

G, which means that f1,...,fn, iS

Gare

jointly surjective.

Proof of Theorem 4

Let Gbe a strictly SP -generated forward model of SP . Since Gis an SP -

generated graph, we know that Gis generated by some finite families of patterns

{Sk}k∈Kand morphisms {fk}k∈K. Let {Sk}k∈Kand {fk}k∈Kbe minimal in the

sense that, for any K′⊂K,Gis not generated by {Sk}k∈K′and {fk}k∈K′.

As we have seen in the proof of Theorem 3, if {Sk}k∈Kconsists of the patterns

S1,...Sn, and {fk}k∈Kconsists of the morphisms f1,...fn, then there is a

T R(SP )-derivation:

i1//



AL2

i2//



... Ln



in//Qn



G|S=G0h1

//G1h2

//G2h3

//... hn−1

//Gn−1hn

//Gn

with Gn=G, where each rule rkis associated to the pattern Skand where

fk=h′

k◦ck, where h′

k=hn◦ · · · ◦ hk+1 :Gk→G. So we will prove that we

can produce the same derivation applying the corresponding rules in TTR(SP ).

More precisely, we need to prove that, for every k,mksatisfies all the termi-

nation NACs in the rule hNAC(rk)∪T NAC(rk), Lk

→Qki, which are all the

monomorphisms g1:Lk→Twhere there is a monomorphism g2:Qk→Tsuch

that g1and g2are jointly surjective and the square subdiagram on the top-left

corner of the diagram below commutes:

(Qk)|S

Qk//

i′



Lkg1//

mk$$



Gk−1

h′

k−1

and where i′

kis the inclusion (Qk)|S⊆Lk. Let us suppose that there is a

monomorphism f:T→Gk−1such that f◦g1=mk. Then we have that

h′

k−1◦f◦g1◦i′

k=h′

k−1◦mk◦i′

k=h′

k◦hk◦mk◦i′

k=h′

k◦ck◦ik◦i′

k=fk◦ik◦i′

k, using

h′

k◦ck=fk. On the other hand we have that h′

k−1◦f◦g1◦i′

k=h′

k−1◦f◦g2◦iS

Qk,

which means h′

k−1◦f◦g2◦iS

Qk=fk◦ik◦i′

kand, hence, (h′

k−1◦f◦g2)S= (fk)S.

Therefore, we have two monomorphisms fkand h′

k−1◦f◦g2from Qkto G

such that their source component coincides. Moreover, we know that fksatisfies

all the preconditions in the pattern Sk, which means that h′

k−1◦f◦g2also

satisfies all the preconditions in Sk. Hence, since Gis assumed to be strictly

SP -generated, fk=h′

k−1◦f◦g2. But this means that Gis generated by the

patterns {S1,...Sn} \ {Sk}, and the morphisms {f1,...fn}\{fk}, since every

element in the image of fkis also on the image of h′

k, which means that this

element is in the image of f1,...fk−1. Therefore S1,...Snand f1,...fnwould

not be minimal, against our original assumption.

Finally, by Theorem 2, we know that if Gnis a model of SP , then Gnis

terminal with respect to TTR(SP ).