In this seminar, I will describe the research at the RoboStar centre in York, UK, and our approach to rigorous engineering of robotic systems underpinned by formal verification. Our tools combine an accessible SysML-like notation (RoboChart) with formal process-algebraic semantics, to support robotic software development with a high level of assurance. I will explain how the Isabelle proof assistant is being used to support this approach with a unified set of verification tools. We focus on two libraries we have developed: Isabelle/ITrees, which supports abstract yet executable semantics based on the Interaction Tree formalism, and IsaVODEs, which supports modelling of cyber-physical systems with discrete controllers, and a continuous physical model.

Simon Foster is a Senior Lecturer (Associate Professor) at the University of York, and member of the RoboStar Centre of Excellence on Software Engineering for Robotics. His primary research applies theorem proving to formal verification and he leads the development of Isabelle/UTP, a practical theorem prover for heterogeneous systems. He has applied Isabelle/UTP to verification tools for autonomous and mobile robots, cyber-physical systems, process algebras, and reactive programs. He has also developed Isabelle/SACM, an interactive tool for assurance cases with evidence coming from multiple formal verification tools in Isabelle. He gained his PhD at the University of Sheffield in 2010, which developed a timed process algebra for Web service composition semantics. Since then, he has worked on a variety of EU and EPSRC projects using diverse aspects of formal verification and assurance. He teaches logic and formal proof to undergraduate students, and assured software engineering to industrialists