Interactive Runtime Verification: Formal Models, Algorithms, and Implementation - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2019

Interactive Runtime Verification: Formal Models, Algorithms, and Implementation

Vérification de propriété interactive : modèles formels, algorithmes et mise en œuvre

(1, 2, 3) , (2, 3, 1) , (1, 2)
1
2
3

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.
Fichier principal
Vignette du fichier
acmsmall.pdf (1.91 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02190656 , version 1 (22-07-2019)

Identifiers

  • HAL Id : hal-02190656 , version 1

Cite

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⟩
44 View
149 Download

Share

Gmail Facebook Twitter LinkedIn More