TY - JOUR A1 - Dyck, Johannes A1 - Giese, Holger A1 - Lambers, Leen T1 - Automatic verification of behavior preservation at the transformation level for relational model transformation JF - Software and systems modeling N2 - The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp.simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata. KW - Relational model transformation KW - Formal verification of behavior preservation KW - Behavioral equivalence and refinement KW - Bisimulation and simulation KW - Graph transformation KW - Triple graph grammars KW - Invariant checking Y1 - 2018 U6 - https://doi.org/10.1007/s10270-018-00706-9 SN - 1619-1366 SN - 1619-1374 VL - 18 IS - 5 SP - 2937 EP - 2972 PB - Springer CY - Heidelberg ER - TY - JOUR A1 - Orejas, Fernando A1 - Pino, Elvira A1 - Navarro, Marisa A1 - Lambers, Leen T1 - Institutions for navigational logics for graphical structures JF - Theoretical computer science N2 - We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex. KW - Institutions KW - Graph logics KW - Navigational logics Y1 - 2018 U6 - https://doi.org/10.1016/j.tcs.2018.02.031 SN - 0304-3975 SN - 1879-2294 VL - 741 SP - 19 EP - 24 PB - Elsevier CY - Amsterdam ER - TY - JOUR A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - Automated reasoning for attributed graph properties JF - International Journal on Software Tools for Technology Transfer N2 - Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation. KW - Attributed graphs KW - Nested graph conditions KW - Model generation KW - Tableau method KW - Graph queries Y1 - 2018 U6 - https://doi.org/10.1007/s10009-018-0496-3 SN - 1433-2779 SN - 1433-2787 VL - 20 IS - 6 SP - 705 EP - 737 PB - Springer CY - Heidelberg ER - TY - JOUR A1 - Lambers, Leen A1 - Born, Kristopher A1 - Kosiol, Jens A1 - Strüber, Daniel A1 - Taentzer, Gabriele T1 - Granularity of conflicts and dependencies in graph transformation systems BT - a two-dimensional approach JF - Journal of Logical and Algebraic Methods in Programming N2 - Conflict and dependency analysis (CDA) is a static analysis for the detection of conflicting and dependent rule applications in a graph transformation system. The state-of-the-art CDA technique, critical pair analysis, provides all potential conflicts and dependencies in minimal context as critical pairs, for each pair of rules. Yet, critical pairs can be hard to understand; users are mainly interested in core information about conflicts and dependencies occurring in various combinations. In this paper, we present an approach to conflicts and dependencies in graph transformation systems based on two dimensions of granularity. The first dimension refers to the overlap considered between the rules of a given rule pair; the second one refers to the represented amount of context information about transformations in which the conflicts occur. We introduce a variety of new conflict notions, in particular, conflict atoms, conflict reasons, and minimal conflict reasons, relate them to the existing conflict notions of critical pairs and initial conflicts, and position all of these notions within our granularity approach. Finally, we introduce dual concepts for dependency analysis. As we discuss in a running example, our approach paves the way for an improved CDA technique. (C) 2018 Elsevier Inc. All rights reserved. KW - Graph transformation (double pushout approach) KW - Parallel independence KW - Critical pair analysis (CPA) Y1 - 2018 U6 - https://doi.org/10.1016/j.jlamp.2018.11.004 SN - 2352-2208 VL - 103 SP - 105 EP - 129 PB - Elsevier CY - New York ER - TY - JOUR A1 - Lambers, Leen A1 - Weber, Jens T1 - Preface to the special issue on the 11th International Conference on Graph Transformation JF - Journal of Logical and Algebraic Methods in Programming N2 - This special issue contains extended versions of four selected papers from the 11th International Conference on Graph Transformation (ICGT 2018). The articles cover a tool for computing core graphs via SAT/SMT solvers (graph language definition), graph transformation through graph surfing in reaction systems (a new graph transformation formalism), the essence and initiality of conflicts in M-adhesive transformation systems, and a calculus of concurrent graph-rewriting processes (theory on conflicts and parallel independence). KW - graph transformation KW - graph languages KW - conflicts and dependencies in KW - concurrent graph rewriting Y1 - 2020 U6 - https://doi.org/10.1016/j.jlamp.2020.100525 SN - 2352-2208 VL - 112 PB - Elsevier CY - Amsterdam ER - TY - BOOK A1 - Giese, Holger A1 - Hildebrandt, Stephan A1 - Lambers, Leen T1 - Toward bridging the gap between formal semantics and implementation of triple graph grammars N2 - The correctness of model transformations is a crucial element for the model-driven engineering of high quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the employed implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches it is usually not really clear under which constraints particular implementations are really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. Whereas the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static analysis can be employed to guarantee these criteria. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 37 Y1 - 2010 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-45219 SN - 978-3-86956-078-6 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Lambers, Leen A1 - Orejas, Fernando T1 - Transformation rules with nested application conditions BT - critical pairs, initial conflicts & minimality JF - Theoretical computer science N2 - Recently, initial conflicts were introduced in the framework of M-adhesive categories as an important optimization of critical pairs. In particular, they represent a proper subset such that each conflict is represented in a minimal context by a unique initial one. The theory of critical pairs has been extended in the framework of M-adhesive categories to rules with nested application conditions (ACs), restricting the applicability of a rule and generalizing the well-known negative application conditions. A notion of initial conflicts for rules with ACs does not exist yet. In this paper, on the one hand, we extend the theory of initial conflicts in the framework of M-adhesive categories to transformation rules with ACs. They represent a proper subset again of critical pairs for rules with ACs, and represent each conflict in a minimal context uniquely. They are moreover symbolic because we can show that in general no finite and complete set of conflicts for rules with ACs exists. On the other hand, we show that critical pairs are minimally M-complete, whereas initial conflicts are minimally complete. Finally, we introduce important special cases of rules with ACs for which we can obtain finite, minimally (M-)complete sets of conflicts. KW - Graph transformation KW - Critical pairs KW - Initial conflicts KW - Application KW - conditions Y1 - 2021 U6 - https://doi.org/10.1016/j.tcs.2021.07.023 SN - 0304-3975 SN - 1879-2294 VL - 884 SP - 44 EP - 67 PB - Elsevier CY - Amsterdam ER - TY - JOUR A1 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - A logic-based incremental approach to graph repair featuring delta preservation JF - International journal on software tools for technology transfer : STTT N2 - We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain. KW - Nested graph conditions KW - Graph repair KW - Model repair KW - Consistency KW - restoration KW - Delta preservation KW - Graph databases KW - Model-driven KW - engineering Y1 - 2021 U6 - https://doi.org/10.1007/s10009-020-00584-x SN - 1433-2779 SN - 1433-2787 VL - 23 IS - 3 SP - 369 EP - 410 PB - Springer CY - Berlin ; Heidelberg ER - TY - INPR A1 - Fish, Andrew A1 - Lambers, Leen T1 - Special issue on graph transformation and visual modeling techniques - guest editors' introduction T2 - Journal of visual languages and computing Y1 - 2013 U6 - https://doi.org/10.1016/j.jvlc.2013.08.004 SN - 1045-926X SN - 1095-8533 VL - 24 IS - 6 SP - 419 EP - 420 PB - Elsevier CY - London ER - TY - JOUR A1 - Golas, Ulrike A1 - Lambers, Leen A1 - Ehrig, Hartmut A1 - Orejas, Fernando T1 - Attributed graph transformation with inheritance: Efficient conflict detection and local confluence analysis using abstract critical pairs JF - THEORETICAL COMPUTER SCIENCE N2 - Inheritance is an important and widely spread concept enabling the elegant expression of hierarchy in object-oriented software programs or models. It has been defined for graphs and graph transformations enhancing the applicability of this formal technique. Up to now, for the analysis of transformations with inheritance a flattening construction has been used, which yields all the well-known results for graph transformation but results in a large number of graphs and rules that have to be analyzed. In this paper, we introduce a new category of typed attributed graphs with inheritance. For the detection of conflicts between graph transformations on these graphs, the notion of abstract critical pairs is defined. This allows us to perform the analysis on polymorphic rules and transformations without the need for flattening, which significantly increases the efficiency of the analysis and eases the interpretation of the analysis results. The new main result is the Local Confluence Theorem for typed attributed graph transformation with inheritance using abstract critical pairs. All constructions and results are demonstrated on an example for the analysis of refactorings. (C) 2012 Elsevier B.V. All rights reserved. KW - Typed attributed graph transformation KW - Critical pair analysis KW - Inheritance KW - M-adhesive category with NACs Y1 - 2012 U6 - https://doi.org/10.1016/j.tcs.2012.01.032 SN - 0304-3975 VL - 424 SP - 46 EP - 68 PB - ELSEVIER SCIENCE BV CY - AMSTERDAM ER -