Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing

TL;DR

Addressing the certification of DNN-based runway object classifiers for safe aircraft taxiing, this work applies formal verification to bound local robustness under perturbations defined by $P = B_\epsilon(x')$ (noise), $bright(x',b)$ with $|b| \le \beta$, and $con(x', c, \mu)$ with $|c-1| \le \gamma$. It encodes brightness and contrast via an added input layer and employs an incremental verification algorithm that leverages monotonicity to reduce verifier invocations by nearly 60%. On a prototype Airbus network evaluated on $1145$ correctly classified images, the results show the classifier is substantially more sensitive to noise than to brightness or contrast perturbations. The findings support the viability of verification-based robustness assessment in aviation and outline scalable directions, including larger networks, higher-resolution inputs, DNN abstractions, and proof-producing verification for safety certification.

Abstract

As deep neural networks (DNNs) are becoming the prominent solution for many computational problems, the aviation industry seeks to explore their potential in alleviating pilot workload and in improving operational safety. However, the use of DNNs in this type of safety-critical applications requires a thorough certification process. This need can be addressed through formal verification, which provides rigorous assurances -- e.g.,~by proving the absence of certain mispredictions. In this case-study paper, we demonstrate this process using an image-classifier DNN currently under development at Airbus and intended for use during the aircraft taxiing phase. We use formal methods to assess this DNN's robustness to three common image perturbation types: noise, brightness and contrast, and some of their combinations. This process entails multiple invocations of the underlying verifier, which might be computationally expensive; and we therefore propose a method that leverages the monotonicity of these robustness properties, as well as the results of past verification queries, in order to reduce the overall number of verification queries required by nearly 60%. Our results provide an indication of the level of robustness achieved by the DNN classifier under study, and indicate that it is considerably more vulnerable to noise than to brightness or contrast perturbations.

Figures (11)

• Figure 1: Modeling brightness and contrast perturbations by adding an input layer.
• Figure 2: Example of incremental verification algorithm's run.
• Figure 3: Percentage of UNSAT queries per noise and brightness parameters.
• Figure 4: Percentage of UNSAT queries per contrast parameter
• Figure 5: Brightness perturbations for an 'Aircraft' and a 'Person' from the test set.