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


The complete set of specifications can be found at: SPECIFICATIONS.xlsx

The specifications data sheet includes the ACS system outputs that R2U2 can view on a separate tab, as well as all 19 specifications organized by specification type in the remaining tabs. Each specification has a definition in english, the necessary atomic conversions, the corresponding MLTL specification, and a general explanation for the specification. The numerical values corresponding to flight simulations of Nova Somnium are used, but these parameters can be determined for any sounding rocket utilizing this ACS system. When choosing temporal operator syntax, we use the operators most similar to the english requirements; for example, though !G[a,b] !p ≡ F[a,b] p, we interchange these forms to improve readability.