Skip to main content
Presentation
Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2
Formal Modeling and Analysis of Timed Systems. FORMATS 2020. Lecture Notes in Computer Science
  • Brian Kempa, Iowa State University
  • Pei Zhang, Iowa State University
  • Phillip H. Jones, Iowa State University
  • Joseph Zambreno, Iowa State University
  • Kristin Yvonne Rozier, Iowa State University
Document Type
Conference Proceeding
Conference
18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2020)
Publication Version
Accepted Manuscript
Link to Published Version
https://doi.org/10.1007/978-3-030-57628-8
Publication Date
8-25-2020
DOI
10.1007/978-3-030-57628-8_12
Conference Title
18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2020)
Conference Date
September 1-3, 2020
Geolocation
(48.2081743, 16.3738189)
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.

Comments

This is a post-peer-review, pre-copyedit version of a proceeding published as Kempa, Brian, Pei Zhang, Phillip H. Jones, Joseph Zambreno, and Kristin Yvonne Rozier. "Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2." In Formal Modeling and Analysis of Timed Systems: 18th International Conference, FORMATS 2020, Vienna, Austria, September 1–3, 2020, Proceedings. Nathalie Bertrand and Nils Jansen, editors. Lecture Notes in Computer Science 1288 (2020): 196-214. The final authenticated version is available online at DOI: 10.1007/978-3-030-57628-8_12. Posted with permission.

Copyright Owner
Springer Nature Switzerland A.G.
Language
en
File Format
application/pdf
Citation Information
Brian Kempa, Pei Zhang, Phillip H. Jones, Joseph Zambreno, et al.. "Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2" Vienna, AustriaFormal Modeling and Analysis of Timed Systems. FORMATS 2020. Lecture Notes in Computer Science Vol. 12288 (2020) p. 196 - 214
Available at: http://works.bepress.com/kristin-yvonne-rozier/49/