Leveraging Applications of Formal Methods, Verification and Validation. Practice: 11th International Symposium, ISoLA 2022, Rhodes, Greece, October ... Part IV (Lecture Notes in Computer Science)

✍ Scribed by Tiziana Margaria (editor), Bernhard Steffen (editor)

• Publisher: Springer
• Year: 2022
• Tongue: English
• Leaves: 431
• Category: Library

✦ Synopsis

This four-volume set LNCS 13701-13704 constitutes contributions of the associated events held at the 11th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022, which took place in Rhodes, Greece, in October/November 2022.

The contributions in the four-volume set are organized according to the following topical sections: specify this - bridging gaps between program specification paradigms; x-by-construction meets runtime verification; verification and validation of concurrent and distributed heterogeneous systems; programming - what is next: the role of documentation; automated software re-engineering; DIME day; rigorous engineering of collective adaptive systems; formal methods meet machine learning; digital twin engineering; digital thread in smart manufacturing; formal methods for distributed computing in future railway systems; industrial day.

✦ Table of Contents

Introduction
Organization
Contents – Part IV
Digital Twin Engineering
Engineering of Digital Twins for Cyber-Physical Systems
1 Introduction
2 Contributions
3 Concluding Remarks
References
Towards Requirements Engineering for Digital Twins of Cyber-Physical Systems
1 Introduction
2 Context
3 Requirements Engineering for Digital Twins
3.1 Requirements Elicitation
3.2 Requirements Specification and Modeling
3.3 Requirements Verification and Validation
4 Common DT Requirements
4.1 Data Synchronization Between DT and CPS
4.2 Modeling Paradigms and Model Fidelity of DT Models
4.3 Extra-functional Requirements
4.4 DT Evolution
4.5 RE for Dealing with Uncertainty
4.6 Requirements Engineering for AI for DT
4.7 AI for RE for DT
5 State of the Art
6 Conclusion
References
Digital Twins for Organ Preservation Devices
1 Introduction
2 Digital Twins
2.1 Aims and Benefits
2.2 Challenges
2.3 Medical Applications
3 Medical Devices
3.1 Challenges
3.2 Organ Preservation
4 Case Study: ScubaTx™ Organ Preservation Device
4.1 The Device
4.2 The Software
4.3 Challenges
5 Discussion
5.1 Beyond Organ Preservation
References
Using Digital Twins in the Development of Complex Dependable Real-Time Embedded Systems
1 Introduction
2 The DTiL-RTES Framework
2.1 Design Philosophy
2.2 DTiL-RTES Overview and Components
2.3 Intended Use and Overhead
3 ETM Modelling and Refinement
3.1 Execution Time Model
3.2 Offline Profiling of CRP Model
3.3 Prediction Error
3.4 Continuous Refinement Through Naive Feedback
3.5 Model Refinement Through Condition-Based Model Rebuilding
4 Evaluation
4.1 Evaluation Setup
4.2 Modelling and Residual Error Evaluation
4.3 Evaluation of Model Refinement and Performance Improvement
4.4 Discussion on Safety Challenges
5 Related Work
5.1 Timing Prediction for Multi-core Real-Time Embedded Systems
5.2 Execution Time Modelling
6 Conclusion
References
Towards Reactive Planning with Digital Twins and Model-Driven Optimization
1 Introduction
2 Background and Running Example
2.1 Automated Planning and Model-Driven Optimization
2.2 Digital Twins
3 Reactive Planning Framework
3.1 Reactive Planning Architecture
3.2 Reactive Planning Strategies
3.3 Prototypical Implementation
3.4 Demonstration Using the Stack Example
4 Evaluation
4.1 Case Study Setup
4.2 Case Study Results
4.3 Discussion
4.4 Threats to Validity
5 Related Work
6 Conclusion and Future Work
References
Digital Twin Reconfiguration Using Asset Models
1 Introduction
2 Motivating Example
3 Preliminaries
3.1 Knowledge Bases
3.2 Asset Modelling
3.3 Simulation Units
4 Semantically Lifted Co-simulation
5 Structural Reconfiguration in SMOL
6 Conclusion
References
Formally Verified Self-adaptation of an Incubator Digital Twin
1 Introduction
2 Background
2.1 Notation
2.2 Incubator
2.3 Flow* Verified Integration
2.4 Verified Monitoring
3 Formally Verified Self-Adaptation
3.1 Incubator Self-Adaptation Loop
3.2 Verified Monitoring Architecture for Safe Self-Adaptation
3.3 Uncertainty Calibration
3.4 Self-adaptation Monitoring and Enforcement
4 Incubator Self-adaptation Verification Results
4.1 System Setup
4.2 Safety Properties
4.3 Self-adaptation Results
4.4 Repairing the Loop
5 Conclusion
References
Adaptive Data-driven Predictor of Ship Maneuvering Motion Under Varying Ocean Environments
1 Introduction
2 Related Work
2.1 Incremental Learning
2.2 Transfer Learning
3 Methodology
3.1 Gaussian Process Regression
3.2 Predictive Anomaly Detection
4 Experiment Results
4.1 Experiment Setup
4.2 Results Analysis
5 Conclusion
References
Robust Adaptive Back-Stepping Control Approach Using Quadratic Lyapunov Functions for MMC-Based HVDC Digital Twins
1 Introduction
2 System Description of MMC
3 Modeling of the Proposed Adaptive Backstepping Control
3.1 Output Current Control
3.2 Other Controlling Loops
4 Studied HVDC Digital Twin
5 Effectiveness of the Proposed Control Method
6 Conclusion
References
Data-Driven Reachability Analysis of Digital Twin FMI Models
1 Introduction
2 Preliminaries and Problem Statement
2.1 Reachability Analysis and JuliaReach
2.2 Co-simulation and Functional Mock-Up Interface
2.3 Problem Statement
3 Robust Convex Programs
4 Simulation-Based Reachability Algorithm
4.1 Reachable Set Computation
4.2 Lipschitz Constant Estimation via Extreme Value Theorem
4.3 Extension to Other Modelling Formalisms
5 Validation Exercises
5.1 Sampling-Based Lipschitz Constant Estimation
5.2 Reachable Set Computation for Linear Systems
5.3 Reachable Set Computation for a Nonlinear System
6 Conclusions and Future Work
References
Towards Secure Digital Twins
1 Introduction
2 Related Work
3 Security Challenges
3.1 Bandwidth Sniffing
3.2 Data Injection
3.3 Data Delay
3.4 Model Corruption
4 Mitigations
4.1 Fragmentation and Data Padding
4.2 Signatures and Tokens
4.3 Threshold Monitoring and Network-Aware Digital Twin Models
4.4 Model Integrity Checks
5 Case Study
5.1 Physical Twin
5.2 Digital Twin
5.3 Example Security Challenges
6 Open Problems
7 Concluding Remarks
References
Digital Thread in Smart Manufacturing
Digital Thread in Smart Manufacturing
1 Motivation and Goals
2 Overview of Contributions
References
Integrating Wearable and Camera Based Monitoring in the Digital Twin for Safety Assessment in the Industry 4.0 Era
1 Introduction
2 Related Work
3 Architecture Overview
3.1 Wearable Node
3.2 HPE Subsystem
4 Application Scenario
5 Conclusions
References
Model-Driven Engineering in Digital Thread Platforms: A Practical Use Case and Future Challenges
1 Introduction
2 Industrial Use-Case: Safe Operation of Machines
2.1 Architecture of the Use Case
2.2 The IT Ecosystem: Tools and Technologies
3 Access Control Using Attribute Based Encryption
3.1 Bilinear Map
3.2 Decision Tree
3.3 Our Construction
4 Conclusions and Reflections
References
Trust and Security Analyzer for Collaborative Digital Manufacturing Ecosystems
1 Introduction
2 Related Work
3 Architecture of Digital Thread Connector
4 Initial Implementation
5 Conclusion
References
DISTiL: DIStributed Industrial Computing Environment for Trustworthy DigiTaL Workflows: A Design Perspective
1 Introduction
1.1 Motivation
1.2 Impact for Smart Manufacturing
2 DISTiL Design Requirements and Features
3 Architecture Design
3.1 Distributed Data Layer
3.2 Trust-Overlay
3.3 Resource Orchestration andProvisioning
3.4 Use Case Scenario: Collaborative Predictive Maintenance
4 Discussion and Next Steps
References
Using Model Selection and Reduction to Develop an Empirical Model to Predict Energy Consumption of a CNC Machine
1 Introduction
2 Literature Review
3 Methodology
4 Case Study
5 Model Development
5.1 Data Preparation
5.2 Data Analysis
5.3 Data Modelling
6 Discussion
References
Crazy Nodes: Towards Ultimate Flexibility in Ubiquitous Big Data Stream Engineering, Visualisation, and Analytics, in Smart Factories
1 Introduction
1.1 Reconfigurable Manufacturing
1.2 Framework Overview
1.3 Paper Structure
2 Service and Crazy Nodes
2.1 Crazy Nodes
2.2 Towards the Cloud
3 Proof of Concept
4 Conclusions
References
Formal Methods for DIStributed COmputing in Future RAILway Systems
Formal Methods for Distributed Control Systems of Future Railways
1 Motivations and Goals
2 Contributions
References
Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway
1 Introduction
2 Certified Verification of Railway Designs
2.1 Automated Verification
2.2 Trustworthy and Certifiable Verification
2.3 Explainable Verification
2.4 Standardisation
3 Formal Modelling and Analysis for the Railway Domain
3.1 Domain Specific Technology and Usability
3.2 Standardised Reference Architectures
3.3 Digital Railway Innovations
4 Formal Methods for AI
4.1 Guaranteeing Safety Behaviour
4.2 Learning Formal Models of Railway Behaviour
4.3 AI for Monitoring and Maintenance
4.4 AI for Optimisation in Scheduling and Design
5 Conclusion and Further Work
References
Future Train Control Systems: Challenges for Dependability Assessment
1 Introduction
2 Context
2.1 Future Railway Systems
2.2 Uncertainty
2.3 Dependability Attributes
3 Model-Based Evaluation of Dependability
3.1 Proposed Modelling Frameworks
4 Survey of Railway Case Studies
4.1 Performability Evaluation of the ERTMS/ETCS - Level 3
4.2 Safety Evaluation of Moving Block Systems by Statistical Model Checking
4.3 Train-to-Train Communication Modeling
4.4 Modelling Uncertainty in Satellite Localisation
4.5 Safety and Availability of Virtual Balises: The SISTER Project
4.6 Virtual Coupling: Performability Evaluation
4.7 Reliability and Maintenance Plans
4.8 Summary
5 Conclusions
References
Standardisation Considerations for Autonomous Train Control
1 Introduction
2 Standardisation and Certification
3 Technology
4 A Reference Architecture for Autonomous Train Controllers
5 A Sample Evaluation According to ANSI/UL 4600
6 Conclusion
References
Automatic Generation of Domain-Aware Control Plane Logic for Software Defined Railway Communication Networks
1 Introduction
2 The European Rail Traffic Management System
3 Software-Defined Communication Networks for Railways
4 Automatic Synthesis of Control Plane Logic
5 SDN Control Logic Supported by Formal Models
6 Current Implementation
7 Conclusions and Future Directions
References
Safe and Secure Architecture Using Diverse Formal Methods
1 Introduction
2 Terminology
3 Ensuring Safety
4 The CLEARSY Safety Platform
5 Cybersecurity Requirements
6 Resulting Architecture
6.1 Introduction
6.2 Original Architecture
6.3 Rationale
6.4 Assessment
7 Conclusion and Perspectives
References
Industrial Day
Formal Methods for a Digital Industry
1 Introduction
2 Contributions
2.1 Software-Enabled Business Engineering.
2.2 Building Eco-Systems
2.3 Domain-Specific Languages for the Industry 4.0
References
Domain-Specificity as Enabler for Global Organization aLignment and Decision
1 Introduction
2 Today's Approaches
2.1 Business Modeling Support as Boundary Objects
2.2 Business Modeling Support: A Research Agenda
2.3 The Gap of Today's Solutions and Research Agenda
2.4 Towards Holistic Business Modeling
3 The GOLD Framework and Tool
3.1 Tailored Modeling Environment
3.2 Model Types and Customization
3.3 Consistent Interlinking
3.4 Component Taxonomies
3.5 Model Validation and Modeling Guidance
3.6 Aggregation and Views
3.7 Collaboration
4 Exemplary Application of the GOLD Framework
5 Conclusion and Outlook
References
Evolving Data Space Technologies: Lessons Learned from an IDS Connector Reference Implementation
1 Introduction
2 Background
3 Approach
3.1 Architecture
3.2 Integration
4 Evaluation
5 Lessons Learned
5.1 Expectations
5.2 Observations
6 Related Work
7 Conclusion
References
Towards a Methodology for Formally Analyzing Federated Identity Management Systems
1 Introduction
1.1 Related Work
2 Preliminaries
2.1 Federated Identity Management Systems
2.2 Specification Languages
3 Proposed Frameworks
3.1 Specifying FIM Systems Using Rewriting Logic
3.2 Specifying FIM Systems Using TLA
4 Case Study: eIDAS LEPS API Connector
4.1 System Description
4.2 Formal Analysis Using Maude
4.3 Formal Analysis Using TLA+
5 Discussion
6 Conclusion and Future Work
A ANNEX
A.1 Maude: Basic Syntax and Notation
A.2 TLA+: Basic Syntax and Notation
References
Model-Driven Edge Analytics: Practical Use Cases in Smart Manufacturing
1 Introduction
2 Related Work
2.1 Literature Review
2.2 Own Previous Work
3 Methodology
3.1 The Integration Process
3.2 Architectural Components in EdgeX
3.3 Architectural Components in FiWARE
3.4 Computing on the Edge and Data Analytics
3.5 Towards Model-Driven Edge Analytics with IoT Agents and eKuiper
4 Results and Discussion
4.1 EdgeX and eKuiper Integrations
4.2 FiWARE and IoT Agent Integrations
5 Conclusion
References
Author Index