Skip to Main content Skip to Navigation

Interactive Runtime Verification: Formal Models, Algorithms, and Implementation

Abstract : Interactive runtime verification (i-RV) combines runtime verification and interactive debugging. Runtime verification consists in studying a system at runtime, looking for input and output events to discover, check or enforce behavioral properties. Interactive debugging consists in studying a system at runtime in order to discover and understand its bugs and fix them, inspecting its internal state interactively. We define an efficient and convenient way to check behavioral properties automatically on a program using a debugger. We aim at helping bug discovery and understanding by guiding classical interactive debugging approaches using runtime verification. In this paper, we provide a formal model for interactively runtime verified programs. For this, we model how of a program executes under a debugger composed with a monitor (for verdict emission) and a scenario (for steering the debugging session). We provide guarantees on the soundness of the verdicts issued by the monitor by exhibiting a weak simulation (relation) between the initial program and the interactively runtime verified program. Moreover, we provide an algorithmic view of this model suitable for producing implementations. We present Verde, an implementation based on GDB to interactively runtime verify C programs. We report on a set of experiments using Verde assessing the usefulness of Interactive Runtime Verification and the performance of our implementation. Our results show that, even though debugger-based instrumentation incurs non-trivial performance costs, i-RV is applicable performance-wise in a variety of cases and helps to study bugs.
Document type :
Complete list of metadata

Cited literature [56 references]  Display  Hide  Download
Contributor : Raphaël Jakse Connect in order to contact the contributor
Submitted on : Monday, July 22, 2019 - 4:07:20 PM
Last modification on : Tuesday, May 11, 2021 - 11:37:47 AM


Files produced by the author(s)


  • HAL Id : hal-02190656, version 1


Raphaël Jakse, Yliès Falcone, Jean-François Méhaut. Interactive Runtime Verification: Formal Models, Algorithms, and Implementation. [Research Report] UGA (Université Grenoble Alpes); LIG (Laboratoire informatique de Grenoble); Inria Grenoble Rhône-Alpes, Université de Grenoble. 2019. ⟨hal-02190656⟩



Record views


Files downloads