Modelling and verification for swarm robotics

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

doi:10.1007/978-3-319-98938-9_1

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 proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings
Publisher	Springer
Pages	1-19
Number of pages	19
Volume	11023 LNCS
ISBN (Print)	9783319989372
DOIs	https://doi.org/10.1007/978-3-319-98938-9_1
Publication status	Published - 1 Jan 2018
Event	14th International Conference on Integrated Formal Methods, IFM 2018 - Maynooth, Ireland Duration: 5 Sept 2018 → 7 Sept 2018

Publication series

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

Conference

Conference	14th International Conference on Integrated Formal Methods, IFM 2018
Country/Territory	Ireland
City	Maynooth
Period	5/09/18 → 7/09/18

Access to Document

10.1007/978-3-319-98938-9_1

Cite this

Cavalcanti, A., Miyazawa, A., Sampaio, A., Li, W., Ribeiro, P., & Timmis, J. (2018). Modelling and verification for swarm robotics. In Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings (Vol. 11023 LNCS, pp. 1-19). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11023 LNCS). Springer. https://doi.org/10.1007/978-3-319-98938-9_1

@inproceedings{3d924bb1dbb54a97a3b96bac9c7448c5,

title = "Modelling and verification for swarm robotics",

abstract = "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.",

author = "Ana Cavalcanti and Alvaro Miyazawa and Augusto Sampaio and Wei Li and Pedro Ribeiro and Jon Timmis",

year = "2018",

month = jan,

day = "1",

doi = "10.1007/978-3-319-98938-9_1",

language = "English",

isbn = "9783319989372",

volume = "11023 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "1--19",

booktitle = "Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings",

address = "Germany",

note = "14th International Conference on Integrated Formal Methods, IFM 2018 ; Conference date: 05-09-2018 Through 07-09-2018",

}

Cavalcanti, A , Miyazawa, A, Sampaio, A, Li, W, Ribeiro, P & Timmis, J 2018, Modelling and verification for swarm robotics. in Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings. vol. 11023 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11023 LNCS, Springer, pp. 1-19, 14th International Conference on Integrated Formal Methods, IFM 2018, Maynooth, Ireland, 5/09/18. https://doi.org/10.1007/978-3-319-98938-9_1

Modelling and verification for swarm robotics. / Cavalcanti, Ana ; Miyazawa, Alvaro; Sampaio, Augusto et al.
Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings. Vol. 11023 LNCS Springer, 2018. p. 1-19 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11023 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Modelling and verification for swarm robotics

AU - Cavalcanti, Ana

AU - Miyazawa, Alvaro

AU - Sampaio, Augusto

AU - Li, Wei

AU - Ribeiro, Pedro

AU - Timmis, Jon

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85053130476&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-98938-9_1

DO - 10.1007/978-3-319-98938-9_1

M3 - Conference contribution

AN - SCOPUS:85053130476

SN - 9783319989372

VL - 11023 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1

EP - 19

BT - Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings

PB - Springer

T2 - 14th International Conference on Integrated Formal Methods, IFM 2018

Y2 - 5 September 2018 through 7 September 2018

ER -

Cavalcanti A , Miyazawa A, Sampaio A, Li W, Ribeiro P, Timmis J. Modelling and verification for swarm robotics. In Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings. Vol. 11023 LNCS. Springer. 2018. p. 1-19. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-98938-9_1

Modelling and verification for swarm robotics

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this