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.

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