Formal verification of octorotor flight envelope using barrier functions and SMT solving

TL;DR

This paper presents a formal verification method for octorotor flight safety using barrier functions and SMT solving, ensuring safe operation and command tracking even with rotor failures.

Contribution

It introduces a novel approach combining barrier functions and SMT solving to verify safety and control invariance of octorotor flight controllers under failure conditions.

Findings

Verified safety regions for octorotor control using dReal SMT solver.

Confirmed command tracking accuracy within specified margins.

Validated safety under rotor failure scenarios.

Abstract

This paper introduces an approach for formally verifying the safety of the flight controller of an octorotor platform. Our method involves finding regions of the octorotor's state space that are considered safe, and which can be proven to be invariant with respect to the dynamics. Specifically, exponential barrier functions are used to construct candidate invariant regions near desired commanded states. The proof that these regions are invariant is discovered automatically using the dReal SMT solver, which ensures the accurate command tracking of the octorotor to within a certain margin of error. Rotor failures in which rotor thrusts become stuck at fixed values are considered and accounted for via a pseudo-inverse control allocator. The safety of the control allocator is verified in dReal by checking that the thrusts demanded by the allocator never exceed the capability of the rotors. We apply our approach on a specific octorotor example and verify the desired command tracking properties of the controller under normal conditions and various combinations of rotor failures.