Accéder directement au contenu Accéder directement à la navigation
Rapport

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.
Type de document :
Rapport
Liste complète des métadonnées

Littérature citée [56 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-02190656
Contributeur : Raphaël Jakse <>
Soumis le : lundi 22 juillet 2019 - 16:07:20
Dernière modification le : jeudi 19 novembre 2020 - 13:02:09

Fichier

acmsmall.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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⟩

Partager

Métriques

Consultations de la notice

89

Téléchargements de fichiers

431