A Case Study in Formal Specification and Runtime Verification of a CubeSat Communications System
Zachary Luppen, Dae Young Lee, Kristin Yvonne Rozier · AIAA Scitech 2021 Forum · 2021
View Video Presentation: https://doi.org/10.2514/6.2021-0997.vid CubeSats are garnering a lot of attention from several research communities due to their cheap price and easy accessibility to space. Although a CubeSat offers the potential to replace large and complex satellites for various space missions, developing a high-integrity platform that can fly in space requires robust software performance. The communications system of a CubeSat is critical to mission success. However, failed communications to the ground stations are commonplace for CubeSat projects. Thus robustifying against these potentially mission-ending failures poses one of the leading challenges for CubeSat missions both now and in the future. %The ability to detect faults in a CubeSat's communications system would aid in preventing a premature mission end as well as carry on the hard work performed by the developers. Runtime verification (RV) specializes in real-time error detection in these types of temporal, reactive systems, and the R2U2 verification engine proved to fit in the CubeSat's resource constraints. We design specifications to detect and trigger appropriate mitigations for communications system faults. We discuss communications system specification debugging, validation, and variable coverage. Experimental evaluation on simulated orbital and telemetry datasets demonstrates that running R2U2 within a CubeSat communications system would detect several unique faults and trigger mitigations for these such as atypical position measurements or a voltage supply failure from occurring. We provide a roadmap from large CubeSat datasets to specification patterns for automatically capturing common monitoring properties. We outline our plans for integrating RV into other CubeSat systems as well as verifying an entire CubeSat telemetry dataset.