Recherche

Principales thématiques de recherche :

• Prise en compte de la sécurité fonctionnelle dans les systèmes d’information
• Étude du passage entre analyse des besoins et spécification formelle
• Spécification formelle multi-paradigme
• Mots-clés : méthode B, Event-B, RODIN, Theory Plugin, langage EB3, ASTD, 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é notamment sur la définition d’une notion de raffinement en ASTD.

Un autre aspect de mes recherches concerne le processus de développement de logiciels. En génie logiciel, la première phase consiste à analyser les besoins du client. Cette étape est cruciale, car les études ont montré qu’une erreur dans la modélisation coûte jusqu’à 200 fois plus chère à réparer dans les étapes ultérieures du développement. La principale difficulté est de spécifier un premier modèle qui corresponde aux attentes du client. Si les méthodes formelles ont apporté des techniques de vérification, de preuve ou d’animation pour garantir la satisfaction de certaines propriétés, elles ne permettent pas de valider le modèle initial le plus abstrait (problématiques liées au passage de l’informel au formel). Un premier travail a consisté à s’inspirer des techniques d’ingénierie des exigences dirigée par les buts, afin de construire les spécifications formelles de plus haut niveau. Un couplage entre un modèle d’exigences exprimé en SysML/KAOS et des spécifications formelles abstraites a été défini. Les langages formels utilisés sont B et Event-B. Ces travaux ont permis de définir une approche de construction de spécifications formelles dirigée par les buts en considérant, dans un premier temps, uniquement les exigences fonctionnelles. Dans le cadre du projet ANR FORMOSE, une étude a été réalisée sur les impacts des buts non-fonctionnels sur les modèles abstraits Event-B obtenus à partir des buts fonctionnels.

Plus récemment, dans le cadre du projet ANR EBRP dont l’objectif est d’étendre Event-B et RODIN pour modéliser des systèmes complexes logiciels, plusieurs études de cas ont été réalisées afin de définir des théories dans le plugin Theory de RODIN.

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.
• EBRP : enhancing EventB and RODIN, projet ANR CE25, 2020-2024. Coordinateur : Y. Ait-Ameur (IRIT). Participants : University of Düsseldorf, LACL (Université Paris-Est), University of Southampton, IRIT (INPT-ENSEEIHT), LORIA (Université de Lorraine), LRI (CentraleSupelec).