Symbolic runtime verification for monitoring under uncertainties and assumptions

DOI10.1007/978-3-031-19992-9_8MaRDI QIDQ6160908zbMATHOpenAlexFDO

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)

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

Mathematics Subject Classification ID

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

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.

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

Cites work

• A brief account of runtime verification
• Comparing LTL semantics for runtime verification
• Monitoring of Real-Time Properties
• Symbolic execution and program testing
• 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)

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

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)