Content

•  
   Short contents
•  
   Contents
•  
   1 Motivation and Overview
•  
   1.1 Role of Models in Software Development
•  
   1.2 Model-Based Software Development Process
•  
   1.3 Correctness of Model Transformation
•  
   1.4 Objective of this Thesis
•  
   1.5 Solution Idea
•  
   1.6 Structure of this Thesis
•  
  2 Problem Statement
•  
   2.1 Model-Driven Architecture Approach
•  
   2.2 Requirements for Model Transformation
•  
  2.3 Survey of Techniques for Semantics Preserving Model Transformations
•  
   2.3.1 Overview of Specific Approaches
•  
   2.3.2 Discussion
•  
   2.3.3 Conclusion from the Survey
•  
   2.4 Concept of our Method
•  
   2.4.1 Syntax Definition
•  
   2.4.2 Behavioural Semantics Definition
•  
   2.4.3 Semantics Preserving Model Transformation
•  
   2.5 Summary
•  
   3 Foundations of Graph Transformations
•  
  3.1 Graphs
•  
   3.1.1 Graphs and Typed Graphs
•  
   3.1.2 Type Restriction
•  
   3.1.3 Attributed Graphs
•  
   3.2 Graphs as a Tool for Syntax Definition
•  
  3.3 Graph Transformations
•  
   3.3.1 Introduction
•  
   3.3.2 Basic Definitions for Graph Transformations
•  
   3.3.3 Injective and Non-injective Matches
•  
   3.3.4 Important Notation
•  
   3.3.5 Universal Quantification
•  
   3.3.6 Graph Transformations for Attributed Graphs
•  
   3.4 Behavioural Semantics Based on Graph Transformations
•  
   3.5 Model Transformation Based on Graph Transformations
•  
   3.6 Graph Transformation Tool
•  
   3.7 Summary
•  
  4 Equivalence Relation on LTS
•  
   4.1 General Approach
•  
   4.2 Transition Systems
•  
   4.3 Bisimulation as Type of Behavioral Equivalence
•  
   4.4 Properties Specification over LTS
•  
   4.4.1 Why ACTL
•  
   4.4.2 Syntax of ACTL
•  
   4.4.3 Semantics of ACTL
•  
   4.4.4 Behavioural Properties Specification with ACTL
•  
  4.5 ACTL Equivalence and Weak Bisimulation
•  
   4.5.1 ACTL Equivalence
•  
   4.5.2 Preservation of ACTL Formulas by Weak Bisimulation
•  
   4.5.3 Additional Theorem about ACTL Formulas Preservation
•  
   4.6 Summary
•  
   5 Method for Semantics Preserving Model Transformation
•  
   5.1 Problem Definition
•  
   5.2 Proposed Solution
•  
  5.3 Method
•  
   5.3.1 Language Syntax (Step 1)
•  
   5.3.2 Language Semantics (Step 2)
•  
   5.3.3 Mapping over the Rule Systems (Step 3)
•  
   5.3.4 Model Transformation (Step 4)
•  
   5.3.5 Establishment of Weak Bisimulation (Step 5)
•  
   5.3.6 Summary
•  
   5.4 Interpretation of Behavioural Properties
•  
   5.5 Summary
•  
   6 Case Study: Model Transformation of CCS into Petri Nets
•  
  6.1 CCS Language (Steps 1-2)
•  
   6.1.1 Original Syntax and Semantics
•  
   6.1.2 From EBNF to Meta-Model
•  
   6.1.3 From Interleaving Operational Semantics to Semantics Defined by Graph Transformations
•  
   6.1.4 Semantics Preservation
•  
  6.2 Petri Nets (Steps 1-2)
•  
   6.2.1 Syntax
•  
   6.2.2 Semantics
•  
   6.3 Mapping over the Rule Systems (Step 3)
•  
  6.4 Model Transformation Specification (Step 4)
•  
   6.4.1 TGG Model Transformation
•  
   6.4.2 Mapping of Well-Formed CCS Graphs to Petri Nets
•  
   6.4.3 Graph Transformation System
•  
   6.4.4 Auxiliary Notation for CCS Graphs
•  
   6.4.5 Important Observations about CCS Graphs
•  
  6.5 Correctness of Model Transformation (Step 5)
•  
   6.5.1 Auxiliary Notation for Corresponding Nodes
•  
   6.5.2 Important Observations about Corresponding Structure
•  
   6.5.3 Definition and Proving of Weak Bisimulation
•  
  6.6 Properties Interpretation for Petri Nets
•  
   6.6.1 System Design
•  
   6.6.2 Properties Specification
•  
   6.6.3 Properties Interpretation
•  
   6.7 Summary
•  
  7 Conclusion
•  
   7.1 Contribution of this Thesis
•  
  7.2 Analysis of the Method
•  
   7.2.1 Restrictions
•  
   7.2.2 Model Transformation
•  
   7.2.3 Proof Statement
•  
   7.2.4 Proof Algorithm
•  
   7.3 Discussion of the method
•  
   7.4 Overview of Publications
•  
   7.5 Future Research
•  
   Bibliography
•  
   List of Figures