recherche

Thèmes de recherche

Mes travaux portent sur la modélisation et l'analyse de systèmes réactifs, critiques ou embarqués, comportant des aspects quantitatifs, notamment liés à l'écoulement du temps.

Etude de modèles comme les automates temporisés ou hybrides, ou comme les réseaux de Petri temporels, en particulier pour les questions d'expressivité et de décidabilité. Modèles quantitatifs pour la sécurité. Problèmes de contrôle et de synthèse, problèmes de robustesse. Applications aux systèmes de transport automatisés.
Etude des langages de spécification utilisés pour énoncer les propriétés de correction des systèmes. Ces langages sont étendus pour prendre en compte les informations quantitatives liées au temps, comme par exemple dans les propriétés de temps de réponse.

Notre équipe est membre du groupe MeFoSyLoMa, animé conjointement par les laboratoires Cedric (CNAM), IBISC (Université d'Evry), LIP6 (UPMC), LIPN (Université Paris 13), LSV (ENS de Cachan), LTCI (ENST). Ce groupe réunit des acteurs intéressés par l'application de méthodes formelles à la vérification de systèmes logiciels ou matériels.

L'équipe MoVe participe également à la mise en place de la plate-forme CosyVerif intégrant des outils de vérification.

Projets

ANR ImpRo (Implementability and Robustness, 2010-2013).
ANR DOTS (Distributed Open Timed Systems , 2006-2011), dont les thèmes de recherche étaient orientés sur le model checking, le contrôle et la non interférence de systèmes temporisés, ouverts et distribués. Dans le cadre de ce projet, j'ai co-organisé, avec Didier Lime, le Workshop DOTS affilié à la conférence CONCUR 2010.
DIM CoChaT (Covert Channels for Timed systems, 2009-2011), consacré aux problèmes de détection et de synthèse de canaux cachés pour des systèmes temporisés (pdf).