English version
Court
CV
Titre
et diplômes
- A partir du 1er
janvier 2022, je suis retraité, professeur émérite de
l'Université de Nantes. Ex-professeur des universités de classe
exceptionnelle.
- 2017-2021 :
Fondateur et directeur du Laboratoire des Sciences du Numérique de Nantes
(LS2N, UMR6004)
- 2012-2021 :
Professeur dans le département informatique de la faculté des sciences de
l'Université de Nantes.
- 2012-2020 :
Directeur adjoint du labex CominLabs
- 2002-2012 : Professeur
de l'Ecole Normale Supérieure de Cachan dans le
département Informatique et Télécommunications.
Directeur du Collège de Recherche Hubert Curien, institut
pluridisciplinaire rassemblant la recherche conduite sur le campus de Bretagne
de l'ENS de Cachan.
Chargé du suivi de la recherche de l'antenne de Bretagne de l'ENS Cachan.
Co-directeur de l'équipe-projet INRIA Distribcom
(modèles et algorithmes pour la supervision des réseaux de
télécommunication).
- 1997-2003 : Directeur
de Recherche au CNRS, responsable de l'équipe PAMPA (modèles et outils
pour la programmation des architectures parallèles réparties) à l'IRISA
puis membre de l'équipe de direction de l'IRISA.
- 1987-1997 : Chargé de
Recherche au CNRS, membre de l'équipe ADP (Algorithmes Distribués et
Protocoles), puis de l'équipe PAMPA (Programmation des Architectures
Massivement PArallèles) à l'IRISA.
- 1994 :
Habilitation à diriger les recherches.
Titre : Contribution à la vérification dynamique des protocoles.
Jury : J.P. Banâtre (président), Gv. Bochmann, JM. Pitié, J.
Sifakis (rapporteurs), F. André, M.
Raynal et J.P. Verjus.
- 1980-1985 : Ingénieur
au Centre National d'Etudes des
Télécommunications (CNET) à Lannion, membre de l'équipe Evaluation et Validation de Protocoles. En 1981, j'ai
passé une petite année dans l'équipe de Gv. Bochmann à l'université de Montréal comme chercheur
invité.
- 1984 : Thèse de
Docteur-Ingénieur de l'université de Rennes1.
Titre : Protocoles et Services - le test des spécifications.
Jury : J.P. Verjus (président), P. Azéma, M. Raynal (rapporteurs), J.P. Ansart, Gv. Bochmann et J.M. Pitié.
- 1981 : Ingénieur des
Télécommunications.
- 1978-1981 : Elève ingénieur civil de l'Ecole
Nationale Supérieure des Télécommunications de Bretagne (Brest).
- 1976-1978 : Mathématiques
Supérieures et Spéciales au lycée Saint Louis, Paris.
Travaux
Mes travaux de recherche
portent sur l'analyse des systèmes parallèles asynchrones. Ils s'inscrivent
dans le cadre général de l'utilisation de méthodes formelles pour la programmation
des architectures parallèles et réparties, et concernent les étapes de
spécification, vérification et test/supervision des logiciels répartis sur des
réseaux de processeurs. Le thème central de mes travaux est l'étude de méthodes
d'analyse dynamiques, dans lesquels le calcul est effectué au cours de
l'exécution - abstraite, simulée ou réelle - du programme à analyser. Je suis
actuellement plutôt mobilisé sur l'analyse de la qualité de service (QoS) à l'aide de modèles permettant d'expliciter la causalité,
le temps et d'autres aspects non fonctionnels, ainsi que l'étude de la
décidabilité des modèles paramétrés et les algorithmes répartis sur des modèles
à cohérence causale faible.
Résultats : je suis
l'auteur ou co-auteur de plus de 150 publications, effectuées essentiellement
au sein de trois communautés de recherche : l'informatique théorique,
l'ingénierie des protocoles, et les systèmes répartis. J'ai participé à la
conception et la réalisation de trois gros logiciels : le premier (Veda) a été
pendant 10 ans au catalogue d'un industriel (Telelogic);
le second a été diffusé largement dans le milieu académique et a été évalué
dans plusieurs sites industriels (Echidna), le
troisième (TGV) a été transféré à la société Telelogic. J'ai encadré (ou co-encadré)
24 thèses de doctorat. J'enseigne sur les thèmes de l'algorithmique, des
langages formels, de l'ingénierie des protocoles et des réseaux.
Thèmes
de recherche
- Techniques de
description formelle : participation au développement de langages
normalisés pour décrire les protocoles, comme ESTELLE, LOTOS, SDL et plus
récemment HMSC et UML.
- Simulation et
"model-checking" : développement
d'une technique à base d'observateurs pour vérifier des propriétés
pendant la simulation. Développement de nouveaux algorithmes en ligne
pour le "model-checking au vol",
fondés sur un parcours exhaustif de l'espace d'état de la spécification.
- Synthèse de
tests : extension des algorithmes de model-checking
pour générer au vol des graphes de test pour le test de conformité.
- Algorithmes
répartis : consensus réparti. Travail en cohérence faible.
- Observation
répartie et suivi de comportements : "trace-checking",
estampillage causal, detection au vol de
propriétés instables.
- Nouveaux
modèles sémantiques du parallélisme : aspects sémantiques d'UML, développement
de BDL, automates d'ordres, dioide Max,+),
sémantique des "High-level Message Sequence Charts".
- Résultats de
décidabilité : test du caractère borné de files de communication FIFO,
logique temporelle.
- Dépliages de
Réseaux de Petri : préfixes
finis symboliques et temporisés.
- Diagnostic de
pannes dans les réseaux : développement de techniques réparties de
filtrage et de diagnostic des alarmes dans les réseaux de
télécommunications (SDH/WDM/IP).
- Web services
: description d'orchestrations, évaluation de la QoS.
Back
to top
Dernière mise à jour : Mars 2023