Isabelle/UTP

Hybrid Computation

Hybrid computation combines the modelling of continuously evolving phenomena, as found in the real-world, with discrete events and transitions that are typically found in digital controllers. In Isabelle/UTP, we have created the hybrid relational calculus, which extends the relational calculus with continuous variables that may be characterised by Ordinary Differential Equations (ODEs). It has operators that allow us to describe the flow of ODEs, interruption of these flows when specific conditions are satisfied, and instantaneous updates to variables, along with the usual operators of imperative programming.

Below, we show a small example of a braking train modelled in Isabelle/UTP, and proof that it stops before travelling 44 metres.