scieee AI-readable full text Open interactive document viewer

GTS Families for the Flexible Composition of Graph Transformation Systems

Durán, Francisco,Zschaler, Steffen

Abstract

Morphisms between graph-transformation systems (GTSs) have been successfully used for the refinement, reuse, and composition of GTSs. All these uses share a fundamental problem: to be able to define a morphism, source and target GTSs need to be quite similar in their structure (in terms of both the type graphs and the set of rules and their respective structures). This limits the applicability of these approaches by excluding a wide range of mappings that would intuitively be accepted as meaningful, but that cannot be captured formally as a morphism. Some researchers have attempted to introduce some flexibility, but these attempts either focus only on the type graphs (e.g., Kleisli morphisms between type graphs) or only support specific forms of deviation (e.g., supporting sub-typing in type graphs through clan morphisms). In this work, we introduce the notion of GTS families, which provide a general mechanism for explicitly expressing the amount of acceptable adaptability of the involved GTSs so that the intended morphisms can be defined. On this basis, we demonstrate how GTS families that are extension preserving can be used to enable flexible GTS amalgamation.

Full text

GTS Families for the Flexible Composition of Graph Transformation Systems Steffen Zschaler1and Francisco Dur´an2 1Department of Informatics, King’s College London, London, UK, WC2R 2LS [email protected] 2Dpto. de Lenguajes y Ciencias de la Computaci´on, University of M´alaga, Spain [email protected] Abstract. Morphisms between graph-transformation systems (GTSs) have been successfully used for the refinement, reuse, and composition of GTSs. All these uses share a fundamental problem: to be able to define a morphism, source and target GTSs need to be quite similar in their structure (in terms of both the type graphs and the set of rules and their respective structures). This limits the applicability of these approaches by excluding a wide range of mappings that would intuitively be accepted as meaningful, but that cannot be captured formally as a morphism. Some researchers have attempted to introduce some flexibility, but these attempts either focus only on the type graphs (e.g., Kleisli morphisms between type graphs) or only support specific forms of deviation (e.g., supporting sub-typing in type graphs through clan morphisms). In this work, we introduce the notion of GTS families, which provide a general mechanism for explicitly expressing the amount of acceptable adaptability of the involved GTSs so that the intended morphisms can be defined. On this basis, we demonstrate how GTS families that are extension preserving can be used to enable flexible GTS amalgamation. 1 Introduction Graph transformation systems (GTSs) were proposed in the late seventies as a formal technique for the rule-based specification of the dynamic behaviour of systems [1]. Since then, GTSs have been used in different contexts in computer science, including the formalisation of systems, programming languages and model-driven engineering. In the many contexts in which GTSs have been used, a key ingredient for exploiting their power is that of GTS morphisms. GTS morphisms have been used for different purposes in system specification, for instance, to characterise the relationship between a system and views of it [2], for expressing refinements [3,4], or for modelling import and export interfaces of modules [5]. Recent uses of GTSs in the context of Model-Driven Engineering (MDE) have gone one step further, proposing practical uses of different forms of parametric GTSs for reusing model transformations, and reusing and composing domain specific language (DSL) definitions. In [6], de Lara and Guerra proposed the use of transformation templates, typed by a graph, that they call concept, which can then be instantiated by binding the concept to a concrete graph. Dur´an et al. proposed in [7,8] what they call parameterised GTSs, where the parameter is not just a type graph, but a complete GTS, and where composition of GTSs is based on a GTS amalgamation construction. In the same way concepts gather the structural requirements, the set of rules of parameter GTSs are behavioural requirements over the concrete GTSs used in the instantiation. In each of these cases, using GTS morphisms enables useful syntactic or semantic guarantees to be given. For example, in [6] the use of morphisms means that transformations can be guaranteed to be syntactically reusable. In the case of [8], the use of suitable morphisms enables guarantees on behaviour protection of amalgamated GTSs. For reuse and composition, the main difficulty is the flexibility of the mechanisms available. In specific domains, ad hoc definitions of GTS morphisms have been proposed. For example, an alternative notion of refinement relation is given for transactional graph transformation systems in [9], where a graph typing mechanism induces a distinction between stable and unstable graph items and where implementation morphisms map single productions to whole transactions so that morphisms define simulations. Taentzer [10] uses a subset of UML extended by reconfiguration and import/export view facilities, represented as embedding morphisms, to propose a formal framework for visual modeling of distributed object systems. Component composition is defined by only allowing embedding morphisms between import and export rules where each two rules connected by an embedding morphism are named equally. These specialised solutions do not easily extend to the general setting. The use of GTSs in MDE introduces even more challenges, as we need to consider more complex graphs including attributes and node-type inheritance [11]. The need for a mechanism for relating different GTSs, or their type graphs, that is more flexible than direct morphisms—to broaden opportunities for GTS reuse—has been recognised before: In the case of models, represented as graphs, this has been resolved more or less pragmatically by supporting a specific, fixed set of adaptations to be applied prior to applying the morphism (see, e.g., [6,11,12,13]). For example, Diskin et al. [12] propose using Kleisli categories for relating models. De Lara and Guerra extended their work on concepts in [13] by using adapters to allow heterogeneities between the concept and the concrete graph. Each of these works “hard wires” a specific set of flexibilities. To support complete GTSs, rules must also be related in a flexible manner. In [14,15], Große-Rhode et al. introduce temporal and spatial refinement relations. In a spatial refinement, each rule is refined by an amalgamation (i.e., a parallel composition with sharing) of rules, while in a temporal refinement it is refined by a sequential composition. Engels et al. [5] present a framework for classifying and systematically defining GTS morphisms. Different types of morphisms are characterised by their relationship between the behaviours of source and target GTSs. For instance, refinements are a case of behaviour-preserving morphisms, while views are a case of behaviour-reflecting morphisms. Dur´an et al. [8] similarly introduce different behaviour-aware GTS morphisms. These solutions are, however, far from satisfactory. Even though the introduction of derived attributes and links as in [12] or [13], and the behavioural relations provided for GTS morphisms as in [8] improve the chances of defining the required morphisms, structural mismatch remains a problem. Often even where there is an intuitive match, no morphism can be established. This substantially limits the reuse potential of these approaches. In many cases, a simple restructuring of the GTSs involved could easily allow a valid mapping to be established. However, there is currently no support for capturing such restructurings, and in particular for capturing exactly the set of restructurings the designer of a GTS would consider valid and meaningful. In this work, we propose the use of GTS transformers to refactor GTSs with the goal of resolving the structural mismatches between source and target GTSs so that GTS morphisms can be defined. In fact, GTS transformers may be seen as re-factoring mechanisms, which provide a general setting for defining adaptations. GTS transformers are functions, and can successively be applied to our source GTS to find the one on which the morphism can be defined. To systematise this, we introduce the notion of GTS families. Given a set of transformers T, the T-family of a GTS GTS0is the set of GTSs reachable from GTS0using the transformers in T. The problem of defining a mapping morphism between a GTS GTS0and a target GTS GTS1then amounts to finding a GTS in the family of GTS0from which the morphism can be defined. This way, the problem becomes a model-based search problem [16]. Of course, any mechanisms enabling more flexibility must balance this against the required level of control so that suitable semantic properties can be guaranteed. We provide different transformers and prove that they preserve extensions [17] between GTSs. As a result, we show how these transformers can be used to enable flexible composition of GTSs. The remainder of this paper is structured as follows. In Sect. 2, we introduce a running example and motivate the limitations of GTS morphisms and the need for more flexibility. After providing some formal background on typed attributed graphs, GTSs, and their morphisms in Sect. 3, Sect. 4 introduces the notions of GTS transformers and GTS families as well as three example GTS transformers. In Sect. 4.3, we show that these transformers are extension preserving and can, thus, be used to compose GTSs using the mechanism from [17]. We wrap up in Sect. 5 with some conclusions and lines of future research. 2 Running Example Let us consider a simple production-line system (PLS) GTS, part of which is depicted in Fig. 1. This GTS models a PLS for making hammers out of hammer heads and handles. In the type graph TGPLS in Fig. 1a we find different types of machines, different types of parts, and different containers of parts.3The behaviour of such systems is defined through a number of graph-transformation 3We use the hollow-arrow notation from UML to denote inheritance relationships. GenHead GenHandle Tray Conveyor Hammer Handle Head Machine Part Container Assemble Generator parts out in out Polisher (a) PLS type graph out p : Polisher t : Tray c : Conveyor p : Part in out p : Polisher t : Tray c : Conveyor p : Part in LHS RHS parts parts (b) Polisher transformation rule :Assemble :Tray :Conveyor in :GenHead :GenHandle :Conveyor :Conveyor out out out out :Tray out :Polisher :Conveyor in out :Tray out (c) Sample typed graph Fig. 1: Production line system Queue Server Element elts out in Output Input made (a) Server type graph (b) Process transformation rule Fig. 2: Server tracking system rules, like the one in Fig. 1b, which models the polishing of a part by a polishing machine. Other actions, like the generation of head and handle parts in generator machines, the assembling of hammers out of hammer heads and handles, the moving of parts along conveyors, or the collection of parts from final trays is modelled by corresponding rules. A sample graph conforming to such type graph, providing an instance of the system, is shown in Fig. 1c. In it, we can see how machines take parts from input trays and put their outputs in corresponding conveyors, which move parts towards trays. Let us suppose now that we wanted to keep track of the elements polished in our production line system. Instead of modifying our PLS GTS, we may use the mechanism in [17] to compose it with a generic tracker system, the Tracker GTS defined in Fig. 2. Its type graph TGTracker is depicted in Fig. 2a. It describes the concepts related to servers that process elements taken from input queues into resulting elements that are placed in output queues. The action of processing an input element is then modelled by the transformation rule in Fig. 2b. The made association allows servers to keep track of all processed instances. To compose the Tracker and the PLS GTSs following the construction in [17], we take the Tracker GTS as a parameterized GTS. The Server GTS, shown in Fig. 3, defines a generic behaviour, the structural and behavioural requirements Queue Server Element elts out in Output Input (a) Server type graph LHS RHS out s : Server q1 : Queue q2 : Queue i : Input in elts elts out s : Server q1 : Queue q2 : Queue o : Output in (b) Process transformation rule Fig. 3: Server system parameter GTS the Tracker GTS builds on. Note that we can easily establish an inclusion gto the Tracker GTS. Then, we can compose the Tracker GTS with the PLS GTS so that polisher machines would keep track of the parts it processes: GTS0 _ g  f//GTS2 _ bg  GTS1// [ GTS where GTS0is the parameter GTS Server, GTS1is the parameterized GTS Tracker, and GTS2is the PLS GTS used in the instantiation. For this to work, we need to establish a GTS morphism between the Server GTS (the parameter) and the PLS GTS. Intuitively, the PLS GTS might be seen as a concrete interpretation of the Server GTS—e.g., polishing of parts can be seen as particular case of the server processing. A morphism between the two GTSs would be the formal expression of this. Let us first focus on the type graphs. At first sight, it may seem quite reasonable to define a binding between TGServer and TGPLS by mapping Server into Polisher, and Queue into Container,4with the in and out associations going to the corresponding ones in the PLS system type graph. However, in TGPLS input and output “queues” are represented by two different types: Tray and Conveyor, respectively. As a result, we cannot establish a valid morphism. Whether source and target queues are of the same type is not actually relevant to our specification of Server nor to the definition of tracking. We would like to be able to express the intuition that this particular mapping should be considered valid. Even where we can establish a morphism between the type graphs, there may still be problems establishing morphisms between the rule sets. In this paper, we introduce the notions of GTS transformers and GTS families and show how they can be used to automatically rewrite the Server and Tracker GTSs in sync to find the GTS depicted in Fig. 4, for which a morphism to the PLS GTS can straightforwardly be defined. Thus, GTS families enable expressing the above intuition about what GTS mappings we would like to allow. 4Notice that although we use Queue to name the device in which input and output elements are placed, no specific order is assumed on its elements in the server GTS. Queue Server Element elts out in Queue1 Queue2 Output Input (a) Type graph with added subclasses LHS RHS out s : Server q1 : Queue1 q2 : Queue2 i : Input in elts elts out s : Server q1 : Queue1 q2 : Queue2 o : Output in (b) Modified process rule Fig. 4: Modified GTS 3 Preliminaries on GTSs, clans, and clan morphisms We focus on the double pushout (DPO) approach to graph transformation [3]. In this section, we introduce some of the basic definitions concerning typed graphs and the algebraic approaches to the rewriting of typed graphs, and provide background definitions underpinning our discussion throughout this paper. The notation and most of the definitions in this section follow very closely those in, e.g., [3,8,13,18]. 3.1 Graph transformation systems Given some category of graphs and graph morphisms Graph, and given a distinguished graph TG, called type graph, a TG-typed graph (G, gG), or simply typed graph if TG is known, consists of a graph Gand a typing homomorphism gG:G→T G associating with each vertex and edge of Gits type in TG. To enhance readability, we will use simply gGto denote a typed graph (G, gG), and when the typing morphism gGcan be considered implicit, we will often refer to a typed graph (G, gG) just as G. A TG-typed graph morphism between TG-typed graphs (Gi, gi:Gi→T G), with i= 1,2, denoted f: (G1, g1)→(G2, g2), is a graph morphism f:G1→G2which preserves types; that is, g2◦f=g1. A graph transformation rule5pis of the form Ll ←Kr →Rwith graphs L, K, and R, called, resp., left-hand side, interface, and right-hand side, and some kind of monomorphisms (typically inclusions) land r. In the DPO approach to graph transformation, the application of a transformation rule p=Ll ←Kr →Rto a graph Gvia a match m:L→Gis constructed as two gluings (1) and (2), which are pushouts in the corresponding graph category, leading to a direct transformation Gp,m =⇒H. L m(1) K l oor// (2) R  G D oo//H 5As a simplification, we do not consider application conditions (cf., e.g., [8]). A graph transformation system (GTS) over a type graph TG is a triple (TG, P, π) where Pis a set of rule names and πis a function mapping each rule name pinto a rule Ll ←Kr →Rtyped over TG. Since we are interested in relating GTSs over different type graphs, we need to move graphs and graph morphisms along morphisms. Assuming GraphTG the category of TG-typed graphs and TG-typed graph morphisms, a graph morphism f:TG →TG0induces forward and backward retyping functors f>: GraphTG →GraphTG0and f<:GraphTG0→GraphTG . Since, as said above, we refer to a TG-typed graph G→TG just by its typed graph G, leaving TG implicit, given a morphism f:TG →TG0, we may refer to the corresponding TG0-typed graph by f>(G). Since we can retype graphs and graph morphisms, we can retype rules. Given a rule pover a type graph TG and a graph morphism f:TG →TG0, we will write things like f<(p) and f>(p) denoting, respectively, the backward and forward retyping of rule p. 3.2 Morphisms between graph transformation systems Although the mechanisms presented in the following sections may be applicable to most notions of GTS morphisms defined in the literature, to simplify the presentation we will focus on a specific type of rule morphism and GTS morphism. We begin with rule morphisms, relating two graph-transformation rules.6 Definition 1. Given rules pi=Li li ←− Ki ri −→ Ri, for i= 0,1, a rule morphism f:p0→p1is a tuple f= (fL, fK, fR)of graph monomorphisms fL:L0→L1, fK:K0→K1, and fR:R0→R1such that the squares with the span morphisms l0,l1,r0, and r1are pullbacks, as in the diagram below. p0: f  L0 fLpb K0 l0 oor0// fK pb R0 fR  p1:L1K1 l1 oor1 //R1 We are now ready to introduce GTS morphisms.7 Definition 2. Given GTSs GTSi= (TGi, Pi, πi), for i= 0,1, a GTS morphism f:GTS0→GTS1, with f= (fTG , fP, fr), is given by a morphism fTG :TG0→ TG1, a surjective mapping fP:P1→P0between the sets of rule names, and a family of rule morphisms fr={fp:f> T G(π0(fP(p))) →π1(p)}p∈P1. A special kind of GTS morphism is a GTS extension, which is essentially an inclusion such that everything being added to the rules of the extended GTS is typed by elements also added to the type graph. 6Similar definitions of rule morphisms can be found in the literature where the squares are pushouts instead of pullbacks, or simply commuting squares (e.g., [19]), or where the relations are between a single rule and a collection of rules (e.g., spatial and temporal refinements [4]). Requiring pullbacks is quite natural though: the intuition of morphisms is that they should preserve the “structure” of objects. 7See [5] for a systematic classification of other definitions of GTS morphisms. Definition 3. (GTS Extension [17]) Given GTSs GTSi= (TGi, Pi, πi), for i= 0,1, a GTS morphism f:GTS0→GTS1, with f= (fTG , fP, fr), is an extension morphism if fTG is a monomorphism and for each p∈P1,π0(fP(p)) = f< TG (π1(p)). 3.3 Typed attributed graphs and clan morphisms Our underlying graphs are attributed graphs typed over attributed type graphs with inheritance [3,11]. In these graphs, attributes are represented as edges between graph nodes and data nodes (captured by the notion of E-graphs in [3]). We use symbolic graphs [20,21] to enrich graphs with a set Φof formulas over a signature Σ= (S, Ω), with Sa set of sorts and Ωa set of operations. We assume that each formula is an equality between a variable and its value (grounded symbolic graphs in [20]). For simplicity, we assume attributed graphs on the same signature and omit a treatment of cardinalities and composition relations, which could be given as constraints as discussed in [22]. We refer the interested reader to [20,21] for a more general presentation of symbolic attributed graphs. An attributed graph ATG = (TG, Φ) may be used as a type graph. As for any type of graph, a typed attributed graph (AG, t) over an attributed type graph ATG consists of an attributed graph AG together with an attributed morphism t:AG →ATG. A typed attributed graph morphism f: (AG1, t1)→(AG2, t2) is an attributed graph morphism f:AG1→AG2such that t2◦f=t1. To deal with object-oriented systems we need some additional machinery. We follow [11] in defining attributed type graphs with inheritance. Definition 4. An attributed type graph with inheritance ATGI = (ATG, I, Ab) consists of an attributed type graph ATG = (TG, Φ), with an E-graph TG = (V, E, A, D, sE, tE, sA, tA), a set I⊆V×Vof inheritance relations, and a set Ab ⊆Vof abstract nodes. The typing of an object diagram with respect to a class diagram is typically represented as a clan morphism [11]. Intuitively, a clan morphism f:AG → ATGI from an attributed graph AG to an attributed type graph with inheritance ATGI is an attributed graph morphism that takes into account the inheritance relation and abstraction definitions of the target ATGI . Definition 5. Let ATGi=(TGi, ΦATGi), with i=1,2, be attributed type graphs, with TGi=(VTGi, ETGi, ATGi, DTGi, sE TGi, tE TGi, sA TGi, tA TGi), and let ATGI 2= (ATG2, I, Ab)be an attributed type graph with inheritance. For each node vin VTG2,clan(v) = {v0∈VTG2|(v0, v)∈I∗}, with I∗the reflexive and transitive closure of I. Then, given an algebra A, a clan morphism f:ATG1→ATGI 2is an attributed graph morphism (fV, fE, fA, fD): ATG1→ATG2such that 1. ∀e∈ETG1, fV(sE TG1(e)) ∈clan(sE TG2(fE(e))) and fV(tE TG1(e)) ∈clan(tE TG2(fE(e))), and 2. ∀a∈ATG1, fA(sA TG1(a)) ∈clan(sA TG2(fA(a))) and fA(tA TG1(a)) = tA TG2(fA(a)). Definition 6. Given ATGI i= (ATGi, Ii, Abi), for i= 1,2, attributed type graphs with inheritance, and an algebra A, a morphism f:ATGI 1→ATGI 2is a clan morphism f= (fV, fE, fA, fD) : ATG1→ATGI 2that 1. preserves the inheritance relation, i.e., if (a, b)∈I1then (fV(a), fV(b)) ∈I∗ 2, 2. reflects subtyping, that is, for each (a, b)∈I∗ 2with some a0∈V1such that fV(a0) = a, there must be a b0∈V1such that fV(b0) = band (a0, b0)∈I∗ 1, where V1is the node set of ATG1, and 3. preserves the abstraction definitions, that is, u∈Ab1⇔fD(u)∈Ab2. Example 1. The mapping in Section 2 between TGServer and TGPLS does not satisfy the conditions to be part of a clan morphism. Specifically, the mapping for the in association fails condition 1 in Definition 5: fV(tE Server (in)) = Container 6∈ clan(tE PLS (fE(in))) = {Tray}. 4 GTS Transformers and Families Intuitively, a GTS family is a set of GTSs inductively defined from a source GTS GTS0, capturing exactly the kind of flexibility we would like to permit when mapping GTS0to another GTS GTS1. Given a set of transformers T, that model the different alterations that may be applied on GTSs, we denote by [GTS0]Tthe family of GTS0using T. Mappings are then formally defined by selecting one GTS from the GTS family of GTS0, written [GTS0]T GTS0 0, and establishing a morphism between GTS0 0and GTS1. We first introduce the notion of GTS transformers, before using them to formally define GTS families. We then show how extension preserving transformers can be used to enable the flexible composition of GTSs and how individual members of a GTS family can be identified based on a given target GTS for a mapping. 4.1 GTS Transformers GTS transformers, and the GTS families we generate with them, generalise the idea of adapters over transformations (also called adaptations in [13,23,24]). We start by defining GTS transformers as transformations between GTSs.8 Definition 7 (GTS transformer). A GTS transformer tis a triple of three inter-related transformations t= (tTG , tP, tπ): tTG takes GTSs to type graphs; tPtakes GTSs to sets of rule names; tπtakes GTSs to functions mapping rule names to rules. GTS transformers define functions over the set of all ATGI-typed GTSs. Given a GTS GTS0= (TG0, P0, π0),t(GTS0) = (TG1, P1, π1)such that: T G1= tTG (GTS0),P1=tP(GTS0),π1=tπ(GTS0), and for all p∈P1,π1(p)is a rule typed over T G1. 8In effect, GTS transformers are a form of higher-order transformation [25]. References 1. Ehrig, H.: Introduction to the algebraic theory of graph grammars. In Claus, V., Ehrig, H., Rozenberg, G., eds.: 1st Graph Grammar Workshop. Volume 73 of Lecture Notes in Computer Science., Springer (1979) 1–69 2. Engels, G., Heckel, R., Taentzer, G., Ehrig, H.: A combined reference modeland view-based approach to system specification. International Journal of Software Engineering and Knowledge Engineering 7(4) (1997) 457–477 3. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series. Springer (2006) 4. Große-Rhode, M., Parisi-Presicce, F., Simeoni, M.: Spatial and temporal refinement of typed graph transformation systems. [30] 553–561 5. Engels, G., Heckel, R., Cherchago, A.: Flexible interconnection of graph transformation modules. In Kreowski, H., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G., eds.: Formal Methods in Software and Systems Modeling. Volume 3393 of Lecture Notes in Computer Science., Springer (2005) 38–63 6. de Lara, J., Guerra, E.: From types to type requirements: Genericity for modeldriven engineering. SoSyM 12(3) (2013) 453–474 7. Dur´an, F., Zschaler, S., Troya, J.: On the reusable specification of non-functional properties in DSLs. In Czarnecki, K., Hedin, G., eds.: Proc. 5th Int’l Conf. on Software Language Engineering (SLE’12). Volume 7745 of LNCS., Springer (2013) 332–351 8. Dur´an, F., Moreno-Delgado, A., Orejas, F., Zschaler, S.: Amalgamation of domain specific languages with behaviour. Journal of Logical and Algebraic Methods in Programming (2015) 9. Baldan, P., Corradini, A., Dotti, F.L., Foss, L., Gadducci, F., Ribeiro, L.: Towards a notion of transaction in graph rewriting. Electr. Notes Theor. Comput. Sci. 211 (2008) 39–50 10. Taentzer, G.: A visual modeling framework for distributed object computing. In Jacobs, B., Rensink, A., eds.: 5th Int’l Conf. Formal Methods for Open Object-Based Distributed Systems (FMOODS’02). Volume 209 of IFIP Conference Proceedings., Kluwer (2002) 263–278 11. de Lara, J., Bardohl, R., Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Attributed graph transformation with node type inheritance. Theoretical Computer Science 376 (2007) 139–163 12. Diskin, Z., Maibaum, T., Czarnecki, K.: Intermodeling, queries, and Kleisli categories. In de Lara, J., Zisman, A., eds.: Proc. Conf. Fundamental Approaches to Software Engineering (FASE’12). Volume 7212 of Lecture Notes in Computer Science., Springer (2012) 163–177 13. de Lara, J., Guerra, E.: Towards the flexible reuse of model transformations: A formal approach based on graph transformation. Journal of Logical and Algebraic Methods in Programming 83(5–6) (2014) 427–458 14. Große-Rhode, M., Parisi-Presicce, F., Simeoni, M.: Refinements of graph transformation systems via rule expressions. Volume 1764 of Lecture Notes in Computer Science., Springer (2000) 368–382 15. Große-Rhode, M., Parisi-Presicce, F., Simeoni, M.: Spatial and temporal refinement of typed graph transformation systems. [30] 553–561 16. Harman, M.: The current state and future of search based software engineering. In Briand, L.C., Wolf, A.L., eds.: International Conference on Software Engineering, ISCE 2007, Workshop on the Future of Software Engineering, FOSE 2007, May 23-25, 2007, Minneapolis, MN, USA, IEEE Computer Society (2007) 342–357 17. Dur´an, F., Orejas, F., Zschaler, S.: Behaviour protection in modular rule-based system specifications. In Mart´ı-Oliet, N., Palomino, M., eds.: 21st Int’l Workshop Recent Trends in Algebraic Development Techniques (WADT’12), Revised Selected Papers. Volume 7841 of LNCS., Springer (2013) 18. Rozenberg, G., ed.: Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, World Scientific (1997) 19. Parisi-Presicce, F.: Transformations of graph grammars. In Cuny, J., Ehrig, H., Engels, G., Rozenberg, G., eds.: GraGra 1994. Volume 1073 of Lecture Notes in Computer Science., Springer (1996) 428–442 20. Orejas, F., Lambers, L.: Symbolic attributed graphs for attributed graph transformation. ECEASST 30 (2010) 21. Orejas, F.: Symbolic graphs for attributed graph constraints. Journal of Symbolic Computation 46(3) (2011) 294–315 22. Taentzer, G., Rensink, A.: Ensuring structural constraints in graph-based models with type inheritance. In Cerioli, M., ed.: Proc. Fundamental Approaches to Software Engineering (FASE’05). Volume 3442 of Lecture Notes in Computer Science., Springer (2005) 64–79 23. Cuadrado, J.S., Guerra, E., de Lara, J.: Flexible model-to-model transformation templates: An application to ATL. Journal of Object Technology 11(2) (2012) 4:1–28 24. Guy, C., Combemale, B., Derrien, S., Steel, J.R., J´ez´equel, J.M.: On model subtyping. In Vallecillo, A., Tolvanen, J.P., Kindler, E., St¨orrle, H., Kolovos, D., eds.: Proc. 8th European Conf. on Modelling Foundations and Applications (ECMFA’12). Volume 7349 of LNCS., Springer (2012) 400–415 25. Tisi, M., Jouault, F., Fraternali, P., Ceri, S., B´ezivin, J.: On the use of higher-order model transformations. In Paige, R.F., Hartman, A., Rensink, A., eds.: Proc. 5th European Conf. on Model Driven Architecture – Foundations and Applications (ECMDA-FA’09). Volume 5562 of Lecture Notes in Computer Science., Springer (2009) 18–33 26. Heged¨us, ´ A., Horv´ath, ´ A., R´ath, I., Varr´o, D.: A model-driven framework for guided design space exploration. In: Proc 26th IEEE/ACM Int’l Conf. Automated Software Engineering (ASE’11). (November 2011) 173–182 27. Zschaler, S., Mandow, L.: Towards model-based optimisation: Using domain knowledge explicitly. In: Proc. Workshop on Model-Driven Engineering, Logic and Optimization (MELO’16). (2016) 28. Fleck, M., Troya, J., Wimmer, M.: Marrying search-based optimization and model transformation technology. In: Proc. 1st North American Search Based Software Engineering Symposium (NasBASE’15). (2015) Preprint available at http://martin-fleck.github.io/momot/downloads/NasBASE_MOMoT.pdf. 29. Clavel, M., Dur´an, F., Eker, S., Lincoln, P., Mart´ı-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude. Volume 4350 of LNCS. Springer (2007) 30. Brim, L., Gruska, J., Zlatuska, J., eds.: Proc. 23rd Int’l Symposium Mathematical Foundations of Computer Science (MFCS’98). Volume 1450 of Lecture Notes in Computer Science., Springer (1998)