Refine
Year of publication
Document Type
- Article (14)
- Monograph/Edited Volume (5)
- Postprint (1)
- Preprint (1)
Language
- English (21)
Is part of the Bibliography
- yes (21)
Keywords
- nested graph conditions (3)
- Graph transformation (2)
- Nested graph conditions (2)
- graph transformation (2)
- verschachtelte Graphbedingungen (2)
- Algebraic methods (1)
- Application (1)
- Attributed graph transformation (1)
- Attributed graphs (1)
- Behavioral equivalence and refinement (1)
- Bisimulation (1)
- Bisimulation and simulation (1)
- Consistency (1)
- Critical pair analysis (1)
- Critical pair analysis (CPA) (1)
- Critical pairs (1)
- Delta preservation (1)
- Description framework (1)
- Discrimination Networks (1)
- Erfüllbarkeitsanalyse (1)
- Formal modelling (1)
- Formal verification of behavior preservation (1)
- Graph databases (1)
- Graph logic (1)
- Graph logics (1)
- Graph queries (1)
- Graph repair (1)
- Graph transformation (double pushout approach) (1)
- Graph-Constraints (1)
- Graph-basierte Suche (1)
- Graphreparatur (1)
- Graphtransformation (1)
- Graphtransformationssysteme (1)
- Inheritance (1)
- Initial conflicts (1)
- Inkrementelle Graphmustersuche (1)
- Institutions (1)
- Intent (1)
- Invariant checking (1)
- Invariant-Checking (1)
- Konsistenzrestauration (1)
- M-adhesive categories (1)
- M-adhesive category with NACs (1)
- M-adhesive transformation systems (1)
- Model generation (1)
- Model repair (1)
- Model transformation (1)
- Model-driven (1)
- Modellerzeugung (1)
- Modellreparatur (1)
- Modelltransformationen (1)
- Navigational logics (1)
- Nested Graph Conditions (1)
- Parallel independence (1)
- Property (1)
- Relational model transformation (1)
- Simulation (1)
- Specification (1)
- Tableau method (1)
- Tableaumethode (1)
- Transformationsebene (1)
- Triple graph grammars (1)
- Triple-Graph-Grammatiken (1)
- Typed attributed graph transformation (1)
- Verhaltensabstraktion (1)
- Verhaltensbewahrung (1)
- Verhaltensverfeinerung (1)
- Verhaltensäquivalenz (1)
- Verification (1)
- behavior preservation (1)
- behavioral abstraction (1)
- behavioral equivalenc (1)
- behavioral refinement (1)
- bisimulation (1)
- categories (1)
- concurrent graph rewriting (1)
- conditions (1)
- conflicts and dependencies in (1)
- confluence (1)
- consistency restoration (1)
- critical pairs (1)
- discrimination networks (1)
- distributed systems (1)
- embedding (1)
- engineering (1)
- grammars (1)
- graph constraints (1)
- graph languages (1)
- graph queries (1)
- graph repair (1)
- graph replacement categories (1)
- graph transformation systems (1)
- graph-transformations (1)
- incremental graph pattern matching (1)
- invariant checking (1)
- lazy transformation (1)
- level-replacement systems (1)
- local confluence (1)
- model (1)
- model generation (1)
- model repair (1)
- model transformation (1)
- nested application conditions (1)
- programs (1)
- relational model transformation (1)
- relationale Modelltransformationen (1)
- restoration (1)
- satisfiabilitiy solving (1)
- semantics preservation (1)
- simulation (1)
- symbolic graph transformation (1)
- synchronization (1)
- tableau method (1)
- transformation level (1)
- triple graph grammars (1)
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.
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.
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.
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.
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).
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.
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.
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.
Special issue on graph transformation and visual modeling techniques - guest editors' introduction
(2013)
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.