Cyber-physical systems share variables with the physical environment. Here, we are modelling the state space of an autonomous marine vehicle (AMV). It has continuous variables to model position, velocity, and acceleration, which are all two dimensional vectors, and also the heading and linear speed. The discrete variables model a list of waypoint coordinates, an obstacle register, and the requested speed and heading set points. We support modelling and verification of Cyber-Physical systems using the Hybrid-Verification session.

Diffential equations are used to model physical phenomena. They characterise how measured quantities like position, velocity, temperature, and flow change over time. A system of ordinary differential equations assigned derivatives to each continuous variable, which gives the rate of change. In Isabelle/UTP, support an intuitive notation for ODEs, and can handle advanced mathematical concepts, like vectors and transcendental functions, through the powerful HOL-Analysis library. Here, we assign derivatives to each of the continuous variables.

As usual, we can verify the behaviour of a CPS by finding suitable invariants, which must hold of both the discrete controller and the system of ODEs. Verifying the latter is supported by the differential induction technique, made famous by André Platzer in his theorem prover KeYmaera X. Differential induction allows us to prove invariants of ODEs without requiring a solution to the equations. Here, we use a proof method called dInduct_mega to prove invariants of the ODEs. You can read more about our verification tool in the following linked publication from FM 2021.