Logic system models checking programs with noisy data at runtime
A Formal Framework for Noisy Runtime Verification
Logic in Computer Science
Summary
Sometimes, computers that watch other running programs to check for errors get confused by noisy or unreliable information. The paper introduces a new logical system called EDMon to better understand and describe how monitoring works when data is noisy. The authors show that this logic can explain many known results about monitoring under these uncertain conditions. They also compare EDMon to other similar logics and prove important properties about it. This helps improve the theory behind making sure software behaves correctly even when the checking process faces imperfect information.
runtime verificationmonitorabilitynoisy dataepistemic logicdynamic logicformal semanticsprogram monitoringtheorem cataloglogic comparison
Authors
Shay Allen Logan, Shawn Standefer, Thomas Ferguson
Abstract
We introduce the logic EDMon---an epistemic dynamic logic meant to model monitorability concepts in noisy runtime verification. Its syntax and semantics are defined and explained and the connection between EDMon and monitorability and noisy runtime verification concepts is explored. We then demonstrate that EDMon is sufficient to capture many of the results in the noisy runtime verification literature and catalog its relation to nearby logics and describe a large class of its theorems.