Title
Property-Driven Design for Robot Swarms: A Design Method Based on Prescriptive Modeling and Model Checking.
Abstract
In this article, 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 who has little scientific or technical support in his activity. Property-driven design aims at providing such scientific and technical support, with many advantages compared to the traditional unstructured approach. 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 step; fourth, the developer implements the desired robot swarm and validates the previous steps. We demonstrate property-driven design using two case studies: aggregation and foraging.
Year
DOI
Venue
2015
10.1145/2700318
TAAS
Keywords
DocType
Volume
Design,Reliability,Verification,Swarm robotics,top-down design,prescriptive modeling,model checking,aggregation,foraging
Journal
9
Issue
ISSN
Citations 
4
1556-4665
1
PageRank 
References 
Authors
0.35
0
4
Name
Order
Citations
PageRank
Manuele Brambilla132515.84
Arne Brutschy225714.19
Marco Dorigo3140311211.61
Mauro Birattari42021146.61