Inhalt

•  
   1 Introduction
•  
   1.1 The problem
•  
   1.2 The objective
•  
   1.3 The approach
•  
   1.4 The contribution
•  
   1.5 The structure of this thesis
•  
  2 Problem Analysis
•  
  2.1 Characteristics of mechatronic systems
•  
   2.1.1 The architecture of advanced mechatronic systems
•  
  2.2 The development of mechatronic systems
•  
   2.2.1 The interdisciplinary design language elaborated in the CRC 614
•  
   2.2.2 Example: specifying two use cases in the RailCab system
•  
   2.3 Problem description
•  
   2.4 Existing scenario-based design techniques
•  
  3 Foundations
•  
  3.1 Modal Sequence Diagrams
•  
   3.1.1 MSDs and the object system
•  
   3.1.2 Events, messages, and runs
•  
   3.1.3 Event unification
•  
   3.1.4 Existential and universal MSDs, hot and cold messages
•  
   3.1.5 Active MSDs, the cut, and hot and cold violations
•  
   3.1.6 The iterative interpretation of MSDs
•  
   3.1.7 Satisfying an MSD specification
•  
   3.1.8 The play-out algorithm
•  
   3.1.9 Consistency, consistent executability, and realizsability
•  
   3.1.10 Parameterized messages
•  
   3.1.11 Object properties and side-effects
•  
   3.1.12 Assignments and conditions
•  
   3.1.13 Visible and Hidden events
•  
   3.1.14 Timed MSD specifications
•  
   3.1.15 Symbolic lifelines
•  
   3.1.16 Forbidden messages
•  
   3.2 Timed Game Automata and Uppaal Tiga
•  
   3.2.1 Timed Automata in Uppaal
•  
   3.2.2 Timed Game Automata in Uppaal Tiga
•  
   3.2.3 On-the-fly synthesis of game strategies
•  
   3.3 Triple Graph Grammars
•  
   3.3.1 Why model transformation with TGGs?
•  
   3.3.2 TGG structure and semantics
•  
   3.3.3 Forward transformation
•  
   3.3.4 Further extensions of TGGs
•  
   4 Synthesis
•  
   4.1 Overview
•  
  4.2 The MSD specification scheme
•  
   4.2.1 Collaboration and class diagram
•  
   4.2.2 Requirement MSDs and assumption MSDs
•  
  4.3 Mapping untimed MSD specifications
•  
   4.3.1 The environment and system automata for untimed MSD specifications
•  
   4.3.2 Mapping the MSDs to TGA
•  
   4.3.3 Encoding assignments and conditions
•  
   4.3.4 Forbidden messages
•  
   4.3.5 Assumption MSDs
•  
  4.4 The winning condition
•  
   4.4.1 Checking consistent executability with Uppaal Tiga
•  
   4.4.2 An alternative winning condition
•  
  4.5 Mapping timed MSD specifications
•  
   4.5.1 The environment and system automata for timed specifications
•  
   4.5.2 Encoding clock resets and time conditions
•  
   4.5.3 Extensions to the winning condition for timed specifications
•  
  4.6 Compositional synthesis
•  
   4.6.1 Compositional reasoning
•  
   4.6.2 The compositional synthesis technique
•  
   4.6.3 Example: the compositional synthesis of the production cell specification
•  
   4.6.4 The compositional synthesis technique is sound
•  
  4.7 Different kinds of consistency
•  
   4.7.1 Disallowing to delay steps in the timed setting
•  
   4.7.2 Consistency vs. consistent executability
•  
  4.8 Summary and Outlook
•  
   4.8.1 Inconsistent environment assumptions
•  
   4.8.2 Partial observability
•  
  5 Symbiosis of Simulation and Synthesis
•  
   5.1 Overview
•  
  5.2 Guiding by controllers from single use cases
•  
   5.2.1 Use case specification example
•  
   5.2.2 Play-out with synthesized controllers
•  
  5.3 Guiding by controllers from composed use cases
•  
   5.3.1 Composed use case example
•  
   5.3.2 Synthesizing controllers from composed use cases
•  
   5.3.3 Guiding the play-out of composed use case occurrences
•  
   5.3.4 Tracking composed use case occurrences
•  
   5.3.5 Systematically tracking composed use case occurrences
•  
   5.3.6 Overly restrictive context expressions
•  
   5.4 Summary and Outlook
•  
  6 Triple Graph Grammar Extensions
•  
   6.1 Overview of the TGG extensions
•  
   6.2 Generalization of TGG rules
•  
   6.2.1 Why a generalization concept for transformation rules?
•  
   6.2.2 The TGG rule generalization concept by Klar et al.
•  
   6.2.3 Improvements to the existing TGG rule generalization concept
•  
   6.3 OCL attribute value constraints
•  
   6.4 UML stereotype constraints
•  
   6.5 Reusable nodes
•  
   6.5.1 Reusable nodes in the example
•  
   6.5.2 The operational semantics of reusable nodes in the target domain during a forward transformation
•  
   6.6 Summary
•  
   6.7 Outlook
•  
  7 Realization and Evaluation
•  
   7.1 The TGG Interpreter
•  
   7.2 MSD-to-TGA mapping and synthesis
•  
  7.3 ScenarioTools
•  
   7.3.1 Modeling
•  
   7.3.2 Simulation
•  
   7.3.3 Physics-engine and visualization
•  
   7.4 Evaluation
•  
   7.4.1 Practicality of the MSD formalism
•  
   7.4.2 Synthesis
•  
   7.4.3 Simulation
•  
   7.4.4 TGG-based model transformation
•  
  8 Related Work
•  
   8.1 Advanced play-out techniques
•  
   8.2 Related synthesis approaches
•  
   8.2.1 Synthesis of global controllers
•  
   8.2.2 Synthesis of distributed controllers
•  
  9 Conclusion and Future Research
•  
   9.1 Summary
•  
   9.2 Future research
•  
  A Meta-Models and Profiles
•  
   A.1 The meta-model for Uppaal Tiga
•  
   A.2 MSD specifications in UML
•  
  B MSD-to-TGA TGG Transformation
•  
   B.1 TGG rule overview
•  
   B.2 OCL attribute definitions
•  
   B.3 TGG rules
•  
   C Examples
•  
  C.1 Simulating an example RailCab specification
•  
   C.1.1 Example specification overview
•  
   C.1.2 Use case DriveOntoTrackSection
•  
   C.1.3 Use case DriveOntoBranchingSwitch
•  
   C.1.4 Use case EnergyManagement
•  
   C.1.5 The simulation model
•  
  C.2 The symbiosis of synthesis and simulation – the use case ``Warn RailCabs On Track''
•  
   C.2.1 Description of the use case ``Warn RailCabs On Track''
•  
   C.2.2 The specification of the use case
•  
   C.2.3 Avoidable violating runs
•  
   C.2.4 The controller synthesized from the use case specification
•  
  C.3 Synthesis example – the production cell
•  
   C.3.1 Description of the production cell example
•  
   C.3.2 The MSD specification of the production cell
•  
   C.3.3 Compositional synthesis of the production cell specification
•  
  C.4 Synthesis performance measurement
•  
   C.4.1 How the measurements were taken
•  
   C.4.2 Untimed specifications with exponentially growing state space
•  
   C.4.3 Timed specification with exponentially growing state space
•  
   Bibliography
•  
   List of Figures
•  
   Index