Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study
This work addresses safety verification for autonomous systems using complex DNNs, but it is incremental as it applies existing formal analysis techniques to a specific case.
The paper tackles the challenge of formally analyzing safety-critical autonomous systems with deep neural network perception by presenting a case study on an airplane taxiway guidance system, where they replace the camera and network with a probabilistic abstraction and use run-time guards to increase safety.
Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an experimental autonomous system that guides airplanes on taxiways using a perception DNN. We address the above challenges by replacing the camera and the network with a compact probabilistic abstraction built from the confusion matrices computed for the DNN on a representative image data set. We also show how to leverage local, DNN-specific analyses as run-time guards to increase the safety of the overall system. Our findings are applicable to other autonomous systems that use complex DNNs for perception.