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  - 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  - 
TY  - JOUR
A1  - Giese, Holger
A1  - Hildebrandt, Stephan
A1  - Lambers, Leen
T1  - Bridging the gap between formal semantics and implementation of triple graph grammars
JF  - Software and systems modeling
N2  - The correctness of model transformations is a crucial element for 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 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 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. While 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 and runtime checks can be employed to guarantee these criteria.
Y1  - 2014
U6  - https://doi.org/10.1007/s10270-012-0247-y
SN  - 1619-1366
SN  - 1619-1374
VL  - 13
IS  - 1
SP  - 273
EP  - 299
PB  - Springer
CY  - Heidelberg
ER  - 
TY  - JOUR
A1  - Ehrig, Hartmut
A1  - Golas, Ulrike
A1  - Habel, Annegret
A1  - Lambers, Leen
A1  - Orejas, Fernando
T1  - M-Adhesive Transformation Systems with Nested Application Conditions  Part 2: Embedding, Critical Pairs and Local Confluence
JF  - Fundamenta informaticae
N2  - Graph transformation systems have been studied extensively and applied to several areas of computer science like formal language theory, the modeling of databases, concurrent or distributed systems, and visual, logical, and functional programming. In most kinds of applications it is necessary to have the possibility of restricting the applicability of rules. This is usually done by means of application conditions. In this paper, we continue the work of extending the fundamental theory of graph transformation to the case where rules may use arbitrary (nested) application conditions. More precisely, we generalize the Embedding theorem, and we study how local confluence can be checked in this context. In particular, we define a new notion of critical pair which allows us to formulate and prove a Local Confluence Theorem for the general case of rules with nested application conditions. All our results are presented, not for a specific class of graphs, but for any arbitrary M-adhesive category, which means that our results apply to most kinds of graphical structures. We demonstrate our theory on the modeling of an elevator control by a typed graph transformation system with positive and negative application conditions.
KW  - M-adhesive transformation systems
KW  - M-adhesive categories
KW  - graph replacement categories
KW  - nested application conditions
KW  - embedding
KW  - critical pairs
KW  - local confluence
Y1  - 2012
U6  - https://doi.org/10.3233/FI-2012-705
SN  - 0169-2968
VL  - 118
IS  - 1-2
SP  - 35
EP  - 63
PB  - IOS Press
CY  - Amsterdam
ER  - 
TY  - JOUR
A1  - Orejas, Fernando
A1  - Lambers, Leen
T1  - Lazy graph transformation
JF  - Fundamenta informaticae
N2  - Applying an attributed graph transformation rule to a given object graph always implies some kind of constraint solving. In many cases, the given constraints are almost trivial to solve. For instance, this is the case when a rule describes a transformation G double right arrow H, where the attributes of H are obtained by some simple computation from the attributes of G. However there are many other cases where the constraints to solve may be not so trivial and, moreover, may have several answers. This is the case, for instance, when the transformation process includes some kind of searching. In the current approaches to attributed graph transformation these constraints must be completely solved when defining the matching of the given transformation rule. This kind of early binding is well-known from other areas of Computer Science to be inadequate. For instance, the solution chosen for the constraints associated to a given transformation step may be not fully adequate, meaning that later, in the search for a better solution, we may need to backtrack this transformation step.
 In this paper, based on our previous work on the use of symbolic graphs to deal with different aspects related with attributed graphs, including attributed graph transformation, we present a new approach that, based on the new notion of narrowing graph transformation rule, allows us to delay constraint solving when doing attributed graph transformation, in a way that resembles lazy computation. For this reason, we have called lazy this new kind of transformation. Moreover, we show that the approach is sound and complete with respect to standard attributed graph transformation. A running example, where a graph transformation system describes some basic operations of a travel agency, shows the practical interest of the approach.
KW  - Attributed graph transformation
KW  - symbolic graph transformation
KW  - lazy transformation
Y1  - 2012
U6  - https://doi.org/10.3233/FI-2012-706
SN  - 0169-2968
VL  - 118
IS  - 1-2
SP  - 65
EP  - 96
PB  - IOS Press
CY  - Amsterdam
ER  -