# Implementation and certification of ML-based surrogate models in avionic systems

Christophe Gabreau, Nicolas Valot, Filipo Perotto, Claire Pagetti

► To cite this version:

Christophe Gabreau, Nicolas Valot, Filipo Perotto, Claire Pagetti. Implementation and certification of ML-based surrogate models in avionic systems. 13th European Congress of Embedded Real Time Systems (ERTS), Feb 2026, Toulouse, France. 10.82331/ERTS.2026.32. hal-05513781

HAL Id: hal-05513781

https://hal.science/hal-05513781v1

Submitted on 19 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Implementation and certification of ML-based surrogate models in avionic systems

Christophe Gabreau¹, Nicolas Valot¹, Filipo S. Perotto², Claire Pagetti²

¹Airbus, ²ONERA

**Abstract:** This paper explores the implementation and certification of Machine Learning (ML) surrogate models within safety-critical avionics, specifically focusing on the ACAS-Xu mid-air collision avoidance system. The purpose is to replace high-memory Look-Up Tables (LUTs) with compact neural networks to reduce computational demands while maintaining the original functional intent. A hybrid architecture is utilized, combining ML models with a legacy safety net to ensure continuous safety across the entire operational design domain. The study details a certification strategy aligned with EASA guidance for Level 1 and 2 ML applications, addressing planning, specification, design, implementation, validation, and verification objectives. Central to the work is the concept of semantics preservation using a controlled replication method and Top-1 accuracy metrics to mitigate numerical errors during the transition from design to target hardware. Furthermore, the paper analyzes the reduction of development assurance burdens for DAL D implementations. Ultimately, the paper demonstrates that ML-based surrogates can be provable and certifiable in legacy systems when the training dataset serves as an absolute ground truth.

**Keywords:** Machine Learning, Formal Verification, Implementation, Semantics Preservation, Certification.

## 1. INTRODUCTION

Machine Learning (ML) techniques have demonstrated effectiveness in approximating complex functions with high accuracy using artificial neural networks and data-driven training. It allows the replacement of heavy analytical models with relatively smaller inference graphs, thus reducing memory and computational needs. The adoption of ML-designed surrogate models in avionics is expected to grow significantly in the coming years. This trend is driven by emerging requirements, such as intelligent sensing or the replacement of legacy functions.

This paper illustrates how an ML-based surrogate model can be implemented in a safety-critical embedded aeronautical system, ensuring compliance with the certification objectives presented in the EASA Concept Paper "Guidance for Level 1 & 2 Machine Learning Applications" [7]. The use case devel-

oped in this paper is ACAS-Xu, the on-board mid-air collision avoidance system for fixed-wing autonomous or remotely piloted drones. It is responsible for determining and issuing evasive maneuvers when a potential trajectory conflict with surrounding traffic is detected.

The joint EUROCAE/SAE working group, WG-114/G-34, is currently developing a new assurance guidance standard, designated ED-324/ARP6983 [9], for aeronautical safety-related components implemented with AI, which is expected to be recognized in the future as an acceptable means of compliance by the authorities.

### 1.1. ACAS-Xu Use Case

The legacy system, ACAS-Xu [8], is based on pre-computed look-up tables (LUTs) and its architecture is illustrated in Figure 1. The "offline-cost-lookup" component relies on these LUTs to extract the expected long-term cost of 5 possible maneuvers, depending on the current "state-estimation", which monitors the own aircraft's instantaneous movement information and tracks the nearby surrounding traffic trajectories by aggregating the "previous-state" and the actual "sensor measurements", thus defining the ACAS-Xu geometric situation, as shown in Figure 2.

<figure><img src="image_2.png" /><figcaption>Figure 1. Initial ACAS-X item architecture inspired from [23]</figcaption></figure>

### 1.2. Related work

**Learning a Surrogate NN of a LUT:** Due to their excellent performance in approximating complex high-dimensional functions, Deep Neural Networks (DNNs) have been used for training compact surrogate models to replace large lookup tables [16], for example, in control command systems [27] or in the calibration of voltage-controlled circuits [20]. This technique was also explored for the ACAS-Xu use case. In [17], the authors analyze both a table compression strategy based on the origami algorithm, which exploits data redundancies and symmetries, and a neural network trained to be a surrogate function, comparing them with the legacy ACAS-Xu system.

<footnote>Christophe Gabreau et al.. This is an open-access article distributed under the terms of the Creative Commons Attribution 4.0 License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.</footnote>

<footnote>This work is partially supported by the National Research Agency under the France 2030 program - ANR-23-DEGR-0001 - DeepGreen Project.</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 2. ACAS-Xu geometry for horizontal resolution [18]</figcaption></figure>

**Surrogate NN for Certified ACAS-Xu:** Some authors have also analyzed the impact of using the NN surrogate model for ACAS-Xu in terms of safety preservation and compliance with certification. [19] proposed the use of an SMT-solver to prove 10 meta-properties, which intuitively represent the expected system avoidance behavior, but without any explicit link to the ACAS-Xu standard [8]. [1] developed a technique to verify a closed-loop approximation of ACAS-Xu using state quantization and back-reachability. [12, 4] introduced the idea of using a hybrid architecture based on a neural network implementation in the accurately approximated input regions, combined with parts of the LUT to ensure correct behavior in the other regions. [3] completed this verification with a closed-loop verification of restricted intruder trajectories.

**Certification of ML Implementation:** In an airborne context, there are some previous works dealing with the implementation of a DNN model on a recent CPU processor [2], studies about the prevention of the propagation of hardware errors that can lead to catastrophic failures in DNN accelerator systems [22], or some guarantees of robustness against hardware soft errors which can corrupt the target memory during implementation [15]. There are also works in other domains, like robotics, where the implementation is also a challenge when it comes to embed DNN models for computer vision and system control purposes in different target hardware such as CPUs, GPUs or Intel's neuromorphic chip [5]. [14] investigates the semantics preservation of the trained model when deployed on the final hardware platform, proposing a strategy to make traceable parallelization and optimizations in a trained model. There is an important survey [25] that structures and analyzes challenges, techniques, and methods for developing AI-based safety-critical systems. In particular, it addresses the development and integration of an ML-based function as part of a safety-critical system hosted on hardware platforms.

