  Control firmware in unmanned aerial vehicles (UAVs) uses sensors to model and
manage flight operations, from takeoff to landing to flying between waypoints.
However, sensors can fail at any time during a flight. If control firmware
mishandles sensor failures, UAVs can crash, fly away, or suffer other unsafe
conditions. In-situ model checking finds sensor failures that could lead to
unsafe conditions by systematically failing sensors. However, the type of
sensor failure and its timing within a flight affect its manifestation,
creating a large search space. We propose Avis, an in-situ model checker to
quickly uncover UAV sensor failures that lead to unsafe conditions. Widely used
control firmware already support operating modes. Avis injects sensor failures
as the control firmware transitions between modes - a key execution point where
mishandled software exceptions can trigger unsafe conditions. We implemented
Avis and applied it to ArduPilot and PX4. Avis found unsafe conditions 2.4X
faster than Bayesian Fault Injection, the leading, state-of-the-art approach.
Within the current code base of ArduPilot and PX4, Avis discovered 10
previously unknown software bugs that lead to unsafe conditions. Additionally,
we reinserted 5 known bugs that caused serious, unsafe conditions and Avis
correctly reported all of them.
