  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.
