Golas Analysis and Correctness of Algebraic Graph and Model Transformations

1. Auflage 2011
ISBN: 978-3-8348-9934-7
Verlag: Vieweg & Teubner
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 226 Seiten, Web PDF

Reihe: Computer Science

Graph and model transformations play a central role for visual modeling and model-driven software development. Within the last decade, a mathematical theory of algebraic graph and model transformations has been developed for modeling, analysis, and to show the correctness of transformations.

Ulrike Golas extends this theory for more sophisticated applications like the specification of syntax, semantics, and model transformations of complex models. Based on M-adhesive transformation systems, model transformations are successfully analyzed regarding syntactical correctness, completeness, functional behavior, and semantical simulation and correctness. The developed methods and results are applied to the non-trivial problem of the specification of syntax and operational semantics for UML statecharts and a model transformation from statecharts to Petri nets preserving the semantics.

Zielgruppe

Research

Autoren/Hrsg.

Golas, Ulrike

Inhaltsverzeichnis

1;Foreword;6
2;Abstract;7
3;Zusammenfassung;9
4;Contents;11
5;List of Figures;14
6;1 Introduction;16
7;2 Introduction to Graph and Model Transformation, and Related Work;22
7.1;2.1 Model Transformation;22
7.2;2.2 Graph Transformation;24
7.3;2.3 Model Transformation Based on Graph Transformation;29
8;3 M-Adhesive Transformation Systems;34
8.1;3.1 Graphs, Typed Graphs, and Typed Attributed Graphs;35
8.2;3.2 M-Adhesive Categories;37
8.2.1;3.2.1 Introduction to M-Adhesive Categories;37
8.2.2;3.2.2 Construction of M-Adhesive Categories;41
8.2.3;3.2.3 Preservation of Additional Properties via Constructions;43
8.2.3.1;3.2.3.1 Binary Coproducts;43
8.2.3.2;3.2.3.2 Epi–M Factorization;45
8.2.3.3;3.2.3.3 E'–M' Pair Factorization;45
8.2.3.4;3.2.3.4 Initial Pushouts;49
8.3;3.3 Algebraic High-Level Petri Nets;55
8.4;3.4 Transformations in M-Adhesive Systems;61
8.4.1;3.4.1 Conditions and Constraints over Objects;62
8.4.2;3.4.2 Rules and Transformations;64
8.4.3;3.4.3 Main Analysis Results in M-Adhesive Transformation Systems;66
8.4.3.1;3.4.3.1 Local Church-Rosser and Parallelism Theorem;66
8.4.3.2;3.4.3.2 Concurrency Theorem;68
8.4.3.3;3.4.3.3 Embedding and Extension Theorem;70
8.4.3.4;3.4.3.4 Critical Pairs and Local Confluence Theorem;72
9;4 Amalgamated Transformations;76
9.1;4.1 Foundations and Analysis of Amalgamated Transformations;76
9.1.1;4.1.1 Kernel, Multi, and Complement Rules;77
9.1.2;4.1.2 Amalgamated Rules and Transformations;84
9.1.3;4.1.3 Parallel Independence of Amalgamated Transformations;96
9.1.4;4.1.4 Other Results for Amalgamated Transformations;102
9.1.5;4.1.5 Interaction Schemes and Maximal Matchings;103
9.1.6;4.1.6 Main Results for Amalgamated Transformations Based on Maximal Matchings;106
9.2;4.2 Operational Semantics Using Amalgamation;108
9.2.1;4.2.1 Semantics for Elementary Nets;108
9.2.2;4.2.2 Syntax of Statecharts;113
9.2.3;4.2.3 Semantics for Statecharts;119
10;5 Model Transformation Based on Triple Graph Transformation;130
10.1;5.1 Introduction to Triple Graph Transformation;130
10.1.1;5.1.1 The Category of Triple Graphs;131
10.1.2;5.1.2 Triple Graph Transformation;132
10.2;5.2 Triple Graph Transformation with Application Conditions;134
10.2.1;5.2.1 S-and T -Consistent Application Conditions;135
10.2.2;5.2.2 Composition and Decomposition of Triple Transformations;146
10.3;5.3 Model Transformation SC2PN from Statecharts to Petri Nets;151
11;6 Analysis, Correctness, and Construction of Model Transformations;168
11.1;6.1 Syntactical Correctness;169
11.2;6.2 Termination and Functional Behavior;171
11.2.1;6.2.1 Termination;171
11.2.2;6.2.2 Termination of Statecharts Semantics;172
11.2.3;6.2.3 Functional Behavior;174
11.3;6.3 Semantical Simulation and Correctness;176
11.3.1;6.3.1 Simulation of Petri Nets;178
11.3.2;6.3.2 Semantical Correctness of the Model Transformation SC2PN;180
11.4;6.4 On-the-Fly Construction of Model Transformations;188
12;7 Conclusion and Future Work;196
12.1;7.1 Theoretical Contributions;196
12.2;7.2 Relevance for Model-Driven Software Development;198
12.3;7.3 Case Studies;200
12.4;7.4 Tool Support;201
12.5;7.5 Future Work;203
13;Appendix;205
13.1;A Categorical Results;206
13.1.1;A.1 Proofs for Construction of M-Adhesive Categories;206
13.1.2;A.2 Proofs for Generalized AHL Schemas as an M-Adhesive Category;208
13.1.3;A.3 Proofs for AHL Systems as an M-adhesive Category;210
13.1.3.1;A.3.1 The Category of Markings;210
13.1.3.2;A.3.2 From Nets to Net Systems;214
13.1.4;A.4 Proofs for Amalgamated Transformations;216
14;Bibliography;224
15;Index;236

Über Autor(innen)

Dr. Ulrike Golas completed her doctoral thesis under the supervision of Prof. Dr. Hartmut Ehrig at the Institut für Softwaretechnik und Theoretische Informatik at Technische Universität, Berlin.