Intérêts scientifiques
Mes recherches s'effectuent dans le cadre de la vérification formelle : principalement pour le test formel, mais aussi le model-checking.
Je m'intéresse au problème de l'explosion combinatoire des systèmes formels qui intervient dès que les modèles étudiés représentent des systèmes non triviaux. Je travaille plus particulièrement sur des solutions qui utilisent des approches statistiques lorsque l'exhaustivité n'est plus envisageable.
Test formel
L'objectif du test formel est d'obtenir, de manière automatique, un sous ensemble de tous les tests possibles qui satisfait un certain critère de couverture. Ce sous-ensemble est communément appelé jeu de test et le critère de couverture est défini à partir de la spécification formelle du système, qu'on peut généralement représenter sous la forme d'un automate (ou une version simplifiée plus communément appelée un système de transitions étiquetées (LTS)).
Les critères de test structurel les plus classiques sont :
- la couverture des instructions : on est passé au moins une fois dans chaque bloc élémentaire après l'exécution du jeu de tests,
- la couverture des enchaînements : passer au moins une fois par chaque arc du graphe,
- la couverture de tous les chemins, qui est généralement impossible (si il y a une boucle dans le programme) ou trop coûteuse et on se ramène donc à un critère plus faible comme la couverture de tous les chemins qui passent au maximum i fois dans chaque boucle.
Exploration aléatoire
Lorsque la couverture d'un critère requiert un nombre trop important de tests, on peut envisager d'abandonner l'exhaustivité au profit de méthodes probabilistes.
La première idée qui vient quand on veut explorer aléatoirement un graphe, est l'utilisation de marches aléatoires isotropes (c'est-à-dire, à chaque étape, choisir au hasard l'état suivant uniformément parmi les successeurs de l'état courant). Les principaux avantages de cette méthode sont la simplicité et le peu de mémoire nécessaire qui lui permettent d'explorer de très grands graphes à un faible coût. Néanmoins, si on s'intéresse à la satisfaction - même partielle - d'un critère de couverture, il est très incertain pour ne pas dire improbable que les marches aléatoires isotropes puissent le satisfaire en un temps raisonnable.
Mes travaux consistent donc à utiliser des approches combinatoires pour construire des méthodes probabilistes permettant d'explorer de très grands systèmes tout en garantissant une bonne couverture du critère de test. On obtient alors des algorithmes rapides, économes en mémoire et très efficaces.