Download Graph Transformation: 7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014, Proceedings PDF

TitleGraph Transformation: 7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014, Proceedings
Author
LanguageEnglish
File Size5.7 MB
Total Pages296
Table of Contents
                            Foreword
Preface
Organization
Table of Contents
Invited Contribution
	Parameterized Verification and Model Checking for Distributed Broadcast Protocols
		1 Introduction
		2 Parameterized Verification
			2.1 Broadcast Protocols
			2.2 Broadcast Protocols with Data
		3 Distributed Broadcast Protocols
			3.1 Synchronous Broadcast
			3.2 Restricted Topologies
			3.3 Faults and Conflicts
			3.4 Time
			3.5 Asynchronous Broadcast
			3.6 Distributed Broadcast Protocols with Data
			3.7 Other Graph-Based Models
		4 Model Checking
		References
Verification
	Tableau-Based Reasoning for Graph Properties
		1 Introduction
		2 Preliminaries
			2.1 Graph Properties Expressed in GL
			2.2 Conjunctive Normal Form and Shifting Results
		3 Tableau-Based Reasoning for GL
			3.1 Tableaux for Graph Conditions
			3.2 Nested Tableaux for Graph Properties
		4 Soundness and Completeness
		5 Conclusion
		References
	Verifying Monadic Second-Order Propertiesof Graph Programs
		1 Introduction
		2 Preliminaries
		3 Expressing Monadic Second-Order Properties
		4 Graph Programs
		5 Constructing a Weakest Liberal Precondition
		6 Proving Non-local Specifications
		7 Related Work
		8 Conclusion
		References
	Generating Abstract Graph-Based Procedure Summaries for Pointer Programs
		1 Introduction
		2 Pointer-Manipulating Programs
		3 Heap Abstraction by Hyperedge Replacement
		4 Deriving Procedure Contracts by Interprocedural Analysis
			4.1 IPA Preliminaries
			4.2 Local Transformers
			4.3 Global Transformer
			4.4 Equation System
		5 Conclusions
		References
	Generating Inductive Predicates for Symbolic
Execution of Pointer-Manipulating Programs
		1 Introduction
		2 Preliminaries
			2.1 Hyperedge Replacement Grammars
			2.2 Separation Logic
			2.3 Translating HRGs to Environments and Back
		3 Generating Predicates for Abstraction and Concretisation
			3.1 Abstraction and Concretisation Using Graph Grammars
			3.2 Abstraction and Unrolling in Separation Logic
			3.3 Structural Properties
		4 Property Preservation under Translation
		5 Conclusion
		References
	Attribute Handling for Generating Preconditions from Graph Constraints
		1 Introduction
		2 BasicConcepts
			2.1 Formal Concepts
			2.2 Modeling and Transformation Concepts
		3 Constructing Precondition NACs with Attributes
			3.1 Construction of Postcondition NACs from Negative Constraints
			3.2 Constructing Precondition NAC from Postcondition NAC
			3.3 Proving the Correctness of the Construction Technique
		4 Attributes in Search Plan Driven Pattern Matching
			4.1 Pattern Specification
			4.2 Creating Operations
			4.3 Search Plan and Code Generation
		5 Related Work
		6 Conclusion
		References
Meta-Modelling and Model Transformations
	From Core OCL Invariants
to Nested Graph Constraints
		1 Introduction
		2 CoreOCLInvariants
		3 Nested Graph Conditions
		4 Translation of Meta-Models with Core OCL Invariants
			4.1 Type and State Correspondences
			4.2 Translation of Core OCL Invariants
			4.3 Correctness and Completeness
		5 From Core OCL Invariants to Application Conditions
		6 Related Work and Conclusion
		References
	Specification and Verification of Graph-Based Model Transformation Properties
		1 Introduction
		2 The DSLTrans Model Transformation Language
		3 The Symbolic Model Transformation Property Prover
		4 Generating the Set of Path Conditions
		5 Verification of the Property of Interest
		6 Industrial Case Study
			6.1 GM-2-AUTOSAR Model Transformation
			6.2 GM-2-AUTOSAR Model Transformation Properties
			6.3 Verifying Properties of the GM-2-AUTOSAR Transformation
		7 Discussion
		8 Related Work
		9 Conclusion and Future Work
		References
	A Static Analysis of Non-confluent Triple Graph Grammars for Efficient Model Transformation
		1 Introduction and Motivation
		2 Running Example and Preliminaries
			2.1 Consistency Specification with Triple Graph Grammars
			2.2 Operationalization of Triple Graph Grammars
		3 Efficient Model Transformation with TGGs
		4 Related Work
		5 Conclusion
		References
