Abstract FR:

Cette thèse porte sur le développement de méthodes combinatoires pour le test et la vérification formelle. En particulier, sur des approches probabilistes lorsque la vérification exhaustive n'est plus envisageable. Dans le cadre du test (basé sur un modèle), je cherche à guider l'exploration aléatoire du modèle afin de garantir une bonne satisfaction du critère de couverture attendu, quelle que soit la topologie sous-jacente du modèle exploré. Dans le cadre du model-checking, je montre comment générer aléatoirement un nombre fini de chemins pour savoir si une propriété est satisfaite avec une certaine probabilité. Dans une première partie, je compare différents algorithmes pour générer uniformément des chemins dans un automate. Puis je propose un nouvel algorithme qui offre un bon compromis avec une complexité en espace sous-linéaire en la longueur des chemins et une complexité quasi-linéaire en temps. Cet algorithme permet l'exploration d'un modèle de plusieurs dizaines de millions d'états en y générant des chemins de plusieurs centaines de milliers de transitions. Dans une seconde partie, je présente une manière de combiner réduction par ordres partiels et génération à la volée pour explorer des systèmes concurrents sans construire le modèle global, mais en s'appuyant uniquement sur les modèles des composants. Enfin, je montre comment biaiser les algorithmes précédents pour satisfaire d'autres critères de couverture. Lorsque ces critères ne sont pas basés sur des chemins, mais un ensemble d'états ou de transitions, nous utilisons une solution mixte pour assurer à la fois un ensemble varié de moyens d'atteindre ces états ou transitions et la satisfaction du critère avec une bonne probabilité.