Runtime verification : 21st international conference, RV 2021, virtual event, October 11-14, 2021 : proceedings

Preface
Organization
Contents
Regular Papers
Predicate Monitoring in Distributed Cyber-Physical Systems
	1 Introduction
		1.1 Our Solution and Contributions
	2 Model of Computation
		2.1 Signal Model
		2.2 Signal Transmission to the Monitor
	3 The Predicate Monitoring Problem
	4 SMT-Based Monitoring Algorithm
		4.1 Retiming Functions
		4.2 SMT Formulation
	5 Exploiting the Knowledge of System Dynamics
	6 Case Studies and Evaluation
		6.1 Case Studies
		6.2 Experimental Setup
		6.3 Analysis of Results
	7 Related Work
	8 Conclusion
	References
Specifying Properties over Inter-procedural, Source Code Level Behaviour of Programs
	1 Introduction
	2 Background: Control-Flow Temporal Logic
		2.1 Symbolic Control-Flow Graphs
		2.2 Dynamic Runs
		2.3 Examples of CFTL Specifications
	3 iCFTL: Inter-procedural CFTL
		3.1 Systems of Multiple Procedures
		3.2 Inter-procedural Dynamic Runs
		3.3 Syntax of iCFTL
		3.4 Examples
	4 A Semantics for iCFTL
		4.1 Finding Bindings
		4.2 Evaluation at a Binding
		4.3 The Semantics Function
	5 Monitoring
	6 Instrumentation
		6.1 Inspection of the Quantifiers
		6.2 Inspection of the Atoms
		6.3 Filtering Dynamic Runs
		6.4 Lookup During Monitoring
		6.5 Implications for Complexity
	7 Case Study
	8 Related Work
	9 Conclusion
	References
Into the Unknown: Active Monitoring of Neural Networks
	1 Introduction
	2 Related Work
	3 Background and Assumptions
	4 Approach
		4.1 Quantitative Monitor
		4.2 Active Monitoring Algorithm
	5 Experiments
		5.1 Benchmark Datasets
		5.2 Experimental Setup
		5.3 Experimental Results
	6 Conclusion and Future Work
	References
Monitoring with Verified Guarantees
	1 Introduction
	2 Runtime Monitoring with Lola
	3 Assumptions and Assertions
	4 Application Experience in Avionics
	5 Conclusion
	References
On the Specification and Monitoring of Timed Normative Systems
	1 Introduction
	2 Background
		2.1 Temporal Logics, Timed Logics and Complexity
		2.2 Formalisation of Normative Systems: Deontic Logics
	3 Interpreting Timed Norms
	4 Monitoring Norms and Timed Norms
		4.1 Monitorability
		4.2 Monitor Synthesis
	5 Conclusions
	References
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
	1 Introduction
		1.1 Related Work
	2 Preliminaries
		2.1 Linear Temporal Logic
		2.2 LTL Model Checking
		2.3 Signal Temporal Logic
		2.4 Active Automata Learning
		2.5 Black-Box Checking
	3 BBC Enhanced via Model Checking with Strengthened LTL Formulas
		3.1 Strengthening Relation of LTL Formulas
		3.2 BBC Enhanced via Model Checking with Strengthened Formulas
		3.3
	4 Experiment
		4.1 Experiment Setup
		4.2 Performance Evaluation
	5 Conclusions and Future Work
	References
Neural Predictive Monitoring Under Partial Observability
	1 Introduction
	2 Problem Statement
	3 Methods
		3.1 Predictive Monitoring Under Noise and Partial Observability
		3.2 Conformal Prediction for Regression and Classification
		3.3 CP-Based Quantification of Predictive Uncertainty
		3.4 Active Learning (AL)
	4 Experimental Evaluation
		4.1 Case Studies
		4.2 Experimental Settings
		4.3 Results
	5 Related Work
	6 Conclusion
	References
A Compositional Framework for Quantitative Online Monitoring over Continuous-Time Signals
	1 Introduction
	2 Algebraic Semantics with Complete Lattices
	3 Monitors
	4 MTL Monitoring
	5 Experiments
	6 Related Work
	7 Conclusion
	References
