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.
@article{arxiv.2302.04634,
title = {Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study},
author = {Corina S. Pasareanu and Ravi Mangal and Divya Gopinath and Sinem Getir Yaman and Calum Imrie and Radu Calinescu and Huafeng Yu},
journal= {arXiv preprint arXiv:2302.04634},
year = {2023}
}