Preface
Organization
Contents
Methodologies, Processes and Platforms
The Smart Grid Simulation Framework: Model-Driven Engineering Applied to Cyber-Physical Systems
1 Introduction
2 State of the Art
3 Overview of the Smart Grid Simulation Framework
3.1 An Approach Based on Model Refinement
3.2 Download
4 Modeling and Execution of a Cosimulation Scenario
4.1 CosiML, a DSL for Cosimulation
4.2 Generation Tools for FMI Cosimulation
5 Functional Architecture for Smart Grid Simulation
5.1 SGridML
5.2 AllocationML and CatalogML: Two DSLs to Define the Transformation
5.3 Generation of a CosiML Cosimulation Model
6 Use-Case Cosimulation
6.1 The Use-Case of an Islanded Smart Grid
6.2 Behavior Model with SGridML
6.3 Allocation, Catalog and Simulation Models
6.4 Simulation Models and Cosimulation Model
6.5 Simulation and Decisions
7 Observations
8 Conclusion
References
Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications
1 Introduction
2 Motivation
2.1 The Established Hardware Design Approach
2.2 Considered Problem
3 Related Work
4 Proposal of the Alternative Design Approach
4.1 Detection of Integer Overflows
5 Extraction of the CaSH Model
6 Overflow Detection Pattern
6.1 Closure of Functions
7 Evaluation
7.1 Integer Overflow Detection Implementations
7.2 Comparison of Integer Arithmetic Operations
8 Discussion
9 Conclusion
References
Systematic Synthesis of Energy-Aware Timing Models in Automotive Software Systems
1 Introduction
1.1 State-of-the Practice by Automotive Organizations
1.2 Relation to Author's Previous Work and Novel Contributions
2 Background and Related Work
2.1 Modeling Automotive Embedded Software Systems
2.2 Model-Based Timing Specification
2.3 Model-Based Timing and Energy Analysis
3 Workflow for Synthesis of Energy-Aware Timing Models
3.1 Steps Involved in the Synthesis of an Energy-Aware Timing Analysis Model
3.2 Generic Timing-Energy Metamodel
3.3 Mapping Among Metamodels for Timing Properties
3.4 Mapping Between MARTE Stereotypes and Custom-Defined Timing-Energy Metamodel for Energy Properties
3.5 Model-to-Model (M2M) Transformations
4 Autonomous Emergency Braking System (AEBS)
4.1 AUTOSAR Design Model
4.2 Timing Specification
4.3 Specification of Energy Properties
4.4 Model Transformations
4.5 Synthesis of Energy-Aware Timing Analysis Model of AEBS
4.6 Performance Analysis
5 Conclusion
References
Model-Based Virtual Prototyping of CPS: Application to Bio-Medical Devices
1 Introduction
2 Related Work
3 Basic Concepts
3.1 Multi-level Model-Based Design
3.2 SystemC AMS
3.3 Co-Simulation
4 Partitioning Level
4.1 Functional Modeling and Verification
4.2 Hardware Components
5 Software Design Level
5.1 Software Components
5.2 Analog and Digital Hardware Components
5.3 Deployment Diagram
6 Case Study
6.1 Partitioning Level
6.2 Component Design Level
7 Discussion and Future Work
References
Applications and Software Development
ProvAnalyser: A Framework for Scientific Workflows Provenance
1 Introduction
2 Scientific Workflow Provenance
2.1 Scientific Workflows
2.2 Scientific Workflow Provenance Model
2.3 Architecture
3 SenpsLAND Provenance: A ProvAnalyser Case Study
3.1 Workflows in SenapsLAND
3.2 SENProv: Provenance Ontology for SenapsLAND
3.3 SenapsLAND Provenance Knowledge Graph
3.4 Implementation and Performance
4 Querying Workflow Provenance
4.1 Evaluation Use Cases
4.2 Provenance Queries
5 Discussion
6 Related Work
7 Conclusion
References
A Multi-Model Reviewing Approach for Production Systems Engineering Models
1 Introduction
2 Background
2.1 Visualisation Techniques for Structural Data
2.2 AutomationML – The Open pse Data Exchange Standard
2.3 Domain-Specific Data Modeling with AutomationML
3 Requirements for the Visualisation of Multi-disciplinary Engineering Data
3.1 Requirements for Engineering Data Visualisation
3.2 Context and Use Cases
4 System Design for Engineering Data Visualisation
4.1 Multi-model Reviewing Approach
4.2 Multi-Model Reviewer System Design
5 Prototype and Evaluation
5.1 Multi-Model Reviewer Prototype Implementation
5.2 Multi-Model Review Performance – Evaluation Design
5.3 Performance Evaluation Results
6 Discussion
7 Related Work
7.1 Domain Modeling in Production Systems Engineering
7.2 Domain-Specific Model Visualisation
8 Conclusion and Future Work
References
Augmenting Deep Neural Networks with Scenario-Based Guard Rules
1 Introduction
2 Background
2.1 Scenario-Based Modeling
2.2 Deep Neural Networks and Override Rules
3 Modeling Override Scenarios
3.1 Modeling DNNs and Override Rules in SBM
3.2 Liveness Properties
3.3 Automated Analysis
4 Three Case-Studies
4.1 Override Rules for DeepRM
4.2 Override Rules for Pensieve
4.3 Override Rules for Custard
5 Recurrent Neural Networks
5.1 Memory Units
5.2 Undesirable Behaviors in RNNs
5.3 Override Rules for RNNs
5.4 Modeling RNN Override Rules in SBM
6 Related Work
7 Discussion and Next Steps
References
Modeling Languages, Tools and Architectures
Resilient Business Process Modeling and Execution Using BPMN and Microservices
1 Introduction
2 Case Study: An Environmental-Friendly Slurry Application
2.1 BPMN Process Model
2.2 BPMN Model Weaknesses
3 Resilient Process Modeling
3.1 Process Modeling Requirements
3.2 Extension Concepts
3.3 Meta Model Extension
3.4 Model Resilience Verification
4 Resilient Process Execution
4.1 Process Execution Requirements
4.2 Initial Participant Configuration
4.3 Movement of Functionality
4.4 Discovery of Neighboring Participants
4.5 On-Demand Usage of Functionality
4.6 Dynamic Decision Making on Alternatives
5 Evaluation
5.1 Adding Resilience to the Slurry Process Model
5.2 Realizing a Resilient Slurry Process Execution
5.3 Discussion of Evaluation Results
6 Related Work
7 Conclusion
References
Model Transformation from CBM to EPL Rules to Detect Failure Symptoms
1 Introduction
2 Use PHM Approach to Detect Failure Symptoms
2.1 Prognostics and Health Management
2.2 Expert System
2.3 Complex Event Processing
2.4 Using CEP and Expert System to Support PHM Approach
3 Proposed Model Driven Architecture
3.1 Model, Metamodel, Model Transformation
3.2 Model-Driven Architecture from CBM to EPL Rules
4 Model Transformation
4.1 Generic Rules Metamodel
4.2 From CBM Knowledge Base to Generic Rules
4.3 From Generic Rules to EPL
5 Case Study/Illustration
5.1 System Description
5.2 Examples of CBM Models
5.3 Generic Rules Examples
5.4 Examples of EPL Models
6 Summary and Future Work
References
Verification and Simulation of Time-Domain Properties for Models of Behaviour
1 Introduction
2 Adopting Logic-Labelled Finite-State Machines
3 Formal Definition of LLFSMs
3.1 Semantics
3.2 Timed LLFSMs
4 Value-Domain Versus Time-Domain
5 From LLFSMs to SMV Models via ATL Transformations
5.1 LLFSM with Non-sectioned States Through an M2M Transformation
5.2 M2M Transformation to Handle a State's Section Atomically
5.3 Handling Variables
5.4 The Transformation When There Are No Temporal Transitions
5.5 Temporalised Transitions
6 Verification in the Time Domain
7 Formal Verification of the SMV Output and Trace Emulation
7.1 Verification of the M2Text SMV Output
7.2 Trace Emulation
7.3 Complexity
8 Final Remarks
References
Domain-Driven Architecture Modeling and Rapid Prototyping with Context Mapper
1 Introduction
2 Context and Previous Work
3 Domain-Driven Design (DDD) Essence, Meta-model
3.1 Motivating Example
3.2 DDD Patterns
3.3 DDD Meta-model for Context Mapper
3.4 Architectural Viewpoints
3.5 Related Work
4 Context Mapper DSL (CML)
4.1 Domains and Subdomains
4.2 Bounded Contexts
4.3 The Context Map
4.4 Relationship Syntax
4.5 Expressing User Requirements
5 Language and Tool Extension: Rapid Prototyping
6 Validation and Discussion
7 Summary and Outlook
References
Abstract Test Execution for Early Testing Activities in Model-Driven Scenarios
1 Introduction
1.1 Problem Statement
1.2 Outline
2 Foundations
2.1 Running Example - Automatic Door Control System
2.2 User-Specific Integrated Model Basis
2.3 Analysis-Specific Integrated Model Basis
3 Abstract Test Execution
3.1 Overall Process
3.2 Preprocessing and Derivation of Abstract Test Cases
3.3 Path Merging Based on Integrated Model Basis Mappings
3.4 Evaluation of Path Space
3.5 Result to Verdict Mapping
3.6 Result Selection and Test Report
4 Qualitative Evaluation and Critical Discussion
5 Related Work
6 Conclusion and Outlook
References
A Methodological Assistant for UML and SysML Use Case Diagrams
1 Introduction
2 Design Guidelines for Use Case Diagrams
2.1 Use Case Diagrams
2.2 Rules and Guidelines for SysML/UML Use Case Diagrams
2.3 Generic Use Case Diagram
2.4 Difficulties for Beginners
3 Methodological Assistant
3.1 Overview
3.2 Verification Module
3.3 Import Module
3.4 Creation Module
4 Case Study
4.1 A Posteriori Assistance
4.2 A Priori Assistance
5 Related Work
5.1 Experiences with Use Case Diagrams
6 Conclusions
References
Model-Based Static and Runtime Verification for Ethereum Smart Contracts
1 Introduction
2 Smart Contract Verification
2.1 Control-Flow Automata
2.2 Dynamic Event Automata
3 Synergy of Static and Runtime Verification
3.1 Residual Correctness
3.2 Residual Analysis
4 Tool
4.1 Architecture and Flow
5 Evaluation
6 Discussion
7 Related Work
7.1 Verification Methods for Smart Contracts
7.2 Partial Verification
8 Conclusions and Future Work
References
A Novel Family of Queuing Network Models for Self-adaptive Systems
1 Introduction
2 Motivating Scenario
3 SMAPEA Queuing Networks
3.1 Reference Self-adaptation Model
3.2 Generalized Queuing Network Model for SaSs
3.3 Modeling Patterns for SMAPEA QNs
3.4 Limitations
4 Experimentation
4.1 Subject of the Experimentation
4.2 QN Parameterization
4.3 Methodology
4.4 Execution
4.5 Results
4.6 Threats to Validity
5 Related Work
6 Conclusion
References
Author Index