Skip to main content
SpringerLink
Log in

Combining Model Checking and Runtime Verification for Safe Robotics

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10548))

Included in the following conference series:

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 programming 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 verification helps us bridge the gap between software verification (discrete) that makes assumptions 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.

This work is funded in part by the DARPA BRASS program under agreement number FA8750-16-C-0043, NSF grants CNS-1646208 and CCF-1139138, and by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Marino, A., Parker, L., Antonelli, G., Caccavale, F.: Behavioral control for multi-robot perimeter patrol: a finite state automata approach. In: International Conference on Robotics and Automation, ICRA, pp. 831–836. IEEE (2009)

    Google Scholar 

  2. Barrientos, A., Colorado, J., del Cerro, J., Martinez, A., Rossi, C., Sanz, D., Valente, J.: Aerial remote sensing in agriculture: a practical approach to area coverage and path planning for fleets of mini aerial robots. J. Field Robot. 28(5), 667–689 (2011)

    Article  Google Scholar 

  3. Kehoe, B., Patil, S., Abbeel, P., Goldberg, K.: A survey of research on cloud robotics and automation. IEEE Trans. Autom. Sci. Eng. 12(2), 398–409 (2015)

    Article  Google Scholar 

  4. Omachonu, V.K., Einspruch, N.G.: Innovation in healthcare delivery systems: a conceptual framework. Publ. Sect. Innov. J. 15(1), 1–20 (2010)

    Google Scholar 

  5. Yamaguchi, T., Kaga, T., Donzé, A., Seshia, S.A.: Combining requirement mining, software model checking, and simulation-based verification for industrial automotive systems. In: Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2016

    Google Scholar 

  6. Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., Zufferey, D.: P: safe asynchronous event-driven programming. In: Programming Language Design and Implementation (PLDI), pp. 321–332 (2013)

    Google Scholar 

  7. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12

    Chapter  Google Scholar 

  8. Koenig, N., Howard, A.: Design and use paradigms for gazebo, an open-source multi-robot simulator. In: Intelligent Robots and Systems, IROS, vol. 3, pp. 2149–2154. IEEE (2004)

    Google Scholar 

  9. LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)

    Book  MATH  Google Scholar 

  10. Mellinger, D., Kumar, V.: Minimum snap trajectory generation and control for quadrotors. In: International Conference on Robotics and Automation (ICRA), pp. 2520–2525 (2011)

    Google Scholar 

  11. Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Automated composition of motion primitives for multi-robot systems from safe ltl specifications. In: Intelligent Robots and Systems, IROS, pp. 1525–1532. IEEE (2014)

    Google Scholar 

  12. Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: Drona: a framework for safe distributed mobile robotics. In: Proceedings of the 8th International Conference on Cyber-Physical Systems, ICCPS 2017, pp. 239–248. ACM, New York (2017)

    Google Scholar 

  13. Karaman, S., Frazzoli, E.: Incremental sampling-based algorithms for optimal motion planning. In: Robotics Science and Systems VI, vol. 104 (2010)

    Google Scholar 

  14. Godefroid, P.: Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174–186. ACM (1997)

    Google Scholar 

  15. Neter, J., Kutner, M.H., Nachtsheim, C.J., Wasserman, W.: Applied Linear Statistical Models, vol. 4. Irwin, Chicago (1996)

    Google Scholar 

  16. Maler, O., Ničković, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf. 15(3), 247–268 (2013)

    Article  Google Scholar 

  17. Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178–192. Springer, Cham (2014). doi:10.1007/978-3-319-11164-3_15

    Google Scholar 

  18. Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231–246. Springer, Cham (2014). doi:10.1007/978-3-319-11164-3_19

    Google Scholar 

  19. Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 55–70. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_4

    Chapter  Google Scholar 

  20. P Github (2017). https://github.com/p-org/P

  21. Desai, A., Qadeer, S., Seshia, S.A.: Systematic testing of asynchronous reactive systems. In: Foundations of Software Engineering (FSE), pp. 73–83 (2015)

    Google Scholar 

  22. Şucan, I.A., Moll, M., Kavraki, L.E.: The open motion planning library. IEEE Robot. Autom. Mag. 19, 72–82 (2012). http://ompl.kavrakilab.org

    Google Scholar 

  23. Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_17

    Chapter  Google Scholar 

  24. 3D Robotics (2017). https://3dr.com/

  25. PX4 Autopilot (2017). https://pixhawk.org/

  26. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)

    Article  MATH  Google Scholar 

  27. Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370–1381 (2009)

    Article  Google Scholar 

  28. Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Implan: scalable incremental motion planning for multi-robot systems. In: International Conference on Cyber-Physical Systems (ICCPS), pp. 1–10. IEEE (2016)

    Google Scholar 

  29. Fainekos, G.E., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for mobile robots. In: International Conference on Robotics and Automation, ICRA, pp. 2020–2025. IEEE (2005)

    Google Scholar 

  30. Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343–352 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  31. Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Automated composition of motion primitives for multi-robot systems from safe ltl specifications. In: International Conference on Intelligent Robots and Systems (IROS), pp. 1525–1532. IEEE (2014)

    Google Scholar 

  32. Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  33. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_18

    Chapter  Google Scholar 

  34. Dreossi, T.: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems. In: Hybrid Systems: Computation and Control, HSCC, HSCC 2017, pp. 29–34 (2017)

    Google Scholar 

  35. Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68–82. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_5

    Google Scholar 

  36. Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127–142. Springer, Cham (2015). doi:10.1007/978-3-319-17524-9_10

    Google Scholar 

  37. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_21

    Chapter  Google Scholar 

  38. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). doi:10.1007/3-540-46002-0_24

    Chapter  Google Scholar 

  39. Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193–207. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_15

    Chapter  Google Scholar 

  40. Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_18

    Chapter  Google Scholar 

  41. Gat, E., Slack, M.G., Miller, D.P., Firby, R.J.: Path planning and execution monitoring for a planetary rover. In: Robotics and Automation, pp. 20–25. IEEE (1990)

    Google Scholar 

  42. Pettersson, O.: Execution monitoring in robotics: a survey. Robot. Auton. Syst. 53(2), 73–88 (2005)

    Article  Google Scholar 

  43. Lotz, A., Steck, A., Schlegel, C.: Runtime monitoring of robotics software components: increasing robustness of service robotic systems. In: 2011 15th International Conference on Advanced Robotics (ICAR), pp. 285–290. IEEE (2011)

    Google Scholar 

  44. Lee, I., Ben-Abdallah, H., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: A monitoring and checking framework for run-time correctness assurance (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of California at Berkeley, Berkeley, CA, USA

    Ankush Desai, Tommaso Dreossi & Sanjit A. Seshia

Authors
  1. Ankush Desai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tommaso Dreossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sanjit A. Seshia
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ankush Desai .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Desai, A., Dreossi, T., Seshia, S.A. (2017). Combining Model Checking and Runtime Verification for Safe Robotics. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation