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 :
Reports
Complete list of metadatas

Cited literature [56 references]  Display  Hide  Download

https://hal.inria.fr/hal-02190656
Contributor : Raphaël Jakse <>
Submitted on : Monday, July 22, 2019 - 4:07:20 PM
Last modification on : Friday, October 25, 2019 - 1:23:39 AM

File

acmsmall.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02190656, version 1

Citation

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⟩

Share

Metrics

Record views

44

Files downloads

254