Reasoning about Safety of Learning-Enabled Components in Autonomous Cyber-physical Systems

TL;DR

This paper introduces a simulation-based method to generate barrier certificates for safety verification of cyber-physical systems with neural network controllers, using linear programming and SMT solvers to ensure safety.

Contribution

It presents a novel approach combining simulation, linear programming, and SMT solving to verify safety of neural network-controlled systems.

Findings

Successfully verified safety of an autonomous vehicle model.

Generated barrier certificates from simulation traces.

Demonstrated effectiveness on a Dubins car case study.

Abstract

We present a simulation-based approach for generating barrier certificate functions for safety verification of cyber-physical systems (CPS) that contain neural network-based controllers. A linear programming solver is utilized to find a candidate generator function from a set of simulation traces obtained by randomly selecting initial states for the CPS model. A level set of the generator function is then selected to act as a barrier certificate for the system, meaning it demonstrates that no unsafe system states are reachable from a given set of initial states. The barrier certificate properties are verified with an SMT solver. This approach is demonstrated on a case study in which a Dubins car model of an autonomous vehicle is controlled by a neural network to follow a given path.