1 of 12

Safety Analysis of �Vision-based Autonomous Systems

Ravi Mangal1�

​

Corina S. Pasareanu1,2,3 Divya Gopinath2,3

Sinem Getir Yaman4 Calum Imrie4 Radu Calinescu4

Huafeng Yu5

�1Carnegie Mellon University 2KBR, Inc 3NASA Ames 4University of York 5Boeing Research

2 of 12

Vision-based Autonomous Systems

2

3 of 12

Challenge

  • Deep Neural Networks (DNNs) used for visual perception can be unreliable

​

​

  • Formal reasoning about safety of autonomous systems is very difficult:
    • High complexity of the DNN (millions or billions of parameters)
    • Complexity of the high-definition cameras
    • Complexity of the environment, subject to random perturbations

​

3

4 of 12

Our Approach

Key ideas:

  • Abstract away the hard-to analyze components
    • Perception DNN, camera, environmental dynamics�
  • Replace them with probabilistic or worst-case abstractions�
  • Model other components (controller, plant) using conventional techniques�
  • System becomes amenable to formal verification with off-the-shelf tools�
  • Approach is compositional
    • Conventional components analyzed separately from perception components

​

​

​

​

4

5 of 12

A Toy System: TaxiNet

  • Autonomous aircraft taxiing system

​

  • Tracks center-line of the taxiway�
  • DNN gets picture of the taxiway as input and estimates the plane’s state w.r.t. the center-line�
  • Returns two numerical outputs
    • Cross-track error (cte): The distance of the plane from the center-line
    • Heading error (he): The angle of the plane w.r.t. the center-line�
  • Hand-written controller from estimated system state (cte,he) to steering angle

​

  • For analysis, controller and dynamics are discretized

5

6 of 12

Safety Specifications

From a fixed initial state, ensure safe operation on a straight segment of the taxiway for a finite number of steps

​

​

Safe operation: |cte| ≤ 8 meters and |he| ≤ 35 degrees

​

6

7 of 12

System Model

7

Controller

Airplane

Dynamics

Perception DNN

Environment & Camera Dynamics

 

 

 

 

8 of 12

Probabilistic Analysis

  •  

8

Controller

Airplane

Dynamics

Probabilistic Abstraction

 

 

 

9 of 12

Probabilistic Abstraction

  • Probabilistic transition from every (discrete) actual system state to every (discrete) estimated state

​

​

  • Transition probabilities estimated based on confusion matrices for perception DNN, measured on “representative” data set

​

​

  • Linear in the size of the DNN output and independent of the number of DNN parameters, the camera or the environment

​

​

  • System can be modeled as a Discrete-time Markov Chain (DTMC)�

​

  • Amenable for verification with probabilistic model checking tools

​

​

​

9

10 of 12

Worst-case Analysis via Assume-Guarantee Reasoning

10

Controller

Airplane

Dynamics

Perception DNN

Environment & Camera Dynamics

 

 

 

 

 

 

Assumption

11 of 12

Worst-case Analysis via Assume-Guarantee Reasoning

​

  • Assumption encodes all the DNN and environment behaviors that guarantee autonomous system satisfies the property

​

​

  • Assumption enforced via run-time checking

�

  • Algorithms exist for computing weakest assumptions for systems modeled as finite state machines

​

11

12 of 12

Summary

  • Formal safety analysis of vision-based autonomous systems is challenging due to complexity of DNN and environment

​

  • Probabilistic and worst-case abstractions can make formal analysis feasible and compositional

​

  • Testing artifacts like confusion matrices can be fruitfully employed for system-level analysis

​

  • Run-time checks can enforce assumptions derived from worst-case analysis

12

Thank you!

rmangal@andrew.cmu.edu