Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study

Corina S. Păsăreanu; Ravi Mangal; Divya Gopinath; Sinem Getir Yaman; Calum Corrie Imrie; Radu Calinescu

doi:10.1007/978-3-031-37706-8_15

Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study

Corina S. Păsăreanu, Ravi Mangal, Divya Gopinath, Sinem Getir Yaman, Calum Corrie Imrie, Radu Calinescu

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Computer Aided Verification. CAV 2023
Editors	C. Enea, A. Lal
Publisher	Springer
Pages	289-303
Number of pages	15
ISBN (Electronic)	978-3-031-37706-8
ISBN (Print)	978-3-031-37705-1
DOIs	https://doi.org/10.1007/978-3-031-37706-8_15
Publication status	Published - 17 Jul 2023

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13964

Bibliographical note

Access to Document

10.1007/978-3-031-37706-8_15Licence: CC BY

Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study
© The Author(s) 2023
Final published version, 560 KBLicence: CC BY

Cite this

@inproceedings{b5c5649f03da402e9b663e8cb91210e9,

title = "Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study",

abstract = "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.",

author = "P{\u a}s{\u a}reanu, {Corina S.} and Ravi Mangal and Divya Gopinath and {Getir Yaman}, Sinem and Imrie, {Calum Corrie} and Radu Calinescu",

note = "{\textcopyright} The Author(s) 2023 ",

year = "2023",

month = jul,

day = "17",

doi = "10.1007/978-3-031-37706-8_15",

language = "English",

isbn = "978-3-031-37705-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "289--303",

editor = "Enea, {C. } and Lal, {A. }",

booktitle = "Computer Aided Verification. CAV 2023",

address = "Germany",

}

TY - GEN

T1 - Closed-loop Analysis of Vision-based Autonomous Systems

T2 - A Case Study

AU - Păsăreanu, Corina S.

AU - Mangal, Ravi

AU - Gopinath, Divya

AU - Getir Yaman, Sinem

AU - Imrie, Calum Corrie

AU - Calinescu, Radu

PY - 2023/7/17

Y1 - 2023/7/17

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-031-37706-8_15

DO - 10.1007/978-3-031-37706-8_15

M3 - Conference contribution

SN - 978-3-031-37705-1

T3 - Lecture Notes in Computer Science

SP - 289

EP - 303

BT - Computer Aided Verification. CAV 2023

A2 - Enea, C.

A2 - Lal, A.

PB - Springer

ER -