Autonomous Robotic Swarms: A Corroborative Approach for Verification and Validation

TL;DR

This paper presents a corroborative approach combining formal verification, simulations, and real-robot experiments to enhance safety assurance of autonomous robotic swarms, addressing challenges in verification and validation.

Contribution

It introduces a multi-level V&V framework for robotic swarms, integrating formal models, simulations, and real-world testing for improved reliability.

Findings

Formal models derived from simulations improve accuracy.

Combining V&V methods increases confidence in safety evidence.

Case study demonstrates practical applicability in a public environment.

Abstract

The emergent behaviour of autonomous robotic swarms poses a significant challenge to their safety assurance. Assurance tasks encompass adherence to standards, certification processes, and the execution of verification and validation (V&V) methods, such as model checking. In this study, we propose a corroborative approach for formally verifying and validating autonomous robotic swarms, which are defined at the macroscopic formal modelling, low-fidelity simulation, high-fidelity simulation, and real-robot levels. Our formal macroscopic models, used for verification, are characterised by data derived from actual simulations to ensure both accuracy and traceability across different swarm system models. Furthermore, our work combines formal verification with simulations and experimental validation using real robots. In this way, our corroborative approach for V&V seeks to enhance confidence in the evidence, in contrast to employing these methods separately. We explore our approach through a case study focused on a swarm of robots operating within a public cloakroom.