A Case Study in Formal Specification and Runtime Verification of a CubeSat Communications System

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. 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.