Skip to main content
SpringerLink
Log in

Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12288))

Abstract

Robonaut2 (R2) is a humanoid robot onboard the International Space Station (ISS), performing specialized tasks in collaboration with astronauts. After deployment, R2 developed an unexpected emergent behavior. R2’s inability to distinguish between knee-joint faults (e.g., due to sensor drift versus violated environmental assumptions) began triggering safety-preserving freezes-in-place in the confined space of the ISS, preventing further motion until a ground-control operator determines the root-cause and initiates proper corrective action. Runtime verification (RV) algorithms can efficiently disambiguate the temporal signatures of different faults in real-time. However, no previous RV engine can operate within the limited available resources and specialized platform constraints of R2’s hardware architecture. An attempt to deploy the only runtime verification engine designed for embedded flight systems, R2U2, failed due to resource constraints. We present a significant redesign of the core R2U2 algorithms to adapt to severe resource and certification constraints and prove their correctness. We further define an optimization enabled by our new algorithms and implement the new version of R2U2. We encode specifications describing real-life faults occurring onboard Robonaut2 using Mission-time Linear Temporal Logic (MLTL) and detail our process of specification debugging, validation, and refinement. We deployed this new version of R2U2 on Robonaut2, demonstrating successful real-time fault disambiguation and mitigation triggering of R2’s knee-joint faults without false positives.

Supported by NASA ECF NNX16AR57G and NSF CAREER Award CNS-1552934.

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

Notes

  1. 1.

    http://temporallogic.org/research/FORMATS20.

  2. 2.

    http://temporallogic.org/research/R2U2/R2U2-on-R2_demo.mp4.

