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: