{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/101051"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/101051","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Design and verification of a safe autonomous satellite rendezvous maneuver","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. 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.","abstract_html":"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.","abstract_has_math":false,"creators":["Chan, Nicole"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-09-04T20:27:25Z","date_published":"2018-09-04T20:27:25Z","updated_at":"2026-07-22T22:24:38Z","subjects":["control, verification, hybrid systems, rendezvous, satellite"],"languages":["en"],"rights":["Copyright 2018 Nicole Chan"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/101051","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan"]},{"key":"dc:creator","label":"Author","values":["Chan, Nicole"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-09-04T20:27:25Z","2018-04-24","2018-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["control, verification, hybrid systems, rendezvous, satellite"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Nicole Chan"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/101051"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-08-31 without embargo terms","The student, Nicole Chan, accepted the attached license on 2018-04-24 at 07:33.","The student, Nicole Chan, submitted this Thesis for approval on 2018-04-24 at 07:38.","This Thesis was approved for publication on 2018-04-24 at 10:24.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12440 on 2018-08-31 at 17:14:23","Made available in DSpace on 2018-09-04T20:27:25Z (GMT). No. of bitstreams: 2 CHAN-THESIS-2018.pdf: 2083305 bytes, checksum: 08e5347a7e5dc7fb005f3bc913069c23 (MD5) LICENSE.txt: 4208 bytes, checksum: 646d99513509dd2ded9f009e61f14da2 (MD5) Previous issue date: 2018-04-24"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Design and verification of a safe autonomous satellite rendezvous maneuver"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Chan, Nicole"],"dc:date":["2018-09-04T20:27:25Z","2018-04-24","2018-05"],"dc:description":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-08-31 without embargo terms","The student, Nicole Chan, accepted the attached license on 2018-04-24 at 07:33.","The student, Nicole Chan, submitted this Thesis for approval on 2018-04-24 at 07:38.","This Thesis was approved for publication on 2018-04-24 at 10:24.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12440 on 2018-08-31 at 17:14:23","Made available in DSpace on 2018-09-04T20:27:25Z (GMT). No. of bitstreams: 2 CHAN-THESIS-2018.pdf: 2083305 bytes, checksum: 08e5347a7e5dc7fb005f3bc913069c23 (MD5) LICENSE.txt: 4208 bytes, checksum: 646d99513509dd2ded9f009e61f14da2 (MD5) Previous issue date: 2018-04-24"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/101051"],"dc:language":["en"],"dc:rights":["Copyright 2018 Nicole Chan"],"dc:subject":["control, verification, hybrid systems, rendezvous, satellite"],"dc:title":["Design and verification of a safe autonomous satellite rendezvous maneuver"],"dc:type":["text"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:38Z"}