**Our previous works:** [4, 10] experienced the development of an ACAS-Xu system that integrates an ML Constituent (MLC) composed of 45 multi-layer perceptrons (with their necessary pre and post data processing). In addition, [11, 14] proposed an implementation of the ACAS-Xu MLC on one or several software items (see figure 3 of [9]). In those references, formal methods are used to demonstrate that the generalization and robustness of a model are provable on the entire input domain space. Then, [13] suggested a first implementation using a bit-accurate replication that would allow taking credit for the

properties formally proved during the design.

<figure><img src="image_4.png" /><figcaption>Figure 3. ACAS-X architecture in the literature</figcaption></figure>

## 1.3. Contributions

With respect to the state-of-the-art in the implementation and certification of safety-related systems using surrogate modeling techniques, this paper offers multi-fold contributions:

**Hybrid architecture** - This paper reuses the hybrid concept proposed by [4] to have a certifiable ML-based designed surrogate model and a safety net to support a completely safe operation.

**Certification strategy** - This paper deeply updates the certification considerations from [12] position paper with a detailed response to the pre-regulatory text from the EASA Concept Paper "Guidance for Level 1 & 2 Machine Learning Applications" [7] regarding the learning assurance aspects, using the ACAS-Xu use case as an illustration. In addition and conversely to previous works [11, 14], we complement the multiple-items approach defined in the Figure 3 by considering the scenario in which a legacy system based on LUTs has already been developed and certified. In this perspective, the challenge faced by this paper is to replace the component "offline cost lookup", adapting the existing software architecture to integrate the MLC as part of the legacy item. This strategy would be compliant with the MLC category 2 as described in appendix H of future ML standard ED-324 [9].

**Replication principle** - While [13] was demonstrating that a bit-accurate replication of the designed model (a.k.a trained model) is possible provided costly manual development, this paper will use the techniques developed in [28] to propose metrics assessing that the properties obtained at the end of the design such as generalisation, performance and robustness, still hold when the designed model is implemented (inference model). These metrics will show that the classification accuracy decrease of the inference model remains acceptable compared to the trained model. With this new technique and conversely to existing work on implementation errors propagation [2, 22, 15], this paper offers a target-agnostic method to mitigate the numerical errors inherent to any implementation.

**DAL D implementation** - This part will argue that the demonstration of conformity to satisfy a DAL D implementation can be reduced compared to the applicable EASA Concept Paper objectives.
## 2. CERTIFICATION STRATEGY

In the airborne context, a safety-critical system cannot be certified as long as it is not demonstrated that this system safely performs its intended function under all foreseeable operating and environmental conditions. The rigor of this demonstration is related to the system safety analysis which states the worst effect that the defined failure conditions can lead to at system level. If a software item is a possible contributor to a failure condition, this rigor is defined by an Development Assurance Level or DAL. This demonstration should entirely take place in the target environment except if the applicant is able to demonstrate that the implementation activities do not alter, in an unacceptable manner, the properties that have been verified in the design environment.

When it comes to the development of a MLC, the development assurance activities will have to be performed as per the W-shaped process described in the future ML standard [9]. This standard offers 2 categories of implementation, the main one (MLC as a container of items) has structured the W-process as described in the figure 3 of [9].

**First assumption: MLC as part of an item** - This paper suggests to explore the second category where the MLC is part of the item as described in appendix H of [9].

The certification strategy developed in this paper takes credit of the previous results of [13], where formal methods were used to verify that the ML models correctly perform the ACAS-Xu functional intent: for each point in the input space, the ML models compute the same advisory avoidance maneuver as the LUTs do (cf property 1 in [4] and called LUT property in the rest of the paper). For sure, formal methods remain a very attractive and powerful means compared to massive and costly testing activities that one would have to perform on the hardware platform to get the same level of confidence. As stated earlier, verification credit can be sought from these activities if the semantics of the designed model is preserved during the implementation.

**Second assumption: Controlled replication** - In the next section, this paper defines a replication metric for demonstrating that the properties of the trained model still hold after the implementation phase.

**Third assumption: Legacy item** - As a main assumption of the certification strategy, we assume that the ACAS-Xu legacy item was developed to the DO-178C/ED-12C standard guidance and that all the related lifecycle data are available. As a consequence, we will use the documents listed in the ED-12C/DO-178C [26] section 11 as a basis for the documentary baseline that will be modified by the MLC development.

**Fourth assumption: MLC replacing an existing SW component** - To this purpose, we propose a modification of the architecture of the ACAS-Xu item (cf Figure 4) replacing the software component “offline-cost-lookup” by “offline-cost-with-surrogate-models”. The design of this new SW component is the same as in [13] where a safety net complements the 45 surrogate models to get a correct advisory avoidance maneuver whatever the geometrical situation of the ownship/intruder in the input space. The partitioning of the input space between the safety net and the ML models was realized by formally

proving where the models were correctly performing or not (demonstration of the LUT property as per [4]).

<figure><img src="image_5.png" /><figcaption>Figure 4. Modified ACAS-Xu item architecture</figcaption></figure>

In the rest of the chapter 2, the EASA CP objectives are fulfilled using the artifacts from the ACAS-Xu function development. The applicability of these objectives versus the DAL (C or D) is mentioned in brackets before each objective.

### 2.1. EASA CP planning objectives fulfillment

[C-D] **Objective DA-01: The applicant should describe the proposed learning assurance process (...) as well as the interface and compatibility with development assurance processes** - The plan for learning aspects of certification is included in a specific section of the Plan for SW Aspect of Certification (PSAC), already developed for the item that hosts the MLC. Indeed, the item development is developed to AMC20-115D guidance for the classical aspect and the ML Concept Paper objectives for the MLC aspect. The future ML standard (EU-ROCAE ED-324) will be used when EASA recognizes its guidance as an acceptable means of compliance.

### 2.2. EASA CP specification objectives fulfillment

In this section we show compliance with some of the specification objectives from the EASA concept paper [7] that mainly require to complement the SW Requirement Data document (SRD) of the existing item.

