Verifying safety of an autonomous spacecraft rendezvous mission
For autonomous space operations, this work provides a benchmark for verifying safety constraints in rendezvous maneuvers, but the verification approach is incremental, applying existing tools to a new domain-specific problem.
This case study presents linear and nonlinear models of an autonomous spacecraft rendezvous mission with a switched LQR controller, and demonstrates that existing hybrid verification tools can verify passive safety (collision avoidance on a propulsion-free trajectory) across a range of initial conditions.
A fundamental maneuver in autonomous space operations is known as rendezvous, where a spacecraft navigates to and approaches another spacecraft. In this case study, we present linear and nonlinear benchmark models of an active chaser spacecraft performing rendezvous toward a passive, orbiting target. The system is modeled as a hybrid automaton, where the chaser must adhere to different sets of constraints in each discrete mode. A switched LQR controller is designed accordingly to meet this collection of physical and geometric safety constraints, while maintaining liveness in navigating toward the target spacecraft. We extend this benchmark problem to check for passive safety, which is collision avoidance along a passive, propulsion-free trajectory that may be followed in the event of system failures. We show that existing hybrid verification tools like SpaceEx, C2E2, and our own implementation of a simulation-driven verification tool can robustly verify this system with respect to the requirements, and a variety of relevant initial conditions.