Model-Based Engineering for Robotics with RoboChart and RoboTool

Ana Cavalcanti*, Ziggy Attala, James Baxter, Alvaro Miyazawa, Pedro Ribeiro

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish
Title of host publicationFormal Methods for an Informal World - ICTAC 2021 Summer School, Virtual Event, Tutorial Lectures
EditorsAntonio Cerone
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages46
ISBN (Electronic)9783031436789
ISBN (Print)9783031436772
Publication statusPublished - 5 Nov 2023
Event18th International Colloquium on Theoretical Aspects of Computing , ICTAC 2021 - Virtual, Online
Duration: 1 Sept 20217 Sept 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13490 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference18th International Colloquium on Theoretical Aspects of Computing , ICTAC 2021
CityVirtual, Online

Bibliographical note

Funding Information:
The work reported here is funded by the Royal Academy of Engineering grant CiET1718/45, UK EPSRC grants EP/M025756/1 and EP/R025479/1, and UKRI TAS programme (verifiability and resilience). We are grateful to the ICTAC organisers for the opportunity to present and write this tutorial. We also thank Augusto Sampaio for very helpful and detailed comments. Finally, we are grateful to all members of the RoboStar group, who directly or indirectly contribute to the realisation of the vision described here.

Publisher Copyright:
© 2023, The Author(s), under exclusive licence to Springer Nature Switzerland AG.

Cite this