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.
CITATION STYLE
Ribeiro, P., Miyazawa, A., Li, W., Cavalcanti, A., & Timmis, J. (2017). Modelling and verification of timed robotic controllers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10510 LNCS, pp. 18–33). Springer Verlag. https://doi.org/10.1007/978-3-319-66845-1_2
Mendeley helps you to discover research relevant for your work.