Citation
Ankush Desai, Tommaso Dreossi, Sanjit Seshia. "Combining Model Checking and Runtime Verification for Safe Robotics". The 17th International Conference on Runtime Verification, 2017.

Abstract
A major challenge towards large scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation. To this end, we present a framework for building safe robots. Our approach for validating the end-to-end correctness of robotics system consists of two parts: 1) a high-level program- ming language for implementing and systematically testing the reactive robotics software via model checking; 2) a signal temporal logic (STL) based online monitoring system to ensure that the assumptions about the low-level controllers (discrete models) used during model checking hold at runtime. Combining model checking with runtime verication helps us bridge the gap between software verication (discrete) that makes as- sumptions about the low-level controllers and the physical world, and the actual execution of the software on a real robotic platform in the physical world. To demonstrate the efficacy of our approach, we build a safe adaptive surveillance system and present software-in-the-loop simulations of the application.

Electronic downloads

• drona2.0.pdf · application/pdf · 3519 kbytes

• HTML

  Ankush Desai, Tommaso Dreossi, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/955.html"
  >Combining Model Checking and Runtime Verification for
  Safe Robotics</a>, The 17th International Conference
  on Runtime Verification, 2017.

• Plain text

  Ankush Desai, Tommaso Dreossi, Sanjit Seshia.
  "Combining Model Checking and Runtime Verification for
  Safe Robotics". The 17th International Conference on
  Runtime Verification, 2017.

• BibTeX

  @inproceedings{DesaiDreossiSeshia17_CombiningModelCheckingRuntimeVerificationForSafeRobotics,
      author = {Ankush Desai and Tommaso Dreossi and Sanjit Seshia},
      title = {Combining Model Checking and Runtime Verification
                for Safe Robotics},
      booktitle = {The 17th International Conference on Runtime
                Verification},
      year = {2017},
      abstract = {A major challenge towards large scale deployment
                of autonomous mobile robots is to program them
                with formal guarantees and high assurance of
                correct operation. To this end, we present a
                framework for building safe robots. Our approach
                for validating the end-to-end correctness of
                robotics system consists of two parts: 1) a
                high-level program- ming language for implementing
                and systematically testing the reactive robotics
                software via model checking; 2) a signal temporal
                logic (STL) based online monitoring system to
                ensure that the assumptions about the low-level
                controllers (discrete models) used during model
                checking hold at runtime. Combining model checking
                with runtime verication helps us bridge the gap
                between software verication (discrete) that makes
                as- sumptions about the low-level controllers and
                the physical world, and the actual execution of
                the software on a real robotic platform in the
                physical world. To demonstrate the efficacy of our
                approach, we build a safe adaptive surveillance
                system and present software-in-the-loop
                simulations of the application.},
      URL = {http://terraswarm.org/pubs/955.html}
  }
  

Posted by Ankush Desai on 24 May 2017.
Groups: tools