CRADLE researchers showcase work at IEEE Engineering Reliable Autonomous Systems (ERAS) Conference

Controllers for real-world robots are constructed based on expectation models which cannot account for all unexpected events. If unexpected events occur, the robot might either stop working altogether or do something that violates its given mission specification. In this paper, we aim to provide a more principled mechanism for dealing with specifications when encountering the inherent uncertainty of the real-world. We utilise agent-based control of a robotic system wherein a rational agent, programmed using a Belief-Desire-Intention (BDI) agent programming language, acts as a high-level robot controller. This agent is aware of its mission specification and is able to recognise violations of this specification caused by unexpected events. On recognising such a violation, the agent can switch to a more suitable plan. However, if there are no suitable plans, the agent can also weaken its mission specification dynamically. The agent can output not only which parts of the mission specification have been achieved but which parts have been weakened and why.

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.