Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I

Alexis Aurandt, Phillip H. Jones, and Kristin Yvonne Rozier

This webpage contains further details and artifacts for reproducibility of the experiments in "Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I"

**The full version of the paper is available here (pdf)**


CubeSats are low-cost platforms that are popular for conducting spaceborne experiments, however they are known to have high failure rates (∼25% failure rate). In order to improve the likelihood of success of Iowa State University’s first CubeSat (CySat-I), we integrate Runtime Verification (RV) on the CySat-I to allow for fault detection at runtime. Although CubeSats have been previously identified as a possible target for RV, this is the first time that a RV engine has been deployed on a CubeSat. We utilize the R2U2 runtime verification engine due to its low overhead; we embed R2U2 directly on the On-Board Computer (OBC) to monitor the current state of the CySat-I. R2U2 continuously monitors the different subsystems on the CySat-I, and R2U2’s fault detection triggers predefined fault recovery strategies. Since the Electrical Power System (EPS) is a common source of failure, we specifically focus on this subsystem. We design a list of twenty-two specifications from English requirements corresponding to the EPS and translate them into Mission-time Linear Temporal Logic (MLTL). We perform mock launches on Earth with external fault injection to illustrate that R2U2 successfully reasons about faults and the CySat-I effectively performs fault recovery. We demonstrate that the CySat-I can successfully recover from eight unique EPS faults at runtime in a timely manner with no errors. During our mock launches, R2U2 discovered a potential error in the manufacturer’s firmware related to the EPS’s under-voltage event monitoring, and this led to a more in-depth investigation of the error by the manufacturers.

NASA Formal Methods (NFM) Symposium 2022 Presentation

This video was developed for the presentation of our paper at NFM 2022.