Overviewing the State Machine, Verification and Deadlock Freedom components of RoboChart
by Marietta Galea
Developing software for autonomous and robotic systems requires modelling techniques that are both expressive and amenable to rigorous verification. RoboChart is a domain-specific modelling language developed by the RoboStar team that enables robotic controllers to be specified independently of the underlying hardware using timed state machines. Its formal foundations make it possible to reason about important correctness properties early in the development process. This talk introduces the core concepts of RoboChart and demonstrates how robotic behaviour can be modelled through controllers, modules, and timed state machines. We will also provide a high-level overview of the verification pipeline, explaining how RoboChart models are translated into formal semantic models that enable automated verification of properties such as deadlock freedom. The talk is intended as an introduction to the RoboStar framework and requires no prior knowledge of formal methods.
Links: RoboChart Manual