Satellite rendezvous and conjunction avoidance: Case studies in verification of nonlinear hybrid systems

Taylor T. Johnson, Jeremy Green, Sayan Mitra, Rachel Dudley, Richard Scott Erwin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Satellite systems are beginning to incorporate complex autonomous operations, which calls for rigorous reliability assurances. Human operators usually plan satellite maneuvers in detail, but autonomous operation will require software to make decisions using noisy sensor data and problem solutions with numerical inaccuracies. For such systems, formal verification guarantees are particularly attractive. This paper presents automatic verification techniques for providing assurances in satellite maneuvers. The specific reliability criteria studied are rendezvous and conjunction avoidance for two satellites performing orbital transfers. Three factors pose challenges for verifying satellite systems: (a) incommensurate orbits, (b) uncertainty of orbital parameters after thrusting, and (c) nonlinear dynamics. Three abstractions are proposed for contending with these challenges: (a) quotienting of the state-space based on periodicity of the orbital dynamics, (b) aggregation of similar transfer orbits, and (c) overapproximation of nonlinear dynamics using hybridization. The method's feasibility is established via experiments with a prototype tool that computes the abstractions and uses existing hybrid systems model checkers.

Original languageEnglish (US)
Title of host publicationFM 2012
Subtitle of host publicationFormal Methods - 18th International Symposium, Proceedings
Number of pages15
StatePublished - 2012
Event18th International Symposium on Formal Methods, FM 2012 - Paris, France
Duration: Aug 27 2012Aug 31 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7436 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Symposium on Formal Methods, FM 2012

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Satellite rendezvous and conjunction avoidance: Case studies in verification of nonlinear hybrid systems'. Together they form a unique fingerprint.

Cite this