Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles: 11th International Symposium, ISoLA 2022 Rhodes, Greece, October 22–30, 2022 Proceedings, Part I

Introduction
Organization
Contents – Part I
SpecifyThis - Bridging Gaps Between Program Specification Paradigms
SpecifyThis – Bridging Gaps Between Program Specification Paradigms
	1 Introduction
	2 Summary of Contributions
	References
Deductive Verification Based Abstraction for Software Model Checking
	1 Introduction
	2 Overview of the Verification Approach
	3 Deductive Verification and Frama-C
	4 Model Checking and TLA
		4.1 The TLA Framework
		4.2 Translating Code and Contracts into TLA
	5 Contracts as a Unifying Theory
		5.1 An Abstract Contract Theory
		5.2 Deductive Verification in the Abstract Contract Theory
		5.3 Procedure-Modular Verification with TLA
		5.4 Contract Based System Design
	6 Preliminary Evaluation
		6.1 Simple File Open-Close Example
		6.2 Simplified Industrial Example
	7 Conclusion
	References
Abstraction in Deductive Verification: Model Fields and Model Methods
	1 Introduction
	2 Logical Encoding of Local Computations
	3 Encoding Heap Access and Update—Previous and Related Work
		3.1 Notation
		3.2 Heaps as Maps
		3.3 Arrays
		3.4 Embedding in SMT
	4 Model Fields and Model Methods
	5 Simple Example
	6 Using Model Methods
	7 Encoding Model Methods
	8 Contrast and Conclusion
	References
A Hoare Logic with Regular Behavioral Specifications
	1 Introduction
	2 Motivation
	3 Approach
		3.1 Preliminaries and Notation
		3.2 Regular Behavioral Specifications
		3.3 Programs and Behavioral Correctness
		3.4 Hoare Logic Proof Rules
	4 Tool Support in SecC
		4.1 Specification Syntax
		4.2 Verification Engine
	5 Case Studies
		5.1 Case Study: Regular Expression Matching
		5.2 Case-Study: VerifyThis Casino Challenge
		5.3 Discussion
	6 Related and Alternative Approaches
	7 Conclusion
	References
Specification-Based Monitoring in C++
	1 Introduction
	2 Related Work
	3 Overview
	4 The Specification Language
		4.1 Events
		4.2 A Simple State Machine
		4.3 Some Alternative Monitors
		4.4 Monitoring Events that Carry Data
		4.5 Referring to the Past
		4.6 A Complex Property
		4.7 The Complete Grammar
	5 Usage
	6 Implementation
	7 Experiment
		7.1 Setting Up the Experiment
		7.2 Result and Interpretation
	8 Conclusion
	A  Visualization of Monitors
	References
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
	1 Introduction
	2 Specifying Termination Detection
	3 Verification by Model Checking and Theorem Proving
		3.1 Finite-State Model Checking Using tlc
		3.2 Bounded Model Checking with Apalache
		3.3 Theorem Proving Using tlaps
	4 Safra\'s Algorithm for Termination Detection
	5 Analyzing Safra\'s Algorithm
		5.1 Model Checking Correctness Properties
		5.2 Safra\'s Algorithm Implements Termination Detection
		5.3 Proving Correctness Using tlaps
	6 Conclusion
	References
Selective Presumed Benevolence in Multi-party System Verification
	1 Introduction
	2 Smart Contracts, Solidity and Reentrancy
	3 Semantics of Solidity and Handling of Callbacks
	4 Presumption of Benevolence
		4.1 Presuming Benevolence of Oneself
		4.2 Presuming Benevolence of a Static Group
		4.3 Presuming Benevolence of a Dynamic Group
	5 Collaborative Malicious Behaviour
	6 Conclusions
	References
On the Pragmatics of Moving from System Models to Program Contracts
	1 Introduction
	2 The PGP Server Hagrid
	3 The Alloy Model
	4 From Alloy to VCC Contracts
		4.1 Precondition and Framing Analysis
		4.2 Translation to Annotated C
		4.3 Contract Augmentation
	5 Discussion
	References
