Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI

We demonstrate a unified approach to rigorous design of safety-critical\nautonomous systems using the VerifAI toolkit for formal analysis of AI-based\nsystems. VerifAI provides an integrated toolchain for tasks spanning the design\nprocess, including modeling, falsification, debugging, and ML component\nretraining. We evaluate all of these applications in an industrial case study\non an experimental autonomous aircraft taxiing system developed by Boeing,\nwhich uses a neural network to track the centerline of a runway. We define\nrunway scenarios using the Scenic probabilistic programming language, and use\nthem to drive tests in the X-Plane flight simulator. We first perform\nfalsification, automatically finding environment conditions causing the system\nto violate its specification by deviating significantly from the centerline (or\neven leaving the runway entirely). Next, we use counterexample analysis to\nidentify distinct failure cases, and confirm their root causes with specialized\ntesting. Finally, we use the results of falsification and debugging to retrain\nthe network, eliminating several failure cases and improving the overall\nperformance of the closed-loop system.\n