Leveraging Applications of Formal Methods, Verification and Validation. Application Areas: 12th International Symposium, ISoLA 2024, Proceedings, Part V 5

The ISoLA 2024 proceedings constitutes contributions of the associated events held at the 12th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2024, which took place in Crete, Greece, in October 2024. ISoLA 2024 provides a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools and methods for the specification, analysis, verification, certification, construction, test, and maintenance of systems from the point of view of their different application domains. Preface Organization Contents – Part V Digital Twin Engineering Digital Twin Engineering 1 Introduction 2 Contributions 3 Concluding Remarks References Foundation Models for the Digital Twins Creation of Cyber-Physical Systems 1 Introduction 2 Background 2.1 Foundation Models 2.2 Example Case: Autonomous Driving Systems (ADSs) 3 Overview: Application Contexts of Foundation Models for CPS Digital Twins 4 Case 1: Foundation Models to Generate Digital Twins 4.1 State of the Art 4.2 Solution Proposal 4.3 Challenges and Opportunities 4.4 Example Case of ADS 5 Case 2: Fine-Tuned Foundation Model as Digital Twin 5.1 State of the Art 5.2 Solution Proposal 5.3 Challenges and Opportunities 5.4 Example Case of ADS 6 Discussions 6.1 Uncertainty of Foundation Models 6.2 Cost and Effectiveness of Using Foundation Models 6.3 Lightweight Foundation Models for Digital Twins 6.4 Challenges in Generating Digital Twins with Foundation Models 7 Conclusion References Interoperability of Digital Twins: Challenges, Success Factors, and Future Research Directions 1 Introduction 2 Strategic View: Multiplicities of Digital Twins (Dawn Tilbury) 3 Technical View: Co-simulation for Interoperability (Claudio Gomes) 4 Standardization: A Key Enabler (Guodong Shao) 5 Organizational View: The Role of Data (Bassam Zarkout) 6 Discussion 6.1 Towards Higher Level of Interoperability 6.2 Challenges 6.3 Success Factors 6.4 Future Research Directions 7 Conclusion References Monitoring Reconfigurable Simulation Scenarios in Co-simulated Digital Twins 1 Introduction 2 State-of-the-Art and Preliminaries 2.1 State-of-the-Art in Runtime Verification of Simulation Units 2.2 Preliminaries: Functional Mock-Up Interface 2.3 Preliminaries: FMI-Based Co-simulation Semantics 2.4 Preliminaries: Consistent Traces with Reconfiguration 3 Runtime Verification of Co-simulations 3.1 The UPPAAL Model 3.2 (Online) Monitoring a Co-simulation 4 Online Monitoring 5 Evaluation 6 Conclusion References DiTEC: Digital Twin for Evolutionary Changes in Water Distribution Networks 1 Introduction 2 Related Work 3 Digital Twin System Architecture 4 System Model 4.1 Data Preparation 4.2 Learning and Reasoning 4.3 Decision Making 5 Validation: WDN Digital Twin in Oosterbeek 5.1 Oosterbeek's WDN Description 5.2 Data Preparation 5.3 Learning and Reasoning 5.4 Decision Making 6 Discussion 7 Conclusions References Small Scale, Big Impact: Experiences from a Miniature ViL Testbed and Digital Twin Development 1 Introduction 2 Requirements and System Selection 3 Related Work 4 Concept of the Setup's Functional Architecture 5 Technical Implementation Physical System 6 Technical Implementation Digital Shadow 7 Application 8 Experiments and Evaluation 9 Learnings 9.1 Understand the System 9.2 Highly Automated Twinning Is Key for Automation and DTs Should Be Designed as Such 9.3 Communicating What a DT Is, Is Still Complicated 9.4 Benefit of in-Sourcing the Experimental Setup 9.5 Dissemination Enabler 10 Conclusion References DisCoRail 2024 Formal Methods for Distributed Computing in Future Railway Systems 1 Introduction 2 Contributions References Model-Based Testing of Railway Interlocking Systems 1 Introduction 2 Context and Motivations 3 Methodology Overview 3.1 The Testing Approach 3.2 The TOSCA Platform 4 Modelling Test Cases 4.1 TOSCA Test Case Types 4.2 TOSCA Test Statements 4.3 Instantiation of Abstract Test Cases 5 Test Case Execution 6 Test Case Generation 7 Evaluation 7.1 TOSCA Usage by Domain Experts 7.2 TOSCA Automated Test Generation 8 Related Works 9 Conclusions References Formal Verification of Railway Interlockings: a Compositional Approach Based on a Library of Pre-verified Components 1 Introduction 2 Interlocking Systems 3 Formal Verification by Model Checking 4 Compositional Verification 4.1 The RobustRailS Compositional Method 4.2 The Louvain Compositional Method 5 Re-use Strategies for Compositional Verification 5.1 A Re-use Strategy for RobustRailS 5.2 A Re-use Strategy for Louvain 5.3 Experiments 5.4 Comparison 6 Conclusions References Formal Validation and ERTMS Simulation 1 Introduction 2 ERTMS In A Nutshell 2.1 Structure and Concepts 2.2 Support 2.3 Conformance to ERTMS 3 Application of Formal Methods 4 Formal Proof of System Level Specification 4.1 Rationale 4.2 Application to ERTMS 4.3 Formal Data Validation 5 Conclusion and Perspectives References Securing Automatic Small Railway Vehicles Using Automatic Train Protection 1 Introduction 2 Small Sized Guided Transport System: Ferromobile Project 3 Model-Based Approach 4 Illustration on a Railway Use Case 4.1 The Safety Case Context 4.2 Specification of a Particular Goal 5 Conclusion References Railway Switch Control Modeling in European Train Control System Level 3 1 Introduction 2 Background 2.1 ETCS-L3 and Switch Control 2.2 Stochastic Activity Networks 2.3 Event-B Modeling 3 Switch Control in SysML 4 Switch Control in SAN 4.1 Objective of the Model 4.2 The Model at a Glance 4.3 Results 5 Switch Control in Event-B 5.1 Objective of the Model 5.2 The Model at a Glance 5.3 Results 6 Conclusions and Future Work References An Integrated Perspective on the Evaluation of Complex Railway Systems 1 Introduction 2 Background and Context 2.1 Distributed Interlocking and Standard Interfaces 2.2 Railroad Switch Heaters 3 Qualitative and Quantitative Evaluation Techniques 3.1 Contract Automata 3.2 Quantitative Modeling and Evaluation Techniques 4 Project Outlook 4.1 Qualitative Methods 4.2 Quantitative Methods 4.3 Path to Integration 5 Conclusion References Author Index