X-by-Construction Meets Runtime Verification
X-by-Construction Meets Runtime Verification
	1 Motivation
	2 Aim
	3 Contributions
		3.1 CbC: Robustness, Co-piloting, and Digital Twinning
		3.2 CbC and RV: Configurable and Cyber-Physical Systems
		3.3 XbC: Security, Resilience, and Consumption Properties
		3.4 CbC and RV: Reinforcement Learning and Synthesis
	References
Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime
	1 Introduction
	2 Preliminaries
	3 Adaptive Strategies
		3.1 Definitions
		3.2 Computing Adaptive Strategies
	4 Strongly Adaptive Strategies
		4.1 Bad Moves
		4.2 Motivating Example
		4.3 Definitions
		4.4 Existence of Strongly Adaptive Strategies
		4.5 Computing Strongly Adaptive Strategies
	5 Conclusion
	References
TriCo—Triple Co-piloting of Implementation, Specification and Tests
	1 Introduction
		1.1 Triple Co-piloting at a Glance
	2 Emerging Trends in Software Technology
		2.1 Code Synthesis Through Large Language Models
		2.2 Automated Test Case Generation
		2.3 Specification Synthesis
		2.4 Formal Software Verification
	3 The TriCo Methodology
		3.1 Envisaged Workflow
		3.2 Use Cases
		3.3 Envisaged Technology
	4 Research Efforts Required for TriCo
	5 Turning Vision into Reality
	References
Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins
	1 Introduction
	2 Twinned-by-Construction Systems
	3 Twinning-by-Construction and Temporal Properties
	4 The Digital Thread as a Temporal Property
	5 Related Work
	6 Conclusion
	References
On Formal Choreographic Modelling: A Case Study in EU Business Processes
	1 Introduction
	2 Background
	3 Legal Provisions
	4 Formal Models
	5 From BPMN to Global Choreographies
	6 Conclusions and Future Work
	References
Configurable-by-Construction Runtime Monitoring
	1 Introduction
	2 The Quest of Configurable Runtime Monitoring
		2.1 Feature-Oriented Example
		2.2 Challenges
		2.3 This Paper
	3 Configurable Automata-Based Monitoring
		3.1 Preliminaries
		3.2 Featured Monitors
		3.3 Synthesizing Featured Monitors
		3.4 Concise Featured Monitors
	4 Configurable Stream-Based Monitoring
		4.1 Preliminaries
		4.2 Configurable Lola
		4.3 Family-Based Specification Analysis
	5 Concluding Remarks
	References
Runtime Verification of Correct-by-Construction Driving Maneuvers
	1 Introduction
	2 Workflow by Example
	3 Modeling and Verifying Maneuvers with Hybrid Mode Automata
		3.1 Formalization of Hybrid Mode Automata
		3.2 Verification Based on Differential Dynamic Logic
	4 Runtime Verification of HMA Models
		4.1 Generating Monitor Conditions for Runtime Verification
		4.2 Simulation
	5 Evaluation
		5.1 Case Studies and Setup
		5.2 Results and Insights
	6 Related Work
	7 Conclusion
	References
Leveraging System Dynamics in Runtime Verification of Cyber-Physical Systems
	1 Introduction
	2 Preliminary Concepts
		2.1 Signal Model
		2.2 Signal Temporal Logic (STL) ch16mn04
	3 Exploiting Knowledge of System Dynamics
		3.1 Motivating Example
		3.2 System Model
		3.3 Knowledge of Signal Dynamics
		3.4 Using Partial Knowledge
	4 Monitoring Distributed CPS
		4.1 Distributed CPS Architecture
		4.2 Additional Challenges in the Distributed Setup
	5 Using Verified Dynamics
	6 Conclusion
	References
Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept
	1 Introduction
	2 Background and Related Work
		2.1 Essentials of Statistical Model Checking
		2.2 Trace Execution Properties
		2.3 Probabilistic Verification
		2.4 SMC Tools
	3 Illustrative Example
		3.1 SMC-Based Validation
		3.2 Using Traces for Automated Program Repair
	4 Designing a Repair Agent
		4.1 A SMC-Based Program Repair Algorithm
	5 Implementation and Experimental Results
		5.1 Experimental Results
	6 Conclusions and Future Work
	References
