@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{desai-iccps17,
author = {Ankush Desai and Indranil Saha and Jianqiao Yang and Shaz Qadeer and Sanjit A. Seshia},
title = {Drona: A Framework for Safe Distributed Mobile Robotics},
booktitle = {Proceedings of the 8th International Conference on Cyber-Physical Systems (ICCPS)},
pages = {239--248},
month = "April",
year = {2017},
abstract = {Distributed mobile robotics (DMR) involves teams of
robots navigating in a physical space to achieve tasks in
a coordinated fashion. A major challenge in DMR is to
program the ensemble of robots with formal guarantees
and high assurance of correct operation. To this end,
we introduce Drona, a framework for building reliable
DMR applications.
This paper makes three central contributions: (1) We
present a novel and provably correct decentralized
asynchronous motion planner that can perform on-the-fly
collision-free planning for dynamically generated tasks.
Moreover, the motion planner is the first to take into
account the fact that distributed robots may have clocks
that are only synchronized up to a tolerance, i.e., they
are almost synchronous; (2) We formalize the DMR
system as a mixed-synchronous system, and present a
sound abstraction-based verification approach for DMR
systems, and (3) Drona provides a state-machine based
language for safe event-driven programming of a DMR
system and the generated C code by the compiler can
be executed on robot operating system (ROS).
To demonstrate the efficacy of Drona, we build and
verify an example priority mail delivery system.
Using our abstraction-based verification approach we were
able to find, within a few minutes, bugs which could not
be found by performing random simulation for several
hours. Our verified decentralized motion-planner scales
efficiently for large number of robots (upto 128 robots)
and workspace sizes (upto a 256x256 grid).},
}