Safety Verification of Reactive Controllers for UAV Flight in Cluttered Environments Using Barrier Certificates
Unmanned aerial vehicles (UAVs) have a so-far untapped potential to operate at high speeds through cluttered environments. Many of these systems are limited by their adhoc reactive controllers using simple visual cues like optical ﬂow. Here we consider the problem of formally verifying an output-feedback controller for an aircraft operating in an unknown environment. Using recent advances in sums-of -squares programming that allow for efﬁcient computation of barrier functions, we search for global certiﬁcates of safety for the closed-loop system in a given environment. In contrast to previous work, we use rational functions to globally approximate non-smooth dynamics and use multiple barrier functions to guard against more than one obstacle. We expect that these formal veriﬁcation techniques will allow for the comparison, and ultimately optimization, of reactive controllers for robustness to varying initial conditions and environments.