Les travaux scientifiques d’Axel Legay se situent à la rencontre de l’informatique théorique et de ses applications. Ils portent notamment sur les méthodes formelles, la vérification et le test des systèmes logiciels, le Statistical Model Checking, les systèmes cyber-physiques et, plus largement, la cybersécurité.
Cette activité de recherche a donné lieu à plusieurs centaines de publications scientifiques dans des conférences, revues et ouvrages internationaux, ainsi qu’à de nombreuses collaborations avec des équipes de recherche en Belgique et à l’étranger.
Les publications peuvent être téléchargées ici:
Google Scholar — Axel Legay: https://scholar.google.com/citations?user=6sGLpJIAAAAJ
DBLP — Axel Legay: https://dblp.org/pid/52/579.html
ORCID — Axel Legay: https://orcid.org/0009-0003-7633-8008
ScienceDirect / Scopus — Axel Legay: https://www.sciencedirect.com/author/56271160800/axel-legay
alphaXiv — Axel Legay : https://www.alphaxiv.org/@axel-legay
Le reste de la section rappelle quelques un de mes domaines de recherche les plus porteurs.
Vérification des systèmes à espaces d’états infinis : les fondements de mes recherches
Mes premiers travaux de recherche, notamment dans le cadre de ma thèse de doctorat, ont porté sur la vérification formelle des systèmes à espaces d’états infinis. Contrairement aux systèmes dont l’ensemble des configurations possibles est fini, ces systèmes peuvent présenter un nombre infini d’états, ce qui rend particulièrement difficile l’application des méthodes classiques de vérification automatique.
L’objectif de ces recherches était de développer et d’étudier des méthodes mathématiques permettant de raisonner sur le comportement de tels systèmes, d’en analyser les propriétés et de déterminer dans quelles conditions leur vérification pouvait être réalisée automatiquement.
Systèmes de systèmes : vérifier des ensembles complexes et interconnectés
Ces travaux s’inscrivent dans le domaine du Model Checking, à l’intersection de l’informatique théorique, de la logique mathématique et de la vérification des systèmes. Ils ont constitué l’un des fondements scientifiques de mes recherches ultérieures sur la validation des logiciels et des systèmes complexes.
Une autre dimension de mes recherches a concerné les systèmes de systèmes (Systems of Systems), c’est-à-dire des ensembles de systèmes autonomes qui interagissent pour accomplir des objectifs communs. Ces architectures se retrouvent notamment dans les transports intelligents, les infrastructures critiques, les réseaux industriels et les systèmes cyber-physiques.
Leur particularité réside dans le fait que chaque composant peut évoluer indépendamment, tout en participant au fonctionnement global. Cette autonomie, combinée aux interactions entre composants, fait apparaître de nouveaux défis en matière de fiabilité, de sécurité et de vérification.
Mes travaux dans ce domaine se sont intéressés aux méthodes de modélisation, de vérification et de validation de systèmes complexes et distribués, avec pour objectif de mieux comprendre leurs interactions et d’évaluer les propriétés du système global.
Ces recherches prolongent les problématiques abordées dans mes travaux sur le Model Checking et le Statistical Model Checking, en les appliquant à des architectures où la complexité ne provient plus uniquement du nombre d’états possibles, mais également de la multiplicité des composants, de leur autonomie et de leurs interactions.
Du Statistical Model Checking aux systèmes complexes
Une partie importante de ces recherches a été consacrée au Statistical Model Checking (SMC). Cette approche utilise notamment la simulation et des méthodes statistiques pour étudier le comportement de systèmes dont la complexité rend difficile l’utilisation de techniques classiques de vérification exhaustive.
Parmi les publications associées à ce domaine figure notamment « Statistical Model Checking: An Overview », qui présente les principes et les principales applications du Statistical Model Checking.
Ces recherches ont également concerné la vérification de systèmes temps réel et cyber-physiques, UPPAAL SMC, ainsi que différentes techniques de test et de validation de logiciels.
De la vérification à la cybersécurité
Au-delà des méthodes formelles, ces travaux se sont progressivement étendus à des problématiques directement liées à la cybersécurité : analyse de logiciels, détection de comportements malveillants, sécurité des systèmes numériques et étude de systèmes informatiques de plus en plus complexes.
Il existe une continuité entre ces différents domaines. Vérifier un système, rechercher ses comportements inattendus, identifier ses vulnérabilités ou détecter une activité malveillante revient toujours, sous des formes différentes, à essayer de comprendre ce qu’un système peut réellement faire plutôt que ce qu’il est supposé faire.
L’évolution récente de l’intelligence artificielle prolonge naturellement ces questions. L’IA offre de nouveaux outils pour analyser des volumes considérables de données et de logiciels, mais introduit également de nouvelles surfaces d’attaque et de nouveaux problèmes de validation, de sécurité et de confiance.