Une couverture Combinant Tests et Preuves pour la Vérification Formelle

Currently, industrial-strength software development usually relies on unit testing or unit proof in order to ensure high-level requirements. Combining these techniques has already been demonstrated more effective than using one of them alone. The verification engineer is yet not been to combine these techniques because of the lack of a common notion of coverage fortesting and proving. Defining such a notion is the main objective of this thesis.We introduce here a new notion of coverage, named « label-mutant coverage ». It subsumes most existing structural coverage criteria for unit testing, including statement coverage, branch coverage or MC/DC coverage, while allowing to decide whether the chosen criterion is satisfied by relying on a formal verification technique, either testing or proving or both.It also subsumes functional coverage criteria. Furthermore, we also introduce a method that makes use of automatic tools for testing or proving in order to reduce the verification cost while satisfying the chosen coverage criterion. This method is implemented inside Frama-C, a framework for verification of C code (Frama-C). This way, it offers to the engineer a way tocontrol and to perform the expected verifications.L’utilisation combinée du test et de la preuve est rendue difficile par l’absence d’une notion de couverture commune. Cette couverture est nécessaire pour rendre compte de la qualité de la vérification effectuée. Elle est d’ailleurs un objectif incontournable des standards de certification du logiciel dans les domaines critiques tels que l’aéronautique. La thèse vise à résoudre ce problème en proposant une nouvelle notion de couverture, adaptée aussi bien pour le test que pour la preuve. Elle fournit aussi une méthode d’interprétation qui permet d’optimiser le pilotage d’une campagne de vérification et une plateforme qui réalise automatiquement la vérification et construit la matrice de couverture. La méthode d’interprétation a été implémentée comme un prototype au sein de la plateforme de vérification Frama-C