Formally Verified Animation for RoboChart using Interaction Trees
Kangfeng Ye, Simon Foster, Jim Woodcock
TL;DR
This work provides a formally verified operational semantics for RoboChart by embedding it into Interaction Trees (ITrees) and mechanising the theory in Isabelle/HOL, enabling executable animations through Isabelle's code generator. By extending CSP with operators such as generalised choice, interrupt, exception, and priority-based hiding/renaming, it resolves nondeterminism statically and supports shared variables across RoboChart components. The authors instantiate the semantics for two robotic models (autonomous chemical detector and patrol robot) and demonstrate animation-driven exploration alongside FDR-based refinement checks that confirm the animations are true trace refinements of CSP denotations. This approach yields verifiable, executable RoboChart animations and points toward automated semantics generation and broader applicability to robotic software verification and ROS integration. Overall, the work advances executable semantics for rich state-rich languages in robotics and provides a practical path from formal modelling to validated animation.
Abstract
RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has formal denotational semantics given in CSP. The semantic technique of Interaction Trees (ITrees) represents behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisation of ITrees, along with ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL, bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this paper, we use ITrees to give RoboChart novel operational semantics, implement it in Isabelle, and use Isabelle's code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector model and a patrol robot model additionally exhibiting nondeterminism and using shared variables. With animation, we show two concrete scenarios for the chemical detector when the robot encounters different environmental inputs and three concrete scenarios for the patrol robot when its calibrated position is in different sections of a corridor. We also verify that the animated scenarios are truly trace refinements of the CSP denotational semantics of the RoboChart models using FDR, a refinement model checker for CSP. This ensures that our approach to resolving nondeterminism using CSP operators with priority is sound and correct.