Integrating Runtime Verification into a
Sounding Rocket Control System

Benjamin Hertz, Zachary Luppen, Kristin Y. Rozier

This webpage contains research artifacts from "Integrating Runtime Verification into a
Sounding Rocket Control System" by B. Hertz, Z. Luppen, and K. Y. Rozier

---

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 and trigger the appropriate mitigations for the ACS faults. 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.

NFM 2021 Presentation

This video was developed for the presentation of our work at the NASA Formal Methods (NFM) Symposium 2021, which occurred from May 24th - 28th, 2021. This 15-minute presentation provides an overview of the manuscript along with additional explanation and visuals of the malfunction that took place with the Nova Somnium rocket's aerobraking control system (ACS).