Programming Safe Robotics Systems: Challenges and Advances

  • Ankush DesaiEmail author
  • Shaz Qadeer
  • Sanjit A. Seshia
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


A significant challenge for large-scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation. Our approach towards enabling safe programming of robotics system consists of two parts: (1) a programming language for implementing, specifying, and compositionally (assume-guarantee) testing the high-level reactive robotics software; (2) a runtime assurance system to ensure that the assumptions used during design-time testing of high-level software hold at runtime. Combining high-level programming language and its systematic testing with runtime enforcement helps us bridge the gap between software testing 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. We implement our approach in Open image in new window , a programming framework for building safe robotics systems. This paper introduces the Open image in new window toolchain and describes how it addresses the unique challenges involved in programming safety-critical robots.



The work of the first and third authors was supported in part by the TerraSwarm Research Center, one of six centers supported by the STARnet phase of the Focus Center Research Program (FCRP) a Semiconductor Research Corporation program sponsored by MARCO and DARPA, by the DARPA BRASS and Assured Autonomy programs, and by Toyota under the iCyPhy center.


  1. 1.
    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) (2013)Google Scholar
  2. 2.
    Desai, A., Phanishayee, A., Qadeer, S., Seshia, S.A.: Compositional programming and testing of dynamic distributed systems. Technical report UCB/EECS-2018-95, EECS Department, University of California, Berkeley, July 2018CrossRefGoogle Scholar
  3. 3.
    Desai, A., Phanishayee, A., Qadeer, S., Seshia, S.A.: Compositional programming and testing of dynamic distributed systems. In: Proceedings of the ACM on Programming Languages (PACMPL) (OOPSLA) (2018)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15, 7–48 (1999)CrossRefGoogle Scholar
  5. 5.
    Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 15, 73–132 (1993)CrossRefGoogle Scholar
  6. 6.
    Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 17, 507–535 (1995)CrossRefGoogle Scholar
  7. 7.
    Sha, L.: Using simplicity to control complexity. IEEE Softw. 18, 20–28 (2001)Google Scholar
  8. 8.
    Schierman, J.D., et al.: Runtime assurance framework development for highly adaptive flight control systems. Technical report AD1010277, Barron Associates, Inc., Charlottesville (2015)Google Scholar
  9. 9.
    Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software (2009)Google Scholar
  10. 10.
    Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal logic based reactive mission and motion planning. IEEE Trans. Robot. 25, 1370–1381 (2009)CrossRefGoogle Scholar
  11. 11.
    Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45, 343–352 (2009)MathSciNetCrossRefGoogle Scholar
  12. 12.
    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
  13. 13.
    Shoukry, Y., et al.: Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming. In: 56th IEEE Annual Conference on Decision and Control (CDC), pp. 1132–1137 (2017)Google Scholar
  14. 14.
    Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: TuLiP: a software toolbox for receding horizon temporal logic planning. In: International Conference on Hybrid Systems: Computation and Control (HSCC) (2011)Google Scholar
  15. 15.
    Finucane, C., Jing, G., Kress-Gazit, G.: LTLMoP: experimenting with language, temporal logic and robot control. In: IEEE/RSJ International Conference on Intelligent Robots and Systems (2010)Google Scholar
  16. 16.
    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). Scholar
  17. 17.
    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). Scholar
  18. 18.
    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). Scholar
  19. 19.
    Dreossi, T., Donzé, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 357–372. Springer, Cham (2017). Scholar
  20. 20.
    Gat, E., Slack, M.G., Miller, D.P., Firby, R.J.: Path planning and execution monitoring for a planetary rover. In: Robotics and Automation. IEEE (1990)Google Scholar
  21. 21.
    Pettersson, O.: Execution monitoring in robotics: a survey. Robot. Auton. Syst. 53, 73–88 (2005)CrossRefGoogle Scholar
  22. 22.
    Lotz, A., Steck, A., Schlegel, C.: Runtime monitoring of robotics software components: increasing robustness of service robotic systems. In: International Conference on Advanced Robotics (ICAR) (2011)Google Scholar
  23. 23.
    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
  24. 24.
    Koenig, N., Howard, A.: Design and use paradigms for gazebo, an open-source multi-robot simulator. In: International Conference on Intelligent Robots and Systems (IROS) (2004)Google Scholar
  25. 25.
    Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: DRONA: a framework for safe distributed mobile robotics. In: International Conference on Cyber-Physical Systems (ICCPS) (2017)Google Scholar
  26. 26.
    Desai, A., Qadeer, S., Seshia, S.A.: Systematic testing of asynchronous reactive systems. In: Foundations of Software Engineering (FSE) (2015)Google Scholar
  27. 27.
    Mudduluru, R., Deligiannis, P., Desai, A., Lal, A., Qadeer, S.: Lasso detection using partial-state caching. In: Conference on Formal Methods in Computer-Aided Design (FMCAD) (2017)Google Scholar
  28. 28.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman, Boston (2002)Google Scholar
  29. 29.
    Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)Google Scholar
  30. 30.
    Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)Google Scholar
  31. 31.
    Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 172–189. Springer, Cham (2017). Scholar
  32. 32.
    Desai, A., Ghosh, S., Seshia, S.A., Shankar, N., Tiwari, A.: SOTER: programming safe robotics system using runtime assurance. Technical report UCB/EECS-2018-127, EECS Department, University of California, Berkeley, August 2018Google Scholar
  33. 33.
    Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence. CoRR, vol. abs/1606.08514 (2016)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of CaliforniaBerkeleyUSA
  2. 2.MicrosoftRedmondUSA

Personalised recommendations