Graph transformation : 7th International Conference, ICGT 2014, held as part of STAF 2014, York, UK, July 22-24, 2014 : Proceedings

This book constitutes the proceedings of the 7th International Conference on Graph Transformations, ICGT 2014, held in York, UK, in July 2014. The 17 papers and 1 invited paper presented were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on verification, meta-modelling and model transformations, rewriting and applications in biology, graph languages and graph transformation, and applications. Graph Transformation Foreword 5 Preface 6 Organization 8 Table of Contents 10 Invited Contribution 10 Parameterized Verification and Model Checking for Distributed Broadcast Protocols 12 1 Introduction 12 2 Parameterized Verification 13 2.1 Broadcast Protocols 13 2.2 Broadcast Protocols with Data 14 3 Distributed Broadcast Protocols 14 3.1 Synchronous Broadcast 16 3.2 Restricted Topologies 16 3.3 Faults and Conflicts 18 3.4 Time 19 3.5 Asynchronous Broadcast 19 3.6 Distributed Broadcast Protocols with Data 21 3.7 Other Graph-Based Models 21 4 Model Checking 22 References 25 Verification 10 Tableau-Based Reasoning for Graph Properties 28 1 Introduction 28 2 Preliminaries 30 2.1 Graph Properties Expressed in GL 30 2.2 Conjunctive Normal Form and Shifting Results 32 3 Tableau-Based Reasoning for GL 33 3.1 Tableaux for Graph Conditions 33 3.2 Nested Tableaux for Graph Properties 37 4 Soundness and Completeness 39 5 Conclusion 42 References 43 Verifying Monadic Second-Order Propertiesof Graph Programs 44 1 Introduction 44 2 Preliminaries 45 3 Expressing Monadic Second-Order Properties 46 4 Graph Programs 47 5 Constructing a Weakest Liberal Precondition 49 6 Proving Non-local Specifications 55 7 Related Work 58 8 Conclusion 58 References 59 Generating Abstract Graph-Based Procedure Summaries for Pointer Programs 60 1 Introduction 60 2 Pointer-Manipulating Programs 62 3 Heap Abstraction by Hyperedge Replacement 63 4 Deriving Procedure Contracts by Interprocedural Analysis 66 4.1 IPA Preliminaries 66 4.2 Local Transformers 68 4.3 Global Transformer 72 4.4 Equation System 72 5 Conclusions 73 References 74 Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs 76 1 Introduction 76 2 Preliminaries 78 2.1 Hyperedge Replacement Grammars 78 2.2 Separation Logic 80 2.3 Translating HRGs to Environments and Back 81 3 Generating Predicates for Abstraction and Concretisation 82 3.1 Abstraction and Concretisation Using Graph Grammars 83 3.2 Abstraction and Unrolling in Separation Logic 83 3.3 Structural Properties 84 4 Property Preservation under Translation 89 5 Conclusion 90 References 91 Attribute Handling for Generating Preconditions from Graph Constraints 92 1 Introduction 92 2 BasicConcepts 93 2.1 Formal Concepts 93 2.2 Modeling and Transformation Concepts 94 3 Constructing Precondition NACs with Attributes 98 3.1 Construction of Postcondition NACs from Negative Constraints 98 3.2 Constructing Precondition NAC from Postcondition NAC 99 3.3 Proving the Correctness of the Construction Technique 100 4 Attributes in Search Plan Driven Pattern Matching 102 4.1 Pattern Specification 103 4.2 Creating Operations 103 4.3 Search Plan and Code Generation 105 5 Related Work 105 6 Conclusion 106 References 106 Meta-Modelling and Model Transformations 10 From Core OCL Invariants to Nested Graph Constraints 108 1 Introduction 108 2 CoreOCLInvariants 109 3 Nested Graph Conditions 112 4 Translation of Meta-Models with Core OCL Invariants 114 4.1 Type and State Correspondences 115 4.2 Translation of Core OCL Invariants 116 4.3 Correctness and Completeness 119 5 From Core OCL Invariants to Application Conditions 120 6 Related Work and Conclusion 121 References 122 Specification and Verification of Graph-Based Model Transformation Properties 124 1 Introduction 124 2 The DSLTrans Model Transformation Language 126 3 The Symbolic Model Transformation Property Prover 128 4 Generating the Set of Path Conditions 129 5 Verification of the Property of Interest 130 6 Industrial Case Study 132 6.1 GM-2-AUTOSAR Model Transformation 133 6.2 GM-2-AUTOSAR Model Transformation Properties 134 6.3 Verifying Properties of the GM-2-AUTOSAR Transformation 135 7 Discussion 137 8 Related Work 137 9 Conclusion and Future Work 139 References 139 A Static Analysis of Non-confluent Triple Graph Grammars for Efficient Model Transformation 141 1 Introduction and Motivation 141 2 Running Example and Preliminaries 143 2.1 Consistency Specification with Triple Graph Grammars 144 2.2 Operationalization of Triple Graph Grammars 148 3 Efficient Model Transformation with TGGs 150 4 Related Work 154 5 Conclusion 155 References 156 Rewriting and Applications in Biology 11 Transformation and Refinement of Rigid Structures 157 1 Introduction 157 2 Structures, Patterns, and States 158 3 Rigidity 161 4 Matches as Open Maps 164 5 Growth Policies and Refinements 167 6 Related Work 170 7 Conclusion 170 References 171 Reversible Sesqui-Pushout Rewriting 172 1 Preliminaries 174 1.1 Final Pullback Complements and Stable Pushouts 175 1.2 Splitting and Composing Pushout and FPBC Squares 176 1.3 Finitely Powered Objects 177 2 Reversible Sesqui-Pushout Rewriting 178 2.1 Definition and First Examples 178 2.2 Independence and Commutativity 179 3 On Nested Application Conditions 181 4 On Reversibility of Sesqui-Pushout Rewriting 183 5 Related and Future Work 185 6 Conclusion 186 References 186 On Pushouts of Partial Maps 188 1 Preliminaries 189 1.1 Pattern Graphs 189 1.2 Categories of PartialMaps 191 2 Pushouts of Partial Maps: The State of theArt 193 2.1 A Necessary Condition for Pushouts of Partial Maps 193 2.2 A Locally Necessary Condition 194 2.3 Challenge for a Sufficient Condition 195 3 Partial Map Pushouts by Inheritance 196 4 On Pushouts in Full Subcategories 198 5 Related and FutureWork 200 6 Conclusion 201 References 201 Graph Languages and Graph Transformation 11 The Subgraph Isomorphism Problem on a Class of Hyperedge Replacement Languages 203 1 Introduction 203 1.1 Notation 203 1.2 Background 204 1.3 Goal 207 2 Head-Mid-Tail Grammars 208 2.1 Definition 208 2.2 Normalised Head-Mid-Tail Grammars 209 2.3 Properties of Normalised Grammars 211 2.4 The Algorithm 213 3 Discussion 214 References 217 Canonical Derivations with Negative Application Conditions 218 1 Introduction 218 2 Basic Definitions 220 3 Independence and Switch Equivalence 221 4 Conditional Step Derivations 224 5 Canonical Derivations with Incremental NACs 229 6 Conclusion 231 References 232 Van Kampen Squares for Graph Transformation 233 1 Introduction 233 2 Coupled Transformations 234 3 Characterizing the Van Kampen Property 236 Definition 1 (Separated Kernels). 238 Theorem 1. 239 – 240 – 240 – 240 – 240 4 An Application of the Van Kampen Characterization 241 4.1 Co-transformations 241 Corollary 1. 242 4.2 A Well-Defined Co-transformation with Non-monic Match 242 5 Related Work 244 6 Outlook 245 References 246 Applications 11 Graph Transformation Meets Reversible Circuits: Generation, Evaluation, and Synthesis 248 1 Introduction 248 2 Graph-Transformational Preliminaries 249 3 Reversible Circuits 250 4 Lines Graphs 252 5 Graph Representation of Toffoli Circuits 253 6 Evaluation 255 7 From Reversible Functions to Toffoli Graphs 257 8 From Binary Decision Diagrams to Toffoli Circuits 258 9 Conclusion 262 References 262 Towards Process Miningwith Graph Transformation Systems 264 1 Introduction 264 2 Preliminaries 266 3 Process Mining with Graph Transformation Systems 268 3.1 From Traces to Graph Transformation Systems 268 3.2 Analyzing Models 269 4 Algorithms for Process Mining 271 4.1 The Maximal Rule Algorithm 272 4.2 The Minimal Rule Algorithm 272 4.3 The Context Algorithm 273 4.4 The Genetic Algorithm 275 4.5 The Greedy Mutation Algorithm 277 4.6 Experimental Results 277 5 Conclusion and Further Research 278 References 278 Jerboa: A Graph Transformation Libraryfor Topology-Based Geometric Modeling 280 1 Introduction 280 2 Object Data Structure: Embedded Generalized Maps 282 2.1 Generalized Maps 282 2.2 Embedding 285 2.3 Creation of a New Modeler 286 3 Operations on G-Maps Defined as DPO Rule Schemes 287 3.1 Formal Framework 287 3.2 Editing Topological Rule Schemes 287 3.3 Editing Geometrical Rule Schemes 288 3.4 Syntax Checking 289 3.5 Jerboa Rule Application 290 4 Discussion 292 5 Conclusion and Future Works 294 References 295 Author Index 296 Front Matter....Pages - Parameterized Verification and Model Checking for Distributed Broadcast Protocols....Pages 1-16 Tableau-Based Reasoning for Graph Properties....Pages 17-32 Verifying Monadic Second-Order Properties of Graph Programs....Pages 33-48 Generating Abstract Graph-Based Procedure Summaries for Pointer Programs....Pages 49-64 Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs....Pages 65-80 Attribute Handling for Generating Preconditions from Graph Constraints....Pages 81-96 From Core OCL Invariants to Nested Graph Constraints....Pages 97-112 Specification and Verification of Graph-Based Model Transformation Properties....Pages 113-129 A Static Analysis of Non-confluent Triple Graph Grammars for Efficient Model Transformation....Pages 130-145 Transformation and Refinement of Rigid Structures....Pages 146-160 Reversible Sesqui-Pushout Rewriting....Pages 161-176 On Pushouts of Partial Maps....Pages 177-191 The Subgraph Isomorphism Problem on a Class of Hyperedge Replacement Languages....Pages 192-206 Canonical Derivations with Negative Application Conditions....Pages 207-221 Van Kampen Squares for Graph Transformation....Pages 222-236 Graph Transformation Meets Reversible Circuits: Generation, Evaluation, and Synthesis....Pages 237-252 Towards Process Mining with Graph Transformation Systems....Pages 253-268 Jerboa: A Graph Transformation Library for Topology-Based Geometric Modeling....Pages 269-284 Back Matter....Pages -