Symbolic runtime verification for monitoring under uncertainties and assumptions

DOI10.1007/978-3-031-19992-9_8zbMATH Open1522.68326arXiv2207.05678OpenAlexW4312552352MaRDI QIDQ6160908FDOQ6160908

Authors: Hannes Kallwies, Martin Leucker, César Sánchez 

Publication date: 2 June 2023

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Abstract: Runtime Verification deals with the question of whether a run of a system adheres to its specification. This paper studies runtime verification in the presence of partial knowledge about the observed run, particularly where input values may not be precise or may not be observed at all. We also allow declaring assumptions on the execution which permits to obtain more precise verdicts also under imprecise inputs. To this end, we show how to understand a given correctness property as a symbolic formula and explain that monitoring boils down to solving this formula iteratively, whenever more and more observations of the run are given. We base our framework on stream runtime verification, which allows to express temporal correctness properties not only in the Boolean but also in richer logical theories. While in general our approach requires to consider larger and larger sets of formulas, we identify domains (including Booleans and Linear Algebra) for which pruning strategies exist, which allows to monitor with constant memory (i.e. independent of the length of the observation) while preserving the same inference power as the monitor that remembers all observations. We empirically exhibit the power of our technique using a prototype implementation under two important cases studies: software for testing car emissions and heart-rate monitoring.

Full work available at URL: https://arxiv.org/abs/2207.05678

Recommendations

• Time-triggered runtime verification
• scientific article; zbMATH DE number 6930545
• Runtime verification past experiences and future projections
• A brief account of runtime verification
• Runtime verification logics. A language design perspective

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Monitoring of Real-Time Properties
• A brief account of runtime verification
• Symbolic execution and program testing
• Comparing LTL semantics for runtime verification
• Symbolic monitoring against specifications parametric in time and data
• TeSSLa: temporal stream-based specification language
• Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions

Cited In (8)

• Computer says no: verdict explainability for runtime monitors using a local proof system
• Uncertainty in runtime verification: a survey
• Runtime Verification with Imperfect Information Through Indistinguishability Relations
• TeSSLa-ROS-bridge -- runtime verification of robotic systems
• Gray-box monitoring of hyperproperties with an application to privacy
• Runtime verification with minimal intrusion through parallelism
• Time-triggered runtime verification
• Symbolic and on the Fly Testing with Real-Time Observers

This page was built for publication: Symbolic runtime verification for monitoring under uncertainties and assumptions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160908)