Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
La vérification de logiciels représente un défi important à l’heure où ces derniers sont présents partout dans notre vie quotidienne. La technique la plus employée pour s’assurer qu’un logiciel répond à certaines exigences reste le test, c’est à dire exécuter le programmes sur un certain nombres d’entrées représentatives. Un enjeu majeur est alors de s’assurer que ces jeux d’entrée couvrent suffisamment de situations différentes.De nombreuses propositions ont été faites, appelées critères de couvertures, qui définissent des objectifs de tests, par lesquels doit passer au moins une exécution au cours du test. Dans cette thèse, nous examinons différentes possibilités pour combiner les méthodes formelles (techniques mathématiques) et le test, dans l’objectif d’améliorer l’efficacité de ce dernier. Nous nous sommes principalement intéressés aux critères de flot de données, qui observent le comportement des définitions et utilisations des variables du programme, et en particulier à la détection des objectifs polluants. Nous avons proposé plusieurs techniques, avec leurs implémentations et évaluations sur des exemples de programmes C réel. Nous étudions ensuite l’impact que ces objectifs de flot de données peuvent avoir sur la génération de test. Enfin, nous terminons en concevant une méthode permettant d’utiliser la détection d’objectifs polluants pour vérifier l’efficacité des contre-mesures contre les attaques par injection de fautes, et de trouver ainsi les erreurs dans leur implémentation. Cette méthode a été appliquée le bootloader de WooKey, un périphérique de stockage chiffré. ; At a time where software are omnipresent in our daily life, verifying their safety and security present an important challenge for the industry. The most used technique to ensure that a software meets certain requirements is testing, where we run the program with some controlled input sets. A major issue is then to ensure that these input sets cover enough different situations. Many proposals have been made, called coverage criteria, which define test ...