Mohammed Foughali, PhD

Google Scholar      dblp








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.