A Multi-Level Corroborative Approach for Verification and Validation of Autonomous Robotic Swarms

Modelling and characterizing emergent behaviour within a swarm can pose significant challenges in terms of 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 holistic, multi-level modelling 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 characterized by data derived from actual simulations, ensuring both accuracy and traceability across different system models. Furthermore, our work combines formal verification with experimental validation involving 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. Swarm robotics offers a method for coordinating a large number of robots, inspired by swarm behaviours in nature [1]. The collective behaviours of a swarm are not directly engineered into the system. Rather, they arise due to interactions among individual robots and their environment, called emergent behaviour [2].