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
Heinzemann, Christian: Verification and simulation of self-adaptive mechatronic systems. 2015
Inhalt
1 Introduction
1.1 The RailCab System
1.2 Problem Statement
1.3 Contribution
1.4 Overview
2 Foundations
2.1 Self-Adaptive Mechatronic Systems
2.1.1 Structuring
2.1.2 Operator-Controller-Module
2.1.3 Models@Runtime
2.2 Timed Model Checking
2.2.1 Timed Automata
2.2.2 Timed Computation Tree Logic
2.2.3 Model Checking Procedure
2.3 Graph-Based Specifications
2.3.1 Typed Attributed Graph Transformations Systems
2.3.2 Story Driven Modeling
2.4 MechatronicUML
2.4.1 Real-Time Coordination Protocols
2.4.2 Real-Time Statecharts
2.4.3 Assumptions on Quality-of-Service Characteristics
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.4.1 Instantiating the RTCP ProtocolInstantiation
3.4.2 The RTCP ProtocolInstantiation
3.5 Modeling Component Properties by Architectural Constraints
3.6 Implementation
3.7 Related Work
3.7.1 Software Component Models
3.7.2 ADLs for Self-Adaptive Systems
3.7.3 Constraint Languages
3.8 Summary
4 Transactional Execution of Hierarchical Reconfigurations
4.1 MechatronicUML Reconfiguration Controller
4.2 Executing Reconfigurations
4.2.1 Single-Phase Execution
4.2.2 Three-Phase Execution
4.2.3 Quiescence
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.4.1 Manager Specification
4.4.2 Executor Specification
4.5 Verifying the Reconfiguration Specification
4.5.1 Consistency
4.5.2 Timing
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.1.1 Real-Time Coordination Protocol EnterSection
5.1.2 Refined Port Real-Time Statecharts
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.7.1 Refinement Checking
5.7.2 Test automata-based Verification
5.8 Summary
6 Simulating Self-Adaptive Mechatronic Systems in MATLAB/Simulink
6.1 MATLAB/Simulink and Stateflow
6.1.1 Simulink
6.1.2 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
7.1 Summary
7.2 Future Work
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.3.1 RailroadCrossing
A.4 Component Instances
A.4.1 RailCab Driving as a Coordinator
A.4.2 RailCab Driving as a Member
A.5 Component RTSCs
A.5.1 RTSCs of the RailCab Components
A.5.2 RTSCs of the Section Components
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
A.8.1 Simulink Model for Atomic Component Instance of Type RefGen
A.8.2 Simulink Model for Structured Component Instance of Type ConvoyCoordination
B Formalization of the Real-time Statechart Semantics
C A Framework for Reachability Analyses
C.1 Reachability Analysis Framework
C.1.1 Metamodel
C.1.2 Reachability Analysis Algorithm
C.2 Story Diagram Reachability Analysis
C.2.1 Metamodel Extension
C.2.2 Functions of the Reachability Analysis
C.3 RTSC Reachability Analysis
C.3.1 Metamodel Extension
C.3.2 Functions of the Reachability Analysis
C.4 UDBM Library
D Metamodels
D.1 MechatronicUML Component Model
D.1.1 Core
D.1.2 Components
D.1.3 Component Instances
D.1.4 Runtime 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
D.3.1 Simulink
D.3.2 Stateflow
D.3.3 Message-Based Communication
D.3.4 Reconfiguration
Own Publications
Supervised Thesis
Literature
List of Abbreviations
List of Figures
Die detaillierte Suchanfrage erfordert aktiviertes Javascript.