Formal Verification of a Neural Network Based Prognostics System for Aircraft Equipment

We demonstrate the use of formal methods to verify properties of a deep convolutional neural network that estimates remaining useful life of aircraft mechanical equipment. We provide mathematical formalizations of requirements of the estimator, such as stability and monotonicity, as properties. To efficiently apply existing tools for verification of neural networks, we reduce the verification of global properties to a representative set of local properties defined for the points of the test dataset. We encode these properties as linear constraints and verify them using a state-of-the-art tool for neural network verification. To increase the completeness and the scalability of the analysis, we develop a two-step verification method involving abstract interpretation and simulation-based falsification. Numerical results confirm the applicability of the approach.