Reasoning about Safety of Learning-Enabled Components in Autonomous Cyber-physical Systems
This addresses safety verification for autonomous systems, but it is incremental as it builds on existing barrier certificate and simulation techniques.
The paper tackled the problem of verifying safety for autonomous cyber-physical systems with neural network controllers by developing a simulation-based method to generate barrier certificates, demonstrating it on a Dubins car model to show no unsafe states are reachable from given initial conditions.
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.