Certification of avionic software based on machine learning: the case for formal monotony analysis

The use of machine learning (ML) in airborne safety-critical systems requires new methods for certification, as the current standards and practices were defined and refined over decades with classical programming in mind and do not support this new development paradigm. This article provides an overview of the main challenges to the demonstration of compliance with regulation requirements raised by the use of ML and focuses on one particular case where the formal verification may become mandatory in future regulations, which is the verification of (partial) monotony properties. For this case, we propose a method to evaluate the monotony property using mixed integer linear programming. Contrary to the existing literature, our analysis provides a lower and upper bound of the space volume where the property does not hold, that we denote “Non-Monotonic Space Coverage”. This work has several advantages: (i) our formulation of the monotony property works on discrete inputs, (ii) the iterative nature of our algorithm allows for refining the analysis as needed, and (iii) from an industrial point of view, the results of this evaluation are valuable for the aeronautical domain, where it can support the certification demonstration. We applied this method to an avionic case study (braking distance estimation using a neural network) where the verification of the monotony property is of paramount interest from a safety perspective.