Je suis actuellement ATER à l'université Paris-Est Créteil (UPEC),
rattaché au LACL.
Les thèmes principaux de mes travaux de recherche sont la vérification
formelle et la communication des systèmes distribués.
Dernièrement, j'ai commencé à travailler sur des tranducteurs.
J'ai obtenu un doctorat en informatique de l'université Côte d'Azur,
dirigé par
Étienne Lozes
et
Cinzia Di Giusto.
Les systèmes distribués sont le plus souvent basés sur l’échange asynchrone
de messages entre des agents. La programmation par échanges de messages est largement
utilisée en calcul haute performance, en programmation événementielle,
dans les architectures orientées service, etc.
Malheureusement du fait de la variété des modèles de communication,
des ambiguïtés dans les spécifications, de la portabilité limitée du code,
ou encore de la difficulté à exécuter des tests,
il est très difficile de vérifier les systèmes communicants.
Le model-checking de systèmes communicants vise à analyser des modèles formels de
systèmes distribués et à détecter automatiquement des erreurs comme des pertes de
messages ou des inter-blocages. Ces problèmes sont indécidables pour des systèmes
à partir de deux machines, et plusieurs hypothèses restrictives ont été
étudiées pour rendre les problèmes décidables.
Nous définissons dans cette thèse une nouvelle classe de systèmes :
les systèmes réalisables avec des communications synchrones (RSC pour faire court).
Les comportements de ces systèmes approximent des comportement synchrones,
où les messages sont envoyés et reçus simultanément.
Nous nous basons sur cette définition pour étudier la généralisation d’une autre
classe de systèmes : les systèmes half- duplex. Un système à deux machines est half-duplex
si lorsqu’une machine envoie des messages, l’autre ne peut pas lui en envoyer.
Nous étudions également un autre formalisme, permettant de raisonner sur les
systèmes de manière globale : les chorégraphies.
Ce formalisme décrit les exécutions de manière synchrone, et un des problèmes qui
y est associé est de vérifier si la combinaison des comportements de chaque acteur
qui y est décrit est conforme à la description globale.
Nous proposons d’utiliser les propriétés des systèmes RSC pour traiter ce problème.