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.

翻译：对群体涌现行为进行建模与表征，在"可信性保证"方面可能面临重大挑战。可信性保证任务涵盖标准遵循、认证流程以及验证与确认方法的执行（如模型检验）。本研究提出一种整体性、多层级的建模方法，用于对自主机器人群体进行形式化验证与确认，该方法在宏观形式化建模、低保真仿真、高保真仿真和真实机器人四个层级进行定义。我们用于验证的形式化宏观模型以实际仿真数据为特征，确保不同系统模型间的准确性与可追溯性。此外，本研究将形式化验证与涉及真实机器人的实验验证相结合。通过这种方式，我们的协同验证与确认方法旨在增强证据的可信度，这与单独使用这些方法形成对比。我们通过一个聚焦于公共衣帽间内机器人群体运行的案例研究来探讨本方法。