Modelling and verification for swarm robotics

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

*Corresponding author for this work

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

7 Citations (Scopus)


RoboChart is a graphical domain-specific language, based on UML, but tailored for the modelling and verification of single robot systems. In this paper, we introduce RoboChart facilities for modelling and verifying heterogeneous collections of interacting robots. We propose a new construct that describes the collection itself, and a new communication construct that allows fine-grained control over the communication patterns of the robots. Using these novel constructs, we apply RoboChart to model a simple yet powerful and widely used algorithm to maintain the aggregation of a swarm. Our constructs can be useful also in the context of other diagrammatic languages, including UML, to describe collections of arbitrary interacting entities.

Original languageEnglish
Title of host publicationIntegrated Formal Methods - 14th International Conference, IFM 2018, Proceedings
EditorsCarlo A. Furia, Kirsten Winter
PublisherSpringer Nature
Number of pages19
ISBN (Print)9783319989372
Publication statusPublished - 2018
Event14th International Conference on Integrated Formal Methods, IFM 2018 - Maynooth, Ireland
Duration: 05 Sept 201807 Sept 2018

Publication series

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


Conference14th International Conference on Integrated Formal Methods, IFM 2018
Period05 Sept 201807 Sept 2018


Dive into the research topics of 'Modelling and verification for swarm robotics'. Together they form a unique fingerprint.

Cite this