Integrating Runtime Verification into a Sounding Rocket Control System

File
2021_RozierKristin_IntegratingRuntime.pdf (11.52 MB)

File Embargoed Until: (2022-05-19)
Date
2021-05-19
Authors
Hertz, Benjamin
Luppen, Zachary
Rozier, Kristin Yvonne
Rozier, Kristin Yvonne
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Aerospace Engineering
Organizational Unit
Computer Science
Organizational Unit
Mathematics
Organizational Unit
Journal Issue
Series
Department
Aerospace EngineeringComputer ScienceVirtual Reality Applications CenterElectrical and Computer EngineeringMathematics
Abstract

An actuation fault in the aerobraking control system (ACS) took down Iowa State’s Nova Somnium rocket during the 2019 Spaceport America Cup competition, prematurely ending the team’s participation. The ACS engaged incorrectly before motor burnout, altering the rocket’s trajectory and leading to a dangerous crash. The ability to detect this fault in real time on-board the ACS’s Arduino microcontroller would have prevented an uncontrolled landing and rapid unscheduled disassembly, which posed a major safety threat and ended a year’s worth of effort by the 50-student team. Runtime verification (RV) specializes in efficiently catching this type of scenario; the R2U2 RV engine uniquely fits in the project’s resource constraints. We design specifications to detect ACS faults and trigger the appropriate mitigations. We discuss specification development, validation, coverage, and robustness against false positives. Experimental evaluation on the real, recorded flight data demonstrates that running R2U2 on the Nova Somnium ACS would have prevented this accident from occurring. We generalize our results and outline our plans for integrating runtime verification into future sounding rockets.

Comments

This is a post-peer-review, pre-copyedit version of a proceeding published as Hertz B., Luppen Z., Rozier K.Y. (2021) Integrating Runtime Verification into a Sounding Rocket Control System. In: Dutle A., Moscato M.M., Titolo L., Muñoz C.A., Perez I. (eds) NASA Formal Methods. NFM 2021. Lecture Notes in Computer Science, vol 12673. Springer, Cham. The final authenticated version is available online at DOI: 10.1007/978-3-030-76384-8_10. Posted with permission.

Description
Keywords
Citation
DOI