Towards Domain Completeness for Model Transformations Based on Triple Graph Grammars

Abstract

The analysis of model transformations is a challenging research 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 speci ed independently from the TGG, we use the notion of domain completeness, which requires that the model transformation has to provide a corresponding 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 rst of two components for verifying domain completeness. The running example is the well studied object-relational mapping.

Keywords

• model transformation
• completeness
• graph grammars
• constraints

-

Triple graph grammars (TGGs) [ 1,2,3 ] are a well-established concept for the speci cation 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 simpli es speci cation 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 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.

De nition 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 2 LS . 4

The challenge for showing domain completeness is to verify that LS L(TGG )S. The main contribution of this paper provides the rst of two steps for showing this property. We provide a general technique for verifying that a language de ned by a type graph and constraints is contained in a language that is de ned using a non-deleting graph grammar. Since, TGGs consist of nondeleting 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 de ned by constraints is contained in a language de ned by a nondeleting 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 speci c languages (DSLs) LS and LT , we cannot assume that the languages are speci ed with graph grammars. In many application scenarios, DSLs are speci ed 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 de nition 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 = L o 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 G o D / H side R. A transformation step G ==p;=m) H via match morphism 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 n K at m(L) and adding R n K. In the case of a non-deleting rule p = (L id L ! R) the rule is simply p = (L ! R) and the rst pushout is ommitted. Classifier type {abstract} 1 *

TGS NamedElement

{abstract} name:String

Class PrimitiveType

Attribute * attrs 1

TGC AC CT TT

TGT

Column name:String pkey colsref type

A triple graph G = (GS sG GC t!G 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 fabstractg) 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 according to [ 6 ] providing the concepts for both, graph constraints and application conditions for rules. Conditions consist of formulas in rst order logic over morphisms (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 expressions 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 re nement) according to the inheritance relation in the type graph (cf. clan morphisms [ 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 re nements and merges of data values along match morphism from conditions in C. 4 1: AttributeMembership c1 = (ac : P  C,true ) P :Attribute

C :Class

:attrs :Attribute 2: AbstractTypes c2 =i{1.3} (aci : P  Ci,true) C1 P :NamedElement v C2 Example 4 (Graph Constraints). Three of nine domain constraints CS for LS are depicted in Fig. 2. They subsume requirements concerning multiplicities (constraint 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- mS = mC = mT sisting of three graph morphisms that preserve the HS o HC / 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 speci es how a given consistently integrated model can be extended simultaneously on all three components yielding again a consistently integrated model. Moreover, triple rules can be extended by application conditions for restricting their application to speci c matches [ 10 ]. Example 5 (Triple Rules). The integrated models of our running example are speci ed by the triple rules in Fig. 3. Rule 1 (C2T) creates a Class with its corresponding 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 member (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 corresponding to the PrimitiveType, but only, if no other ColumnType is already de ned 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 de ned 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 consistent source and target languages L(TGG )S = fGS j (GS GC ! GT) 2 L(TGG )g and L(TGG )T = fGT j (GS GC ! GT) 2 L(TGG )g. The operational 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 rst 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 language L0S = L(TG S ; TGG S ) generated by the grammar of source rules T GGS (LS L0S ). E ectively, 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 verifying language inclusions. This notion instantiates to the special case of nondeleting grammars of source rules in our TGG scenario. C-extension completeness 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 de nes 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 ful ll violation stable constraints (namely C-inconsistent graphs) when computing extensions.

The extension of a graph G via a set of constraints C is de ned recursively starting with the initial extension that contains graph G only. A new extension 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 E0 by adding the non-overlapping part of the conclusion to GE with extension step E =e=x=te=n=d=(G=E=;=c)) E0. De nition 6 (C-Extensions). Let G be a graph. f The extensions of G via morphism f and match P p / P 0 f0 */ C bmelofowr.mTthhee seextteonfsgiornapshsofgiGvenvbiay eaxtceonnds(tGra;ifn;tmc) m m0 (1) and a match m form the set of graphs given by - GE / G0E 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) = fG0E j (1) above is a pushout with f; f 0; m; m0; p 2 M; m0 p = m; and f 0 p = f;

G0E is not C-inconsistentg { extend(GE; c; m) = Si2I extend(GE; aci; m); m 2 M;

c _i2I 9(aci : P ! Ci; true) { Extensions(G; C) = ffGgg [ fE0 j E0 = E n fGEg [ extend(GE; c; m); E 2 Extensions(G; C); GE 2 E; c 2 Inst(C); c _i2I 9(aci : P ! Ci; true); m : P ! GE 2 Mg 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 following extension steps: fGg ==ex=t=en=d=(G==;c=5)) fG1g =e=x=te=n=d=(G=1=;c=5)) fG1; G2g; fG1g =e=x=te=n=d=(G=1=;c=2)) fG3; G4g =e=x=te=n=d=(G=3=;=c1=)) fG4; G5g =e=x=te=n=d=(G=4=;c=1)) fG5; G6g =e=x=te=n=d=(G=5=;=c3=)) fG6; G7g =e=x=te=n=d=(G=6=;=c3=)) fG7; G8g. Constraint c5 is similar to c1 and ensures that each attribute is of type Classi er. 4