References

  1. Adam, S., Larsen, M., Jensen, K., Schultz, U.P.: Towards rule-based dynamic safety monitoring for mobile robots. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS (LNAI), vol. 8810, pp. 207–218. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11900-7_18

    Chapter  Google Scholar 

  2. Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)

    Article  MathSciNet  Google Scholar 

  3. Badger, J., Hulse, A., Taylor, R., Curtis, A., Gooding, D., Thackston, A.: Model-based robotic dynamic motion control for the Robonaut 2 humanoid robot. In: 2013 13th IEEE-RAS International Conference on Humanoid Robots (Humanoids), pp. 62–67, October 2013. https://doi.org/10.1109/HUMANOIDS.2013.7029956

  4. Badger, J., Gooding, D., Ensley, K., Hambuchen, K., Thackston, A.: ROS in space: a case study on Robonaut 2. In: Koubaa, A. (ed.) Robot Operating System (ROS). SCI, vol. 625, pp. 343–373. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-26054-9_13

    Chapter  Google Scholar 

  5. Clemens, J., Pal, R., Sherrell, B.: Runtime state verification on resource-constrained platforms. In: MILCOM 2018–2018 IEEE Military Communications Conference (MILCOM), pp. 1–6. IEEE (2018)

    Google Scholar 

  6. Cooper, K., Eckhardt, J., Kennedy, K.: Redundancy elimination revisited. In: Proceedings of the 17th International Conference on Parallel Architectures and Compilation Techniques, pp. 12–21. ACM (2008)

    Google Scholar 

  7. Cowley, A., Taylor, C.J.: Towards language-based verification of robot behaviors. In: 2011 IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 4776–4782. IEEE (2011)

    Google Scholar 

  8. Diftler, M.A., et al.: Robonaut 2 - the first humanoid robot in space. In: 2011 IEEE International Conference on Robotics and Automation, pp. 2178–2183, May 2011. https://doi.org/10.1109/ICRA.2011.5979830

  9. Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and Bayesian network reasoners on-board FPGAs: flight-certifiable system health management for embedded systems. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 215–230. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_18

    Chapter  Google Scholar 

  10. Halder, R., Proença, J., Macedo, N., Santos, A.: Formal verification of ROS-based robotic applications using timed-automata. In: 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 44–50. IEEE (2017)

    Google Scholar 

  11. Huang, J., et al.: ROSRV: runtime verification for robots. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 247–254. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_20

    Chapter  Google Scholar 

  12. Badger, J.M., Hulse, A.M., Thackston, A.: Advancing safe human-robot interactions with Robonaut 2. In: Proceedings of the 12th International Symposium on Artificial Intelligence, Robotics and Automation in Space (2014)

    Google Scholar 

  13. Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_7

    Chapter  Google Scholar 

  14. Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 3–22. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_1

    Chapter  Google Scholar 

  15. Lu, H., Forin, A.: The design and implementation of p2v, an architecture for zero-overhead online verification of software programs. Technical report MSR-TR-2007-99, Microsoft Research, August 2007

    Google Scholar 

  16. Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. arXiv preprint arXiv:1807.00048 (2018)

  17. Mukherjee, R., Purandare, M., Polig, R., Kroening, D.: Formal techniques for effective co-verification of hardware/software co-designs. In: Proceedings of the 54th Annual Design Automation Conference 2017, p. 35. ACM (2017)

    Google Scholar 

  18. Pellizzoni, R., Meredith, P., Caccamo, M., Rosu, G.: Hardware runtime monitoring for dependable cots-based real-time embedded systems. In: 2008 Real-Time Systems Symposium, pp. 481–491, November 2008

    Google Scholar 

  19. Pratt, G.A., Williamson, M.M.: Series elastic actuators. In: Proceedings 1995 IEEE/RSJ International Conference on Intelligent Robots and Systems. Human Robot Interaction and Cooperative Robots, vol. 1, pp. 399–406, August 1995. https://doi.org/10.1109/IROS.1995.525827

  20. Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software, vol. 3, p. 5. Kobe, Japan (2009)

    Google Scholar 

  21. Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357–372. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_24

    Chapter  Google Scholar 

  22. Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), vol. 3, pp. 138–156. Kalpa Publications, Seattle, September 2017. TBD, https://easychair.org/publications/paper/Vncw

  23. Rozier, K., Vardi, M.: LTL satisfiability checking. Int. J. Software Tools Technol. Transfer (STTT) 12(2), 123–137 (2010). https://doi.org/10.1007/s10009-010-0140-3

  24. Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233–249. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_15

    Chapter  Google Scholar 

  25. Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: a tool exhibition report. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 504–509. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_35

    Chapter  Google Scholar 

  26. Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. Int. J. Prognost. Health Manage. (IJPHM) 6(1), 1–27 (2015)

    Google Scholar 

  27. Solet, D., Béchennec, J.L., Briday, M., Faucou, S., Pillement, S.: Hardware runtime verification of a RTOS kernel: Evaluation using fault injection. In: 2018 14th European Dependable Computing Conference (EDCC), pp. 25–32. IEEE (2018)

    Google Scholar 

  28. Wong, L., Arora, N.S., Gao, L., Hoang, T., Wu, J.: Oracle streams: a high performance implementation for near real time asynchronous replication. In: 2009 IEEE 25th International Conference on Data Engineering, pp. 1363–1374. IEEE (2009)

    Google Scholar 

  29. Zhang, P., Zambreno, J., Jones, P.H., Rozier, K.: Model predictive runtime verification for embedded platforms with real-time deadlines (2020, Under submission)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Iowa State University, Ames, IA, 50010, USA

    Brian Kempa, Pei Zhang, Phillip H. Jones, Joseph Zambreno & Kristin Yvonne Rozier

Authors
  1. Brian Kempa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pei Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Phillip H. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Joseph Zambreno
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Kristin Yvonne Rozier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Brian Kempa .

Editor information

Editors and Affiliations

  1. Inria, Université de Rennes, Rennes, France

    Nathalie Bertrand

  2. Radboud University, Nijmegen, The Netherlands

    Nils Jansen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y. (2020). Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. In: Bertrand, N., Jansen, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2020. Lecture Notes in Computer Science(), vol 12288. Springer, Cham. https://doi.org/10.1007/978-3-030-57628-8_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-57628-8_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-57627-1

  • Online ISBN: 978-3-030-57628-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation