Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems (bibtex)
by , , , ,
Abstract:
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.
Reference:
Taylor T. Johnson, Jeremy Green, Sayan Mitra, Rachel Dudley, Richard Scott Erwin, "Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems", Chapter in Proceedings of the 18th International Conference on Formal Methods (FM 2012) (Dimitra Giannakopoulou, Dominique Méry, eds.), Springer Berlin Heidelberg, vol. 7436, Paris, France, pp. 252–266, 2012, aug.
Bibtex Entry:
@incollection{johnson2012fm,
        author          =       {Taylor T. Johnson and Jeremy Green and Sayan Mitra and Rachel Dudley and Richard Scott Erwin},
        title           =       {Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems},
        year            =       {2012},
        booktitle       =       {Proceedings of the 18th International Conference on Formal Methods (<a href="http://fm2012.cnam.fr/">FM 2012</a>)},
    address     =   {Paris, France},
        month           =       aug,
    isbn        =   {978-3-642-32758-2},
    volume      =   {7436},
    gsid        =   {6661230319939383532},
    editor      =   {Giannakopoulou, Dimitra and M\'{e}ry, Dominique},
    doi     =   {10.1007/978-3-642-32759-9_22},
    publisher   =   {Springer Berlin Heidelberg},
    pages       =   {252--266},
        abstract        =       {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.},
        pdf = {http://www.taylortjohnson.com/research/johnson2012fm.pdf},
}
Powered by bibtexbrowser