Heinzemann, Christian: Verification and simulation of self-adaptive mechatronic systems. 2015
Inhalt
1 Introduction
2 Foundations
2.1 Self-Adaptive Mechatronic Systems
2.2 Timed Model Checking
2.3 Graph-Based Specifications
2.4 MechatronicUML
3 MechatronicUML Component Model
3.1 Modeling Components
3.1.1 Ports
3.1.2 Atomic Components
3.1.3 Structured Components
3.1.4 Connectors
3.1.5 Component Properties
3.2 Component Instances
3.3 Modeling Reconfiguration
3.3.1 Component Story Diagrams
3.3.2 Controller Exchange Nodes
3.3.3 Constraints for Multi Port Variables
3.3.4 Reconfiguration of Atomic Components
3.4 Instantiating Real-Time Coordination Protocols on System Level
3.5 Modeling Component Properties by Architectural Constraints
3.6 Implementation
3.7 Related Work
3.8 Summary
4 Transactional Execution of Hierarchical Reconfigurations
4.1 MechatronicUML Reconfiguration Controller
4.2 Executing Reconfigurations
4.3 Declarative, Table-based Specification of the Reconfiguration Controller
4.3.1 Interface Specification of RM Ports
4.3.2 Manager Specification
4.3.3 Executor Specification
4.3.4 Interface Specification of RE Ports
4.4 Generating Operational Behavior Specifications
4.5 Verifying the Reconfiguration Specification
4.6 Implementation
4.7 Assumptions and Limitations
4.8 Related Work
4.8.1 Approaches Supporting Reconfiguration of Hierarchical Components
4.8.2 Quiescence of Components
4.9 Summary
5 Verifying Refinements based on Test Automata
5.1 Refining Real-Time Coordination Protocols to Port Implementations
5.2 Considered Refinement Definitions
5.3 Test automata-based Refinement Checking
5.3.1 Refinement Selection
5.3.2 Construction of the Test Automaton
5.3.3 Adjusting the Port Real-Time Statechart
5.3.4 Parallel Composition and Reachability Analysis
5.4 Implementation
5.5 Assumptions and Limitations
5.6 Case Study
5.6.1 Case Study Context
5.6.2 Setting the Hypothesis
5.6.3 Preparing the Input Models
5.6.4 Validating the Hypothesis
5.6.5 Analyzing the Results
5.7 Related Work
5.8 Summary
6 Simulating Self-Adaptive Mechatronic Systems in MATLAB/Simulink
6.1 MATLAB/Simulink and Stateflow
6.2 MIL Simulation of MechatronicUML Models in Simulink and Stateflow
6.3 Translating Component Instance Configurations to Simulink Block Diagrams
6.3.1 Translating Atomic Component Instances
6.3.2 Translating Structured Component Instances
6.3.3 Using Message-Based Communication
6.3.4 Considering QoS Assumptions
6.4 Translating Real-Time Statecharts to Stateflow Charts
6.4.1 Basic Transformation Concepts
6.4.2 Message-Based Communication
6.4.3 Clock Concept
6.4.4 Urgency
6.4.5 Real-Time Statecharts of Multi Port Instances
6.4.6 Synchronizations
6.5 Translating Reconfiguration Specifications to Simulink and Stateflow
6.5.1 Step 1: Compute Possible Configurations
6.5.2 Step 2: Create Integrated CIC for Component
6.5.3 Step 3: Generate the MATLAB-specific Reconfiguration Controller
6.5.4 Step 4: Encode Configurations and Generate Control Signals
6.5.5 Step 5: Create Integrated System CIC
6.5.6 Integrate MATLAB-specific reconfiguration controller into the Simulink Block Diagram
6.5.7 Realizing Port Reconfiguration in Stateflow Charts
6.6 Implementation
6.7 Limitations
6.8 Case Study
6.8.1 Case Study Context
6.8.2 Setting the Hypothesis
6.8.3 Preparing the Input Models
6.8.4 Validating the Hypothesis
6.8.5 Analyzing the Results
6.9 Related Work
6.9.1 Reconfiguration in MATLAB/Simulink
6.9.2 Reconfiguration in other Simulation Environments
6.9.3 Reconfiguration in AUTOSAR 3.x
6.9.4 Hybrid Verification
6.10 Summary
7 Conclusions
A Complete RailCab Example
A.1 RTCPs
A.1.1 ConvoyEntry
A.1.2 ConvoyCoordination
A.1.3 ProfileDistribution
A.1.4 SpeedTransmission
A.1.5 StartExecution
A.1.6 StrategyExchange
A.1.7 NextSectionFree
A.2 Instantiating Real-Time Coordination Protocols on System Level
A.2.1 A Simple Discovery Protocol and Environment Model
A.2.2 Instantiating the RTCP ProtocolInstantiation
A.2.3 The RTCP ProtocolInstantiation
A.3 Components
A.4 Component Instances
A.5 Component RTSCs
A.6 Reconfiguration Behavior Specification of Components
A.6.1 Declarative, Table-based Reconfiguration Specification
A.6.2 Reconfiguration Rules
A.6.3 Generated RTSCs for Manager and Executor of RailCabDriveControl
A.6.4 Specification of the Executor Operations
A.7 Component SDDs
A.7.1 RailCabDriveControl
A.7.2 ConvoyCoordination
A.7.3 VelocityController
A.7.4 OperationStrategy
A.7.5 RefGen
A.8 Excerpt of Generated MATLAB/Simulink Model
B Formalization of the Real-time Statechart Semantics
C A Framework for Reachability Analyses
C.1 Reachability Analysis Framework
C.2 Story Diagram Reachability Analysis
C.3 RTSC Reachability Analysis
C.4 UDBM Library
D Metamodels
D.1 MechatronicUML Component Model
D.2 MechatronicUML Reconfiguration
D.2.1 Reconfigurable Components
D.2.2 Component Story Patterns
D.2.3 Component Story Diagrams
D.2.4 Component Story Decision Diagrams
D.3 MATLAB/Simulink and Stateflow
Own Publications
Supervised Thesis
Literature
List of Abbreviations
List of Figures