Rewriting and Applications in Biology
	Transformation and Refinement of Rigid Structures
		1 Introduction
		2 Structures, Patterns, and States
		3 Rigidity
		4 Matches as Open Maps
		5 Growth Policies and Refinements
		6 Related Work
		7 Conclusion
		References
	Reversible Sesqui-Pushout Rewriting
		1 Preliminaries
			1.1 Final Pullback Complements and Stable Pushouts
			1.2 Splitting and Composing Pushout and FPBC Squares
			1.3 Finitely Powered Objects
		2 Reversible Sesqui-Pushout Rewriting
			2.1 Definition and First Examples
			2.2 Independence and Commutativity
		3 On Nested Application Conditions
		4 On Reversibility of Sesqui-Pushout Rewriting
		5 Related and Future Work
		6 Conclusion
		References
	On Pushouts of Partial Maps
		1 Preliminaries
			1.1 Pattern Graphs
			1.2 Categories of PartialMaps
		2 Pushouts of Partial Maps: The State of theArt
			2.1 A Necessary Condition for Pushouts of Partial Maps
			2.2 A Locally Necessary Condition
			2.3 Challenge for a Sufficient Condition
		3 Partial Map Pushouts by Inheritance
		4 On Pushouts in Full Subcategories
		5 Related and FutureWork
		6 Conclusion
		References
Graph Languages and Graph Transformation
	The Subgraph Isomorphism Problem on a Class of Hyperedge Replacement Languages
		1 Introduction
			1.1 Notation
			1.2 Background
			1.3 Goal
		2 Head-Mid-Tail Grammars
			2.1 Definition
			2.2 Normalised Head-Mid-Tail Grammars
			2.3 Properties of Normalised Grammars
			2.4 The Algorithm
		3 Discussion
		References
	Canonical Derivations with Negative Application Conditions
		1 Introduction
		2 Basic Definitions
		3 Independence and Switch Equivalence
		4 Conditional Step Derivations
		5 Canonical Derivations with Incremental NACs
		6 Conclusion
		References
	Van Kampen Squares for Graph Transformation
		1 Introduction
		2 Coupled Transformations
		3 Characterizing the Van Kampen Property
			Definition 1 (Separated Kernels).
			Theorem 1.
			–
			–
			–
			–
		4 An Application of the Van Kampen Characterization
			4.1 Co-transformations
			Corollary 1.
			4.2 A Well-Defined Co-transformation with Non-monic Match
		5 Related Work
		6 Outlook
		References
Applications
	Graph Transformation Meets Reversible Circuits: Generation, Evaluation, and Synthesis
		1 Introduction
		2 Graph-Transformational Preliminaries
		3 Reversible Circuits
		4 Lines Graphs
		5 Graph Representation of Toffoli Circuits
		6 Evaluation
		7 From Reversible Functions to Toffoli Graphs
		8 From Binary Decision Diagrams to Toffoli Circuits
		9 Conclusion
		References
	Towards Process Miningwith Graph Transformation Systems
		1 Introduction
		2 Preliminaries
		3 Process Mining with Graph Transformation Systems
			3.1 From Traces to Graph Transformation Systems
			3.2 Analyzing Models
		4 Algorithms for Process Mining
			4.1 The Maximal Rule Algorithm
			4.2 The Minimal Rule Algorithm
			4.3 The Context Algorithm
			4.4 The Genetic Algorithm
			4.5 The Greedy Mutation Algorithm
			4.6 Experimental Results
		5 Conclusion and Further Research
		References
	Jerboa: A Graph Transformation Libraryfor Topology-Based Geometric Modeling
		1 Introduction
		2 Object Data Structure: Embedded Generalized Maps
			2.1 Generalized Maps
			2.2 Embedding
			2.3 Creation of a New Modeler
		3 Operations on G-Maps Defined as DPO Rule Schemes
			3.1 Formal Framework
			3.2 Editing Topological Rule Schemes
			3.3 Editing Geometrical Rule Schemes
			3.4 Syntax Checking
			3.5 Jerboa Rule Application
		4 Discussion
		5 Conclusion and Future Works
		References
