Enhanced Frameworks for Safety Verification of Autonomous Rendezvous Systems

We consider the safety of a V-bar hopping manoeuvre which forms part of the final stage in autonomous space rendezvous. This manoeuvre is controlled by thrusters: we assume these inputs are perfect impulses and model the system in a hybrid automaton framework. We consider the operation of the system under bounded parametric uncertainties, e.g. thruster misalignment, and use the concept of Barrier function certificates to assess system safety. This methodology provides an efficient tool for the systematic investigation of the safety property and does not rely on Monte-Carlo simulations. In particular, the existence of a Barrier function certificate guarantees that all trajectories of the system starting from a given initial set do not enter a predefined unsafe region under any possible combination of parameter deviations. Such a Barrier function certificate can be constructed efficiently using the Sum of Squares (SOS) decomposition and semi-definite programming (SDP).