Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry

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 of 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 Traffic Management (UTM) system, 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.