Présentation
Je suis un post-doctorant en informatique. Depuis septembre 2012, je travaille à l'INRIA Rennes/IRISA dans le projet TAMIS avec Axel Legay. J'ai fait partie précédemment des groupes ESTASYS, TRISKELL et DISTRIBCOM.
Précédemment je travaillais pour le centre de recherche danois MT-LAB. J'ai travaillé à l'IT University de Copenhague, dans le groupe de recherche d'Andrzej Wąsowski et à l'université d'Aalborg, avec le professeur Kim G. Larsen. En 2010, j'ai travaillais à l'Université de Florence en Italie, dans le Software Technologies Laboratory, avec le professeur Enrico Vicario
De 2006 à 2009, j'ai réalisé mon doctorat en Automatique et Informatique Appliquée, à l' Université de Nantes, dans le laboratoire IRCCyN. J'ai travaillé pendant cette période dans l'équipe Systèmes Temps Réel avec Olivier (H.) Roux, David Delfieu et Didier Lime.
J'ai souteu ma thèse de doctorat le 27 novembre 2009 à l'IRCCyN à Nantes.
Le titre est :
"Vérification et dépliages de réseaux de Petri temporels paramétrés"
Le manuscrit de thèse et les transparents de la soutenance sont disponibles sur HAL ou bien ici.
J'ai été impliqué dans les évènements scientifiques suivants:
- SiSoS'16 conférence : membre du PC
- FORMATS'15 conférence : membre du PC
- FORMATS'14 conférence : membre du PC
- EXPRESS/SOS 2013 workshop : membre du PC
- RV'13 conférence : organisateur local
- QMC École de doctorants : organisateur local
Recherche
Mes travaux de recherche portent sur l'analyse quantitative de systèmes informatiques critiques en utilisant des méthodes formelles. En utilisant des modèles formels d'un système, je tente de vérifier des spécifications formelles pour assurer la sureté de fonctionnement du système. Nous appliquons pour cela des méthodes mathématiques rigoureuses, permettant par exemple de mesurer des temps d'exécution ou la consommation d'énergie, ou bien d'estimer les probabilités d'erreurs, ou encore d'optimiser les performances en synthétisant des paramètres temporels oui stochastiques. Ces travaux ont des applications concrêtes dans les systàmes embarqués utilisés en astronautique, dans les transports (avionique, automobile...) ou les équipements médicaux. J'étudie les approches suivantes:
- Spécification des systèmes temps réel en utilisant des réseaux de Petri temporels ou des automates temporels (TIOA).
- Spécification de systèmes adaptatifs.
- Vérification formelle par model-checking, et synthèse de contrôleur à l'aide de jeux temporels.
- Model-checking statistique.
- Robustesse et implémentation des automates temporels.
- Approches paramétrées.
- Les méthodes de préservation de la concurrence telles que les dépliages.
Outils
Je participe au développement des outils suivants :
- PLASMA LAB, une plateforme de model-checking statistique de modèles stochastiques.
- PyECDAR, un outil en python pour l'analyse de spécifications temporelles et de jeux temporisés. Il implémente certaines des fonctionalités de l'outil ECDAR. Par ailleurs il permet l'analyse de la robustesse des spécifications.
- QUAIL, un outil d'analyse quantitative de langages impératifs.
- Romeo, un outil pour la manipulation et l'analyse de réseaux de Petri temporels. Il permet l'édition et la simulation de réseaux de Petri temporels et performe des vérifications à la volée de propriétés temporelles. J'ai développé dans Romeo l'utilisation des paramètres temporels, notamment par model-checking paramétré, ainsi qu'un plugin de calcul de dépliages symboliques temporels.
- PyPPL: Bindings en Python de la bibliothèque Parma Polyhedra Library pour les automates temporisés paramétrés.
- LLbox, un outil qui effectue des analyses temporelles de scenarios dans les réseaux de Petri temporels à l'aide de formules de logique linéaire.