Verification and Validation of Algorithms for Resilient Complex Software Controlled Systems

Verification of the Guidance, Navigation and Control (GN&C) algorithms and software utilized onboard spacecraft is of paramount importance to ensure resilient, correct operation after launch. Rather than wait until the GN&C software has been deployed to perform on-orbit verification, offline verification integrated into the design process will improve mission performance, significantly reduce the risk of mission failure, and reduce overall deployment costs. Verus Research and our partner the Georgia Institute of Technology (Georgia Tech) propose to establish the applicability of formal methods to offline verification of GN&C systems, as opposed to simulation-based methods, to capture the multitude of uncertainties still present at earlier stages of development and prior to on-orbit testing, while providing rigorous assertions of requirements despite such uncertainties. The Verus Research team proposes a combination of transverse Lyapunov stability and reachability analysis techniques to verify robust stability and invariance properties of GN&C algorithms. In Phase I, we will focus on verifying stability requirements of the attitude control system, with extensions to more general requirements and algorithms in Phase II. We will leverage the ASTROS facility at Georgia Tech to perform verification of GN&C algorithms via Simulink models, and finally confirm the algorithm performance through hardware testing.