Doctorat
Equipe : Test Formel et Exploration de Systèmes
Approches combinatoires pour le test statistique à grande échelle
Début le 01/10/2007
Direction : GAUDEL, Marie-Claude
[co-encadrement avec Alain DENISE]
Ecole doctorale : Paris XI
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI
Soutenue le 19/11/2010 devant le jury composé de :
Philippe DAGUE, Professeur, Université Paris-Sud
Alain DENISE, Professeur, Université Paris-Sud
Marie-Claude GAUDEL, Professeur, Université Paris-Sud
Richard LASSAIGNE, Maître de conférence, Université Paris 7
Sylvain PEYRONNET, Maître de conférence, Université Paris-Sud
Olivier ROUX, Professeur, École Centrale de Nantes
Michèle SORIA, Professeur, Université Paris 6
Activités de recherche :
- Test de Logiciels
- Model-Checking
Résumé :
Cette thèse porte sur le développement de méthodes combinatoires pour
le test et la vérification formelle de logiciel.
On s'intéresse, en particulier, aux approches probabilistes lorsque la
vérification exhaustive n’est pas envisageable.
Dans le cadre du test basé sur un modèle, on montre comment guider
l’exploration aléatoire du modèle afin de garantir une bonne
satisfaction d'un critère de couverture du modèle exploré, quelle que
soit la topologie sous-jacente de celui-ci. Dans le cadre du
model-checking, on 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, on compare différents algorithmes pour
générer uniformément des chemins dans un automate. Puis on 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 de
modèles 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, on présente une manière de combiner réduction
par ordres partiels et génération à la volée pour explorer des
systèmes représentés par des composants concurrents sans construire le
modèle global, mais en s’appuyant uniquement sur les modèles des
composants.
Enfin, on montre comment biaiser les algorithmes précédents pour
satisfaire des critères de couverture qui ne sont pas basés sur des
chemins, mais par exemple sur un ensemble d’états ou de transitions.
On propose 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é.
