Model-Based Engineering for Robotics with RoboChart and RoboTool

TY - GEN

T1 - Model-Based Engineering for Robotics with RoboChart and RoboTool

AU - Cavalcanti, Ana

AU - Attala, Ziggy

AU - Baxter, James

AU - Miyazawa, Alvaro

AU - Ribeiro, Pedro

N1 - 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.

PY - 2023/11/5

Y1 - 2023/11/5

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85177231933&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-43678-9_4

DO - 10.1007/978-3-031-43678-9_4

M3 - Conference contribution

AN - SCOPUS:85177231933

SN - 9783031436772

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 106

EP - 151

BT - Formal Methods for an Informal World - ICTAC 2021 Summer School, Virtual Event, Tutorial Lectures

A2 - Cerone, Antonio

PB - Springer Science and Business Media Deutschland GmbH

T2 - 18th International Colloquium on Theoretical Aspects of Computing , ICTAC 2021

Y2 - 1 September 2021 through 7 September 2021

ER -