CyPhyAssure: compositional safety assurance for cyber-physical systems

The goal of the CyPhyAssure project is to develop a methodology for compositional assurance of autonomous robots.

Funded by: 


Grant: EP/S001190/1

This will be supported by a mechanical safety case platform for robotic multi-models, and associated verification tools. The platform will be based in Isabelle, and will support both construction of arguments and production of supporting evidence from formal verification tools.

We will validate it by application to assurance demonstrators from our industrial partners, and support our technology with an outreach programme. We will mechanise denotational semantics for a number of modelling languages using our Isabelle/UTP framework, which will facilitate the production of verification tools.

Featured researcher

Dr Simon Foster

Simon's research interests include verification, theorem proving (Isabelle/HOL, Agda), formal semantics, unifying theories of programming and cyber-physical systems.

View profile