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 supports the soundness of our approach that the use of CSP operators with priority resolves nondeterminism correctly.

翻译：RoboChart是RoboStar框架中的核心表示法，是一种面向机器人领域、基于状态机且支持定时与概率的领域特定语言。其组件模型支持共享变量及实体间通信，拥有基于通信顺序进程（CSP）的指称语义。交互树（ITrees）作为语义技术，可描述响应式及并发程序与其环境交互的行为。近期ITrees的机械化实现，以及基于ITree的CSP语义和Isabelle/HOL中的Z数学工具集，为RoboChart等富状态过程语言带来了验证与动画的新应用。本文利用ITrees为RoboChart定义新颖的操作语义，在Isabelle中实现该语义，并通过Isabelle的代码生成器生成可验证的可执行动画。我们以自主化学探测器模型和巡逻机器人模型为例进行说明，后者还展现了非确定性并使用了共享变量。通过动画演示，我们呈现了机器人遭遇不同环境输入时化学探测器的两种具体场景，以及校准位置处于走廊不同区段时巡逻机器人的三种具体场景。此外，我们使用CSP精化模型检验器FDR验证了动画场景确实是RoboChart模型CSP指称语义的真迹精化。这支持了我们方法的可靠性，即通过使用带优先级的CSP算子正确消解非确定性。