[C-D] **Objective DA-02: Based on (sub) system requirements allocated to the AI/ML constituent, the applicant should capture the following minimum for the AI/ML constituent requirements** - The ACAS-Xu function was developed in an existing software component already specified in the SRD of the ACAS-Xu item. This means that those requirements that are specific to the MLC component specification (MLCRs) should be added as a specific section of the SRD.

* **Existing in SRD:** some MLC requirements (MLCRs) are already expressed through the existing High Level Requirements (HLRs) of the software item (described in the SRD - Software Requirement Data):

- Functional: the functional intent of the ACAS-Xu model (computation of the cost of each avoidance maneuver from the LUTs)

- Operational: SW performances allocated to the ACAS-Xu function along with any design constraints linked to the hardware features (e.g. timing and memory resources)

* ML specific in SRD:
- Behaviour: the ML models classification capability is refined from the SRD functional requirements allocated to the MLC SW component. The LUT property characterizes the behaviour of the ML models and is defined in the specific section of the SRD document.

[C-D] *Objectives DA-03/DA-04: ODD characterization* - this objective is easily fulfilled due to the fact that the LUTs fully captures the input space and consequently the entire Operational Design Domain (ODD), therefore these requirements are covered by the existing MOPS [8].

[C-D] *Objective DA-05: The applicant should capture the requirements on data to be pre-processed and engineered for the inference model in development and for the operations* - The MLCRs are completed with data processing requirements capturing the need for data normalization before feeding the models.

[C] *Objective DA-06: The applicant should describe a preliminary MLC architecture, to serve as reference for related safety (support) assessment and learning assurance objectives* - The MLC logical architecture into 45 models has been defined in the previous work [13] (cf Figure 5). This description is added in the existing SW Design Document (SDD).

<figure><img src="image_6.png" /><figcaption>Figure 5. MLC logical architecture</figcaption></figure>

[C-D] *Data Management (DM) Objectives* - These objectives are also easily met since the LUTs provide a complete dataset that fully covers the input space and, consequently, the entire ODD, with their corresponding deterministic and exact outputs. The DM objectives are defined to ensure trustworthy and correct data sampling (DM-01) and labeling (DM-02), data preparation (DM-04) and pre-processing (DM-03), feature engineering (DM-05), independence between split training, validation, and test datasets (DM-06), completeness, accuracy, and representativeness of the data (DM-07). Note that demonstrating compliance with them is generally necessary because the sampling distribution often differ, even slightly, from the true distribution, and the measured data often present some kind of noise or stochasticity. However, in the particular case of ACAS-Xu, the dataset (i.e. the LUTs) fully corresponds to the ground truth. The LUTs contain the exact q-cost of each possible discrete situation enumerated in the original problem. In other words, the tables do not estimate or observe the expression of some underlying function to be approximated, but they constitute the function itself. There is no sampling bias, distribution divergence, data imprecision or lacking. In this way, there is no overfitting problem. There is no need to separate data for training and test, since the dataset is the ground

truth, and a good model is supposed to maximally fit it. Related derived data management requirements are added in the SRD.

<figure><img src="image_7.png" /><figcaption>Figure 6. ACAS-Xu MLP model architecture</figcaption></figure>

## 2.3. EASA CP design objectives fulfillment

In this section we show compliance with some of the design objectives from the EASA concept paper [7]. The produced evidences that are specific to the MLC design aspect are documented in the SW Design Description document (SDD) of the existing item.

[C-D] *Objective LM-01: The applicant should describe the ML model architecture.* - In the ACAS-Xu, that model can correspond to a single multilayer perceptron presenting an input layer with 7 neurons (the 7 input variables), N hidden-layers containing $n_i$ neurons each, and an output layer containing 5 neurons (the 5 outputs). The MLP approximates the ground truth by regression, and the expected outputs are the q-costs of each of the 5 possible discrete actions. The input and hidden layers are followed by a specific activation function layer. In our implementation, and following the same architecture presented in the literature [17], we defined 6 hidden layers, each containing 50 neurons, followed by a ReLU activation function in a fully-connected design (all the neurons of a layer are connected to all the nodes in the preceding and subsequent layers). That architecture can be fully represented as a computation graph, in which each node represents a layer, and the edges represent the data flow. Alternatively, and since the input variables can be discrete, this big single ML model can be separated in diverse sub-models by removing one or more inputs. In the literature, some architectures split the solution among 45 smaller neural networks using 2 input variables for selecting, then sending the 5 other inputs to the selected network. The architecture is illustrated in the Figure 6

[C-D] *Objective LM-02: The applicant should capture the requirements pertaining to the learning management and training processes* - This objective asks for making explicit the used training metrics. The ACAS-Xu problem presents a particular characteristic that the objective is to approximate the q-costs, a regression task to which the loss function generally is MSE, but, at the same time, preserving the same decision, i.e. the choice of the action with minimal q-cost, a classification task
to which the loss function generally is cross-entropy. Depending on the defined requirements, both approaches are possible, as well as the use of a customized loss function designed to follow both objectives simultaneously (regression and classification), as it can be found in the literature with the asymmetric conditional MSE loss, which strongly penalizes q-cost overestimation for the best action, and underestimation for the other actions. When evaluating the model's performance, the accuracy score can be used to verify classification (action choice) correctness. The classification accuracy can be measured in two ways, either using weighted recall (which corresponds to the standard accuracy), or using macro recall (which corresponds to the balanced accuracy). In the first case, the weight of each class (decision) is equivalent to its frequency in the dataset, and in the second case, all the classes have the same weight, independent of their frequencies, as presented in the formulas:

$$Recall_{weighted} = \frac{p}{M} \qquad (1)$$

$$Recall_{macro} = \sum_{i=1}^{N} \frac{1}{K} \frac{p_i}{M_i} \qquad (2)$$

where p is the number of samples correctly classified (true positives), $p_i$ is the number of correct classifications for a given class $i \in \{1, \dots, K\}$, K is the number of classes, M is the total number of samples, and $M_i$ is the total number of samples pertaining to class i. In the 5D ACAS-Xu case developed in this paper, K = 5, which corresponds to the five possible actions in the problem, namely straight forward (COC - clear of conflict), weak right (WR), weak left (WL), strong right (SR), strong left (SL), and M = 32×41×41×12×12 = 7746048, corresponding to the number of combinations of the considered discretized dimensions ($\rho, \theta, \psi, v_{own}, v_{int}$).

In the general case, the loss evolution should be compared during learning between training and test dataset to detect overfitting. However, in the particular ACAS-Xu case, overfitting is fostered since the LUT covers the input space with exact values. There is no specific thresholds defined on the performance of the trained ML models because the hybrid architecture can mitigate the points where the ML models do not correctly approximate the LUTs. However, the better the ML models performance is, the less LUTs are embedded in the software.

[C] **Objective LM-03: The applicant should document the credit sought from the training environment and qualify the environment accordingly** - No credit is sought from the training environment for certification activities. In our implementation, the neural networks have been defined and trained in Python using the PyTorch libraries in a Linux workstation endowed with GPU. For certification, the versions of operating system, python and pytorch packages, as well as the model of CPU and GPU devices are specified in the SW Life Cycle Environment Configuration Index (SECI) document.

[C] **Objective LM-04: The applicant should provide quantifiable generalisation bounds** - Not addressed.

[C-D] **Objective LM-05: The applicant should document the result of the model training** - While training the neural network, the entire dataset is presented at each epoch, and the error averaged from batches of samples. The loss of each epoch

<figure><img src="image_8.png" /><figcaption>Figure 7. Evolution of cross-entropy loss and classification error during training (15000 epochs)</figcaption></figure>

is then averaged from the set of batches, and registered, with other metrics like the classification accuracy. That evolution is shown in the Figure 7.

[C] **Objective LM-06: The applicant should document any model optimisation that may affect the model behaviour (e.g. pruning, quantisation) and assess their impact on the model behaviour or performance.** - None optimisation is implemented.

[C] **LM-07-SL and LM-08-SL: The applicant should (a) account for the bias-variance trade-off in the model family selection and should (b) provide evidence of the reproducibility of the model training process; The applicant should ensure that the estimated bias and variance of the selected model meet the associated learning process management requirements** - In classic machine learning methods (e.g. polynomial regression), the bias-variance relation helps to demonstrate that the complexity of the chosen model is adequate to the problem. Simple complexity (e.g., linear regression) has a strong bias and can cause underfitting, while conversely, a too complex model (e.g., high-order polynomial) presents high variance, indicating high sensitivity to data, which can cause overfitting. However, such indicators are not adapted to deep multilayer perceptrons, which are considered universal approximators when the number of neurons per layer is sufficient. In [24], that number is defined as $max\{d_x + 1, d_y\}$, where $d_x$ is the number of input dimensions, and $d_y$ the number of output dimensions. For the ACAS-Xu problem, the minimal width for a MLP is then supposed to be 6, and the model architecture considered here, the hidden layers have 50 neurons.

[C-D] **LM-09: The applicant should perform an evaluation of the performance of the trained model based on the test dataset and document the result of the model verification** - As indicated in DM objectives, in the ACAS-Xu problem there is no separated train and test datasets since the available data corresponds to the ground truth and comprehends the integral and non-biased function to be learned. We consider that the model evaluation should then be made against that same dataset. In that verification, we obtain $Recall_{weighted} = 0.979$ and $Recall_{macro} = 0.951$. The resulting verification is presented in the form of a confusion matrix in the Figure 8.

[C-D] **LM-10: The applicant should perform requirements based verification of the trained model behaviour** - The functional intent of the ACAS-Xu models is defined by its capability to make the LUTs decisions whatever the point in the entry space (LUT property). It was defined by a mathematical property that was verified using formal methods on all the
<figure><img src="image_9.png" /><figcaption>Figure 8. Confusion matrix presenting the model accuracy.</figcaption></figure>

continuous input space during previous work [4]. As stated earlier, this verification activity is key in the ACAS-Xu use case as it guarantees the LUT classification by the ML models on a partition of the ODD (the rest of the ODD is covered by the safety net). This activity is described in the existing SW Verification Cases and Procedures document (SVCP) and their results reported in the SW Verification Results document (SVR).

[C] LM-11: The applicant should provide an analysis on the stability of the learning algorithms - Not addressed.

[C-D] LM-12: The applicant should perform and document the verification of the stability of the trained model, covering the whole AI/ML constituent ODD - refer to the analysis in section 4.3.

[C-D] LM-13 (robustness) and [C] LM-14 (generalisation bounds): These verification objectives are covered by the fulfillment of the objective LM-10.

[C-D] LM-15: The applicant should capture the description of the resulting ML model - The models are exported from the design framework using the Implementation Model Specification (IMS) format. We will use IMS in the rest of the paper. The IMS format supports the ML model semantics description (see section 3.1 for details). The IMS can be used as input requirements to implement the ML inference models in the MLC SW component and considered as SDD detailed design. In addition, SRD and SDD documents contain all the necessary information for the MLC implementation:

* MLCRs including the data processing requirements

* the MLC logical architecture

* any design constraints for the implementation

[C] LM-16: The applicant should confirm that the trained model verification activities are complete - The review of the SVCP and SVR as per ED-12C/DO-178C [26] guidance should cover this objective.

## 2.4. EASA CP implementation objectives fulfillment

In this section we show compliance with some of the implementation objectives from the EASA concept paper [7].

[C-D] Objective IMP-01: The applicant should capture the requirements pertaining to the ML model implementation process - The ML models are replacing the LUTs in an existing software component which is already identified in the architecture of the ACAS-Xu item. Therefore, the requirements and the design description are those defined during the design phase (LM-01, LM-02) and gathered in the SRD/SDD documents (see LM-15). As per the 2nd assumption of the certification strategy (controlled replication), this paper offers a demonstration that the properties of the ML trained models still hold after implementation (this is the purpose of chapter 3). To this purpose, we have added specific implementation requirements to define metrics to compute the approximation error between the inference and the trained model, and the tolerance on these metrics to consider that the error is acceptable. These derived requirements are added in the SDD as detailed design constraints. These requirements are defined in section 3.2.

[C-D] Objective IMP-02: The applicant should validate the model description captured under Objective LM-15 as well as each of the requirements captured under Objective IMP-01 - Though no activities were performed to cover this objective, we suggest using the requirement review process as per ED-12C/DO-178C [26] guidance to address it.

