Leveraging Applications of Formal Methods, Verification and Validation: Software Engineering Methodologies: 12th International Symposium, ISoLA 2024, October 27–31, 2024, Proceedings, Part IV

Preface
Organization
Contents – Part IV
Invited Paper
QuAK: Quantitative Automata Kit
	1 Introduction
	2 Quantitative Properties and Automata
		2.1 Basic Decision Problems of Quantitative Automata
		2.2 Safety and Liveness of Quantitative Automata
	3 The Tool
	4 Experimental Evaluation
		4.1 Comparing Inclusion Algorithms
		4.2 Evaluating Constant-Function Checking
		4.3 Runtime Monitoring
	5 Conclusion
	References
Automating Software Re-engineering
Automating Software Re-Engineering Introduction to the ISoLA 2024 Track
	1 Motivation
	2 The Track
	3 The Contributions
		3.1 Digital Twins
		3.2 Maintainable Tests
		3.3 Trusted Distribution
	4 Conclusion
	References
On Using Large Language Models Pre-trained on Digital Twins as Oracles to Foster the Use of Formal Methods in Practice
	1 Introduction
	2 LLMs for Formal Methods
		2.1 LLMs in Theorem Proving
		2.2 LLM for Property Formalization
		2.3 LLM in Program Verification
		2.4 LLMs in Program Synthesis
	3 Digital Twins
	4 Fostering Further Practical Use of Formal Methods
		4.1 Requirements Elicitation
		4.2 Formal Specification
		4.3 Software/Program Synthesis
		4.4 Continuous Monitoring
	5 Discussion
	References
Cloud Continuum Digital Twins: Architectures of Solution, Open Technical Challenges, and Lessons Learned
	1 Introduction
	2 Cloud Continuum Digital Twins
		2.1 Integration Strategies for Cloud Continuum DTs
	3 Real-Time Digital Twins
		3.1 Virtualized Workloads and QoS Management
		3.2 Network Acceleration Technologies
	4 The INSANE Middleware for Low Latency Data Distribution
		4.1 Data Distribution and QoS Policies in INSANE
		4.2 The INSANE Runtime and Application Interface
		4.3 INSANE Performance Evaluation: Some In-the-Field Experimentation Insights
	5 Conclusive Remarks and Primary Directions of Future Work
	References
(Re-)Engineering Digital Twins Towards Federation: Vision and Roadmap
	1 Introduction
	2 Background and State of the Art
	3 Classifying Digital Twins Federation
		3.1 Based on Architecture Patterns
		3.2 Based on System Characteristics
		3.3 Based on Functional Aspects
	4 Modelling and Engineering Federated Digital Twins
		4.1 Architecture Example
		4.2 Abstract Model Instance
		4.3 (Re)-Engineering DTF
	5 Roadmap for Digital Twins Federation
		5.1 Enabling Technologies
		5.2 Current Challenges and Barriers
		5.3 Next Steps and Outlook
	6 Conclusion
	References
Threats to Instrument Validity Within ``in Silico\'\' Research: Software Engineering to the Rescue
	1 Introduction
	2 Instrument Validity Within ``In Silico\'\' Research
		2.1 Defining ``In Silico\'\' Research
		2.2 Illustrative Examples of ``In Silico\'\' Research
		2.3 Threats to Instrument Validity
	3 Software Engineering Within ``In Silico\'\' Research
		3.1 Software Engineering Best Practices
		3.2 Software Engineering Missed Opportunities
	4 Remediation of Threats to Validity in ``In Silico\'\' Research
		4.1 Smoke Tests and Regression Tests
		4.2 Clone Genealogies
		4.3 Static and Dynamic Code Analysis
	5 Conclusion
	References
Automated Clone Elimination in Python Tests
	1 Introduction
	2 Design
	3 Evaluation
		3.1 Picking Code Repositories
		3.2 Metric Selection
		3.3 Evaluation
		3.4 Discussion
		3.5 Threats to Validity
	4 Conclusion
		4.1 Related Work
		4.2 Future Work
	References
Towards Automated Security Hardening Using Timed Path Conditions in Shared Bus Systems
	1 Introduction
	2 Background
		2.1 Information Flow Analysis
		2.2 Path Conditions
		2.3 SystemC
	3 Related Work
	4 Motivating Example
	5 Timed Path Conditions for Automated Security Hardening
		5.1 Timed System Dependence Graph
		5.2 Timed Path Conditions
		5.3 Vulnerability Detection and Analysis
		5.4 Automated Security Hardening
	6 Conclusion
	References
