Analysis and Correctness of Algebraic Graph and Model Transformations

Cover......Page 1
Analysis and Correctness\rof Algebraic Graph\rand Model Transformations......Page 4
ISBN 9783834814937......Page 5
Foreword......Page 6
Abstract......Page 8
Zusammenfassung......Page 10
Contents......Page 12
List of Figures......Page 16
1 Introduction......Page 19
2.1 Model Transformation......Page 25
2.2 Graph Transformation......Page 27
2.3 Model Transformation Based on Graph Transformation......Page 32
3 M-Adhesive Transformation Systems......Page 37
3.1 Graphs, Typed Graphs, and Typed Attributed Graphs......Page 38
3.2.1 Introduction to M-Adhesive Categories......Page 40
3.2.2 Construction of M-Adhesive Categories......Page 44
3.2.3.1 Binary Coproducts......Page 46
3.2.3.3 E\'–M\' Pair Factorization......Page 48
3.2.3.4 Initial Pushouts......Page 52
3.3 Algebraic High-Level Petri Nets......Page 58
3.4 Transformations in M-Adhesive Systems......Page 64
3.4.1 Conditions and Constraints over Objects......Page 65
3.4.2 Rules and Transformations......Page 67
3.4.3.1 Local Church-Rosser and Parallelism Theorem......Page 69
3.4.3.2 Concurrency Theorem......Page 71
3.4.3.3 Embedding and Extension Theorem......Page 73
3.4.3.4 Critical Pairs and Local Confluence Theorem......Page 75
4.1 Foundations and Analysis of Amalgamated Transformations......Page 79
4.1.1 Kernel, Multi, and Complement Rules......Page 80
4.1.2 Amalgamated Rules and Transformations......Page 87
4.1.3 Parallel Independence of Amalgamated Transformations......Page 99
4.1.4 Other Results for Amalgamated Transformations......Page 105
4.1.5 Interaction Schemes and Maximal Matchings......Page 106
4.1.6 Main Results for Amalgamated Transformations Based on Maximal Matchings......Page 109
4.2.1 Semantics for Elementary Nets......Page 111
4.2.2 Syntax of Statecharts......Page 116
4.2.3 Semantics for Statecharts......Page 122
5.1 Introduction to Triple Graph Transformation......Page 133
5.1.1 The Category of Triple Graphs......Page 134
5.1.2 Triple Graph Transformation......Page 135
5.2 Triple Graph Transformation with Application Conditions......Page 137
5.2.1 S-and T -Consistent Application Conditions......Page 138
5.2.2 Composition and Decomposition of Triple Transformations......Page 149
5.3 Model Transformation SC2PN from Statecharts to Petri Nets......Page 154
6 Analysis, Correctness, and Construction of Model Transformations......Page 171
6.1 Syntactical Correctness......Page 172
6.2.1 Termination......Page 174
6.2.2 Termination of Statecharts Semantics......Page 175
6.2.3 Functional Behavior......Page 177
6.3 Semantical Simulation and Correctness......Page 179
6.3.1 Simulation of Petri Nets......Page 181
6.3.2 Semantical Correctness of the Model Transformation SC2PN......Page 183
6.4 On-the-Fly Construction of Model Transformations......Page 191
7.1 Theoretical Contributions......Page 199
7.2 Relevance for Model-Driven Software Development......Page 201
7.3 Case Studies......Page 203
7.4 Tool Support......Page 204
7.5 Future Work......Page 206
Appendix......Page 209
A.1 Proofs for Construction of M-Adhesive Categories......Page 211
A.2 Proofs for Generalized AHL Schemas as an M-Adhesive Category......Page 213
A.3.1 The Category of Markings......Page 215
A.3.2 From Nets to Net Systems......Page 219
A.4 Proofs for Amalgamated Transformations......Page 221
Bibliography......Page 229
Index......Page 241