Inhalt

•  
   Titlepage
•  
   Abstract
•  
   Zusammenfassung
•  
   Acknowledgments
•  
   Table of Contents
•  
   1 Introduction
•  
   1.1 Running Example: Coordinated Overtaking
•  
  1.2 Problem Definition
•  
   1.2.1 Specification of Real-Time Coordination Protocols
•  
   1.2.2 Specification of Domain-Specific Verification Properties for CPS
•  
   1.2.3 Domain-Specific Model Checking (DSMC) of RTCP
•  
   1.2.4 Reusing Experience for the RTCP Design
•  
   1.3 Contribution
•  
   1.4 Thesis Structure
•  
  2 Foundations
•  
  2.1 Timed Model Checking
•  
   2.1.1 Timed Automata
•  
   2.1.2 Timed Computation Tree Logic (TCTL)
•  
   2.1.3 Model Checking Process
•  
   2.1.4 Uppaal Tooling
•  
  2.2 MechatronicUML
•  
   2.2.1 Compositional Verification Approach and DSL Overview
•  
   2.2.2 Real-Time Statecharts
•  
   2.2.3 MechatronicUML Tool Suite
•  
  3 Real-Time Coordination Protocols
•  
   3.1 Contributions
•  
   3.2 Stakeholder and Requirements
•  
   3.3 Structural Specification
•  
   3.3.1 Role
•  
   3.3.2 Role Connector
•  
   3.3.3 Classification of Real-Time Coordination Protocols
•  
   3.3.4 Incoming Message Buffer
•  
   3.3.5 Real-Time Coordination Protocol Instance
•  
   3.3.6 Unsupported Structures
•  
  3.4 Modeling Assumptions
•  
   3.4.1 Assumed Software Layers
•  
   3.4.2 Assumed Steps of a Message Transmission
•  
   3.4.3 Quality of Service (QoS) Assumptions
•  
   3.4.4 Discussion
•  
   3.5 Behavioral Specification
•  
   3.5.1 Single Role Behavior Specification
•  
   3.5.2 Multi Role Behavior Specification
•  
   3.6 Applying RTCPs into the Component Model
•  
   3.6.1 Incoming Message Buffers at Discrete Ports
•  
   3.6.2 Quality-of-Service Assumptions at the Component Model
•  
   3.6.3 One-To-Many Communication Schemata
•  
   3.6.4 Example
•  
  3.7 Implementation
•  
   3.7.1 User Interface
•  
   3.7.2 Plugin Structure
•  
   3.8 Evaluation
•  
   3.8.1 Case Study Context
•  
   3.8.2 Setting the Hypotheses
•  
   3.8.3 Preparing the Validation
•  
   3.8.4 Validating the Hypotheses
•  
   3.8.5 Threats to Validity
•  
   3.8.6 Analyzing the Results
•  
   3.9 Limitations
•  
  3.10 Related Work
•  
   3.10.1 Contracts and Protocols
•  
   3.10.2 Behavioral Connectors
•  
   3.10.3 Component Models
•  
   3.11 Summary
•  
  4 Domain-specific Verification Properties for RTCPs
•  
   4.1 Contributions
•  
   4.2 Stakeholder and Requirements
•  
   4.3 MTCTL - A Domain-Specific Verification Property Language for MechatronicUML
•  
   4.3.1 Simplified EBNF Grammar
•  
   4.3.2 Basic Semantics
•  
   4.3.3 Temporal Quantifiers
•  
   4.3.4 Referencing Elements
•  
   4.3.5 Predicates
•  
   4.3.6 Operations
•  
   4.3.7 Combining Temporal Properties
•  
   4.4 Default Verification Properties for RTCPs
•  
   4.5 Translating MTCTL into English Sentences
•  
  4.6 Implementation
•  
   4.6.1 User Interface
•  
   4.6.2 Plugin Structure
•  
   4.7 Evaluation
•  
   4.7.1 Case Study Context
•  
   4.7.2 Setting the Hypotheses
•  
   4.7.3 Preparing the Validation
•  
   4.7.4 Validating the Hypotheses
•  
   4.7.5 Threats to Validity
•  
   4.7.6 Analyzing the Results
•  
   4.8 Limitations
•  
  4.9 Related Work
•  
   4.9.1 TCTL-Based Languages
•  
   4.9.2 OCL-Based Languages
•  
   4.9.3 Generating the DSVPL
•  
   4.9.4 DSVPLs in MechatronicUML
•  
   4.9.5 Expressing Verification Properties in Natural English
•  
   4.9.6 Patterns for Verification Properties
•  
   4.10 Summary
•  
  5 Domain-specific Model Checking of RTCPs
•  
   5.1 Contributions
•  
   5.2 Stakeholder and Requirements
•  
   5.3 DMSC for CPS by Utilizing Model-To-Model Traceability
•  
   5.4 Model-To-Model Translation from RTCPs to Uppaal
•  
   5.4.1 Protocol to CIC Translation
•  
   5.4.2 MTCTL Set Quantifier Normalization
•  
   5.4.3 MTCTL Static Evaluation Normalization
•  
   5.4.4 MTCTL Split Properties Translation
•  
   5.4.5 Time Unit Normalization
•  
   5.4.6 Renaming Identifiers Normalization
•  
   5.4.7 RTSC Deadline Normalization
•  
   5.4.8 RTSC Composite Transition Normalization
•  
   5.4.9 RTSC State Do-Effect Normalization
•  
   5.4.10 RTSC Hierarchy Normalization
•  
   5.4.11 RTSC State Entry- / Exit-Effect Normalization
