Mes activités de recherche s’inscrivent dans le domaine du génie logiciel appliqué au développement de systèmes discrets fiables. Elles portent notamment sur l’intégration d’approches sémantiques et ontologiques dans les processus de développement afin d’améliorer la cohérence et la fiabilité des systèmes logiciels, en particulier dans des environnements composés de composants hétérogènes.
Ces travaux s’intéressent à la prise en compte explicite de la sémantique des données et des opérations manipulées par les systèmes. L’objectif est de distinguer et de formaliser la sémantique implicite, généralement portée par les méthodes formelles, de la sémantique explicite liée au contexte d’utilisation. Cette distinction permet de mieux garantir la validité des compositions de systèmes et d’améliorer la robustesse des processus de développement, notamment dans des architectures dynamiques et distribuées.
Mes recherches explorent l’utilisation des méthodes formelles pour la modélisation et le développement de systèmes logiciels. Elles reposent sur des approches fondées sur le raffinement et la preuve, qui permettent de structurer progressivement la conception tout en garantissant la correction des modèles.
Un axe particulier porte sur l’intégration des ontologies dans les méthodes formelles afin d’enrichir la représentation sémantique des systèmes. Cette approche vise à compléter la sémantique implicite des techniques formelles par une sémantique explicite permettant de mieux représenter le contexte et la signification des informations manipulées.
Ces travaux contribuent ainsi à renforcer la capacité des méthodes formelles à modéliser des systèmes complexes, notamment lorsque ceux-ci impliquent des interactions entre composants hétérogènes ou des contextes d’exécution variés.
Une part importante de mes travaux porte sur la modélisation et la vérification de systèmes fondés sur des événements. Dans ce cadre, la méthode Event-B est utilisée pour représenter les systèmes sous forme de modèles d’états et de transitions entre états déclenchées par des événements.
Le développement repose sur l’utilisation du raffinement pour structurer progressivement les modèles et sur la preuve de théorèmes pour vérifier les propriétés fonctionnelles et comportementales des systèmes. Cette approche permet de garantir la correction des systèmes dès les premières étapes de leur conception.
Ces méthodes ont été appliquées à plusieurs problématiques, notamment :
ANR TAPAS (2025-2029) — "Time-Aware Proof ASsistants"
ANR EBRP (2020-2026) — "Event-B Rodin Plus"
ANR IMPEX (2013-2018) — "IMPlicit and EXplicit semantics integration in proof based developments of discrete systems"