Towards Precision-Aware Safe Neural-Controlled Cyber-Physical Systems

Cyber-physical systems (CPS) are increasingly utilizing neural networks (NN) as controllers. Thus, ensuring the safety of these systems becomes crucial, specifically in the context of safety-critical application domains. Current safety verification focuses on reachability analysis, considering bounded errors from
noisy environments or inaccurate implementations. However, it assumes real-valued arithmetic and does not account for the fixed-point quantization often used in embedded systems. Some recent efforts have focused on generating sound quantized NN implementations in fixed-point, ensuring specific target error bounds, but they assume the safety of NNs is already proven.

To bridge this gap, we introduce Nexus, a novel two-phase framework combining reachability analysis with sound NN quantization. Nexus provides an end-to-end solution that ensures CPS safety within bounded errors while generating mixed-precision fixed-point implementations for NN controllers. Additionally, we optimize these implementations for automated parallelization on FPGAs using a commercial HLS compiler, reducing machine cycles specifically for larger NN controllers.