Nested Monitors: Monitors as Expressions to Build Monitors
	1 Introduction
	2 Preliminaries
	3 Nested Monitors and Slices
		3.1 Nested Monitors and Slices in Lola
		3.2 Extensions in Striver
	4 Nested Monitors and Slices in Action
	5 Empirical Evaluation
	6 Conclusions
	References
Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous Programs
	1 Introduction
	2 Example
		2.1 Sources of Uncertainty
		2.2 Verification
	3 Diamont System
		3.1 Syntax
		3.2 Diamont Semantics
		3.3 Soundness of Runtime Monitoring
	4 Optimizations for Reducing Overhead
		4.1 Soundness
	5 Methodology
	6 Evaluation
		6.1 Can We Verify Important Uncertainty Properties Using Diamont?
		6.2 What Are the Overheads Associated with Diamont?
		6.3 How Does Diamont Overhead Depend on the Program Inputs?
	7 Related Work
	8 Conclusion
	References
Assumption-Based Runtime Verification of Infinite-State Systems
	1 Introduction
	2 Preliminaries
		2.1 Satisfiability Modulo Theory
		2.2 First-Order Quantifier Elimination
		2.3 Fair Transition System
		2.4 Linear Temporal Logic
		2.5 Assumption-Based Runtime Verification
	3 Motivating Example
	4 ABRV Algorithms for Infinite-State Systems
		4.1 ABRV Reduced to Model Checking
		4.2 ABRV Reduced to MC and Quantifier Elimination
		4.3 Optimizations
		4.4 ABRV Reduced to Model Checking and Incremental BMC
	5 Experimental Evaluation
		5.1 Tests on the Motivating Example (Sect.3)
		5.2 Tests on Dwyer's LTL Patterns
	6 Related Work
	7 Conclusion
	References
Short Papers and Tool Papers
Differential Monitoring
	1 Introduction
	2 Background and Related Work
	3 Challenges
	4 Experimental Results
	5 Conclusion
	References
Ortac: Runtime Assertion Checking for OCaml (Tool Paper)
	1 Introduction
	2 Overview and Motivating Example
	3 Code Generation and Tool Architecture
		3.1 Translating Formulas
		3.2 Wrapping the Functions
		3.3 A Modular Architecture
	4 Related Work
	5 Conclusion and Perspectives
	References
Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks
	1 Introduction
	2 Preliminaries
		2.1 Deep Neural Networks
	3 Our Solution Approach
	4 Experiments
		4.1 Datasets and Training
		4.2 Gaussian Assumption
		4.3 Evaluation Steps
		4.4 Parameter Study
	5 Outlook
	6 Conclusion
	References
Parallel and Multi-objective Falsification with Scenic and VerifAI
	1 Introduction
	2 Background
	3 Parallel Falsification
	4 Multi-objective Falsification
		4.1 Specification of Multiple Objectives Using Rulebooks
		4.2 Multi-objective Active Sampling
	5 Evaluation
	6 Conclusion and Future Work
	References
A Theoretical Framework for Understanding the Relationship Between Log Parsing and Anomaly Detection
	1 Introduction
	2 Preliminaries
	3 Ideal Log Parsing Results for Anomaly Detection
		3.1 Log Parsing as Abstraction
		3.2 Ideal Log Parsing Results
	4 Applications
		4.1 Localization of the Causes of Inaccurate Anomaly Detection
		4.2 Removal of Unnecessary Log Messages for Anomaly Detection
	5 Related Work
	6 Conclusion and Future Research Directions
	References
Specification and Runtime Verification of Temporal Assessments in Simulink
	1 Introduction
	2 Authoring Temporal Specifications
		2.1 Preliminaries
		2.2 Authoring Temporal Assessments via a UI Element
		2.3 Visual Representation
		2.4 Symbol Resolution
		2.5 Example
	3 Runtime Verification of Temporal Assessments
	4 Discussion
	References
PerceMon: Online Monitoring for Perception Systems
	1 Introduction
	2 Spatio-Temporal Quality Logic
	3 PerceMon: An Online Monitoring Tool
		3.1 Integration with CARLA and ROS
	4 Experiments
	5 Conclusion
	A  Semantics for STQL
	References
Tutorial Paper
Formal Analysis of AI-Based Autonomy: From Modeling to Runtime Assurance
	1 Introduction
	2 Motivating Example: Autonomous Aircraft Taxiing
	3 The VerifAI Framework
	4 Training Data Generation
		4.1 Mapping
		4.2 Segmentation
		4.3 Disambiguation
	5 Monitor Generation
		5.1 Learning Methods
		5.2 Learning Monitors for TaxiNet
	6 Runtime Assurance
	7 Discussion
		7.1 Desiderata for Effective Monitors
		7.2 Monitor Refinement and Synthesis
	References
Author Index