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
N1 - Funding Information:
The work mentioned here is supported by the EPSRC grants EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering, and by INES, grants CNPq/465614/2014-0 and FACEPE/APQ/0388-1.03/14.
Funding Information:
RoboChart is supported by RoboTool, which provides facilities for graphical modelling, validation, and automatic generation of C++ simulations. RoboTool automatically generates also the formal semantics of RoboChart models. The semantics definition uses the process algebra CSP [20], and RoboTool also provides a direct connection to the FDR model checker for CSP [10].
Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018
Y1 - 2018
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 Proceeding (Non-Journal item)
AN - SCOPUS:85053130476
SN - 9783319989372
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
A2 - Furia, Carlo A.
A2 - Winter, Kirsten
PB - Springer Nature
T2 - 14th International Conference on Integrated Formal Methods, IFM 2018
Y2 - 5 September 2018 through 7 September 2018
ER -