Cyber-Physical Systems use computation to sense and control physical interaction with the real world. Examples include autonomous robots, drones, and self driving cars. These systems can often been safety critical in nature, meaning that software and hardware components must be demonstrably trustworthy. The use of formal methods is known to greatly improve the quality of software through rigorous mathematical modelling and verification. However, formal methods can often be difficult to apply in, and transfer to, an industrial setting due to the steep learning curve.

In this talk, I will introduce the CyPhyAssure project, which aims to improve software engineering for cyber-physical systems with accessible graphical notations, unifying formal semantics, and verification support. I'll introduce two important notations for assured development: the Structured Assurance Case Meta-model (SACM), and the RoboChart language for robotic controllers. These sophisticated and accessible notations have both tool support in the Eclipse platform, and also mechanised semantics with automated verification support in Isabelle/HOL. I'll describe the main CyPhyAssure technology: Isabelle/UTP, a unified verification tool framework, and Isabelle/SACM, for assurance cases, and their applications. I'll conclude with an industrial case study based around the assurance case for an autonomous underwater vehicle.

Simon Foster is a postdoctoral research fellow at the University of York, UK. He holds an EPSRC-UKRI fellowship called CyPhyAssure, which investigates assurance of cyber-physical systems. His areas of interest include Interactive Theorem Proving with Isabelle/HOL, Formal Semantics, Process Algebra, Assurance Cases, Cyber-Physical Systems, and Robotics. He is the main developer of Isabelle/UTP, a framework for relational semantics and automated verification.