@inproceedings{df31a7fb2d13454786957302284449ea,
title = "Modelling and verification of timed robotic controllers",
abstract = "Designing robotic systems can be very challenging, yet controllers are often specified using informal notations with development driven primarily by simulations and physical experiments, without relation to abstract models of requirements. The ability to perform formal analysis and replicate results across different robotic platforms is hindered by the lack of well-defined formal notations. In this paper we present a timed state-machine based formal notation for robotics that is informed by current practice. We motivate our work with an example from swarm robotics and define a compositional CSP-based discrete timed semantics suitable for refinement. Our results support verification and, importantly, enable rigorous connection with sound simulations and deployments.",
keywords = "CSP, Process algebra, Refinement, Robotics, Semantics",
author = "Pedro Ribeiro and Alvaro Miyazawa and Wei Li and Ana Cavalcanti and Jon Timmis",
note = "Funding Information: Acknowledgments. This work is funded by EPSRC grant EP/M025756/1. No new primary data was created during this study. Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 13th International Conference on Integrated Formal Methods, IFM 2017 ; Conference date: 20-09-2017 Through 22-09-2017",
year = "2017",
doi = "10.1007/978-3-319-66845-1_2",
language = "English",
isbn = "9783319668444",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Nature",
pages = "18--33",
editor = "Steve Schneider and Nadia Polikarpova",
booktitle = "Integrated Formal Methods - 13th International Conference, IFM 2017, Proceedings",
address = "Switzerland",
}