Research

Today

I am mainly interested in rigorous modeling and verification of real-world, real-time systems. One major challenge I enjoy tackling, one theorem/model/artefact at a time, is how to reconcile scalability with correctness and user-friendliness. A major part of my research is based on timed automata and timed logics.

Currently, my research activities gravitate around three major axes:

Hybrid approaches for the scalable verification of multicore real-time systems. My most advanced work on the topic, for the moment, is described in the JSA 2023 and COMPSAC 2024 publications, joint work with P-E Hladik, A. Züpke, M. Mikučionis and M. Zhang, see the Publications section.
Runtime monitoring of real-time systems.
Safe AI-enabled CPS, within the CyPhAI project.

Recently, I took some interest in computing education research. See the Koli Calling 2023 paper under the Publications section.

L’histoire ancienne

During my PhD, I had worked within the RIS team at LAAS-CNRS on semantisizing the robotic framework GenoM3, based on which I developed several mathematically proven translations to major formal verification frameworks, namely Fiacre/TINA, UPPAAL, UPPAAL-SMC, and Real-Time BIP (RT-BIP). This work involved several partners from different universities, laboratories and companies: the VERTICS team (LAAS-CNRS), the Verimag Lab, the FMAES team (University of Mälardalen) and EasyMile Toulouse, and resulted in templates that automatically translate any GenoM3 specification into the aforementioned formal environments. The case studies ranged from a drone flight control to a terrestrial navigation, on which various real-time properties were verified using different techniques (model checking, statistical model checking and runtime verification). See my PhD thesis, Publications and Artefacts for more details.

A summary of my postdoctoral research activities is given below.

I participated in the DSAAM decentralized simulation framework for cyber-physical systems, developed within the RIS team at LAAS-CNRS. My contribution to the framework consisted in proposing rigorous formal syntax and semantics and the development of liveness proofs. See the QRS paper under Publications for more details.
I pioneered a binary-search-based method that allows extending timed automata models of robotic applications with dynamic-priority schedulers in a (more) scalable way. See my two papers on the subject (DETECT 2019 & JSA 2020 in Publications) and the Artefacts section for more details.
I was the lead contributor to a research activity on formal execution and runtime verification of robotic applications using the BIP real-time engine. In particular, this work relies on a fully automatic translation of robotic specifications into RT-BIP, executing the resulting RT-BIP models on a real robotic platform, and verifying timed properties at runtime using RT-BIP monitors. See the MEMOCODE paper under Publications and the videos links under Artefacts for more details.
I was the main investigator of Verimag/Université Grenoble Alpes in the European ADE project. Using the BIP Toolset, I developed, validated and integrated the Fault Detection, Isolation and Recovery (FDIR) components to embark on the planetary rover used in ADE. See the i-Sairas paper under Publications for more details.
I proposed a hybrid approach combining schedulability analysis and statistical model checking techniques to rigorously verify autonomous aerial robots. See the RTCSA paper under Publications for more details.
I played a major role in a research effort pertaining to contract-based verification of model transformations in Model-Driven Engineering approaches. In particular, I proposed a formal, yet engineer friendly environment for a lightweight verification of some “correctness” properties of transformations from AADL. See the SAC paper under Publications for more details.