Software engineering for robotics depends on the ability to model and verify the software, hardware, and physical environment of a robotic system. Robots are cyber-physical systems, consisting of a discrete model of the software, and a continuous model of physical phenomena, such as position and velocity. At the RoboStar Centre, we are developing notations, tools, and techniques to support roboticists in developing robotic software that is demonstrably safe and trustworthy.

IsaVODEs is a tool for modelling and verifying cyber-physical systems based on Isabelle/HOL. Its core notation combines discrete programming operators with ordinary differential equations (ODEs), to allow modelling of both software and the physical environment. IsaVODEs particularly benefits from Isabelle’s proof automation, and its implementation of multivariate analysis in the HOL-Analysis package, which provides support for vectors and matrices. In particular, IsaVODEs support verification of non-linear systems through symbolic reasoning.

This tutorial will teach participants how IsaVODEs can be applied to modelling and verification. We will introduce the basics of Isabelle/HOL, and then show how we can automate modelling and verification of imperative programs using Hoare logic. Following this, we will show how dynamics can be modelled using ordinary differential equations, and verify a number of examples, such as a thermostat and an aircraft collision avoidance algorithm, using techniques like differential induction and symbolic solutions to ODEs.

The structure of the tutorial will be four sessions, each consisting of 45 minutes of lecture, followed by 45 minutes of practical. Participants should bring their own laptop to benefit from the practical sessions, and the tools will be made available beforehand.

Recent publication: https://doi.org/10.1007/s10817-024-09709-2

Website: https://isabelle-utp.york.ac.uk/