Co-verification for robotics: from simulation to verification

Speaker: Pedro Ribeiro Research Fellow, University of York

Tuesday, 6 June 2023, 14:00, 1Z71

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.

Pedro Ribeiro will be visiting the LMF the entire day - interactions welcome.