Towards a More Sustainable Re-engineering of Heterogeneous Distributed Systems Using Cooperating Run-Time Monitors
	1 Introduction
	2 Approach and Application Scenario
		2.1 The MBRE Method: Monitor-Based Re-Engineering
		2.2 The Application Scenario
	3 Re-Engineering Case Studies
		3.1 Preventing Avoidable Delays of High-Priority Tasks
		3.2 Eliminating Unnecessary Interferences Between Tasks
		3.3 Progressing High-Priority Tasks Despite Collisions
	4 Implementation and First Performance Evaluations
		4.1 A Test-Bed for the Hospital Scenario
		4.2 Two Monitor Implementations
		4.3 Performance Evaluation and Comparison
	5 Related Work
	6 Conclusion
	References
X-By-Construction Meet AI
X-by-Construction Meets AI
	1 Motivation
	2 Aim
	3 Contributions
	References
Intersymbolic AI
	1 Introduction
	2 Symbolic AI
	3 Subsymbolic AI
	4 Intersymbolic AI
	5 A Case for Intersymbolic AI in Cyber-Physical Systems
	6 Some Successful Intersymbolic AI Combinations
	7 Conclusions and Outlook
	References
Logic-Based Explainability: Past, Present and Future
	1 Introduction
	2 Preliminaries
	3 The Recent Past: Shaping Logic-Based Explainability
		3.1 Defining Logic-Based Explanations
		3.2 Complexity of Computing Explanations
	4 The Present: Expanding Logic-Based Explainability
		4.1 Explainability Queries
		4.2 Explanation Size
		4.3 Expressivity of Explanations
		4.4 Additional Topics and Applications
	5 By-Products: Misconceptions in XAI & ML
		5.1 The Misconception of Interpretability
		5.2 The Misconception of Model-Agnostic Explainability
		5.3 Misconceptions in XAI by Feature Attribution
		5.4 The Misconception of (Global) Adversarial Robustness
	6 A Glimpse of the Future
		6.1 Explaining Large-Scale ML Models
		6.2 From Feature Selection to Feature Attribution
		6.3 Certified Explainability
		6.4 Additional Topics
	7 Conclusions
	References
Towards Hybrid-AI in Imaging Using VoxLogicA
	1 Introduction
	2 Background
	3 A Microservice Architecture for Hybrid AI
		3.1 Microservices: Motivations
		3.2 System Design
		3.3 Four Fundamental Services
	4 Example
	5 Discussion
	References
Towards AI-Assisted Correctness-by-Construction Software Development
	1 Introduction
	2 Background
	3 Correctness-by-Construction Engineering in CorC
	4 AI-Assistance for Correctness-by-Construction
		4.1 General Process
		4.2 Specification Generation
		4.3 Code Generation
		4.4 Deductive Verification
		4.5 Interpretation
	5 Conclusion
	References
Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification
	1 Introduction
	2 Use Cases for Automated Specification Annotation
		2.1 Generating Requirement Specification
		2.2 Generating Auxiliary Specifications
		2.3 Conversational Co-Development of Specification and Code
	3 A Prototype for Verified Annotation Generation
	4 Experiments
		4.1 Experimental Results
		4.2 Correcting Generated Specifications with Traces
	5 Vision and Research Plan
	References
Traceability and Accountability by Construction
	1 Introduction
	2 Example: University Admission
		2.1 An Ideal Process
		2.2 Requirements
	3 The DBOM Approach
		3.1 Predicates and Assertions
		3.2 Cryptographic Signatures
		3.3 Signature Verification
		3.4 DBOM Encoding
		3.5 Exploiting Existing Techniques
	4 Reasoning About DBOMs
		4.1 Rules
		4.2 Reasoning Example
		4.3 Rules Encoding
	5 Conclusion and future work
	References
Synthesis from Infinite-State Generalized Reactivity(1) Specifications
	1 Introduction
	2 Related Work
	3 Synthesis Method
		3.1 Problem Definition
		3.2 Game Solving
		3.3 Enforceable Predecessor
	4 Strategy Extraction
		4.1 Simple Strategy
		4.2 Eager Strategy
		4.3 Simplifying Strategies
	5 Evaluation
		5.1 Benchmarks
		5.2 Game Solving
		5.3 Strategy Extraction
	6 Conclusion
	A Experimental Results
	References
On Threat Model Repair
	1 Introduction
	2 System and Threat Models
	3 Threat Model Analysis and Repair
		3.1 Threat Analysis
		3.2 Threat Repair
		3.3 Full System Repair
	4 Conclusions
	References
Towards Formal Design of FDIR Components with AI
	1 Introduction
	2 AI for FDIR
	3 Integrative AI
	4 Workflow
		4.1 Requirements Specification
		4.2 Architectural Modeling
		4.3 Modeling of HW Components
		4.4 Fault Injection
		4.5 Modeling of SW Components
		4.6 Modeling of ML-Based Components
		4.7 Training of ML Models
		4.8 Verification and Validation
		4.9 Deployment
	5 Conclusions and Future Work
	References
Author Index