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

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