Mohammed Foughali

Mohammed Aristide Foughali

The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. % In particular, it has been shown that the \emph{interval-based} semantics of MTL is strictly more expressive than the \emph{pointwise} one. % These results may suggest that enabling the evaluation of formulae at arbitrary time points \emph{instead of} positions of timed events increases the expressive power of MTL. % In this paper, we formally argue otherwise. % We demonstrate that under standard models of finite or non-Zeno infinite (action-based) timed executions, the interval-based and the pointwise semantics are incomparable, and therefore disprove a twenty-year-old result. % suggesting otherwise. % We then propose a new \emph{mixed} semantics that embeds both the pointwise and the interval-based ones.

Mohammed Foughali, Félix Ingrand, Anthony Mallet

GenoM is an approach to develop robotic software components, which can be controlled, and assembled to build complex applications. Its latest version GenoM3, provides a template mechanism which is versatile enough to deploy components for different middleware without any change in the specification and user code. But this same template mechanism also enables us to automatically synthesize formal models (for two Validation and Verification frameworks) of the final components. We illustrate our approach on a real deployed example of a drone flight controller for which we prove offline real-time properties, and an outdoor robot for which we synthesize a controller to perform runtime verification.