Mes recherches explorent l'utilisation des méthodes formelles pour la modélisation et le développement des systèmes/logiciels critiques. Elles reposent sur des approches fondées sur l'utilisation du raffinement, permettent de structurer la conception, et de la preuve, comme moyen de vérifier la correction des modèles obtenus.
Un axe particulier porte sur l'intégration des modèles de données et des ontologies dans les processus de développement afin d'améliorer la cohérence et la fiabilité des systèmes/logiciels évoluant dans des environnements hétérogènes. Cette approche vise à compléter la sémantique implicite des techniques formelles par une sémantique explicite permettant de mieux représenter le contexte dans lequel évolue les systèmes/logiciels étudiés.
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 dans des contextes d'exécution variés.
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"
ANR EWOK-HUB (2007-2010) — "Environnemental Web Ontology Knowledge HUB"
RNRT VERBATIM (2004-2006) — "VERication Biformelle et Automatisation du Test d'Interfaces Multimodales"
Rodin platform — Open tool platform for the cost effective rigorous development of dependable complex software systems services. This platform is based on the Event-B formal method and provides natural support for refinement and mathematical proof.
OntoEventB Rodin plugin — The OntoEventB Rodin plugin automatically generates Event-B formalisations of ontologies-described in ontology description languages such as OWL or OntoML-using set theory and predicate logic.
BPEL2B Rodin plugin — The BPEL2B Rodin plugin automatically generates Event-B formalisations of Web service compositions—described in the BPEL language—using set theory and predicate logic.
Paul Somson — Modèle temporel hiérarchique pour Event-B — 11/2025-../... — encadrée avec Frédéric MALLET, Frédéric BOULANGER, et Maris-Agnès PERALDI-FRATI
Nicolas Méric — Conception et
Implémentation d'un Environnement d'Ontologie pour des Bibliothèques Formelles — 2020-2024 —
encadrée avec Burkhart WOLFF
Linda Mohand Oussaïd —
Conception et vérification formelles des interfaces homme-machine multimodales — 2011-2014 —
encadrée avec Yamine AIT AMEUR
Guillaume Verdier — 2020/2021
Linda Mohand Oussaïd — 2018/2019
PhD thesis — Modelling and verifying services compositions — Le laboratoire LIAS de Poitiers et l'école d'ingénieurs ISAE-ENSMA de Poitiers — 2010
Master thesis — Animating Event-B Models by Formal Data Models — Le laboratoire LIAS de Poitiers et l'Université de Poitiers — 2007
Engineer thesis — Formal Validation and Verification of Multimodal Interactive Systems — Le laboratoire LIAS de Poitiers et l'école d'ingénieurs ESI d'Alger — 2005