DRONA: A Framework for Safe Distributed Mobile Robotics
Ankush Desai

Citation
Ankush Desai. "DRONA: A Framework for Safe Distributed Mobile Robotics". Tutorial, 30, March, 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 presentation 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).

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Ankush Desai. <a
  href="http://www.terraswarm.org/pubs/910.html"
  ><i>DRONA: A Framework for Safe Distributed Mobile
  Robotics</i></a>, Tutorial,  30, March, 2017.

• Plain text

  Ankush Desai. "DRONA: A Framework for Safe Distributed
  Mobile Robotics". Tutorial,  30, March, 2017.

• BibTeX

  @tutorial{Desai17_DRONAFrameworkForSafeDistributedMobileRobotics,
      author = {Ankush Desai},
      title = {DRONA: A Framework for Safe Distributed Mobile
                Robotics},
      day = {30},
      month = {March},
      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 presentation 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). },
      URL = {http://terraswarm.org/pubs/910.html}
  }
  

Posted by Christopher Brooks on 18 Jan 2017.
Groups: tools