@article{0232c04016634047ae33cd82f1ff80bd,
title = "RoboChart: modelling and verification of the functional behaviour of robotic applications",
abstract = "Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of constructs suitable for both modelling robotic applications and supporting verification via model checking and theorem proving. Our goal is to support roboticists in writing models and applying modern verification techniques using a language familiar to them. To that end, we present RoboChart, a domain-specific modelling language based on UML, but with a restricted set of constructs to enable a simplified semantics and automated reasoning. We present the RoboChart metamodel, its well-formedness rules, and its process-algebraic semantics. We discuss verification based on these foundations using an implementation of RoboChart and its semantics as a set of Eclipse plug-ins called RoboTool.",
keywords = "CSP, Domain-specific language for robotics, Formal semantics, Model checking, Process algebra, State machines, Timed properties",
author = "Alvaro Miyazawa and Pedro Ribeiro and Wei Li and Ana Cavalcanti and Jon Timmis and Jim Woodcock",
note = "Funding Information: This work is funded by the EPSRC Grants EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering. No new primary data was created during this study. We thank James Baxter and Augusto Sampaio for many suggestions to improve RoboChart and this paper. The icons used in RoboChart have been made by Sarfraz Shoukat, Freepik, Google, Icomoon and Madebyoliver from www.flaticon.com , and are licensed under CC 3.0 BY. 1 Available for download at www.cs.york.ac.uk/circus/RoboCalc/robotool/ . 2 www.itemis.com/en/yakindu/state-machine . 3 doc.aldebaran.com/1-14/software/choregraphe . 4 lego.com/mindstorms/downloads/download-software . 5 Omitted here, but available at www.cs.york.ac.uk/circus/RoboCalc/case_studies/ . 6 www.cs.york.ac.uk/circus/RoboCalc/robotool/ . 7 www.eclipse.org . 8 www.eclipse.org/xtext . 9 www.eclipse.org/sirius . 10 A dialect of Java ( www.eclipse.org/xtend/ ). 11 www.cs.ox.ac.uk/projects/fdr/ . 12 www.ros.org . Funding Information: This work is funded by the EPSRC Grants EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering. No new primary data was created during this study. We thank James Baxter and Augusto Sampaio for many suggestions to improve RoboChart and this paper. The icons used in RoboChart have been made by Sarfraz Shoukat, Freepik, Google, Icomoon and Madebyoliver from www.flaticon.com , and are licensed under CC 3.0 BY. Publisher Copyright: {\textcopyright} 2019, The Author(s).",
year = "2019",
month = oct,
day = "1",
doi = "10.1007/s10270-018-00710-z",
language = "English",
volume = "18",
pages = "3097--3149",
journal = "Software and Systems Modeling",
issn = "1619-1366",
publisher = "Springer Nature",
number = "5",
}