TY - GEN
T1 - Satellite rendezvous and conjunction avoidance
T2 - 18th International Symposium on Formal Methods, FM 2012
AU - Johnson, Taylor T.
AU - Green, Jeremy
AU - Mitra, Sayan
AU - Dudley, Rachel
AU - Erwin, Richard Scott
N1 - Funding Information:
Most of this research was conducted under the Air Force’s 2011 Summer Faculty Fellowship Program and Space Scholars Program at the Air Force Research Laboratory at Kirtland Air Force Base. The Illinois researchers were also supported by NSF CAREER Grant 1054247.
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84865989672&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84865989672&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-32759-9_22
DO - 10.1007/978-3-642-32759-9_22
M3 - Conference contribution
AN - SCOPUS:84865989672
SN - 9783642327582
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 252
EP - 266
BT - FM 2012
Y2 - 27 August 2012 through 31 August 2012
ER -