@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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).},
}