Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Inférence d'invariants pour le model checking de systèmes paramétrés
Début le 03/10/2011
Direction : CONCHON, Sylvain
[ZAIDI Fatiha]
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI PROVAL
Soutenue le 29/09/2014 devant le jury composé de :
Directeur de thèse :
- M. Sylvain Conchon, Professeur, Université Paris-Sud
Co-encadrante :
- Mme Fatiha Zaïdi, Maître de conférences, Université Paris-Sud
Rapporteurs :
- M. Ahmed Bouajjani, Professeur, Université Paris Diderot et IUF
- M. Silvio Ranise, Chercheur, Fondazione Bruno Kessler
Examinateurs :
- M. Rémi Delmas, Ingénieur de recherche, ONERA
- M. Alan Schmitt, Chargé de recherche, INRIA Rennes Bretagne Atlantique
- M. Philippe Dague, Professeur, Université Paris-Sud
Activités de recherche :
- Démonstration automatique, SMT et applications
Résumé :
Cette thèse aborde le problème de la vérification automatique de systèmes
paramétrés complexes. Cette approche est importante car elle permet de garantir
certaines propriétés sans connaître a priori le nombre de composants du
système. On s'intéresse en particulier à la sûreté de ces systèmes et on traite
le côté paramétré du problème avec des méthodes symboliques. Ces travaux
s'inscrivent dans le cadre théorique du model checking modulo théories et ont
donné lieu à un nouveau model checker : Cubicle.
Une des contributions principale de cette thèse est une nouvelle technique pour
inférer des invariants de manière automatique. Le processus de génération
d'invariants est intégré à l'algorithme de model checking et permet de vérifier
en pratique des systèmes hors de portée des approches symboliques
traditionnelles. Une des applications principales de cet algorithme est
l’analyse de sûreté paramétrée de protocoles de cohérence de cache de taille
industrielle.
Enfin, pour répondre au problème de la confiance placée dans le model checker,
on présente deux techniques de certification de notre outil Cubicle utilisant
la plate-forme Why3. La première consiste à générer des certificats dont la
validité est évaluée de manière indépendante tandis que la seconde est une
approche par vérification déductive du cœur de Cubicle.
