Treffer: Interactive Runtime Verification ; Vérification interactive de propriétés à l'exécution
Weitere Informationen
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 ...