For C-extension completeness it is su cient to consider only the smallest graphs that may occur in a language, namely e ective 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 e ective atoms of a language L that is typed over ATG. E ective atoms are those atoms in Atoms(ATG) that may occur in graphs of language L.

G1

G2

G3

G4 :Attribute :Attribute

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 e ective atoms over ATG , an extension via constraints C can be found that is in L.

De nition 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 8 a 2 EAtoms(ATG ) : 9 S 2 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 e ective 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 fG7; G8g 2 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 de ne an upper bound for the graph size of input graphs for the model transformation. In addition to C-extension completeness another property called C-con ict-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).

The con ict-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 Cinconsistent 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 violation 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-con ict-freeness of marking rules. The marking rules are C-con ict-free, if for each critical pair K1 (=p1=;o==1 O ==p2=;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-con ict-free and L2 is C-extension complete, then L1 L2. 4 Proof (Idea). Let G 2 L1. G can be decomposed into its atoms A = Atoms(G) with G = Sa2A(a). C-extension completeness of L2 ensures that each atom a can be extended via C to aE with aE 2 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-con ict 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 2 L2). The full proof is given in [ 12 ]. tu

For the running example in Sec. 2 we successfully veri ed the language inclusion 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 -con ict 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 correctness and completeness, e.g. [ 14,15 ]. Pattern-based model-to-model transformations 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 domain language, whose speci cation 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 de ned 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 constructing marking rules that allowed us to apply the theory for critical pair analysis 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 di erences 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 domaincompleteness, in order to be general enough to match practical scenarios, where domain languages are speci ed by meta models and constraints. If the model transformation does not concern the complete source domain, we assume that the source language LS speci es 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 ts perfectly to the non-deleting nature of TGGs for model transformations. However, an extension to other (possibly deleting) model transformation formalisms 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 presented approach to a model transformation in the domain of satellite control languages.

Acknowledgements We thank Barbara Konig and Hartmut Ehrig for their comments on preparing this paper.

Supported by the Fonds National de la Recherche, Luxembourg (4895603).

Nachtigall et. al.

References

1. Schurr, A.: Speci cation 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. Schurr, 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 Transformation 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.: E cient Analysis and Execution of Correct and Complete Model Transformations Based on Triple Graph Grammars . In Bezivin, J., Soley , R. , Vallecillo , A., eds.: MDI' 10 , ACM ( 2010 ) 22 { 31

11. Ehrig , H. , Ermel , C. , Hermann , F.: Transformation of Type Graphs with Inheritance for Ensuring Security in E-Government Networks . In Wirsing, M. , Chechik , M., eds. : Proc. International Conference on Fundamental Aspects of Software Engineering (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. : Correctness 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 Termination 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. , Clariso , R. , Guerra , E., de Lara , J.: Veri cation and validation of declarative model-to-model transformations through invariants . J. Syst. Softw . 83 ( 2 ) ( February 2010 ) 283 { 302