Leveraging applications of formal methods, verification and validation, adaptation and learning. Practice : 11th international symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings, Part IV / / Tiziana Margaria-Steffen, Bernhard Steffen, editors

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (431 pages)
• Disciplina: 005.14
• Soggetto topico: Computer software - Verification; Formal methods (Computer science)
• Persona (resp. second.): MargariaTiziana; SteffenBernhard
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- 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.
• Titolo autorizzato: Leveraging applications of formal methods, verification and validation, adaptation and learning. Practice
• ISBN: 3-031-19762-3
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910619277403321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science ; ; 13704.