Safety Verification of Neural Network Controlled Systems

TL;DR

This paper introduces a formal verification method for neural network controlled systems by combining reachability analysis, validated simulation, and abstract interpretation to ensure safety in complex cyber-physical systems.

Contribution

It presents a novel system-level verification approach that soundly approximates system states and provides safety guarantees for neural network controlled systems.

Findings

Successfully verified safety of a real-world system

Provided safety bounds when full safety proof is infeasible

Demonstrated effectiveness of combined analysis techniques

Abstract

In this paper, we propose a system-level approach for verifying the safety of neural network controlled systems, combining a continuous-time physical system with a discrete-time neural network based controller. We assume a generic model for the controller that can capture both simple and complex behaviours involving neural networks. Based on this model, we perform a reachability analysis that soundly approximates the reachable states of the overall system, allowing to achieve a formal proof of safety. To this end, we leverage both validated simulation to approximate the behaviour of the physical system and abstract interpretation to approximate the behaviour of the controller. We evaluate the applicability of our approach using a real-world use case. Moreover, we show that our approach can provide valuable information when the system cannot be proved totally safe.