Modelling and verification of timed robotic controllers

Pedro Ribeiro*, Alvaro Miyazawa, Wei Li, Ana Cavalcanti, Jon Timmis

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Proceeding (Non-Journal item)

11 Citations (SciVal)


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.

Original languageEnglish
Title of host publicationIntegrated Formal Methods - 13th International Conference, IFM 2017, Proceedings
EditorsSteve Schneider, Nadia Polikarpova
PublisherSpringer Nature
Number of pages16
ISBN (Print)9783319668444
Publication statusPublished - 2017
Event13th International Conference on Integrated Formal Methods, IFM 2017 - Turin, Italy
Duration: 20 Sept 201722 Sept 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10510 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Conference on Integrated Formal Methods, IFM 2017
Period20 Sept 201722 Sept 2017


  • CSP
  • Process algebra
  • Refinement
  • Robotics
  • Semantics

Cite this