Heinzemann, Christian: Verification and simulation of self-adaptive mechatronic systems. 2015
Content
- 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