Elucidation and Analysis of Specification Patterns
in Aerospace System Telemetry

Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae-Young Lee, and Kristin Yvonne Rozier

This webpage contains research artifacts from "Elucidation and Analysis of Specification Patterns
in Aerospace System Telemetry" by Z. Luppen, M. Jacks, N. Baughman, M. Stilic, R. Nasers, B. Hertz, J. W. Cutler, D. Y. Lee, K. Y. Rozier

---

System Telemetry Specification Spreadsheets

We organize the formal specifications for each aerospace system via individual spreadsheets. 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.

The complete set of formal specifications for the high-altitude balloon can be found at:
High-Altitude Balloon Specifications

The complete set of formal specifications for the sounding rocket can be found at:
Sounding Rocket Specifications

The complete set of formal specifications for the unmanned aerial system (UAS) can be found at:
UAS Specifications

The complete set of formal specifications for the CubeSat can be found at:
CubeSat Specifications