Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering, Mathematics, Virtual Reality Applications Center

Document Type

Conference Proceeding


NASA Formal Methods Symposium (NFM 2021)

Publication Version

Accepted Manuscript

Link to Published Version

Publication Date


Journal or Book Title

NASA Formal Methods. NFM 2021. Lecture Notes in Computer Science



First Page


Last Page




Conference Title

NASA Formal Methods Symposium (NFM 2021)

Conference Date

May 24-28, 2021


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.


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.

Copyright Owner

Springer Nature Switzerland AG



File Format


Available for download on Thursday, May 19, 2022

Published Version