RSE2023 talk - Co-verification for robotics: from simulation to verification of hybrid systems

Pedro Ribeiro will be talking about “Co-verification for robotics: from simulation to verification of hybrid systems” at the Robotics Software Engineering Symposium 2023, King’s College London.

Abstract: Robots are expected to play important roles in furthering prosperity, however providing formal guarantees on their (safe) behaviour is not yet fully within grasp given the multifaceted nature of such cyber-physical systems. Simulation, favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how models may be brought together for (co-)verification of system properties, with simulation complementing verification. This will be cast using the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using state-of-the-art model-checkers and theorem provers, such as Isabelle/UTP.