Computer Aided Formal Design of Swarm Robotics Algorithms

TL;DR

This paper demonstrates how formal methods, specifically the PACTOLE library and COQ proof assistant, can be used early in the design of swarm robotics protocols to ensure correctness for real-world problems.

Contribution

It introduces a formal design approach for swarm robotics protocols that ensures correctness from the outset, applied to real-world scenarios.

Findings

Successfully designed protocols with formal correctness proofs

Applied formal methods to real-world swarm robotics case study

Showed early-stage formal design improves protocol reliability

Abstract

Previous works on formally studying mobile robotic swarms consider necessary and sufficient system hypotheses enabling to solve theoretical benchmark problems (geometric pattern formation, gathering, scattering, etc.). We argue that formal methods can also help in the early stage of mobile robotic swarms protocol design, to obtain protocols that are correct-by-design, even for problems arising from real-world use cases, not previously studied theoretically. Our position is supported by a concrete case study. Starting from a real-world case scenario, we jointly design the formal problem specification, a family of protocols that are able to solve the problem, and their corresponding proof of correctness, all expressed with the same formal framework. The concrete framework we use for our development is the PACTOLE library based on the COQ proof assistant.