Author Index
                        
Document Text Contents
Page 1

Holger Giese
Barbara König (Eds.)

123

LN
CS

8
57

1

7th International Conference, ICGT 2014
Held as Part of STAF 2014
York, UK, July 22–24, 2014, Proceedings

Graph
Transformation

Page 2

Lecture Notes in Computer Science 8571
Commenced Publication in 1973
Founding and Former Series Editors:
Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen

Editorial Board

David Hutchison
Lancaster University, UK

Takeo Kanade
Carnegie Mellon University, Pittsburgh, PA, USA

Josef Kittler
University of Surrey, Guildford, UK

Jon M. Kleinberg
Cornell University, Ithaca, NY, USA

Alfred Kobsa
University of California, Irvine, CA, USA

Friedemann Mattern
ETH Zurich, Switzerland

John C. Mitchell
Stanford University, CA, USA

Moni Naor
Weizmann Institute of Science, Rehovot, Israel

Oscar Nierstrasz
University of Bern, Switzerland

C. Pandu Rangan
Indian Institute of Technology, Madras, India

Bernhard Steffen
TU Dortmund University, Germany

Demetri Terzopoulos
University of California, Los Angeles, CA, USA

Doug Tygar
University of California, Berkeley, CA, USA

Gerhard Weikum
Max Planck Institute for Informatics, Saarbruecken, Germany

Page 148

A Static Analysis of Non-confluent Triple Graph Grammars 137

:Op :Com:O2C
++ ++ ++

ComRule

:Rapid

:Op :Com

:G0

:O2C

:M2S
++ ++ ++ ++++

G0Rule

:Op :Com:O2C

:Feed
++

:M2S
++

:G1
++

:Op

:Rapid

++++

G0G1Rule

:Com

:G0:M2S

:O2C
:Rapid

:Op :Com

:G0

:O2C

:M2S
++ ++ ++++

:Com

G0G0Rule

:Feed

:Op :Com

:G1

:O2C

:M2S
++ ++ ++++

:Com

G1G1Rule

:Op

:Op :Com

:Com

:O2C

:O2C

++ ++ ++ ++++

ComComRule

Fig. 3. Triple rules for running example

Example 2. The six TGG rules for the running example are depicted in Fig. 3.
Every triple rule r : L → R is depicted in a compact syntax by denoting created
elements, i.e., R\L, with a ++ markup (and by displaying them in green). Com-
Rule creates an Op and a Com connected by an O2C correspondence, depicted
as a hexagon to improve readability. ComComRule also creates a corresponding
pair of Op and Com elements, requiring a preceding triple as context to which
the new elements are connected. The remaining rules handle the creation of cor-
responding Modi and Switches. The rules show that we have decided to allow
possibly redundant repetitions of G0 switches with G0Rule, as well as reusing
the G0 switch from the previous Com with G0G0Rule. This degree of freedom is,
therefore, not restricted by the TGG and can be decided upon at runtime. For
G1 switches, however, we have chosen to forbid redundant repetitions already at
design time, i.e., a new G1 switch can only be created with G0G1Rule if it is im-
possible to reuse the G1 switch of the previous Com with G1G1Rule. The running
example (Fig. 2) is consistent as it can be created by the following derivation:
ComRule → G0Rule → ComComRule → G0G1Rule → ComComRule → G1G1Rule.

2.2 Operationalization of Triple Graph Grammars

Although TGG rules can be used directly to generate consistent source and
target models, e.g., for testing purposes, TGGs are often operationalized to de-
rive unidirectional forward and backward transformations [13,9]. To this end, a
forward rule is derived from each TGG rule according to the following definition.

