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
Experimental aerospace projects often require flight vehicle platforms for testing, such as high-altitude balloons, sounding rockets, unmanned aerial systems (UAS), and CubeSats. The system telemetry transmitted by these vehicles is crucial to understanding overall performance. A growing desire to implement greater levels of system autonomy and AI-enhanced control into these systems merits introducing rigorous safety analysis from formal methods techniques, such as Runtime Verification (RV). RV depends heavily upon the accuracy and robustness of the specifications it reasons over, and the task of developing a comprehensive set of system specifications often poses a significant challenge. To aid specification development for new systems, we provide an analysis on the process of implementing RV into four real aerospace systems with increasing complexity. We design and validate fourteen formal specifications for a real high-altitude balloon mission and draw on three past formal specification efforts on a sounding rocket, UAS, and CubeSat to compare specification patterns and overlapping system needs. We identify four common temporal logic subformulas for specifications within and between these systems, providing metrics on development resources, frequency, and perceived automation difficulty. We generalize our results and discuss considerations for automatically generating formal specifications in aerospace projects.
NFM 2022 Presentation
This video was developed for the presentation of our work at the NASA Formal Methods (NFM) Symposium 2022, which occurred from May 24th - 27th, 2022. This 15-minute presentation provides an overview of the manuscript along with additional explanation and visuals regarding our work developing comparing the formal specifications of the aerospace systems.