Design and verification of a safe autonomous satellite rendezvous maneuver

control, verification, hybrid systems, rendezvous, satellite

Chan, Nicole ; Mitra ; Sayan

关键词: control, verification, hybrid systems, rendezvous, satellite;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/101051/CHAN-THESIS-2018.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

A fundamental maneuver in autonomous space operations is known as rendezvous, where an active spacecraft navigates towards and maneuvers within close proximity of a free-flying passive spacecraft. Any mistake during autonomous space flight can be extremely costly, yet these systems are difficult to verify due to limitations of testing spacecraft. In this thesis, we present a benchmark model formulation for the rendezvous mission, two control solutions to achieve this mission, and a rigorous method to demonstrate that the resulting system’s behavior remains safe.The benchmark model provides both a nonlinear description of the spacecraft’s motion and a linearized approximation, and the mission objectives, or equivalently, our set of safety properties. We present a set of control solutions, which includes a hybrid, or switched, version of linear quadratic regulator (LQR)—a fundamental approach in the theory of optimal control for linear systems. We formulate a novel hybrid controller, dubbed state-dependent linear quadratic (SDLQ) control, which extends the former controller in a way that may improve its ability to generate only safe trajectories. With these choices of dynamical models and controllers, we obtain a collection of models that are shown to robustly achieve safety properties of interest using a suite of hybrid verification tools. We utilize several existing tools, each developed for different classes of hybrid models, and we implement a new tool called SDVTool which improves upon one of the former tools. We present experimental results that illustrate the promise (and ongoing challenges) of this approach; that is, applying a class of simulation-based verification algorithms to our proposed set of benchmark models and safety requirements to design and rigorously demonstrate safety of the autonomous satellite maneuver. We will demonstrate both successful, safe scenarios and incomplete or unsafe examples.