Drona: A Framework for Safe Distributed Mobile Robotics

Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer, and Sanjit A. Seshia. Drona: A Framework for Safe Distributed Mobile Robotics. In Proceedings of the 8th International Conference on Cyber-Physical Systems (ICCPS), pp. 239–248, April 2017.

Download

[pdf] 

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).

BibTeX

@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).},
}

Generated by bib2html.pl (written by Patrick Riley ) on Tue Apr 24, 2018 09:06:48