Introducing formal methodologies to monitor small aerospace system telemetry
Zachary Luppen · 2021
This thesis explores the applications of formal methods to small aerospace systems. In modern-day experimental aerospace research, a flight vehicle is often required that acts as a platform for testing and analysis. Unmanned aerial systems (UAS), high-altitude balloons, sounding rockets, and CubeSats often fill this role, owing to their relatively low-budgets and fast turnarounds. These aspects of such projects also generate bottlenecks however, and small aerospace systems tend to experience more frequent fault scenarios and face higher risk of system failures. Small aerospace projects will continue to face such problems until dedicated methods are developed to handle them. My work is set out in a series of three academic papers. The first paper in this set, titled "A Case Study in Formal Specification and Runtime Verification of a CubeSat Communications System", discusses the applications of formal methods to a simulated CubeSat subsystem. The second manuscript, provides a series of formal specifications used to reason about a sounding rocket's aerobraking control system (ACS). The final paper in this series, "Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry" contains sets of formal specifications for a high-altitude balloon mission and a CubeSat, then compares the similarities and patterns between these systems and those laid out in previous work. I generalize my results from these papers and conclude with a discussion on the development of automated specification elicitation for aero and non-aerospace projects.