Towards Safe and Resilient Hybrid Systems in the Presence of Learning and Uncertainty
	1 Introduction
	2 Background
		2.1 Reinforcement Learning (RL)
		2.2 Simulink and the RL Toolbox
		2.3 Differential Dynamic Logic
		2.4 Transformation from Simulink to dL
		2.5 Stochastic Hybrid Model
		2.6 Signal Temporal Logic
		2.7 Learning Optimal Decisions for Stochastic Hybrid Systems
	3 Related Work
	4 Combining Deductive and Quantitative Analyses
		4.1 An Intelligent Water Distribution System
		4.2 Formal Verification of Safety and Resilience
		4.3 Resilient Scheduling Under Uncertainty
	5 Evaluation
		5.1 Deductive Verification
		5.2 Quantitative Analysis
	6 Conclusion
	References
Non-functional Testing of Runtime Enforcers in Android
	1 Introduction
	2 Background
		2.1 Runtime Policy
		2.2 Policy Enforcement Models
	3 Test4Enforcers
		3.1 Test Case Generation
		3.2 Test Execution
	4 Evaluation
	5 Related Work
	6 Conclusion and Future Work
	References
Automata Learning Meets Shielding
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 Markov Decision Processes and Reinforcement Learning
		3.2 Learning of MDPs
		3.3 Shielding in MDPs
	4 Learned Shields for Safe RL
		4.1 Setting and Problem Statement
		4.2 Overview of Iterative Safe RL via Learned Shields
		4.3 Details for Training Using Learned Shields
	5 Experiments
		5.1 Case Study Subjects
		5.2 Experimental Results
		5.3 Zigzag Gridworlds
		5.4 Slippery Shortcuts Gridworlds
		5.5 Wall Gridworlds
		5.6 Discussion
	6 Conclusion
	References
Safe Policy Improvement in Constrained Markov Decision Processes
	1 Introduction
	2 Motivating Example
	3 Related Work
	4 Preliminaries
		4.1 Reinforcement Learning
		4.2 Hierarchical Task Specifications
	5 Contribution
		5.1 Problem Formulation
		5.2 Reward Shaping
		5.3 Safe Policy Improvement in Online Setting
	6 Experiments
		6.1 Automatic Reward Shaping from Task Specification
		6.2 Safe Policy Improvement in Online Setting
	7 Conclusion and Future Work
	References
Runtime Verification Meets Controller Synthesis
	1 Introduction
	2 Background
		2.1 Runtime Verification
		2.2 Reactive Synthesis
	3 Monitoring for Guarantees
	4 Monitoring for Assumptions
	5 Monitors as Orchestrators in Contextual Missions
	6 Other Potential Combinations
	7 Related Work
	8 Conclusions
	References
Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification
	1 Introduction
	2 The Stream Runtime Verification Language Lola
		2.1 Lola Syntax and Semantics
	3 Implicit Assumptions and Silent Mission Failures
		3.1 Handling Assumption Violations
	4 Empirical Evaluation
	5 Conclusion
	References
Verification and Validation of Concurrent and Distributed Heterogeneous Systems
Verification and Validation of Concurrent and Distributed Heterogeneous Systems (Track Summary)
	1 Motivation and Goals
	2 Overview of Contributions
	References
A Thread-Safe Term Library
	1 Introduction
	2 The Term Data Structure
		2.1 The External Behaviour of the Term Library
		2.2 Behavioural Properties of the Term Library
		2.3 The Implementation of the Thread-Safe Term Library
	3 The Busy-Forbidden Protocol
		3.1 The External Behaviour of the Busy-Forbidden Protocol
		3.2 The Implementation of the Busy-Forbidden Protocol
		3.3 Behavioural Properties of the Busy-Forbidden Protocol
		3.4 Existing Readers-Writer Locks
		3.5 Performance of the Busy-Forbidden Protocol
	4 Modelling and Verifying the Algorithms
	5 Performance Evaluation
	A The mCRL2 Language and Modal Formulas
	B mCRL2 Specifications for the Busy-Forbidden Protocol
	C mCRL2 Specifications for the Term Library
	D Benchmark Data
	References
