Towards Domain Completeness for Model Transformations Based on Triple Graph Grammars Nico Nachtigall1 , Frank Hermann1 , Benjamin Braatz1 , and Thomas Engel1 Interdisciplinary Centre for Security, Reliability and Trust, Université du Luxembourg, Luxembourg firstname.lastname@uni.lu Abstract. The analysis of model transformations is a challenging re- search area within model driven engineering. Triple graph grammars (TGGs) have been applied in various transformation scenarios and their formal foundation has been a vital ground for general results concerning notions of correctness and completeness. This paper addresses existing gaps between practical scenarios and the formal results of TGGs concerning the notion of completeness. Since the source domain language of a model transformation is usually specified in- dependently from the TGG, we use the notion of domain completeness, which requires that the model transformation has to provide a corre- sponding target model for each model of the source domain language. As main result, we provide a general method for showing that the source domain language is included in the language that is generated by the source rules of the TGG. This provides the first of two components for verifying domain completeness. The running example is the well studied object-relational mapping. Keywords: model transformation, completeness, graph grammars, con- straints 1 Introduction Triple graph grammars (TGGs) [1,2,3] are a well-established concept for the specification and execution of bidirectional model transformations within model driven software engineering. Their main advantage is an automatic generation of operational rules for forward and backward model transformations, which simplifies specification and enhances usability as well as consistency. Several formal results for analysing general properties of model transformations based on TGGs have been developed. In present work [4], the notion of completeness and correctness of model transformations via TGGs is based on the language L(TGG) that is induced by the TGG itself. However, in practical scenarios, the source and target languages are given independently from the TGG. We consider the general case where the source domain language LS = L(TG S , CS ) is given by a source type graph TG S and 2 Nachtigall et. al. a set of source constraints CS . The TGG generates the language L(TGG)S of source models. In this more general case, we may observe that LS 6= L(TGG)S . This is not problematic, as long as we can still ensure completeness with respect to LS , which we call domain-completeness in this paper. Definition 1 (Domain Completeness). A model transformation M T with source language LS is called domain complete, if it generates a target model MT for each source model MS ∈ LS . 4 The challenge for showing domain completeness is to verify that LS ⊆ L(TGG)S . The main contribution of this paper provides the first of two steps for showing this property. We provide a general technique for verifying that a language defined by a type graph and constraints is contained in a language that is defined using a non-deleting graph grammar. Since, TGGs consist of non- deleting rules only, we can instantiate this result for showing that the source domain language is contained in the language that is generated by the source rules of the TGG, i.e. LS ⊆ L(TGG S ). The second step is then to show that L(T GGS ) ⊆ L(TGG)S using the constraints of LS . In Sec. 2, we present the general scenario and framework for proving domain completeness and Sec. 3 presents our method and main result for showing that a language defined by constraints is contained in a language defined by a non- deleting grammar. Sec. 4 discusses related work and Sec. 5 summarises the main results and describes aspects of future work. 2 General Framework In the general case of model transformations M T : LS V LT between domain specific languages (DSLs) LS and LT , we cannot assume that the languages are specified with graph grammars. In many application scenarios, DSLs are specified by a meta model and OCL constraints [5]. In the theory of graph transformation systems, meta models correspond to type graphs and constraints to nested graph constraints [6]. Hence, we generally assume that the source language is given by LS = (TG S , CS ) with type graph TG S and constraints CS . Graph constraints and grammars allow the definition of graph languages in a declarative, or respectively, procedural manner. In this paper, we use the general notion of M-adhesive transformation systems [7,8] as basis for plain graph grammars GG and triple graph grammars TGG. A transformation rule p is given by a span p = Lo K /R (L ← K → R) of injective graph-morphisms (mappings m  (P O)  (P O)  for nodes and edges) with left hand side L and right hand Go D /H p,m side R. A transformation step G === ⇒ H via match mor- phism m : L → G is given by two pushouts as depicted on the right. Intuitively, H is obtained by removing from G the parts in L \ K at m(L) and adding id R \ K. In the case of a non-deleting rule p = (L ← − L → R) the rule is simply − p = (L → R) and the first pushout is ommitted. Towards Domain Completeness for Triple Graph Grammars 3 TGS TGC TGT NamedElement {abstract} name:String Classifier type Column Attribute AC {abstract} 1 * name:String * ref type attrs pkey cols 1 Table Class CT name:String ColumnType PrimitiveType TT name:String Fig. 1. Domain meta-model (TG S ) and triple type graph (T GS ← T GC → T GT ) sG tG A triple graph G = (GS ← −− GC − −→ GT ) is an integrated model consisting of a source graph GS , a target graph GT and explicit correspondences given by correspondence graph GC together with graph morphisms sG : GC → GS and tG : GC → GT . As running example, we use a variant of the well-known model transformation from class diagrams to relational database models (CD2RDBM) [9,2]. Example 2 (Meta model and triple type graph). Fig. 1 depicts the meta-model T GS of the source language and the type graph T GS ← T GC → T GT of the TGG. Class diagrams contain classes (Class) with Attributes (Attribute) and relational database models contain corresponding tables (Table) with columns (Column). Abstract node types (label {abstract}) may not appear in instances and multiplicity constraints on edge types type and attrs require that each Attribute has exactly one type and is contained in exactly one Class. 4 Formally, we use graph constraints in the notion of (nested) conditions ac- cording to [6] providing the concepts for both, graph constraints and application conditions for rules. Conditions consist of formulas in first order logic over mor- phisms (implications) P → C with premise graph P and conclusion graph C. Remark 3 (Matches and instances of constraints Inst(C)). In the context of model transformations, rules should be applied along match morphisms that do not identify structures of graphs, but which may identify attribute expres- sions to identical values. This class of morphisms is called almost injective [10]. Moreover, matches may map nodes to nodes with a more concrete type (type refinement) according to the inheritance relation in the type graph (cf. clan mor- phisms [8,11]). The same situation arises for matches of constraints. Therefore, we use the concept of a schema constraint, which interprets a constraint c as the disjunction of its possible instances Inst(c) which may occur in a graph. The instances Inst(C) of conditions C subsume all possible type refinements and merges of data values along match morphism from conditions in C. 4 4 Nachtigall et. al. 1: AttributeMembership 2: AbstractTypes 3: NamedElementHasName c1 = ( ac : P  C , true ) c2 =  i{1..3} (aci : P  Ci , true) c3 = ( ac : P  C , true ) C1 :Class P C :Class P P C C2 :NamedElement :Attribute :attrs :NamedElement v :Attribute :NamedElement name = n :Attribute C3 :PrimitiveType Fig. 2. Some domain constraints CS of domain language LS 1: C2T = Class2Table(n:String) ++ ++ ++ :Class ++ ++ :Table :CT name = n ++ name = n ++ 4: TP2T = TypeOfPrimitive2TypeOf() :cols ++ ++ :pkey NAC ++ :ColumnType :Column ++ :type :type ++ :Attribute :AC :Column :ColumnType :type ++ ++ :type name = INT ++ :PrimitiveType :TT :ColumnType 2: PT2CT = PrimitiveType2ColumnType(n:String) 5: TC2T = TypeOfClass2TypeOf() ++ ++ ++ NAC :PrimitiveType ++ ++ :ColumnType :ColumnType :TT name = n ++ name = n ++ :type :Attribute :AC :Column 3: A2C = Attribute2Column(n:String) :type ++ :ref ++ ++ :type :Class :CT :Table :Class :CT :Table :ColumnType :attrs ++ ++ :cols :pkey :type ++ ++ ++ ++ ++ :Attribute :AC :Column :Column name = n ++ name = n ++ Fig. 3. Triple rules of TGG for CD2RDBM transformation Example 4 (Graph Constraints). Three of nine domain constraints CS for LS are depicted in Fig. 2. They subsume requirements concerning multiplicities (con- straint 1 – each attribute must be contained in a class) and forbidden abstract types (constraint 2 – each named element must be of type Class, Attribute or PrimitiveType) given in Fig. 1. Additionally, each named element must have one name (constraint 3). 4 Triple graphs are related by triple graph mor- GS o GC / GT phisms m = (mS , mC , mT ) : G → H [1,2] con- m  m   mT S = C = sisting of three graph morphisms that preserve the S o C / H H HT associated correspondences (i.e., the diagrams on the right commute). A triple rule tr is given by a morphism (tr : L → R). Thus, it is non-deleting and specifies how a given consistently integrated model can be extended simultaneously on all three components yielding again a consis- tently integrated model. Moreover, triple rules can be extended by application conditions for restricting their application to specific matches [10]. Towards Domain Completeness for Triple Graph Grammars 5 Example 5 (Triple Rules). The integrated models of our running example are specified by the triple rules in Fig. 3. Rule 1 (C2T) creates a Class with its corre- sponding Table having the same name and a column of type INT that stores the primary key (edge pkey). Rule 2 (PT2CT) creates a primitive type (PrimitiveType) with its mapped ColumnType. Rule 3 (A2C) creates an Attribute as a class mem- ber (edge attrs) with its mapped Column that belongs to the corresponding Table (edge cols). Rule 4 (TP2T) connects an Attribute with a PrimitiveType as type and correspondingly, connects a Column via edge type with the ColumnType corre- sponding to the PrimitiveType, but only, if no other ColumnType is already defined for this Column (negative application condition NAC). Rule 5 (TC2T) connects an Attribute with a class as type and correspondingly, connects a Column via edge ref with the Table corresponding to the Class and via edge type with the corresponding ColumnType determined by the primary key, but only, if no other ColumnType is already defined for this Column. 4 A triple graph grammar TGG = (TG, SG, P ) consists of a triple type graph TG, a triple start graph SG and a set P of triple rules, and generates the triple graph language of consistently integrated models L(TGG) ⊆ L(TG) with con- sistent source and target languages L(TGG)S = {GS | (GS ← GC → GT ) ∈ L(TGG)} and L(TGG)T = {GT | (GS ← GC → GT ) ∈ L(TGG)}. The op- erational rules of a TGG for forward and backward model transformations are derived by an automatic construction [3,10]. The operational source rules TGG S of a TGG are obtained by restricting the rules of P to their source components. 3 C-Extensions for Domain Completeness This section presents the first of two parts for showing domain completeness of a model transformation via TGGs, namely showing that a given source language LS = L(TG S , CS ) with constraints CS is contained in the lan- guage L0S = L(TG S , TGG S ) generated by the grammar of source rules T GGS (LS ⊆ L0S ). Effectively, this means to provide a method for showing that all graphs satisfying the constraints can be constructed via the source rules. We introduce the general notion of C-extension completeness of a language for ver- ifying language inclusions. This notion instantiates to the special case of non- deleting grammars of source rules in our TGG scenario. C-extension complete- ness is used to ensure that the constraints guarantee all language restrictions that are induced by the grammar. We iterate over all minimal fragments of the meta model and – when needed – extend them to show that they can be constructed via the grammar. For full formal details we refer to [12]. Def. 6 defines the step-wise extension of a graph G via constraints C. A constraint c is violation stable under embedding, if for any graph G that violates c it holds that for any inclusion G ,→ H also H violates c. Thus, we can neglect graphs that do not fulfill violation stable constraints (namely C-inconsistent graphs) when computing extensions. The extension of a graph G via a set of constraints C is defined recursively starting with the initial extension that contains graph G only. A new extension 6 Nachtigall et. al. is derived from an existing extension E as follows: a) Let GE be a graph of E, let c be an instance of a constraint in C without negations that may have one or more conclusions connected by disjunctions and let m : P → GE be a match from the premise P of c to GE . b) Compute all overlappings of the conclusions of c with GE with respect to m. c) For each overlapping, a new graph G0E is potentially added to E leading to extension E 0 by adding the non-overlapping extend(G ,c) part of the conclusion to GE with extension step E =======E==⇒ E 0 . Definition 6 (C-Extensions). Let G be a graph. f / * The extensions of G via morphism f and match P p P 0 f0 / C m form the set of graphs given by extend(G, f, m) below. The extensions of G via a constraint c m m0  (1)  - GE / G0 and a match m form the set of graphs given by E extend(G, c, m) below. The extensions of G via a set of constraints C form the set of sets of graphs given by Extensions(G, C) below. – extend(GE , f, m) = {G0E | (1) above is a pushout with f, f 0 , m, m0 , p ∈ M, m0 ◦ p = m, and f 0 ◦ p = f, G0E is not C-inconsistent} S – extend(GE , c, m) = i∈I extend(GE , ac i , m), m ∈ M, c ≡ ∨i∈I ∃(aci : P → Ci , true) – Extensions(G, C) = {{G}} ∪ {E 0 | E 0 = E \ {GE } ∪ extend(GE , c, m), E ∈ Extensions(G, C), GE ∈ E, c ∈ Inst(C), c ≡ ∨i∈I ∃(aci : P → Ci , true), m : P → GE ∈ M} 4 In practice, C-extensions are considered only up to isomorphism. Example 7 (C-Extensions). Fig. 4 depicts some extensions Extensions(G, CS ) of graph G via constraints CS of Fig. 2. The extensions are obtained by the extend(G,c5 ) extend(G1 ,c5 ) following extension steps: {G} ========= ⇒ {G1 } =========⇒ {G1 , G2 }; extend(G ,c ) extend(G ,c )∗ extend(G ,c ) {G1 } =======1==2⇒ {G3 , G4 } =======3==1=⇒ {G4 , G5 } =======4==1⇒ ∗ ∗ extend(G ,c ) extend(G ,c ) {G5 , G6 } =======5==3=⇒ {G6 , G7 } =======6==3=⇒ {G7 , G8 }. Constraint c5 is similar to c1 and ensures that each attribute is of type Classifier. 4 For C-extension completeness it is sufficient to consider only the smallest graphs that may occur in a language, namely effective atoms, and from which more complex graphs can be composed. With Atoms(ATG) we denote the set of those graphs that are typed over an attributed type graph ATG and that are atomic in the sense that they can not be divided into smaller subgraphs. Therefore, for attributed graphs the structure of each atom is given by either a) an empty graph, or b) a node, or c) an edge with source and target nodes, or d) an attribute edge with source and target. With EAtoms(L) we denote the set of effective atoms of a language L that is typed over ATG. Effective atoms are those atoms in Atoms(ATG) that may occur in graphs of language L. Towards Domain Completeness for Triple Graph Grammars 7 G G1 G2 G3 G4 G5 G6 G7 G8 :Class :Class :Class :Class name = n1 name = n1 :attrs :attrs :attrs :attrs :Attribute :Attribute :Attribute :Attribute :Attribute :Attribute :Attribute :Attribute :Attribute name = n2 name = n2 :type :type :type :type :type :type :type :type :type :Classifier :Classifier :Class :Primitive :Class :Primitive :Class :Primitive Type Type name = n3 Type :Classifier name = n3 Extensions(G, CS ) = {{G}, {G1 }, {G1 , G2 }, {G3 , G4 }, {G4 , G5 }, {G5 , G6 }, {G6 , G7 }, {G7 , G8 }, . . .}. Fig. 4. C-extensions of effective atom : Attribute Example 8 (Effective Atom). The effective atoms with respect to the domain lan- guage LS = L(T GS , CS ) of the running example are those atoms in Atoms(T GS ) that fulfill the domain constraint 2 for abstract types in Fig. 2. Graphs G, G3 and G4 in Fig. 4 are effective atoms with respect to LS . Graph G1 is an atom but not effective, since, Classifier is an abstract type. Graphs G2 , G5 , G6 , G7 and G8 are not atoms. 4 C-extension completeness (cf. Def. 9) of a language L typed over ATG with respect to a set of constraints C states that for all effective atoms over ATG, an extension via constraints C can be found that is in L. Definition 9 (C-Extension Completeness). Let C be a set of constraints typed over ATG. Then, a language L typed over ATG is called C-extension complete, if ∀ a ∈ EAtoms(ATG) : ∃ S ∈ Extensions(a, C) : S ⊆ L. 4 Example 10 (C-Extension Completeness). We show CS -extension completeness of language L(TG S , TGG S ) from Sec. 2 (cf. Fig. 1 for TG S , Fig. 2 for CS and Fig. 3 for TGG S ). For each effective atom over TG S an extension via constraints CS must be found that is contained in language L(T GS , TGG S ). An extension is contained in the language, if it can be constructed via the rules in TGG S . For atom G in Fig. 4, the extension {G7 , G8 } ∈ Extensions(G, CS ) can be found via CS (cf. Ex. 7). The extension can be constructed by applying source rules (1, 1, 3, 5) or (1, 2, 3, 4) successively leading to graphs G7 or G8 , respectively. 4 In order to ensure termination, when checking C-extension completeness one can define an upper bound for the graph size of input graphs for the model transformation. In addition to C-extension completeness another property called C-conflict-freeness of marking rules is neccessary in order to verify full language inclusions L1 = L(T G, C) ⊆ L2 = L(TG, GG) of languages L1 and L2 . For a non-deleting grammar, the set of marking rules contains for each rule r, a marking rule r0 . Whenever r creates an element x (node, edge or attribute), then r0 preserves this element and updates its marker from F (false) to T (true). 8 Nachtigall et. al. The conflict-freeness of the marking rules with respect to a language L with constraints C is analysed by performing a critical pair analysis with AGG [13]. Similarly to C-inconsistent graphs, a critical pair (K1 ⇐ = O⇒ = K2 ) is C- inconsistent if graph O violates a violation stable constraint of constraints C. C-inconsistent critical pairs do not need to be analysed, since, there exists a vi- olation stable constraint that forbids the critical pair and any of its embeddings into larger contexts to be in L. This leads to the notion of C-conflict-freeness of marking rules. The marking rules are C-conflict-free, if for each critical pair p ,o1 p ,o2 K1 ⇐=1=== O ==2==⇒ K2 that is not C-inconsistent with marking rules p1 and p2 , the rules and matches are the same (p1 = p2 , o1 = o2 ). The main result is stated by Thm. 11. Intuitively, the inclusion holds if each graph G in L1 can be decomposed into its atoms G0 ⊆ G such that for each atom G0 an extension E ⊆ G can be constructed via constraints C that is contained in L2 and the composition of the extensions leads to graph G in L2 again by applying the rules of grammar GG. Theorem 11 (C-extension Completeness). Let L1 = L(ATG, C) be a language typed over ATG and with constraints C and let language L2 = L(ATG, GG) be restricted by a non-deleting grammar GG = (ATG, SG, P ) with an empty start graph SG = ∅. If the marking rules m(GG) are C-conflict-free and L2 is C-extension complete, then L1 ⊆ L2 . 4 S Let G ∈ L1 . G can be decomposed into its atoms A = Atoms(G) Proof (Idea). with G = a∈A (a). C-extension completeness of L2 ensures that each atom a can be extended via C to aE with aE ∈ L2 and aE ⊆ G. Therefore, aE can be created via GG. By the equivalence of marking and transformation sequences, each aE can be fully marked with true. The C-conflict freeness of the marking rules allows to apply the Local-Church-Rosser-Theorem and we derive a marking sequence that fully marks all extended atoms aE to true. Thus, there is a sequence via GG that creates G (G ∈ L2 ). The full proof is given in [12]. t u For the running example in Sec. 2 we successfully verified the language inclu- sion L1 = L(T GS , CS ) ⊆ L2 = L(T GS , T GGS ). Language L2 is CS -extension complete and the marking rules m(T GGS ) are CS -conflict free. This means that the domain constraints CS are strict enough to cover all language restrictions that are induced by the source rules in T GGS . 4 Related Work The formal construction and analysis of model transformations based on TGGs has been started in [2] by analysing information preservation of bidirectional model transformations and continued in a series of papers concerning correct- ness and completeness, e.g. [14,15]. Pattern-based model-to-model transforma- tions have been introduced in [16] and show a strong correspondence to TGGs. Corresponding correctness and completeness and termination results have been presented in [17]. The existing results, however, do not concern the actual source Towards Domain Completeness for Triple Graph Grammars 9 domain language, whose specification is independent from the TGG and given by the application scenario for the model transformation. In [18], the notion of total TGGs is introduced similar to the notion of domain completeness. A TGG is total if it generates a valid target model for each valid source domain model where validity is defined by conformance with meta-models and the satisfaction of domain constraints. Totality is checked by analysing OCL invariants that must hold for pairs of source and target models. The concept of translation attributes [10] is applied in this paper for con- structing marking rules that allowed us to apply the theory for critical pair anal- ysis in the context of domain completeness. Translation attributes were inspired by the translation algorithm in [3], which uses a set for storing the elements that have been translated during a transformation. In [2], a similar case study based on forward rules is presented, but without using NACs. The grammar with NACs in this paper handles primary keys and foreign keys in a more appropriate way and allows us to illustrate the formal details and possible differences between the involved language types. 5 Conclusion & Discussion In formal analysis of model transformations, completeness is certainly one of the most important properties in many domains of model driven engineering. In this paper, we described the general scenario in which model transformations based on triple graph grammars (TGGs) are used. We introduced the notion of domain- completeness, in order to be general enough to match practical scenarios, where domain languages are specified by meta models and constraints. If the model transformation does not concern the complete source domain, we assume that the source language LS specifies the relevant part. In most previous results it was required that the source domain language is contained in the language that is derived by restricting the integrated language generated by the TGG to the source component. This paper closes one half of this gap by providing a method for showing that the source domain language is contained in the language that is generated by the source rules of the TGG. For this purpose, we provided general results for graph transformation systems and extended the existing formal results for TGGs. The restriction of the results to non-deleting grammars seems to be very strict but fits perfectly to the non-deleting nature of TGGs for model transformations. However, an extension to other (possibly deleting) model transformation for- malisms is interesting and left for future work. Furthermore, we will extend the method by the second step to show domain completeness and to apply the pre- sented approach to a model transformation in the domain of satellite control languages. Acknowledgements We thank Barbara König and Hartmut Ehrig for their comments on preparing this paper. Supported by the Fonds National de la Recherche, Luxembourg (4895603). 10 Nachtigall et. al. References 1. Schürr, A.: Specification of graph translators with triple graph grammars. In: Graph-Theoretic Concepts in Computer Science. Volume 903 of LNCS., Springer (1994) 151–163 2. Ehrig, H., Ehrig, K., Ermel, C., Hermann, F., Taentzer, G.: Information preserving bidirectional model transformations. In: Fundamental Approaches to Software Engineering. Volume 4422 of LNCS., Springer (2007) 72–86 3. Schürr, A., Klar, F.: 15 Years of Triple Graph Grammars. In: Proc. ICGT’08. Volume 5214 of LNCS. (2008) 411–425 4. Hermann, F., Ehrig, H., Orejas, F., Czarnecki, K., Diskin, Z., Xiong, Y., Gottmann, S., Engel, T.: Model synchronization based on triple graph grammars: correctness, completeness and invertibility. Software & Systems Modeling (2013) 1–29 5. Object Management Group: Object Constraint Language, Version 2.2. (2010) 6. Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. in Computer Science 19 (2009) 1–52 7. Ehrig, H., Golas, U., Hermann, F.: Categorical Frameworks for Graph Transfor- mation and HLR Systems based on the DPO Approach. Bulletin of the EATCS 102 (2010) 111–121 8. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006) 9. Bezivin, J., Rumpe, B., Schuerr, A., Tratt, L.: Model transformations in practice workshop. In Bruel, J.M., ed.: Satellite Events at the MoDELS 2005 Conference. Volume 3844. Springer (January 2006) 120–127 10. Hermann, F., Ehrig, H., Golas, U., Orejas, F.: Efficient Analysis and Execution of Correct and Complete Model Transformations Based on Triple Graph Grammars. In Bézivin, J., Soley, R., Vallecillo, A., eds.: MDI’10, ACM (2010) 22–31 11. Ehrig, H., Ermel, C., Hermann, F.: Transformation of Type Graphs with Inheri- tance for Ensuring Security in E-Government Networks. In Wirsing, M., Chechik, M., eds.: Proc. International Conference on Fundamental Aspects of Software En- gineering (FASE’09). Volume 5503 of LNCS., Springer (2009) 325–339 12. Nachtigall, N., Hermann, F., Braatz, B., Engel, T.: Towards Domain Completeness for Model Transformations Based on Triple Graph Grammars - Extended Version. Technical Report TR-SnT-2014-14, University of Luxembourg, SnT (2014) 13. TFS-Group, TU Berlin: AGG. (2014) http://www.tfs.tu-berlin.de/agg. 14. Hermann, F., Ehrig, H., Orejas, F., Czarnecki, K., Diskin, Z., Xiong, Y.: Correct- ness of model synchronization based on triple graph grammars-extended version. Technical Report 2011-07, TU Berlin, Fak. IV (2011) 15. Giese, H., Hildebrandt, S., Lambers, L.: Bridging the gap between formal semantics and implementation of triple graph grammars. Software & Systems Modeling 13(1) (2014) 273–299 16. de Lara, J., Guerra, E.: Pattern-Based Model-to-Model Transformation. In Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G., eds.: Proc. 4th Int. Conf. on Graph Transformations (ICGT 2008). Volume 5214 of LNCS., Springer (2008) 426–441 17. Orejas, F., Guerra, E., de Lara, J., Ehrig, H.: Correctness, Completeness and Ter- mination of Pattern-Based Model-to-Model Transformation. In Kurz, A., Lenisa, M., Tarlecki, A., eds.: Int. Conf. on Algebra and Coalgebra in Computer Science (CALCO’09). Volume 5728 of LNCS., Springer (2009) 383–397 18. Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw. 83(2) (February 2010) 283–302