A Novel Approach to Verification of Neural Cyber-physical Systems

The verification of Cyber-physical System (CPS),
particularly those incorporating neural networks for safety-critical
functions remains an ongoing challenge due to the lack
of advanced verification and validation frameworks. Current
methods are often limited in their scalability and ability to
comprehensively verify system-level and component-level properties,
leading to potential vulnerabilities in these systems. This
issue becomes even more pronounced when dealing with hybrid
systems that integrate physical processes and neural network-based
controllers. We propose a novel verification framework
tailored for complete CPS verification using a decomposition-based
approach to address this challenge. Our method performs
sequential-distributed verification, ensuring each component
adheres to compositional Metric Interval Temporal Logic
(MITL). By applying this framework to a model (CPS), we use
backward induction to verify that component-level and system-level
properties remain within predefined operational ranges,
derived from simulation data. Implemented in MATLAB,
this approach enhances the verification process by identifying
potential failure points across subsystems, providing a scalable
solution for verifying complex hybrid systems. This method
significantly improves verification accuracy and enables precise
identification of faulty components, making it a highly effective
tool for robust system design and analysis.