Vérification dynamique ciblée et interactive de programmes grâce à une architecture modulaire

Le cycle de développement d'une application contient plusieurs phases, de l'écriture au soutien technique suivant la publication. Une phase particulièrement importante est la vérification du programme. Il s'agit de vérifier que le programme produit répond à la spécification au sens large, c'est à dire qu'il présente le comportement prévu sans bogue, quel que soit le scénario et les entrées présentées. De nombreux outils sont disponibles pour assister l'utilisateur dans cette tâche. Parmi ceux-ci, on trouve les outils de vérification formelle qui permettent de modéliser le déroulement d'un programme et d'en prouver mathématiquement la validité. Les analyses statiques peinent cependant à vérifier des programmes complexes, et une autre famille d'outils est souvent nécessaire. Ce sont les outils dynamiques, qui vérifient l'intégrité du programme pendant son exécution. Dans ce domaine, on trouve surtout des outils spécialisés et efficaces, mais peu flexibles. En effet, en l'absence d'une structure commune, beaucoup d'outils réécrivent intégralement toutes les fonctionnalités de base, et ce coût de développement fait qu'ils se limitent souvent aux fonctionnalités strictement nécessaires. Peu d'outils proposent ainsi une instrumentation dynamique ou une interface graphique.

Abstract

The development cycle of an application covers multiple different stages, from code writing to technical support. One crucial phase is program verification and debugging. During this stage, the developers need to make sure that the program they deliver corresponds to both its explicit and implicit specification, meaning that it has to behave correctly and without any bug whatever input is given to it. Multiple tools exist to assist the developers. Among them, formal verification is a method which proves mathematically the validity of a program by modeling its behavior. However, this type of static analysis struggle to analyse properly complex programs, and developers often also rely on dynamic tools, which check the integrity of a running program. A large number of specialized tools exist in that domain, but they often go for a lean approach, with little flexibility and adaptability. This is partly due to the lack of a common framework for high performance runtime verification tools. Most tools have to reprogram every functionality from the ground up, which means they often limit their scope to what is strictly necessary to reduce development costs. Features such as dynamic instrumentation or even a graphical user interface are seldom available. As part of this research project, we propose a solution to this problem, taking example on the recent development in integrated development environments. The goal is to provide modularity in order to share underlying features as much as possible. This removes the need for rewriting those basic features and enables developers to focus on more advanced tasks, which in turn produces better verification tools.