Animation of a patrol robot model

Based on operational semantics of RoboChart using Interaction Trees

Jan 26, 2023

Here we demonstrate the animation of a patrol robot model below using Interaction Trees in Isabelle/HOL.

RoboChart model with nondeterministic choice and shared variables
RoboChart model with nondeterministic choice and shared variables

The corridor for the robot to patrol has three sections, shown below.

Sectioned corridor with soft and hard boundaries
Sectioned corridor with soft and hard boundaries

The Isabelle/HOL theories for the animation can be found here.

Kangfeng (Randall) Ye
Kangfeng (Randall) Ye
Research Associate (Computer Science)

My research interests include probabilistic modelling and verification using formal specification and verification (both model checking and theorem proving) and model-based engineering.