Safety Guarantees for Drones through Set-Based Formal Verification Methods

Abstract

We investigate approaches and algorithms for both offline and on-the-fly verification of low-level drone control algorithms. Specifically, we seek to verify that low-level control algorithms for drones satisfy performance requirements desired during the conception of the system. To this end, we perform an in depth analysis of quadrotor dynamics and its uncertainties. Then, we build on Taylor-based methods to estimate the reachable sets of the systems, which are then exploited to verify if the system could reach unsafe states. The results obtained during this master thesis are as follows: (a) We develop a hardware and software in the loop, Gazebo-based swarm simulator for the Crazyflie drones, (b) We leverage the Crazyflie simulator to investigate safety of dynamical systems through Taylor-based methods and abstract interpretation. Specifically, We investigate on-the-fly, lightweight, real-time verification (reach and safety properties) algorithms to be embedded on the Crazyflie drones.