Definition 8 (Derivation of Forward Rules).
A TGG = (TG,R) without conditional application conditions can be forward
operationalized by deriving FWD(TGG) := (TG, RF ), where RF consists of
forward rules. A forward rule (rF : FL → FR,NF ) for triple rule r ∈ R is
defined by the diagram below (the triangle denotes a set of NACs):

LS

RS

LC

RC

LT

RT

σL

rS

τL

rT

σR τR

rS ◦ σLLC

RC

LT

RT

τL

rT

σR τR

RS

RS

rC rC

L

R

FL

FR

r

=

= =

=

NF

idrF

Page 149

138 A. Anjorin et al.

NF consists of correspondence NACs (id, nC , id) : FL → (RS
σFN← NC

τFN→ NT )
for every node vC ∈ VRC \ VLC (cf. Def. 7). NC and NT are extensions of LC
and LT by vC and τRC (vC), respectively.

Remark 3 (Avoiding Conflicts in Forward Rules).
For presentation purposes, we assume that TGG rules are always constructed
so that every created source and target element is connected to at least one new
correspondence element. With this assumption, forward rules with correspon-
dence NACs derived according to Def. 8 “translate” every source element ex-
actly once and simplify the formalization as compared to introducing translation
attributes [8], or bookkeeping [9]. To avoid unnecessary create/forbid conflicts,
NF can be further extended by application conditions to avoid obvious dead-ends
when applying forward rules. We only give an intuition of how this works with
our running example and refer to [9,8] for a description of filter NACs.

Example 3. Figure 4 depicts the forward rules derived from the triple rules in
Fig. 3, where labels indicate the original triple rules (e.g., ComFwdRule derived
from ComRule). Forward rules “translate” the source elements that are created
in the respective triple rules by attaching correspondence elements to them, but
only if the correspondence elements do not already exist, i.e., the elements have
not already been translated. Similarly, context elements of source models in triple
rules are required to be already translated in forward rules by demanding an
attached correspondence element. ComFwdRule, for example, “translates” an Op
by connecting it to a new O2C and a Com in the target model. This should only
be possible if the Op has not been translated already (hence the correspondence
NAC denoted here as a crossed out (forbidden) element). An additional source
NAC in ComFwdRule forbids the existence of a previous Op, i.e., this forward
rule can translate only the first Op in a sequence of connected Ops. If this is not
prevented, the incoming edge from a previous Op would no longer be translatable
as the original triple rules cannot create such an edge between two existing Ops.
This is automatically detected and prevented by generating a source “filter”
NAC (cf. Remark 3).

:Op :Com:O2C
++ ++

ComFwdRule

:Op :O2C

:Op

:Op :Com

:Com

:O2C

:O2C
++ ++ ++

ComComFwdRule

:O2C

:Rapid

:Op
:Com

:G0

:O2C

:M2S
++ ++

:Com

G0G0FwdRule

:M2S

:Rapid

:Op :Com

:G0

:O2C

:M2S
++ ++ ++

G0FwdRule

:M2S

:Feed

:Op
:Com

:G1

:O2C

:M2S
++ ++

:Com

G1G1FwdRule

:M2S

:Op :Com:O2C

:Feed :M2S
++

:G1
++

:Op

:Rapid

++

G0G1FwdRule

:Com

:G0:M2S

:O2C

:M2S

Fig. 4. Derived forward rules for the running example

Page 295

284 H. Belhaouari et al.

expressions or the need of a rule script language in order to apply several rule
schemes accordingly to some strategies.

References

[BALG11] Bellet, T., Arnould, A., Le Gall, P.: Rule-based transformations for ge-
ometric modeling. In: 6th International Workshop on Computing with
Terms and Graphs (TERMGRAPH), Saarbrucken, Germany (2011)

[BH02] Baresi, L., Heckel, R.: Tutorial introduction to graph transformation: A soft-
ware engineering perspective. In: Corradini, A., Ehrig, H., Kreowski, H.-J.,
Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 402–429. Springer,
Heidelberg (2002)

