Formally Verified Animation for RoboChart Using Interaction Trees

Kangfeng Ye*, Simon Foster, Jim Woodcock

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 a formal denotational semantics given in CSP. Interaction Trees (ITrees) is a semantic technique to represent behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisations 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 a 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. With animation, we show two concrete scenarios when the robot encounters different environmental inputs.

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Proceedings
EditorsAdrian Riesco, Min Zhang
Number of pages17
ISBN (Electronic)9783031172441
ISBN (Print)9783031172434
Publication statusPublished - 10 Oct 2022
Event23rd International Conference on Formal Engineering Methods, ICFEM 2022 - Madrid, Spain
Duration: 24 Oct 202227 Oct 2022

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Conference on Formal Engineering Methods, ICFEM 2022

Bibliographical note

This work is funded by the EPSRC projects CyPhyAssure (Grant EP/S001190/1), RoboCalc (Grant EP/M025756/1), and RoboTest (Grant EP/R025479/1). The icons used in RoboChart have been made by Sarfraz Shoukat, Freepik, Google, Icomoon and Madebyoliver from www.flaticon. com, and are licensed under CC 3.0 BY.

© Springer Nature Switzerland AG 2022. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details


  • Interaction Trees
  • CSP
  • Theorem proving
  • RoboChart
  • Code Generation
  • Robotic software
  • Operational semantics

Cite this