By the same authors

From the same journal

From the same journal

Verified simulation for robotics

Research output: Contribution to journalArticlepeer-review



Publication details

JournalScience of Computer Programming
DateAccepted/In press - 7 Jan 2019
DateE-pub ahead of print (current) - 11 Jan 2019
Number of pages42
Early online date11/01/19
Original languageEnglish


Simulation is a favoured technique for analysis of robotic systems. Currently, however, simulations are programmed in an ad hoc way, for specific simulators, using either proprietary languages or general languages like C or C++. Even when a higher-level language is used, no clear relation between the simulation and a design model is established. We describe a tool-independent notation called RoboSim, designed specifically for modelling of (verified) simulations. We describe the syntax, well-formedness conditions, and semantics of RoboSim. We also show how we can use RoboSim models to check if a simulation is consistent with a functional design written in a UML-like notation akin to those often used by practitioners on an informal basis. We show how to check whether the design enables a feasible scheduling of behaviours in cycles as needed for a simulation, and formalise implicit assumptions routinely made when programming simulations. We develop a running example and three additional case studies to illustrate RoboSim and the proposed verification techniques. Tool support is also briefly discussed. Our results enable the description of simulations using tool-independent diagrammatic models amenable to verification and automatic generation of code.

Bibliographical note

© 2019 Elsevier B.V. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.

    Research areas

  • State machines, Process algebra, CSP, Semantics, Refinement

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations