Embeddability and safety assurance of ML-based systems under certification

For that purpose, four challenges have been identified. The first consists in feeding the ML training activities with constraints coming from the hardware target and the verification needs. Taking these needs into account greatly facilitates efficient deployment on hardware accelerators (for example, by choosing an appropriate tensor size or type of convolution) and can reduce verification time. The second concerns the proper description of ML models for exchanging them between frameworks and for interfacing them with usual parallel programming paradigms. The main purpose is to ensure semantic preservation of the trained model on the final target. Initial work was done on NNEF format and more recently some members of the chair contribute to the ONNX safety-related profile (see 1) below). The third challenge addresses the extensive use of formal methods to verify the correctness of the ML-based system either off-line and at runtime to ensure that no catastrophic situations will be reached due to a poor performance. Formal methods are recognized as an acceptable means in certification and have shown already strong capabilities to track errors and reduce development costs. Mélanie Ducoffe is developing the verifier DECOMON (see 2) below). Off-line formal verification of small dimension neural networks has been successfully applied during ANITI 3AI Institute. For the cluster, the chair tackles more complex ML task based on computer vision (e.g. object detection). In addition to off line verification, on-line fault tolerance mechanisms, which we refer to as runtime monitors, are analyzed and designed to maintain an acceptable behavior during operation despite perception errors (i.e. to remain in the ODD – operational design domain). Finally, the last challenge tackles the predictable and safe deployment of ML models on complex hardware. Among the outcome of the chair are the predictable C code generator ACETONE (see 3) below) and the standalone compiler (see 4) below). The research activities will be supported by four industrial use cases, namely ACAS Xu, vision-based landing for aircraft, vision-based emergency landing for UAV and counter UAV-systems. The chair is an active contributor of the LARD (Landing Approach Runway Detection) dataset (see 1) below).

1)    Link to SONNX safety profile on GitHub

2)    Link to DECOMON verifier on GitHub

3)     Link to ACETONE predictable C code generator on GitHub

4)     Link to VTA standalone compiler on GitHub

5)     Link to LARD data set on GitHub