Recherche

Principales thématiques de recherche :

  • Spécification formelle des systèmes d’information
  • Modélisation et vérification des propriétés de sécurité
  • Méthode B, langage EB3, vérification, validation, raffinement

Description :

L’objectif de mes travaux consiste à bénéficier des avantages de différentes formes de modélisation complémentaires pour représenter de manière formelle les systèmes d’information (SI). Par exemple, les langages formels de spécification basés sur les transitions d’état, comme le langage B, permettent de bien décrire les structures de données et les propriétés d’invariance du modèle, tandis que les langages formels de spécification basés sur les événements, comme EB3, sont mieux adaptés pour représenter les propriétés dynamiques et, plus généralement, le comportement d’un système. En 2014, j’ai créé un groupe de travail au LACL pour étudier les combinaisons possibles entre ASM et B.

Pour faciliter l’utilisation des méthodes formelles, je me suis intéressé également à la réutilisation (patterns de spécification) et au raffinement. Depuis 2007, je m’intéresse aux problèmes de modélisation et de vérification des propriétés de sécurité fonctionnelle dans les SI. J’ai notamment participé à deux projets de recherche (projet ANR SELKIS et projet CRSNG EB3sec au Canada) sur la modélisation et la dérivation de politiques de sécurité avec des méthodes formelles. Je me suis également intéressé à la définition d’un langage graphique et formel appelé ASTD, qui s’inspire des Statecharts et des opérateurs des algèbres de processus. Mes travaux ont porté récemment sur la définition d’une notion de raffinement en ASTD.

Enfin, je participe depuis novembre 2014 au projet ANR FORMOSE, qui porte sur l’analyse des besoins et la modélisation des systèmes complexes.

Participation à des contrats de recherche :

  • POLUX : POLicy Unified eXpression, projet ANR SETIN, membre uniquement la dernière année en 2010. Coordinateur : F. Cuppens (TELECOM Bretagne). Participants : TELECOM Bretagne, Supélec Rennes Team SSIR, GRIL (Université de Sherbrooke), LACL (Université Paris-Est).
  • EB3sec : spécification et implémentation de systèmes web sécurisés, projet stratégique CRSNG, 2008-2011. Coordinateur : M. Frappier (Université de Sherbrooke). Participants : GRIL (Université de Sherbrooke), LACL (Université Paris-Est), National Bank Financial Group.
  • SELKIS : a development method of secure health care networks information systems – from requirements engineering to implementation, projet ANR ARPEGE, 2009-2012. Coordinatrice : R. Laleau (Université Paris-Est). Participants : LACL (Université Paris-Est), CEDRIC (CNAM), LIG, IFREMMONT, TELECOM Bretagne, SWID, MED.e.COM, CHU Brest.
  • FORMOSE : formal requirements modeling for critical complex systems, method and toolkit, projet ANR SIC, 2014-2019. Coordinatrice : R. Laleau (Université Paris-Est). Participants : LACL (Université Paris-Est), Institut Mines-Telecom, ClearSy, OpenFlexo, Thales.

 

Publicités
%d blogueurs aiment cette page :