Evaluation of Neural Network Verification Methods for Air-to-Air Collision Avoidance
Evaluation of Neural Network Verification Methods for Air-to-Air Collision Avoidance
复制标题
DOI：
10.2514/1.d0255
复制
发表时间：
2022-10
影响因子：
--
通讯作者：
Diego Manzanas Lopez;Taylor T. Johnson;Stanley Bak;Hoang-Dung Tran;Kerianne L. Hobbs
中科院分区：
文献类型：
--
作者：
Diego Manzanas Lopez;Taylor T. Johnson;Stanley Bak;Hoang-Dung Tran;Kerianne L. Hobbs
神经网络近似已成为自动化数据和自主算法的吸引力这样的系统的一个例子是无人机避免碰撞系统（ACAS XU），这是开环神经网络控制系统验证工具的非常流行的基准。一组十个闭环特性选择在存在共同的闭合飞机的情况下评估拥有飞机的安全性。 ）静态案例）以及5个神经网络之间的切换逻辑。在提议的每种情况下，都保证了在初始位置下的所有权飞机。
Neural network approximations have become attractive to compress data for automation and autonomy algorithms for use on storage-limited and processing-limited aerospace hardware. However, unless these neural network approximations can be exhaustively verified to be safe, they cannot be certified for use on aircraft. An example of such systems is the unmanned Airbone Collision Avoidance System (ACAS Xu), which is a very popular benchmark for open-loop neural network control system verification tools. This paper proposes a new closed loop extension of this benchmark, which consists of a set of ten closed loop properties selected to evaluate the safety of an ownship aircraft in the presence of a co-altitude intruder aircraft. These closed loop safety properties are used to evaluate 5 of the 45 neural networks that comprise the ACAS Xu benchmark (corresponding to co-altitude cases) as well as the switching logic between the 5 neural networks. The combination of nonlinear dynamics and switching between five neural networks is a challenging verification task accomplished with star set reachability methods in two verification tools. The safety of the ownship aircraft under initial position uncertainty is guaranteed in every scenario proposed.