•  
   5.4.12 RTSC Urgency Normalization
•  
   5.4.13 MechatronicUML to Uppaal Migration
•  
  5.5 Uppaal-Level Activities
•  
   5.5.1 Layouting Timed Automata Templates
•  
   5.5.2 Model-to-Text-Transformation
•  
   5.5.3 Automating Uppaal
•  
   5.5.4 Text-to-Model-Transformation
•  
   5.6 Model-To-Model Back-Translation from Uppaal to RTCPs
•  
   5.6.1 UTCTL to MTCTL
•  
   5.6.2 Uppaal Trace to MechatronicUML Trace
•  
  5.7 Implementation
•  
   5.7.1 User Interface
•  
   5.7.2 Plugin Structure
•  
  5.8 Evaluation
•  
   5.8.1 Case Study Context
•  
   5.8.2 Setting the Hypotheses
•  
   5.8.3 Preparing the Validation
•  
   5.8.4 Validating the Hypotheses
•  
   5.8.5 Threats to Validity
•  
   5.8.6 Analyzing the Results
•  
   5.9 Limitations
•  
  5.10 Related Work
•  
   5.10.1 Translating DSLs for Communicating CPS to a Model Checking
•  
   5.10.2 DSMC
•  
   5.11 Summary
•  
  6 Formal Design Patterns for RTCPs
•  
   6.1 Contributions
•  
   6.2 Stakeholder and Requirements
•  
   6.3 Real-Time Coordination Patterns
•  
   6.3.1 Concept
•  
   6.3.2 Definition
•  
   6.3.3 Identified Patterns
•  
   6.3.4 Description Format of Real-Time Coordination Patterns
•  
   6.3.5 Example: The Pattern Acquire Assurance
•  
   6.4 Abstracting an RTCP to a Pattern
•  
   6.5 Selecting and Adapting a Pattern to an RTCP
•  
   6.6 Implementation
•  
   6.6.1 User Interface
•  
   6.6.2 Plugin Structure
•  
  6.7 Evaluation
•  
   6.7.1 Case Study Context
•  
   6.7.2 Setting the Hypotheses
•  
   6.7.3 Preparing the Validation
•  
   6.7.4 Validating the Hypotheses
•  
   6.7.5 Threats to Validity
•  
   6.7.6 Analyzing the Results
•  
   6.8 Limitations
•  
  6.9 Related Work
•  
   6.9.1 Informal Design Patterns
•  
   6.9.2 Formal Design Patterns
•  
   6.10 Summary
•  
  7 Conclusion
•  
   7.1 Summary
•  
   7.2 Future Work
•  
  A Catalog of One-To-Many Communication Schemata
•  
   A.1 Normalization Template for Multicast with Subrole Condition
•  
   A.2 Normalization Template for Multireceive with Subrole Condition
•  
  A.3 Unicast
•  
   A.3.1 Definition
•  
   A.3.2 Normalization Template
•  
  A.4 Singlereceive
•  
   A.4.1 Definition
•  
   A.4.2 Normalization Template
•  
  A.5 Iterate
•  
   A.5.1 Definition
•  
   A.5.2 Normalization Template
•  
  A.6 Loadbalancing
•  
   A.6.1 Definition
•  
   A.6.2 Normalization Templates
•  
  B Catalog of Real-Time Coordination Patterns
•  
   B.1 Request Information
•  
   B.2 Fail-operational Delegation
•  
   B.3 Fail-safe Delegation
•  
   B.4 Event-based Transmission
•  
   B.5 Periodic Transmission
•  
   B.6 Alternating Lock
•  
   B.7 Block Execution
•  
   B.8 Limit Observation
•  
  C Evaluation Details
•  
  C.1 Examples
•  
   C.1.1 Overtaking Cars (Extended)
•  
   C.1.2 RailCab
•  
   C.1.3 BeBot
•  
   C.2 MTCTL
•  
   C.3 DSMC
•  
  D Details of the RTCP Overtaking
•  
   D.1 Uppaal Representation
•  
   D.2 Exemplary SVG Counterexample Trace
•  
  E Implementation Details
•  
   E.1 RTCP
•  
   E.1.1 Package Core
•  
   E.1.2 Package ValueType
•  
   E.1.3 Package Behavior
•  
   E.1.4 Package Action Language
•  
   E.1.5 Packages Connector and MsgType
•  
   E.1.6 Packages Protocol and Constraint
•  
   E.1.7 Package Realtimestatechart
•  
   E.1.8 Package One-To-Many Communication Schemata
•  
   E.1.9 Package Component
•  
   E.1.10 Package Instance
•  
  E.2 MTCTL
•  
   E.2.1 Metamodel
•  
   E.2.2 Grammar
•  
   E.3 DSMC of RTCPs via Uppaal
•  
   E.3.1 DSMC Options Metamodel
•  
   E.3.2 MechatronicUML Verification Extension Metamodel
•  
   E.3.3 Uppaal Timed Automata Metamodel
•  
   E.3.4 UTCTL Metamodel
•  
   E.3.5 Uppaal Trace Grammar
•  
   E.3.6 Uppaal Trace Metamodel
•  
   E.3.7 MechatronicUML Trace Metamodel
•  
  E.4 Real-Time Coordination Patterns
•  
   E.4.1 Metamodel
•  
   E.4.2 Ontology
•  
   F List of Abbreviations
•  
   G Paper Contributions
•  
  Bibliography
•  
   Own Publications
•  
   Supervised Theses
•  
   Literature
•  
   Norms and Specifications
•  
   List of Figures
•  
   List of Tables