Formal Development and Quantitative Assessment of a Resilient Multi-robotic System

Ensuring resilience of multi-robotic systems is a notoriously difficult task. Decentralised architectures and asynchronous communication require powerful modelling techniques to demonstrate system resilience. In this paper, resilience of a multi-robotic system is defined as the ability to achieve goals despite robot failures. We demonstrate how to rigorously specify and verify essential properties of resilience mechanisms of multi-robotic systems by refinement in Event-B. To assess the desired resilience characteristics, we augment our formal models with statistical data and rely on probabilistic verification. The automated support provided by the PRISM model checker allows us to calculate the probability of goal reachability in the presence of robot failures and compare different reconfiguration strategies for selected architectures. We demonstrate our approach by a case study - development and assessment of a cleaning multi-robotic system.