Au sein de l'équipe VESONTIO (VErification, SpécificatiON Test et Ingéniérie dirigée par les mOdèles), j'anime des activités de recherche au sein de l'action Test. Je co-encadre les thèses de P.-C. Bué, O. Chebaro et K. Cabrera.
Notre objectif actuel est de contribuer à améliorer les techniques de génération de tests au sein de la plate-forme BZ-Testing Tools en permettant de définir des critères de sélection de tests formalisant des propriétés. Nous associons des outils de preuve et de résolution de contraintes pour calculer des abstractions permettant de maîtriser la taille des modèles d'applications réelles. Mes principales contributions de recherche des dix dernières années sont les suivantes :
- Raffinement de propriétés de Logique Temporelle Linéaire (LTL). La contribution est une méthode de vérification de propriétés raffinées combinant model-checking (model-checking de la propriété abstraite) et preuve de la propriété raffinée. L'apport est d'effectuer la vérification sans avoir à produire de variant. Voir publications [FASE 2000], [ZB 2000], [FME 2001], [ZB 2003], [SAVCB 2006], [IET 2008] thèse de B. Parreaux, C. Darlot et J. Groslambert.
- Vérification par partie de propriétés LTL. La contribution est une méthode model-checking sur une décomposition du système de transition par le raffinement. La méthode est correcte pour une classe de propriétés LTL incluant les vivacités leadsto et until. Voir publications [IFM 99], [IFM 2000], [TSI 2001], [IC 2009], thèse de P.A. Masson.
- Vérification de propriétés LTL sous hypothèses d'équité. La contribution est une définition du raffinement sous équité et une adaptation de l'algorithme de model-checking fondé sur les automates de Büchi pour l'appliquer sans coder les hypothèses d'équité dans l'automate afin d'en réduire la taille. Voir publications [AFADL 2001], [ZB 2002], thèse de S. Chouali.
- Test de propriétés de sécurité. La contribution est la génération de tests à partir d'un modèle comportemental de sécurité et d'un critère de sélection décrivant une propriété de sécurité combinée à un besoin de test.. Voir publications [A-MOST 2006], [AST 2008], [ABZ 2008], [JIAS 2010], [FAC 2010], thèse de R. Tissot, thèses en cours de P.C. Bué, de O. Chebaro et de K. Cabrera.
J'ai participé également à trois autres activités :
- ACI Sécurité Informatique GECCOO
- Raffinement de systèmes temps-réels. thèse de Emilie Oudot. Voir [AFADL 2003a], [RTS 2004], [SAVCB 2006] et [IJMIC 2010].
- Génération de tests à partir de Politique de Sécurité, projets VALIAS, POSE et TASCCC. Thèses de F. Lebeau, R. Tissot et thèses en cours de P. C. Bué et K. Cabrera.
