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é.
- 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), LAMSADE
(Université Paris-Dauphine), 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.
Je participe également aux projets :
- ANR DOTS
(Distributed Open Timed Systems
),
dont les thèmes de recherche sont orientés sur le model
checking, le contrôle et la non interférence de systèmes
temporisés, ouverts et distribués.
- DIM CoChaT (Covert Channels for Timed systems), consacré aux
problèmes de détection et de synthèse de canaux cachés pour des
systèmes temporisés (pdf).