de
en
Schliessen
Detailsuche
Bibliotheken
Projekt
Impressum
Datenschutz
Schliessen
Publizieren
Besondere Sammlungen
Digitalisierungsservice
Hilfe
Impressum
Datenschutz
zum Inhalt
Detailsuche
Schnellsuche:
OK
Ergebnisliste
Titel
Titel
Inhalt
Inhalt
Seite
Seite
Im Werk suchen
Specification and verification for real-time coordination protocols of cyber-physical systems / by Stefan Dziwok ; supervised by Prof. Dr. Wilhelm Schäfer and Prof. Dr. Matthias Tichy. Paderborn, 2017
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
Die detaillierte Suchanfrage erfordert aktiviertes Javascript.