[BPA+10] Bellet, T., Poudret, M., Arnould, A., Fuchs, L., Le Gall, P.: Designing a
topological modeler kernel: A rule-based approach. In: Shape Modeling
International (SMI 2010). IEEE Computer Society (2010)

[EEPT06] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic
Graph Transformation. Monographs in Theoretical Computer Science. An
EATCS Series. Springer (2006)

[Hof05] Hoffmann, B.: Graph transformation with variables. Formal Methods in
Software and System Modeling 3393, 101–115 (2005)

[HP02] Habel, A., Plump, D.: Relabelling in graph transformation. In: Corradini,
A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS,
vol. 2505, pp. 135–147. Springer, Heidelberg (2002)

[KBHK07] Kniemeyer, O., Barczik, G., Hemmerling, R., Kurth, W.: Relational growth
grammars - a parallel graph transformation approach with applications
in biology and architecture. In: Schürr, A., Nagl, M., Zündorf, A. (eds.)
AGTIVE 2007. LNCS, vol. 5088, pp. 152–167. Springer, Heidelberg (2008)

[KUJ+14] Kraemer, P., Untereiner, L., Jund, T., Thery, S., Cazier, D.: CGoGN:
n-dimensional meshes with combinatorial maps. In: 22nd International
Meshing Roundtable. Springer (2014)

[Lie91] Lienhardt, P.: Topological models for boundary representation: A compar-
ison with n-dimensional generalized maps. Computer-Aided Design 23(1)
(1991)

[Mod] Moka Modeler. XLim-SIC, http://moka-modeller.sourceforge.net/
[MP96] Měch, R., Prusinkiewicz, P.: Visual models of plants interacting with their

environment. In: 23rd Conference on Computer Graphics and Interactive
Techniques, SIGGRAPH. ACM (1996)

[PACLG08] Poudret, M., Arnould, A., Comet, J.-P., Le Gall, P.: Graph transformation
for topology modelling. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer,
G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 147–161. Springer, Heidelberg
(2008)

[PLH90] Prusinkiewicz, P., Lindenmayer, A., Hanan, J.: The algorithmic beauty of
plants. Virtual laboratory. Springer (1990)

[TGM+09] Terraz, O., Guimberteau, G., Merillou, S., Plemenos, D., Ghazanfarpour,
D.: 3Gmap L-systems: An application to the modelling of wood. The Visual
Computer 25(2) (2009)

[VAB10] Vanegas, C.-A., Aliaga, D.-G., Benes, B.: Building reconstruction using
manhattan-world grammars. In: Computer Vision and Pattern Recogni-
tion (CVPR). IEEE (2010)

Page 296

Author Index

Anjorin, Anthony 130
Arendt, Thorsten 97
Arnould, Agnès 269

Belhaouari, Hakim 269
Bellet, Thomas 269
Bruggink, H.J. Sander 253

Cordy, James R. 113
Corradini, Andrea 207

Danos, Vincent 146, 161
Deckwerth, Frederik 81
Delzanno, Giorgio 1
de Ridder, H.N. 192
de Ridder, N. 192
Dingel, Juergen 113

Göbe, Florian 65

Habel, Annegret 97
Hayman, Jonathan 177
Heckel, Reiko 146, 207
Heindel, Tobias 161, 177
Honorato-Zimmer, Ricardo 161

Jansen, Christina 49, 65

König, Harald 222
Kreowski, Hans-Jörg 237
Kuske, Sabine 237

Lambers, Leen 17
Leblebici, Erhan 130
Le Gall, Pascale 269
Löwe, Michael 222
Lúcio, Levi 113
Luderer, Melanie 237
Lye, Aaron 237

Noll, Thomas 49, 65

Oakes, Bentley J. 113
Orejas, Fernando 17

Plump, Detlef 33
Poskitt, Christopher M. 33

Radke, Hendrik 97

Schulz, Christoph 222
Schürr, Andy 130
Selim, Gehan M.K. 113
Sobocinski, Pawel 146
Stucki, Sandro 161

Taentzer, Gabriele 97, 130

Varró, Gergely 81

Wolter, Uwe 222

Similer Documents