Isabelle/UTP

A verification toolbox for Isabelle/HOL based on Unifying Theories of Programming

View project on GitHub

State Machines

A state machine describes a system using a set of states and transitions between them. Several languages exist for modelling them, includes Harel’s Statecharts and also the RoboChart language, which has been developed specifically for modelling robotic controllers. An example RoboChart is shown below:

GasAnalysis RoboChart

It consist of an initial node (i), final node (F), and a number of other states, some of which have during actions. Transitions between them can be annotated with events that trigger them, and other behaviour that can be executed. For more information, please see the RoboChart reference manual. We have constructed a representation of the underlying meta-model in Isabelle/UTP, so that it is possible to verify state machines:

RoboChart in Isabelle/UTP

The Isabelle/HOL statemachine command generates a state machine graph, and uses it to compute its denotational semantics as a reactive program. This can then be used for symobolically checking refinements.


Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure