RoboChart is a domain-specific language for modelling autonomous and mobile robots. It employs a graphical modelling paradigm, similar to UML and SysML. A RoboChart model consists of (1) a robotic platform, which abstracts the hardware; and (2) one or more software controllers that describe the robot's behaviour. The behaviour of controllers are described using a state machine notation, as shown to the right.

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 stm command generates a state machine graph, and uses it to compute its denotational semantics as a reactive program. This can then be used for symbolically checking refinements. The implementation can be found in the RoboChart-Isabelle GitHub repository.