Elimination des fautes : contribution au test du logiciel

The research summarized in this report focuses on the dependability of computer systems. It adresses fault removal by means of software testing. The contributions are grouped into four chapters. Chapter I presents work seeking to adapt the test design to software development technologies. It considers both object-­‐oriented development and the formal B method. Chapter II investigates ways of coupling testing and formal verification. The aim may be to consolidate the verification of partially proved algorithms, or to aid in the analysis of counterexamples obtained from a model checker. Chapter III concerns search-­‐based test generation, taking the example of simulated annealing search. It focuses on a measurement approach to tune the parameters of the metaheuristics. Finally, Chapter IV tackles testing of mobile computing systems. Test traces are checked with respect to properties described in graphical scenarios. The checking involves both graph matching and event order analysis.Les travaux résumés dans ce mémoire ont pour cadre la sûreté de fonctionnement des systèmes informatiques. Ils portent sur l'élimination des fautes, en s'intéressant plus particulièrement au test du logiciel. Les contributions sont regroupées en quatre chapitres. Le premier chapitre rassemble des travaux pour adapter la conception du test aux technologies de développement logicielles. Deux technologies sont considérées : la technologie orientée-­‐objet et la méthode formelle B. Le deuxième chapitre porte sur des associations test et vérification formelle. Il s'agit selon les cas de consolider la vérification d'algorithmes partiellement prouvés, ou de faciliter l'analyse de contrexemples retournés par un model checker. Le troisième chapitre traite de la génération de test par des procédés métaheuristiques, en prenant l'exemple du recuit simulé. L'accent est mis sur l'utilisation de mesures pour guider le paramétrage de la métaheuristique. Enfin, le quatrième chapitre aborde le test de systèmes mobiles. Lestraces d'exécutions sont vérifiées par rapport à un ensemble de propriétés décrites par des scénarios graphiques, en combinant des algorithmes d'appariement de graphes et de calcul d'ordres partiels d'événements