[C-D] Objective IMP-03: The applicant should document evidence that all derived requirements generated through the model implementation process have been provided to the (sub) system processes, including the safety (support) assessment - Any adversarial area from the input space where the approximation error is greater than the acceptable thresholds (defined in 3.2) should be identified as a derived requirement and passed up to the system in order to modify the partitioning of the input space between the ML models and the safety net. Again ED-12C/DO-178C [26] guidance should cover this objective.

[C] Objective IMP-04: Any post-training model transformation (conversion, optimisation) should be identified and validated for its impact on the model behaviour and performance, and the environment (i.e. software tools and hardware) necessary to perform model transformation should be identified. - The verification of the trained models is performed using their native format (python code). Then the ML models are described within the IMS mathematical format. At last, the models are implemented into a language (C code) compatible with the selected target. The target is a NXP T1042 CPU, the source code is generated by a SCADE generator and compiled with a Windriver Diab compiler. The re-interpretation of the sequence of operations of the ML trained models into a new language, the compiler options, the configured floating point rounding mode does impact the models behaviour and performance, due to numerical error propagation. However, the next chapter will demonstrate that this impact can be mastered using the controlled replication method [28] in order to preserve the ML models semantics and meet the derived requirements defined in IMP-01.

[C] Objective IMP-05: The applicant should plan and execute appropriate development assurance processes to develop the inference model into software and/or hardware items. - The MLC is developed as a classical SW component from its
requirements defined in the SRD and SDD of the ACAS-Xu
item with respect to the ED-12C/DO-178C [26] development
assurance guidance. The IMS can be considered as both in-
put requirements (see LM-15) and Low-Level Requirements
(LLRs) for the implementation of the new software compo-
nent. In addition, the data processing software aspects can be
developed from the MLCRs.

[C] **Objective IMP-06: The applicant should verify that any transformation (conversion, optimisation, inference model development) performed during the trained model implementation step has not adversely altered the defined model properties.** - The chapter 3 provides elements to demonstrate that the models properties have been preserved after the implementation phase and the evidences are reported in the SVR.

[C] **Objective IMP-07: The differences between the software and hardware of the platform used for model training and those used for the inference model verification should be identified and assessed for their possible impact on the inference model behaviour and performance** - The implementation of the models low level semantics (e.g. floating point arithmetic) is target-dependent and consequently different in the design and the target environment. This may lead to cost computation different from the LUTs. Again, the chapter 3 provides elements to mitigate this risk and demonstrate that the models properties have been preserved after the implementation phase.

[C-D] **Objective IMP-08: The applicant should perform an evaluation of the performance of the inference model based on the test data set and document the result of the model verification.** - These activities are detailed in the chapter 3. The ML models performance metrics were firstly computed using the trained models (called $\hat{f}_1$). Then, they are computed again using the inference models (called $\hat{f}_2$) to verify that the defined tolerances (see derived requirements defined in IMP-01) are attained using the test dataset in the target environment. These verification activities are performed on the target and the result is documented in the SVR.

[C-D] **Objective IMP-09: The applicant should perform and document the verification of the stability of the inference model.** - The ML implementation stability is verified through the analysis of the distribution of the $|\hat{f}_2(x) - \hat{f}_1(x)|$ in section 3.3.

[C-D] **Objective IMP-10: The applicant should perform and document the verification of the robustness of the inference model in adverse conditions** - The ML models performance is evaluated inside the original dataset which represents the full input space and the ODD (there are no points outside the ODD). In addition the models are verified to perform correctly in their allocated part of the ODD. This covers the robustness aspect.

[C-D] **Objective IMP-11: The applicant should perform requirements based verification of the inference model behaviour when integrated into the AI/ML constituent** - Thanks to the "controlled replication" method described in chapter 3, a verification credit can be sought from the design verification activities and the demonstration of the LUT property is not to be performed in the target environment. Therefore, the functional intent of the NN-based controller (see Figure 5) is verified.

[C] **Objective IMP-12: The applicant should confirm that the AI/ML constituent verification activities are complete.** - The review of the SVCP and SVR as per ED-12C/DO-178C [26] guidance should cover this objective.

**2.5. EASA CP verification objectives fulfillment**

[C-D] **DA-10: Each of the captured AI/ML constituent requirements should be verified** - As per Figure 5, test cases needs to be added to fully cover the MLCRs at the boundary of the MLC. In particular, the verification of the operational aspects should be performed. These tests are run on the target. Specific test cases and procedures are added in the SVCP document and their results reported in the SW Verification Results document (SVR).

**3. SEMANTICS PRESERVATION**

**From Implementation Model Specification (IMS) to code.**
The ACAS-Xu trained models previously described in their IMS intermediate format (see LM-15), are transformed into C code in two steps. First the Scade tool [6] is used to design manually the model structure with respect to the trained model hyper parameters definition. The matrix multiplications are designed with Map and Fold operators 9. The tool also generates qualified (DO-330/ED-215) C source code, with some guarantees on memory usage, and the correctness of the control and data flow, with respect to DO-178/ED-12 objectives.

<figure><img src="image_10.png" /><figcaption>Figure 9. Model Design (dot-product)</figcaption></figure>

Second, the model parameters are converted to imported constant into the Scade model. The verification of this transformation is supported by both the review of the model graph, and the computation of the model parameters checksum. The generated source code is compiled with the CompCERT [21] compiler for the target processor.

One way to preserve the semantics of the trained model, is to perform a black box assessment of the function performed by the model. In this paper, we rely on the computation of metrics on the trained model, with some threshold requirement and specified margins, in order to guarantee the target model performance.

**3.1. Classification task metric**

The ACAS-Xu model output is used to take the decision maneuver, in order to avoid air collision. Let the decision alternatives be Clear Of Conflict (COC), Weak Right (WR), Weak Left (WL), Strong Right (SR), Strong Left (SL). The LUTs contain an integer score $u$ for each class of avoidance maneuver. The lowest score leads to the decision. Therefore we define $\text{argmin}(u) := \{i, \forall u_j \in u, u_i < u_j\}$. The ground truth for training will be defined as the one hot encoding of the decisions (e.g. $y = \{0, 1, 0, 0, 0\}$ means WR decision shall be taken).
$$y_i := \begin{cases} 1 & \text{if } i = \operatorname{argmin}(u) \\ 0 & \text{otherwise.} \end{cases}$$

