I am mainly interested in rigorous modeling and verification of real-world systems. I focus on automatizing the modeling and verification of specifications deployed on real systems, as to render formal methods accessible to non-expert practitioners.
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 & JSA 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 am 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.