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:
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:
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