RoboStar and RoboTool tutorial at SBMF 2022

On the 8th of December 2022, Alvaro Miyazawa delivered a tutorial on “RoboStar and RoboTool: Software Engineering for Robotics using Formal Methods” at the 25th Brazilian Symposium on Formal Methods.

Abstract

While the development of robotics is rich in artefacts such as informal state machines, block diagrams, kinematic equations, simulations, and architectural patterns, these artefacts are either informal or only used in very specific stages of development. The RoboStar group aims to make formal models central to the field of robotics and has developed several formal diagrammatic domain-specific notations tailored to different aspects of robotic applications at different levels of abstraction. These notations are connected via their formal semantics and precise notions of refinement, and support a number of analysis techniques. In this tutorial, I will present some of these notations using our tool, RoboTool, and illustrate some of the analyses and transformations that can be performed automatically.

This tutorial will cover the following topics:

• Modelling with RoboChart;
• Specifying assertions with RoboCert;
• Verifying RoboChart models with FDR4 and PRISM;
• Generating RoboSim d-models for Simulation;
• Generating code for simulation and animation;
• Modelling robots with RoboSim p-models;
• Applications of the semantics of RoboSim d-models and p-models.