Combining Model Checking and Runtime Verification for Safe Robotics
Ankush Desai, Tommaso Dreossi, Sanjit Seshia

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

Citation formats  
  • 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

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.