In the LUT, if there are several minimal scores for the same sample, the argmin chooses deterministically the first one as the ground truth (e.g. {3021, 2030, 2030, 4040, 2030} leads to {0, 1, 0, 0, 0}). During training, the cross entropy loss function converts the model output into probabilities with the softmax function defined by:

$$\hat{y} = \hat{f}_1(x), \operatorname{softmax}(\hat{y}_i) = \frac{e^{\hat{y}}}{\sum_i e^{\hat{y}_i}}$$

During inference, the decision id i is defined by:

$$\begin{aligned} \operatorname{argmax}(\hat{y}) &:= \{i, \forall \hat{y}_j \in \hat{y}, \hat{y}_i > \hat{y}_j\} \\ i &= \operatorname{argmax}(\operatorname{softmax}(\hat{y})) = \operatorname{argmax}(\hat{y}) \end{aligned}$$

In this paper, we consider and use the classification task metric Top-1¹ accuracy defined by:

$$\operatorname{Top1}(y, \hat{f}_1) = \frac{\sum_{j}^{n} (\hat{f}_1(x_j) = y_j)}{n} \text{ where } n \text{ is the number of samples.}$$

**ML model semantics definition** The ML model semantics is the set of relations between the model output and its input. These relations are formalized in the specification of the ML model that is exported from the design framework in the IMS for implementation purposes. The IMS both describes the trained model produced by the training execution environment and the model to be deployed in the target environment. The semantics of the ML model can be decomposed into semantic layers, which refine the computations performed to implement the relationships between the input and output of the ML model. In this paper, the IMS will capture the mathematical relationships semantics. Low-level semantics (rounding policy, arithmetic operation ordering,...) are design-dependent. Therefore, the differences between the training execution environment and the target implementation execution environment lead to differences in the prediction output. Nevertheless, we can bound these differences, with a controlled margin that preserves the semantic level of the IMS. Let x be the sample input, y = f(x) the ACAS-Xu ground truth, $\hat{f}_1(x)$ the ACAS-Xu model prediction output in the training environment, $\hat{f}_2(x)$ the target implementation prediction output, $\operatorname{Top1}(f, \hat{f}_1)$ is the Top1 accuracy metric in the training environment, $\operatorname{Top1}(f, \hat{f}_2)$ this metric in the target environment. We claim that the semantics is preserved when $\operatorname{Top1}(f, \hat{f}_2)$ is greater than the threshold requirement $R_{Top1}$, within a margin budget $g_{Top1}$, i.e.

$$\operatorname{Top1}(f, \hat{f}_2) \geq \operatorname{Top1}(f, \hat{f}_1) - g_{\operatorname{Top1}} \geq R_{\operatorname{Top1}}. \quad (3)$$

Using the method of [28], We also claim that equation 3 is verified if $\forall x, \hat{f}_2(x) - \hat{f}_1(x) < \varepsilon_{Top1}$. In this method, we compute the relation between $g_{Top1}$ and $\varepsilon_{Top1}$. The ML model verification is then split into 3 phases: 1- Defining the Average Precision margin budget $g_{Top1}$, 2- Verification of $\operatorname{Top1}(f, \hat{f}_1)$ - $g_{Top1} \geq R_{Top1}$ in the training environment, 3- Verification of $\hat{f}_2(x) - \hat{f}_1(x) < \varepsilon_{Top1}$ in the target environment.

## 3.2. Metrics requirement specification

Let us elicit the requirements:

The Top1 accuracy of $\hat{f}_2$ shall be greater than $R_{Top1} = 97\%$. For the samples corresponding to the 3% of mis-predicted decisions, we fallback into the safety net. We specify a margin budget $g_{Top1}$ of 0.5%.

In the training framework, we shall verify on the full dataset that:

$$\begin{aligned} \operatorname{Top1}(f, \hat{f}_1) - g_{\operatorname{Top1}} &\geq R_{\operatorname{Top1}} \\ \operatorname{Top1}(f, \hat{f}_1) - 0.5\% &\geq 97\% \\ \operatorname{Top1}(f, \hat{f}_1) &\geq 97.5\% \end{aligned}$$

The Top1 accuracy of $\hat{f}_1$ shall be greater than $R_{Top1} + g_{Top1} = 97.5\%$ (first condition), allowing an implementation margin $g_{Top1}$ of 0.5%. On the figure 10, we are computing $\operatorname{Top1}(f, \hat{f}_1)$ as a function of $\varepsilon$. As $\hat{f}_2$ is not known yet, we sample $\varepsilon$ values as $2^{-n}$ for $n \in [24, 8]$, and for the decision class of sample x we simulate a worst case error for $\hat{f}_2(x) = \hat{f}_1(x) - \varepsilon$.

On the figure 10, we intersect horizontally the curve $\operatorname{Top1}(\varepsilon)$ at the requirement $R_{Top1} + g_{Top1} = 97.5\%$ threshold, which vertically intersect $\varepsilon$ axis at $\varepsilon_{Top1} \approx 2^{-10}$.

Therefore, the implementation model satisfies the requirement $\operatorname{Top1}(f, \hat{f}_2) \geq R_{Top1}$ if $\hat{f}_2$ satisfies $\forall x, |\hat{f}_2(x) - \hat{f}_1(x)| < 2^{-10}$ (second condition).

<figure><img src="image_11.png" /><figcaption>Figure 10. $\operatorname{Top1}(\varepsilon)$</figcaption></figure>

## 3.3. Metrics requirement verification

On the figure 10, we observe that $\operatorname{Top1}(\varepsilon = 0) = 97.9\% > 97.5\%$, which satisfies the first condition.

On the target system, we verify that $\varepsilon(x) = \hat{f}_2(x) - \hat{f}_1(x) < \varepsilon_{Top1} \forall x$ randomly sampled in the input space. On the figure 11, the computed values of $\varepsilon(x)$ are reported in function of $\hat{f}_1(x)$, which learns us that the maximum error is greater than $2^{-13}$. This represents a 12-bit reduction in precision relative to the 24-bit floating point mantissa. We can confirm this relative numerical instability issue with a complementary observation: we compute $\hat{f}_1(x + 1 \text{ ULP})$, with ULP the Unit in the Last Place. We obtain the same distribution as the $\varepsilon(x)$ distribution in figure 11. It confirms that $\hat{f}_1$ conditioning limits

