Autonomous Robotic Swarms: A Corroborative Approach for Verification and Validation

TL;DR

The work addresses the challenge of ensuring safety for emergent behaviours in autonomous robotic swarms by proposing a corroborative V&V framework that spans macroscopic formal modelling, low- and high-fidelity simulations, and real-robot experiments. It combines data-driven macroscopic PFSMs with differential equations, uses PRISM CSL properties to verify swarm-level safety properties, and demonstrates the approach on a public cloakroom case study with DOTS robots. The main contributions are the multi-level modelling approach that grounds formal models in simulation data, the integration of formal verification with experimental validation, and an end-to-end demonstration of safety verification across virtual and real swarms. The practical impact lies in increasing confidence in swarm safety through cross-level evidence, guiding design adjustments, and outlining steps toward correct-by-construction swarm controllers for dynamic, real-world environments.

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.

Figures (11)

• Figure 1: A multi-level corroborative approach for V&V of autonomous robotic swarms, illustrated by instantiating Webster2020 in this work.
• Figure 2: Cloakroom arena: carriers are shown as blue squares, robots as circles. The deposit zone along the right wall is shaded light blue. The fire exit non-blocking zone is shaded red in the bottom left, with the buffer zone shaded amber. The fire exit is marked by an X and shaded green.
• Figure 3: Cloakroom: Probabilistic finite state machine model.
• Figure 4: The HF simulator’s graphical interface depicting the initial positions of robots and carriers within the arena boundaries for data collection. The fire exit is shaded green and marked with an X.
• Figure 5: Analysis of LF and HF simulations which show REQ 1 is violated.