Mo Foughali, PhD

Google Scholar      dblp

Logo

Biography

Research

Teaching

Publications

Artefacts

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:

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.