Towards a formal safety framework for trajectories

Abstract

Trajectory generation is at the heart of an autonomous Unmanned Aerial Vehicle (UAV). Given a navigation context, the UAV has to conceive a trajectory that fulfills its mission goal while avoiding collisions with obstacles and surrounding traffic. This intended trajectory is an idealization of the various actual physical trajectories that the UAV may perform during flight. The validation of actual physical trajectories with respect to their intended counterparts is challenging due to the interaction over time of several uncontrolled factors such as the environmental conditions, measurement errors and the cyber-physical components of the UAV. For this reason, the most common validation technique for trajectory generators is flight simulation, which is not exhaustive and thus cannot prove the actual absence of collisions. This paper presents a preliminary formal framework to reason about the safety of UAV trajectories with respect to static-obstacle collision avoidance taking account of the uncertainties derived from uncontrolled factors. The proposed framework was formally verified in a mechanical theorem prover. Its application as an oracle for black-box testing validation of trajectory generators is also proposed. Such testing strategy would allow the safety evaluation of trajectories while removing the need for simulation procedures, thus reducing the cost of the validation process.