Abstract
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 
, a programming framework for building safe robotics systems. This paper introduces the 
toolchain and describes how it addresses the unique challenges involved in programming safety-critical robots.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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)
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 2018
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)
Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15, 7–48 (1999)
Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 15, 73–132 (1993)
Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 17, 507–535 (1995)
Sha, L.: Using simplicity to control complexity. IEEE Softw. 18, 20–28 (2001)
Schierman, J.D., et al.: Runtime assurance framework development for highly adaptive flight control systems. Technical report AD1010277, Barron Associates, Inc., Charlottesville (2015)
Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software (2009)
Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal logic based reactive mission and motion planning. IEEE Trans. Robot. 25, 1370–1381 (2009)
Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45, 343–352 (2009)
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)
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)
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)
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)
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). https://doi.org/10.1007/978-3-642-22110-1_30
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). https://doi.org/10.1007/978-3-642-39799-8_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). https://doi.org/10.1007/978-3-662-46681-0_5
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). https://doi.org/10.1007/978-3-319-57288-8_26
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)
Pettersson, O.: Execution monitoring in robotics: a survey. Robot. Auton. Syst. 53, 73–88 (2005)
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)
Lee, I., Ben-Abdallah, H., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: A monitoring and checking framework for run-time correctness assurance (1998)
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)
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)
Desai, A., Qadeer, S., Seshia, S.A.: Systematic testing of asynchronous reactive systems. In: Foundations of Software Engineering (FSE) (2015)
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)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman, Boston (2002)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)
Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)
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). https://doi.org/10.1007/978-3-319-67531-2_11
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 2018
Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence. CoRR, vol. abs/1606.08514 (2016)
Acknowledgments
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Desai, A., Qadeer, S., Seshia, S.A. (2018). Programming Safe Robotics Systems: Challenges and Advances. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-03421-4_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03420-7
Online ISBN: 978-3-030-03421-4
eBook Packages: Computer ScienceComputer Science (R0)