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 flow. 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 efficient computation of barrier functions, we search for global certificates 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 verification techniques will allow for the comparison, and ultimately optimization, of reactive controllers for robustness to varying initial conditions and environments.