<footnote n="1">¹https://scikit-learn.org/stable/modules/generated/sklearn.metrics.top_kendorscore.html</footnote>
the computational accuracy achievable by any implementation
$f_2$.

Despite this issue, we observe on the figure 11, that $\forall x, \varepsilon(x) = |\hat{f}_2(x) - \hat{f}_1(x)| < 2^{-12} < 2^{-10} = \varepsilon_{Top1}$. Therefore, the second condition is satisfied, and we indeed verified that $Top1(f, \hat{f}_2) \geq R_{Top1}$.

<figure><img src="image_12.png" /><figcaption>Figure 11. $log2(\varepsilon) = log2(|\hat{f}_2(x) - \hat{f}_1(x)|)$</figcaption></figure>

4. DAL D IMPLEMENTATION

With respect to a due analogy with the EUROCAE/RTCA
standard ED-12C/DO-178C ([26] used by the avionic industry
to develop classical safety-related software, one should con-
sider that the modulation of the EASA concept paper objec-
tives ([7]) and their anticipated means of compliance could
be challenged with respect to the black box approach of the
current existing standard. In this section, we may challenge
the applicability of some objectives. For those which are not
quoted, the applicability [C and/or D] described in chapter 2
applies.

1. Planning objectives: all objectives are applicable.

2. Specification objectives: they are fully applicable as they are considered to complement the high level requirements of the item, in particular the data management activities are instrumental to the specification of the MLC functional intent. Considering the documentation of the SW architecture and conversely to EASA recommendation, we think that the MLC logical architecture description (DA-06) should be described even for a DAL D as it is the case for ED-12/DO-178 (SW architecture) and for ED-324/ARP6983.

3. Design objectives: On one hand we consider that the first part of the objectives (LM-01 to LM-08) are directly linked to the detailed design of the ML models and as such are not relevant for a DAL D MLC development as it is for ED-12/DO-178. On the other hand, LM-09, LM-10, LM-12 and LM-13 objectives are related to the verification of the performance of the trained models with respect to the test dataset, to the verification of their behaviour in their allocated ODD. Therefore, they have their place whatever the DAL is. Eventually the outcomes of LM-15

(ML models description) are needed to provide the re-
quirements for the implementation of the MLC SW com-
ponent as part of the existing item.

4. Implementation objectives: The content of the IMS is sufficient for a DAL D item implementation and so no other requirement capture is needed. Therefore, IMP-01 will capture the IMS input requirements, however IMP-02, IMP-03 and IMP-04 which document the detailed design are not relevant. IMP-05 obviously applies using ED-12C/DO-178C. As already modulated by the EASA concept paper, the objectives IMP-06 and IMP-07 about the analysis of the alteration of the target environment on the trained models is not retained. If there is no doubt that IMP-11 (rerun of the test dataset on the target) is relevant, we challenge the needs for applying objectives IMP-10 because we think that the performance of the full dataset with IMP-11 activities cover. IMP-09 was achieved by the demonstration that numerical instability does not impair the model performance.

5. Verification objectives: all objectives are applicable.

5. CONCLUSIONS

This paper presented a comprehensive strategy for implement-
ing and certifying legacy safety-critical avionics systems en-
hanced with ML-based surrogate models. By focusing on the
ACAS-Xu use case, we demonstrated a method to replace
heavy analytical models (Look-Up Tables) with neural net-
works while ensuring compliance with the anticipated EASA
"Guidance for Level 1 & 2 Machine Learning Applications"
issue 2.

Our approach was structured around three main contributions. First, we defined a Certification Strategy based on the integration of an ML Constituent (MLC) into an existing DO-178C software item. We detailed the fulfillment of EASA objectives across planning, specification, design, and verification phases, proposing a hybrid architecture where ML models are complemented by a safety net to ensure correct behavior across the input space.

Second, regarding Semantics Preservation, we addressed the
challenge of the "controlled" replication. We established a rig-
orous method using Top-1 accuracy metrics and defined error
margins to demonstrate that the properties formally verified on
the trained model remain valid for the inference model running
on the target hardware. This ensures that the implementation
process does not unacceptably alter the model's functional in-
tent.

Third, we analyzed the implications of a DAL D Implemen-
tation, arguing that for lower assurance levels, the burden of
certain detailed design and robustness objectives can be re-
duced. We proposed that standard ED-12C/DO-178C verifi-
cation activities (specifically the rerun of test datasets on the
target) sufficiently cover stability and robustness requirements
for this level.

While the proposed workflow offers a robust framework for
certification, the applicability of this approach to other ML
functions requires careful consideration of the specific nature
of the ACAS-Xu use case. ACAS-Xu presents a unique advan-
tage: the legacy Look-Up Tables (LUTs) provide a compre-
hensive definition of the Operational Design Domain (ODD) and serve as an absolute ground truth. Consequently, the dataset contains no sampling bias, noise, or distribution divergence, effectively eliminating common ML risks such as overfitting or data unrepresentativeness. In contrast, other avionics use cases (such as virtual sensing based on noisy sensor data) lack this "perfect" reference. In those scenarios, the ground truth is an approximation, and the ODD may not be fully enumerable. Therefore, while the pipeline for Semantics Preservation (ensuring the target matches the design) is universally applicable, the Design Assurance strategy would need adaptation. Specifically, other use cases would require significantly more effort in Data Management (checking representativeness) and Robustness verification (handling Out-Of-Distribution data) than was necessary for ACAS-Xu, where the input space was fully covered and deterministic.

Finally, as future work, we intend to rebuild the neural networks described in the paper using Aidge, a machine learning framework designed to train, transform, optimize, quantize, and generate the corresponding source code for the specific target hardware. Aidge<fnref n="2" /> is designed to make all those operations in a deterministic, reproducible, and transparent manner, which can help to demonstrate compliance with some of the considered certification objectives.

## REFERENCES

[1] S. Bak and H.-D. Tran. *Neural Network Compression of ACAS Xu Early Prototype Is Unsafe: Closed-Loop Verification Through Quantized State Backreachability*, page 280–298. Springer, 2022.

[2] S. Chichin, D. Portes, M. Brundler, and V. Jegu. Capability to Embed Deep Neural Networks: Study on CPU Processor in Avionics Context. In *Proc. of ERTS*, 2020.

[3] A. Clavière, E. Asselin, C. Garion, and C. Pagetti. Safety Verification of Neural Network Controlled Systems. In *51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)*, Taipei, Taiwan, June 2021.

