Formation et emplois successifs

Situation actuelle

Je suis ingénieur de recherche à France Télécom R&D. En plus de mes travaux de recherche et développement, j'assure l'intérim de mon unité de recherche et Développement. Mes activités se concentrent autour du test et des outils de test et diagnostic.

Emplois successifs

Titres Universitaires

Enseignements

•  Responsable du cours "Spécification des systèmes réactifs" dispensé en troisième année aux élèves ingénieur de l'ENSSAT.

•  Encadrement de TD et TP à l'Université de Franche-Comté..

A Lannion

A Lannion, je donne des cours à l'ENSSAT en 3ième année dans le domaine des méthodes formelles. Mon cours porte sur la spécification des systèmes réactifs. Ce cours comporte une partie sur le langage de spécification SDL et sur la modélisation et les techniques de model checking. Une autre partie du cours porte sur le test et les techniques associées.

A l'Université de Franche Comté

Lors de mon passage à l'université de Franche Comtré, j’ai réalisé 465 heures équivalent TD d’enseignement durant mes cinq années d’expérience. Ce total a été réalisé sur les statuts suivants :

•   Vacataire en 1996-1997 (108 h), en 1997-1998 (104 h) et en 1998-1999 (48 h) 

•    ATER à mi-temps en 1999-2000 (100 h) et en 2000-2001 (105 h)

Matières enseignées

•   Bases de données (Initiation ACCESS) en IUP1 et en MIAS2 (197 h heures équivalent TD) 

•   Mathématiques et Informatique (Initiation à la programmation) en DEUG Génie Mécanique (20 heures équivalent TD)

•   Programmation fonctionnelle (Utilisation de Scheme) en IUP2 (24 heures équivalent TD) 

•   Modélisation des systèmes (Programmation d’un simulateur en C++ et Java) en IUP2 (40 heures équivalent TD) 

•   Algorithmique combinatoire (Programmation d’une boite à outils en C++ et Java) en IUP3 (88 heures équivalent TD) 

•   Ingénierie des protocoles et applications réparties (Modélisation en PROMELA et utilisation de SPIN) en DESS Génie Informatique Systèmes Distribués (86 heures équivalent TD) 

•   Modélisation (Modélisation en B et PROMELA et utilisation de l’atelier B et de SPIN) en DESS Génie Informatique Systèmes Distribués (10 heures équivalent TD).

Encadrement de projets

•   Implémentation d’une nouvelle méthode de compression dans l’outil de Model-Checking SPIN - DESS Génie Informatique Systèmes distribués.

•   Évaluation et amélioration de performances de la méthode de compression dans l’outil de Model-Checking SPIN - DESS Génie Informatique Systèmes distribués.

•    Création d’une interface en Java pour le model-checker par résolution de contraintes - DESS Génie Informatique Systèmes distribués.

•    Création de pages Web permettant la gestion des appels à communication et de la bibliographie au niveau du laboratoire – IUP2.

Recherche

A France Télécom R&D, mes travaux ont d'abord porté sur les méthode de spécification d'une part en participant à des activités de normalisation à l'ITU. Puis, j'ai travaillé dans des projets Européens et Français portant sur la spécification, la supervision et le test. J'ai aussi encadré quelques thésards qui ont réalisés celle-ci au sein de France télécom. 

Au sein de l’équipe Techniques Formelles et à Contraintes du Laboratoire d’Informatique de l’Université de Franche-Comté ma problématique de recherche consistait à utiliser des solveurs de contraintes ensemblistes pour diminuer l’explosion combinatoire de l’algorithme de vérification de propriétés de Logique Temporelle Linéaire sur des spécifications de systèmes réactifs.

Ma thèse « Vérification de systèmes d’événements B par model-checking PLTL - Contribution à la réduction de l’explosion combinatoire en utilisant de la résolution de contraintes ensemblistes » a été soutenue le 08 Décembre 2000 à l’Université de Franche-Comté et a été réalisée sous la direction du Professeur Jacques Julliand et du Maître de Conférences Hassan Mountassir.

Thématiques

•    Systèmes distribués en DEA

•    Vérification de logiciels en doctorat

•  Modélisation de système et de services

•  Langage, méthode et techniques de test (théorie et automatisation)

•  Méthode et techniques de diagnostic

•  Méthode et techniques de supervision

Résultats

•   Création et implantation dans SPIN d’un algorithme original de compression pour le model-checking.

•    Adaptation et implantation de l’algorithme de model-checking PLTL à la volée de Wolper et Vardi pour tirer parti de l’utilisation de techniques de résolution de contraintes.

•  Contribution à la normalisation des systèmes temps réels à l'ITU

•  Contribution à différents projets Européen, RNRT et RNTL.

•  Participation à la création d'un outil de modélisation de services vocaux

•  Création d'un outil de test pour les gateways

•  Participation à la création d'un outil de supervision réseau et services

Publications dans des conférences

•   Notere 2007 : Métamodèle d'architectures distribuées à des fins d'analyse et de performance

•   TestCom 2006 : LaTe, a non-fully deterministic testing language

•   FORTE 2004 : Formal Composition of distributed scenarios

•   NOTERE 2004 : Integrating Scenarios  with Explicit Loops

•   SAM 2004 : Scenarios with Explicit Loop Specification (Poster)

•   SDL Forum 2003 : RMTP2 : Validating the Interval Timed Extension for SDL with an Industrial-Size Multicast Protocol.

•   SDL Forum 2003 : Refining Timed MSCs (meilleur papier/présentation de la conférence SDL Forum 2003)

•   SPIN WS 1998 : Difference compression in Spin

•   B 1998 : Specification of an Integrated Circuit Card Protocol Application Using the B Method and Linear Temporal Logic

Publications dans des revues

•   TSI 99 : De l'expression des besoins à l'expression formelle des propriétés dynamiques

 Exposés

•  Exposés aux groupes de travail du GDR ARP RGE (Réseau Grand-Est), en 1997

•  Exposé à l’école des jeunes chercheurs en programmation du GDR ALP en 1998

•  Exposé au Workshop On Modeling and Verification ayant eu lieu à Besançon en 1999

•  Invité aux journées du CNAM-CMSL du 15-16 octobre 2003
                       "Test des systèmes logiciels : automatiser pour mieux valider ?"
                       Exposé sur un retour d'expérience.

•  CFIP 2005 : Métrologie Internet : Techniques, Expériences et Applications (tutorial)
                       Machines de mutations pour l'enrichissement de test de protocoles

Participation à la formation par la recherche

•  Encadrement de thèses :

  •  portant sur la génération de tests utilisant des spécifications formelles incomplètes

  •  portant sur les langages de test (soutenue en 2007)

  •  portant sur la génération automatique de tests utilisant des mutants (soutenue en 2006)

•  Participation à l’encadrement d’un étudiant de DEA ayant pour but la réalisation d’un outil permettant la décomposition de l’espace d’états accessibles en modules en utilisant le raffinement,

•  Réalisation de Travaux Pratiques d’introduction à l’utilisation de l’outil SPIN et de l’atelier B.

Travaux et activités scientifiques

Encadrements et responsabilités

Activités d'expertise et
participation à des groupes de travail

Travaux et activités de développement

Autres compétences informatiques

Autres renseignements