Property-driven design for robot swarms: A design method based on prescriptive modeling and model checking

Manuele Brambilla, Marco Dorigo, and Mauro Birattari. 2014


This page contains all supplementary information that was not possible to included in the paper.

Table of Contents
  1. Paper Abstract
  2. Aggregation: Simulation Videos
  3. Aggregation: Real Robots Videos
  4. Foraging: Simulation Videos
  5. Foraging: Real Robots Videos

Paper Abstract

In this paper, we present property-driven design, a novel top-down design method for robot swarms based on prescriptive modeling and model checking. Traditionally robot swarms have been developed using a code-and-fix approach: in a bottom-up iterative process, the developer tests and improves the individual behaviors of the robots until the desired collective behavior is obtained. The code-and-fix approach is unstructured and the quality of the obtained swarm depends completely on the expertise and ingenuity of the developer. Property-driven design is composed of four phases: first, the developer formally specifies the requirements of the robot swarm by stating its desired properties; second, the developer creates a prescriptive model of the swarm and uses model checking to verify that this prescriptive model satisfies the desired properties; third, using the prescriptive model as a blueprint, the developer implements a simulated version of the desired robot swarm and validates the prescriptive model developed in the previous steps; fourth, the developer implements the desired robot swarm and validates the previous steps. In this paper, we demonstrate property-driven design using two case studies: aggregation and foraging.


Keywords: Swarm robotics, Swarm engineering, Top-down design, Aggregation, Foraging



Aggregation: Simulation Videos

All the simulated experiments have been performed using the ARGoS simulator. All videos are in real time.



Simulated video with 10 robots


Download this video.




Simulated video with 20 robots

Download this video.




Simulated video with 50 robots

Download this video.




Aggregation: Real Robots Videos

The real robots experiments have been performed using the e-puck robot. All videos are in real time.



Video of an experiment with 10 e-pucks

Download this video.



Foraging: Simulation Videos

All the simulated experiments have been performed using the ARGoS simulator.



Simulated video with 10 robots, O=6


Download this video.




Simulated video with 20 robots, O=6

Download this video.




Simulated video with 50 robots, O=6

Download this video.

Simulated video with 100 robots, O=6

Download this video.




Foraging: Real Robots Videos

The real robots experiments have been performed using the e-puck robot.



Video of an experiment with 20 e-pucks, O=6

Download this video.