[4] M. Damour, F. de Grancey, C. Gabreau, A. Gauffriau, J.-B. Ginestet, A. Hervieu, T. Huraux, C. Pagetti, L. Ponsolle, and A. Clavière. Towards Certification of a Reduced Footprint ACAS-Xu System: a Hybrid ML-based Solution. In *Safecomp 2021*, pages 34–48, 2021.

[5] T. DeWolf, P. Jaworski, and C. Eliasmith. Neurorobotics Nengo and Low-Power AI Hardware for Robust, Embedded Neurorobotics. *Frontiers in Neurorobotics*, 2020.

[6] F. X. Dormoy. SCADE 6 A Model Based Solution For Safety Critical Software Development. In *ERTS 2008 proceedings*, toulouse, France, Jan. 2008.

[7] EASA. Concept Paper: Guidance for Level 1&2 Machine Learning Applications (Issue 2), March 2024. European Aviation Safety Agency (EASA), Cologne.

[8] EUROCAE. ED-275: Minimal Operational Performance for Airborne Collision Avoidance System Xu (ACAS-Xu) – Vol. I, 2020.

[9] EUROCAE/SAE. ARP6983 / ED-324: Process Standard for Development and Certification/Approval of Aeronautical Safety-Related Products Implementing Artificial intelligence. EUROCAE WG-114 / SAE G-34, (Draft 7/Open Consultation).

[10] C. Gabreau, A. Gauffriau, F. de Grancey, J.-B. Ginestet, and C. Pagetti. Toward the certification of safety-related systems using ML techniques: the ACAS-Xu experience. In *Proc. of ERTS*, page Session Th.4.C Assurance & Certification, 2022.

[11] C. Gabreau, A. Gauffriau, M.-C. Teulières, D. Marandas, C. Pagetti, and C. Maxim. Implementation using ED-XXX/ARP6983: the ACAS-Xu experience. In *CTIC 2023*, 2023.

[12] C. Gabreau, B. Pesquet-Popescu, F. Kaakai, and B. Lefevre. AI for Future Skies: On-going standardisation activities to build the next certification/approval framework for airborne and ground aeronautical products. In *Proc. of the Workshop on Artificial Intelligence Safety (AISafety)*, 2021.

[13] C. Gabreau, M.-C. Teulières, E. Jenn, A. Lemesle, D. Potop-Butucaru, F. Thiant, L. Fischer, and M. Turki. A study of an ACAS-Xu exact implementation using ED-324/ARP6983. In *Proc. of ERTS*, 2024.

[14] A. Gauffriau, I. De Albuquerque Silva, and C. Pagetti. Formal description of ML models for unambiguous implementation. In *12th European Congress on Embedded Real Time Software and Systems (ERTS 2024)*, Toulouse, France, June 2024.

[15] F. Geissler, S. S. Qutub, S. Roychowdhury, A. A. Khoshouyeh, Y. Peng, A. Dhamasia, R. Graefe, K. Pattabiraman, and M. Paulitsch. Towards a safety case for hardware fault tolerance in convolutional neural networks using activation range supervision. *CoRR*, abs/2108.07019, 2021.

[16] K. Gupta, B. Pesquet-Popescu, F. Kaakai, and J.-C. Pesquet. A quantitative analysis of the robustness of neural networks for tabular data. In *ICASSP 2021 - 2021 IEEE Int. Conf. on Acoustics, Speech and Signal Processing (ICASSP)*, pages 8057–8061, 2021.

[17] K. D. Julian, J. Lopez, J. S. Brush, M. P. Owen, and M. J. Kochenderfer. Policy compression for aircraft collision avoidance systems. In *35th IEEE/AIAA Digital Avionics Systems Conference, DASC*, pages 1–10. IEEE, 2016.

[18] G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. *CoRR*, abs/1702.01135, 2017.

<footnote n="2">²https://www.deepgreen.ai/en/platform</footnote>
[19] G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. CoRR, abs/1702.01135, 2017.

[20] A. Leoni, Z. Marinković, and L. Pantoli. On the introduction of neural network-based optimization algorithm in an automated calibration system. In 2019 14th Int. Conf. on Advanced Technologies, Systems and Services in Telecommunications (TELSIKS), pages 323–326, 2019.

[21] X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister, and C. Ferdinand. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Toulouse, France, Jan. 2016. SEE.

[22] G. Li, S. K. S. Hari, M. Sullivan, T. Tsai, K. Pattabiraman, J. Emer, and S. W. Keckler. Understanding error propagation in deep learning neural network (dnn) accelerators and applications. In Proc. of the Int. Conf. for High Performance Computing, Networking, Storage and Analysis (SC17), pages 1–12, 2017.

[23] Manfredi and Jestin. An introduction to ACAS-Xu and the challenges ahead. In 35th IEEE/AIAA Digital Avionics Systems Conference, DASC, 2016.

[24] S. Park, C. Yun, J. Lee, and J. Shin. Minimum width for universal approximation, 2020.

[25] J. Perez-Cerrolaza and al. Artificial intelligence for safety-critical systems in industrial and transportation domains: A survey. ACM Computing Surveys, 2023.

[26] RTCA Inc / EUROCAE. DO-178 / ED-12C – Software Considerations in Airborne Systems and Equipment Certification, 2011.

[27] C. Seren, P. Ezerzere, and G. Hardier. Model-based techniques for virtual sensing of longitudinal flight parameters. Int. J. Appl. Math. Comput. Sci., 25(1):23–38, Mar. 2015.

[28] N. Valot, L. Fabre, B. Lesage, A. Mechouche, and C. Pagetti. Implementation of airborne ML models with semantics preservation. In 44th Digital Avionics Systems Conference (DASC), Montreal, Canada, Sept. 2025.