Raphaël Jakse - Vérification Interactive de propriété à l'exécution

Computers are ubiquitous. We trust them for a huge and increasing number of tasks, some critical.
Consequences of software defects are various, from little annoyances to the loss of multiple lives. Hence, ensuring software reliability is instrumental.

Fixing bugs is a very time-consuming activity of the software development cycle. In this thesis, we present interactive runtime verification (i-RV), which combines runtime verification and interactive debugging. Runtime verification is a formal method to study the behavior of a system at runtime. It consists in matching runtime traces of a system at runtime against behavioral properties. These properties are part of the system specification. Interactive debugging consists in studying a system at runtime in order to understand its bugs and fix them, inspecting its internal state interactively. Interactive runtime verification aims to make interactive debugging less tedious and more systematic by leveraging the rigorous and automated aspects of runtime verification. We aim to ease the debugging part of the software development cycle.
We define an efficient and convenient way to check behavioral properties automatically on a program using an interactive debugger. We gather bug detection and bug understanding in an integrated workflow, by guiding interactive debugging using runtime verification.

We provide a formal model for interactively runtime verified programs. We model the execution of a program 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 then introduce a distributed and adaptive framework for interactive runtime verification. It allows checking several requirements simultaneously and debugging a distributed system composed of communicating processes. The monitors, the scenario and the debugged programs themselves run distributed using an orchestrating protocol which we verified using the SPIN model checker. Our distributed framework is designed to adapt to existing components.

We present Verde, an implementation of interactive runtime verification. A first version is based on the GNU Debugger (GDB) to interactively runtime verify C and C++ programs. A second version, Dist-Verde, is an implementation of our distributed framework compatible with C and C++ programs through GDB and Java programs through JDB, the Java Debugger.

We report on experiments using Verde assessing the usefulness of interactive runtime verification and the performance of our implementation. Our results show that interactive runtime verification is applicable in a variety of cases and helps to study bugs.