Goran Frehse (ENSTA-IPP) s’est rendu à l’IRT SystemX le 6 février, sur le site de Nano-Innov, pour animer un séminaire sur le thème « Formal Verification with Reachability ».
Ensuring the safety of dynamical systems in complex and uncertain environments is challenging. A mathematically rigorous way to ensure safety is to first create a formal model of the system and then to compute the states that are reachable in this model. Provided that the model is conservative, a safe model implies that the true system is also safe. In this talk, we give an overview of a state-of-the art technique for such a reachability analysis. We discuss some of the challenges and illustrate some applications in recent case studies.
Goran Frehse received a Diploma in electrical engineering and information technology from Karlsruhe Institute of Technology and a PhD in computer science from Radboud University Nijmegen. From 2006 to 2018, he was an associate professor at the University Grenoble Alpes, holding a research fellowship (chaire) from 2016. Since 2018, he is an associate professor at ENSTA ParisTech. He is the architect and lead developer of two well-known model checking tools for hybrid and cyber-physical systems, PHAVer and SpaceEx.
En savoir plus :