Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver. Chan, N. Master's thesis, University of Illinois as Urbana-Champaign, May, 2018. abstract bibtex 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. The control solutions include a hybrid, or switched, version of linear quadratic regulator (LQR)?a fundamental result 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, given this select number of models, safety requirements, and verification techniques. We will demonstrate both successful, safe scenarios and incomplete or unsafe examples.
@MastersThesis{NicoleMasters,
author = {Nicole Chan},
title = {Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver},
school = {University of Illinois as Urbana-Champaign},
year = {2018},
month = {May},
abstract = {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. The control solutions include a hybrid, or switched, version of linear quadratic regulator (LQR)?a fundamental result 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, given this select number of models, safety requirements, and verification techniques. We will demonstrate both successful, safe scenarios and incomplete or unsafe examples.},
keywords = {Verification},
owner = {mitras},
}
Downloads: 0
{"_id":"mNojiBdMGf35kLJBq","bibbaseid":"chan-designandverificationofasafeautonomoussatelliterendezvousmaneuver-2018","authorIDs":[],"author_short":["Chan, N."],"bibdata":{"bibtype":"mastersthesis","type":"mastersthesis","author":[{"firstnames":["Nicole"],"propositions":[],"lastnames":["Chan"],"suffixes":[]}],"title":"Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver","school":"University of Illinois as Urbana-Champaign","year":"2018","month":"May","abstract":"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. The control solutions include a hybrid, or switched, version of linear quadratic regulator (LQR)?a fundamental result 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, given this select number of models, safety requirements, and verification techniques. We will demonstrate both successful, safe scenarios and incomplete or unsafe examples.","keywords":"Verification","owner":"mitras","bibtex":"@MastersThesis{NicoleMasters,\n author = {Nicole Chan},\n title = {Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver},\n school = {University of Illinois as Urbana-Champaign},\n year = {2018},\n month = {May},\n abstract = {A fundamental maneuver in autonomous space operations is known as rendezvous,\nwhere 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\nto 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\nthe 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. The control solutions include a hybrid, or switched, version of linear quadratic regulator (LQR)?a fundamental result 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\nclasses 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, given this select number of models, safety requirements, and verification techniques. We will demonstrate both successful, safe scenarios and incomplete or unsafe examples.},\n keywords = {Verification},\n owner = {mitras},\n}\n\n","author_short":["Chan, N."],"key":"NicoleMasters","id":"NicoleMasters","bibbaseid":"chan-designandverificationofasafeautonomoussatelliterendezvousmaneuver-2018","role":"author","urls":{},"keyword":["Verification"],"downloads":0,"html":""},"bibtype":"mastersthesis","biburl":"http://mitras.ece.illinois.edu/research/sayan.bib","creationDate":"2019-08-04T16:11:55.730Z","downloads":0,"keywords":["verification"],"search_terms":["design","verification","safe","autonomous","satellite","rendezvous","maneuver","chan"],"title":"Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver","year":2018,"dataSources":["yMXZF3wFnctJRohbP"]}