Goran Frehse (ENSTA ParisTech) ran a seminar at IRT SystemX on February on the following topic « Formal Verification with Reachability » from 2pm to 3.30pm.
Abstract :
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.
Biography :
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 :