ST4MP: A Blueprint of Multiparty Session Typing for Multilingual Programming
	1 Introduction
	2 MPST Theory in a Nutshell
		2.1 Global Types
		2.2 Local Types and Projection
		2.3 Processes and Typing Rules
	3 Blueprint of ST4MP
		3.1 UI
		3.2 Parser
		3.3 Local Type Generator
		3.4 Interpreter
		3.5 API Generator
	4 Related Work
	5 Conclusion
	References
On Binding in the Spatial Logics for Closure Spaces
	1 Introduction
	2 Preliminaries
		2.1 SLCS: The Spatial Logic for Closure Spaces
		2.2 SLCS: The Temporal Extension of SLCS
	3 xSLCS: Point Existential Extension of SLCS
	4 xSLCS: Point Existential Temporal Extension of SLCS
	5 xSLCS: Dealing with Fresh Point Names
	6 pSLCS: Predicate Existential Extension of SLCS
	7 Conclusions and Future Work
	References
An Efficient VCGen-Based Modular Verification of Relational Properties
	1 Introduction
	2 Syntax and Semantics of the Considered Language L
		2.1 Locations, States, and Procedure Contracts
		2.2 Syntax for Expressions and Commands
		2.3 Operational Semantics
	3 Functional Correctness
	4 Relational Functional Correctness
	5 Optimized Verification Condition Generator
		5.1 Verification Condition Generator
		5.2 Hoare Triple Verification
	6 Modular Verification of Relational Properties
	7 Related Work
	8 Conclusion
	References
On Deductive Verification of an Industrial Concurrent Software Component with VerCors
	1 Introduction
	2 Background
		2.1 Tunnel System Architecture
		2.2 VerCors
	3 Verification of the Concurrent Data Manager Module
		3.1 Event Loop Analysis
		3.2 Discussion on the Discovered Bugs
	4 Results Presentation
		4.1 Presentation Design Process
		4.2 Presentation Conclusions
	5 Future Research
	6 Conclusion
	References
Exploring a Parallel SCC Algorithm
	1 Introduction
	2 Preliminaries
		2.1 A Parallel SCC Algorithm Based on Concurrent Union-Find
		2.2 TLA+ and TLC
	3 Modeling and Analysis Process
		3.1 Initial Specification – Good for Simulation
		3.2 Improved Specification – Good for Model Checking
		3.3 Specifying the Correctness Property and Other Assertions
	4 Findings from Model Checking Experiments
		4.1 Simplifying the Equivalence Check (SameSet)
		4.2 Monotonicity of Worker Sets and Atomic Updates
		4.3 Duplication on the Stack
		4.4 Changing the Order of Updates During Unite
	5 Conclusion
	A The Original Concurrent Union-Find SCC Algorithm
	B Example Input Graphs for SCC Algorithm
	References
An IoT Digital Twin for Cyber-Security Defence Based on Runtime Verification
	1 Introduction
	2 Related Work
	3 Digital Twin and Application-Agnostic Security Modules for IoT Communication
		3.1 IoTsafe Security Architecture
		3.2 Transparent Secure Communication with Security Decoupling
		3.3 Monitoring Testbed
	4 Digital Twin for Runtime Verification of IoT Device Communications
		4.1 Formal Definition of the Runtime Verification Problem
		4.2 Runtime Verification for the Monitoring Testbed
	5 Conclusions and Future Work
	References
A Formal Model of Metacontrol in Maude
	1 Introduction
	2 Background
		2.1 Metacontrol
		2.2 Maude
	3 The Smart House Use Case
		3.1 The Controller Layer
	4 The Metacontrol Layer for the Smart House Use Case
		4.1 The TOMASys Metamodel
		4.2 Metacontrol Operation
	5 Modelling the Smart House Use Case in Maude
		5.1 Model Dynamics
		5.2 The Smart House Model
		5.3 The Controller Layer
		5.4 The Metacontrol Layer
	6 Evaluating the Executable Model of the Smart House
	7 Related Work
	8 Conclusion and Future Work
	References
Author Index