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.

翻译：自主机器人集群的涌现行为对其安全保障构成了重大挑战。保障任务包括遵循标准、认证流程以及执行验证与确认（V&V）方法（如模型检验）。在本研究中，我们提出了一种用于形式化验证与确认自主机器人集群的协同方法，该方法在宏观形式建模、低保真仿真、高保真仿真和真实机器人层面进行定义。我们用于验证的形式化宏观模型，其特点在于采用来自实际仿真的数据，以确保不同集群系统模型的准确性和可追溯性。此外，我们的工作将形式化验证与仿真以及使用真实机器人进行的实验验证相结合。通过这种方式，我们的V&V协同方法旨在增强对证据的可信度，这与单独使用这些方法形成对比。我们通过一个专注于在公共衣帽间内操作的机器人集群的案例研究来探讨我们的方法。