Model-Based Engineering for Robotics with RoboChart and RoboTool.

Use of simulation to support the design of software for robotic systems is pervasive. Typically, roboticists draw a state machine using an informal notation (not precise or machine checkable) to convey a design and guide the development of a simulation. This involves writing code for a specific simulator (using C, C++, or some proprietary language and API). Verification is carried out using simulation runs and testing the deployed system. The RoboStar technology supports a model-based, rather than this (simulation) code-centered, approach to development. Models are written using domain-specific notations in line with those accepted by roboticists. In this tutorial, we focus on modelling and verification using RoboChart, our design notation, and its tool, called RoboTool. In RoboChart, software controllers are described by timed state machines. The semantics is defined using a process algebra, namely, tock-CSP, which we can use for verification by model checking or theorem proving. Use of RoboChart complements simulation and testing.