Formal Verification of Attitude Control Systems Using Geometric Barrier Functions

Compared to safe obstacle avoidance in the position space, ensuring the safety of the attitude system in today's aerial vehicle operations is more challenging due to the non-Euclidean nature of the attitude space and the underactuated nature of the system. To address this issue, we first propose the geometric exponential barrier condition (GEBC) to produce barrier certificates on the manifold, by which attitude safety requirements can be encoded globally into the verification problems of attitude control systems. Then, we use exponential coordinates to characterize GEBCs, which makes them describable in terms of quantifier-free real arithmetic logic (QF-NRA) and efficiently solvable by current satisfiability modulo theories (SMT) solvers. A performance criterion is further discussed where we propose an effective algorithm to construct safe operational regions with different controllers, which can help with nominal controller selection and tuning. Finally, we demonstrate our approach in a quadrotor system and analyze the safe performance of two PD controllers on the proposed safe operation criterion.