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

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