Campus Units

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

Document Type

Conference Proceeding

Conference

NASA Formal Methods Symposium (NFM 2021)

Publication Version

Accepted Manuscript

Link to Published Version

https://doi.org/10.1007/978-3-030-76384-8_10

Publication Date

5-19-2021

Journal or Book Title

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

Volume

12673

First Page

151

Last Page

159

DOI

10.1007/978-3-030-76384-8_10

Conference Title

NASA Formal Methods Symposium (NFM 2021)

Conference Date

May 24-28, 2021

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.

Copyright Owner

Springer Nature Switzerland AG

Language

en

File Format

application/pdf

Available for download on Thursday, May 19, 2022

Published Version

Share

 
COinS