CTL
9 novembre 2009 - 14h00
Etude et mise en oeuvre de méthodes de validation à l'exécution (Phd Defense)
par Yliès Falcone de Vérimag
Résumé : L'étude de cette thèse porte sur trois méthodes de validation dynamiques : les méthodes de vérification, d'enforcement (mise en application), et de test de propriétés lors de l'exécution des systèmes. Nous nous intéresserons à ces approches en l'absence de spécification comportementale du système à valider. Pour notre étude, nous nous plaçons dans la classification Safety-Progress des propriétés. Ce cadre offre plusieurs avantages pour la spécification de propriétés sur les systèmes. Nous avons adapté les résultats de cette classification, initialement développés pour les séquences infinies, pour prendre en compte de manière uniforme les séquences finies. Ces dernières peuvent être vues comme une représentation abstraite de l'exécution d'un système. Se basant sur ce cadre général, nous nous sommes intéressés à l'applicabilité des méthodes de validation dynamiques. Nous avons caractérisé les classes de propriétés vérifiables, enforçables, et testables. Nous avons ensuite proposé trois approches génériques de vérification, d'enforcement, et de test de propriétés opérant à l'exécution des systèmes. Nous avons montré comment il était possible d'obtenir, à partir d'une propriété exprimée dans le cadre de la classification Safety-Progress, des mécanismes de vérification, d'enforcement, ou de test dédiés à la propriété considérée. Enfin, nous proposons également les outils j-VETO et j-POST mettant en oeuvre l'ensemble des résultats proposés sur les programmes Java.
Jury composé de :
- Klaus Havelund (SRS @ JPL, NASA, USA), Rapporteur
- Thierry Jéron (DR @ IRISA -- INRIA de Rennes), Rapporteur
- Howard Barringer (PR @ Manchester University), Examinateur
- Ahmed Bouajjani (PR @ Université de Paris 7), Éxaminateur
- Jean-François Méhaut (PR @ Université Joseph Fourier), Éxaminateur
- Jean-Claude Fernandez (PR @ Université Joseph Fourier), Directeur
- Laurent Mounier (MCF @ Université Joseph Fourier), Co-Directeur
- Jean-Luc Richier (CR @ LIG), Co-Directeur
