Daouda Diakite
email: daouda.diakite@l2s.centralesupelec.fr

Nicolas Gac
email: nicolas.gac@l2s.centralesupelec.fr

FPGA implementation of 2D Convolution using OneAPI and OpenCL

Keywords: Convolution, Local memory, OneAPI, OpenCL

Thanks to High-Level Synthesis (HLS) tools, FPGAs have become an alternative to GPUs for compute-intensive applications. These tools have been developed to provide flexibility in FPGA design at a higher abstraction level than hardware description languages. Major FPGA manufacturers have proposed many HLS tools depending on the target audience. In this paper, we propose a hardware architecture on FPGA for 2D convolution designed through two software-like development tools based on oneAPI and OpenCL languages. This paper also focuses on comparing the oneAPI and OpenCL HLS tools in terms of performance and productivity with the case study of the 2D convolution operator using an Intel Stratix 10 device.

I. INTRODUCTION

Convolution is one of the most used operators in signal and image processing applications such as edge detection, image blurring, noise reduction [START_REF] Burger | Digital image processing: an algorithmic introduction using Java[END_REF]. The operator is very compute-intensive, mainly used in iterative algorithms for inverse problems such as deconvolution [START_REF] Idier | Bayesian approach to inverse problems[END_REF]. It is essential to have significant computing power and a consequent bandwidth to meet the high computational demand. The acceleration of 2D convolution has been explored on different computing architectures such as CPU, GPU, or FPGA [START_REF] Fowers | A performance and energy comparison of convolution on gpus, fpgas, and multicore processors[END_REF], [START_REF] Jin | Exploration of OpenCL 2d convolution kernels on intel FPGA, CPU, and GPU platforms[END_REF]. Many approaches have been developed to accelerate the convolution operator, such as the reduction of the arithmetic complexity notably by using Winograd method [START_REF] Winograd | Arithmetic complexity of computations[END_REF], simple matrix multiplication using core tensors [START_REF] Seznec | A new convolutions algorithm to leverage tensor cores[END_REF] or element-wise multiplication in the Fourier domain [START_REF] Brigham | The fast Fourier transform and its applications[END_REF]- [START_REF] Vasilache | Fast convolutional nets with fbfft: A gpu performance evaluation[END_REF]. The element-wise multiplication in the Fourier domain followed by the inverse Fourier transform delivers better throughput than the convolution in the image domain for large mask sizes [START_REF] Seznec | A study on convolution using half-precision floating-point numbers on gpu for radio astronomy deconvolution[END_REF]. These works also explored different computational accuracy (half, fixed, single, or double precision) to leverage the underlying architecture better. This paper will focus on the pipeline execution model for FPGA. We proposed a convolution accelerator with a memory access strategy to reuse the data and improve the algorithm's arithmetic intensity, allowing us to use FPGA BRAM efficiently.

II. 2D CONVOLUTION

The 2D convolution represents a multiply-accumulation operation between a mask (convolution kernel) and the pixels of a given image. Let f be a 2D image of size (H, W) and h a mask of size (K, K), the convolution of f by h noted F is given by:

F (x, y) = K-1 j=0 K-1 i=0 f (x -(i - K 2 ), y -(j - K 2 ))h(i, j) (1)
To deal with the problem of image edge, we use the zeropadding method, which allows us to maintain the size of the input image. The pixel padding technique is often the acceptable solution to handle image edges, and zero-padding is the simplest to implement among the different types of padding used [START_REF] Ström | A parallel fpga implementation of image convolution[END_REF].

III. FPGA-BASED CONVOLUTION

We have described equation 1 in OpenCL and oneAPI for an FPGA implementation by performing the same optimizations to evaluate the efficiency of both tools. We will compare the efficiency of these tools on this operator using several mask sizes. method is used on FPGA to perform the convolution using Hardware Description Languages (HDL). In that case, the shift is applied to the local buffer for the input data to add new incoming data at the bottom of the buffer. Therefore, the buffer size cannot be too large to avoid expensive shift costs. In our implementation, the shift is only applied to the mask buffer, which is implemented into FPGA registers. A local buffer is At each iteration of loop yn, a new image line is inserted into the local buffer replacing the buffer line whose coefficients will no longer be used for this iteration as illustrated in Fig. 1.

The circular shift intends to switch the rows of the convolution mask so that the element-wise multiplication of the input image and the mask is done with correct correspondence between their lines. At a given iteration n, the circular buffer contains all the input data to compute a line of the output image without access to global memory. However, for the next iteration n + 1, the line at the top of the buffer is no longer required to compute the next output line. Therefore this line is replaced by a new image line, and then the bottom line of the mask buffer becomes the top to match coefficients. Then, for iteration n + 2, the second line of the local buffer is replaced by the new image line, and at the same time, the mask buffer is shifted. The convolution is performed this way until the output image is completely calculated. Compared to the prefetched data buffer, the mask buffer is smaller and is implemented using registers instead of BRAM resources. Therefore, this circular shift register will be less expensive and energy-efficient for the overall design. The pseudo-code of this version is presented in Algorithm 1.

IV. RESULTS AND DISCUSSION

We notice better performance for the OpenCL tool in almost all cases for the convolution operator. This performance advantage of OpenCL lies in the difference in depth of the generated pipeline. Indeed, we noticed a significant difference in these two tools' global memory access latencies (201 versus 818 cycles). This memory latency impacts the number of pipeline stages, especially in the blocks where access to global memory is required. This has little impact on performance for an ideal pipeline as long as the pipeline can produce a result at each clock cycle. Regardless of the depth, once filled, the pipeline can perform an update at every clock cycle (or at regular intervals), given that we are working on massive data. On the other hand, all the pipeline stages will be impacted if the computation is stalled due to memory accesses (high stall percentage). This delay will propagate in pipeline depth, which will prevent an update from being produced at each clock cycle. Synthesis tool with oneAPI is less advantageous in this regard, with a 4× higher global memory latency than using OpenCL, and this latency will affect the generated pipeline. In any case, a reduction of global memory access is necessary to guarantee better performance, and for this reason, local memory usage must be privileged. Our optimized versions reduce the memory access, and the stall percentage is alleviated. The results of the optimized versions are presented in table I for the oneAPI and OpenCL kernels. We can observe similar performance with a slight advantage for OpenCL due to the performance loss for oneAPI kernels.

V. CONCLUSION This paper deals with the acceleration of the 2D convolution operator on FPGA with high level languages. Several implementations have been implemented to evaluate the OpenCL and oneAPI synthesis tools from Intel. These tools allow to have an implementation on FPGA with a reduced development time, but a powerful design requires a deep analysis of the application in order to apply consequent FPGA-specific optimizations. We find that OpenCL offers the best tradeoff between development time and performance. However, oneAPI is gaining more and more maturity and could become an alternative to OpenCL.

Fig. 1 .

 1 Fig. 1. Memory access strategy with circular shift applied to the mask

  Our implementation uses shift register technique to leverage FPGA local memory. Traditionally, the shift register

	Algorithm 1 Optimized kernel
	end for
	end for
	output local[xn] = result
	end for
	F ← output local
	end for

for all yn do P ref etched new line into f local Circular Shif t the mask buf f er #pragma unroll 4 for all xn do result ← 0 #pragma unroll for all j do #pragma unroll for all i do Handle image border result+ = f local [xn, yn] * h[i, j]


Nicolas Julien

Ioana Paşca

Formal verification of exact computations using Newton's method

We are interested in the certification of Newton's method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq's Standard Library in order to validate the computation with Newton's method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton's method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient.

Introduction

The Standard Library of the Coq proof assistant [START_REF]The Coq Proof Assistant Reference Manual[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions[END_REF] contains a formalization of real numbers based on a set of axioms. This gives the real numbers all the desired theoretical properties and makes theorem proving more agreeable and close to "pencil and paper" proofs [START_REF] Mayero | Formalisation et automatisation de preuves en analyses reelle et numerique[END_REF]. However, this formalization has no (or little) computational meaning. During this paper we shall refere to the reals from this implementation as "axiomatic reals". We note that Coq is not an special case and proof assistants in general provide libraries with results from real analysis [START_REF] Cruz-Filipe | C-CoRN: The Constructive Coq Repository at Nijmegen[END_REF][START_REF] Fleuriot | On the mechanization of real analysis in Isabelle/HOL[END_REF][START_REF] Gamboa | Nonstandard Analysis in ACL2[END_REF][START_REF] Harrison | Theorem Proving with the Real Numbers[END_REF], but with formalizations for real numbers that are not well suited for computations. However, in a proof process, it is often the case that we are interested in computing with the real numbers (or at least approximating such computations), so a considerable effort has been invested in having libraries of exact computations for proof systems [START_REF] Julien | Certified exact real arithmetic using co-induction in arbitrary integer base[END_REF][START_REF] Lester | Real Number Calculations and Theorem Proving[END_REF][START_REF] Russell | Certified Exact Transcendental Real Number Computation in Coq[END_REF]. We shall refer to numbers from such implementations as "exact reals". These libraries provide certification of computations for a set of operations and elementary functions on real numbers.

The results in this paper are concerned with Newton's method. Under certain conditions, this method ensures the convergence at a certain speed towards a root of the given function, the unicity of this root in a certain domain and the local stability. But, as the "paper" proof for these results depends on non-trivial theorems from analysis like the mean value theorem and concepts like continuity, derivation etc. the formal development conducted around them is based on the axiomatic reals of Coq. We would like to transfer these "theoretical" properties to the computations done with exact reals. Our work is thus conducted in two directions. On one side we are interested in proving correct Newton's method on exact reals and having algorithms that are suited for our implementation of the real numbers as co-inductive streams. On the other hand we are concerned in providing appropriate theoretical results to support the correctness of the algorithms and optimizations we make.

The paper is organized as follows: in section 2 we present the theoretical results around Newton's method that have been verified with the axiomatic reals in Coq. This section gives the formalization of well-known results in [START_REF] Démidovitch | Éléments de calcul numérique[END_REF] and presents a new proof that was motivated by our implementation of the method on exact reals. To clarify the need for this proof, in section 3 we present a library of exact real arithmetic implemented with Coq's co-inductive streams and we discuss how computations with Newton's method can be certified in this setting. We also design and prove correct an algorithm for computing the root of a function that is based on Newton's method and is adapted for streams. However, this algorithm is much more efficient when rounding is used during the process. The theorem we present in section 2.1 justifies this optimization, though the optimized algorithm is not completely certified. The applications of our algorithm are given in section 4.4 along with perspectives opened by the suggested improvements. We finish by discussing related work in section 5 as well as conclusions and possible extensions of our work in section 6.

Kantorovitch's theorem and related results

Kantorovitch's theorem gives sufficient conditions for the convergence of Newton's method towards the root of a given function and establishes the unicity of this root in a certain domain. A version of this theorem as well as results concerning the speed for the convergence of the process and its stability are discussed in [START_REF] Démidovitch | Éléments de calcul numérique[END_REF]. Preliminary results around a formalization of these theorems inside the Coq proof assistant are described in [START_REF] Paşca | A Formal Verification for Kantorovitch's Theorem[END_REF]. At present all the theorems listed in this section are verified in the Coq proof assistant. The formal proof is based on the axiomatic real numbers from Coq's Standard Library. This choice is motivated by the concepts we needed to handle, as the library contains results from real analysis concerning convergence, continuity, derivability etc. The theorems listed bellow illustrate the type of concepts involved in the proof.

Theorem 1 (Existance) Consider an equation f (x) = 0, where f :]a, b[→ R , a, b ∈ R f (x) ∈ C (1) (]a, b[). Let x (0) be a point contained in ]a, b[ with its closed ε-neighborhood U ε (x (0) ) = {|x -x (0) | ≤ ε} ⊂]a, b[. If the following conditions hold: 1. f ′ (x (0) ) = 0 and | 1 f ′ (x (0) ) | ≤ A 0 ; 2. | f (x (0) ) f ′ (x (0) ) | ≤ B 0 ≤ ε 2 ; 3. ∀x, y ∈]a, b[, |f ′ (x) -f ′ (y)| ≤ C|x -y| 4. the constants A 0 , B 0 , C satisfy the inequality µ 0 = 2A 0 B 0 C ≤ 1.
then, for an initial approximation x (0) , the Newton process

x (n+1) = x (n) - f (x (n) ) f ′ (x (n) ) , n = 0, 1, 2, . . . ( 1
)
converges and lim n→∞ x (n) = x * is a solution of the initial system, so that |x * -

x (0) | ≤ 2B 0 ≤ ε.
Theorem 2 (Uniqness) Under the conditions of Theorem 1 the root

x * of the function f is unique in the interval [x (0) -2B 0 , x (0) + 2B 0 ].
Theorem 3 (Speed of convergence) Under the conditions of Theorem 1 the speed of the convergence of Newton's method is given by |x

(n) -x * | ≤ 1 2 n-1 µ 2 p -1 0 B 0 .
Theorem 4 (Local stability) If the conditions of Theorem 1 are satisfied and if, additionally, 0

< µ 0 < 1 and [x (0) -2 µ0 B 0 , x (0) + 2 µ0 B 0 ] ⊂]a, b[, then for any initial approximation x ′(0) that satisfies |x ′(0) -x (0) | ≤ 1-µ0
2µ0 B 0 the associated Newton's process converges to the root x * .

The convergence of the process ensures that Newton's method is indeed appropriate for determining the root of the function. The unicity of the solution in a certain domain is used in practice for isolating the roots of the function. The result on the speed of the convergence means we know a bound for the distance between a given element of the sequence and the root of the function. This represents the precision at which an element of the sequence approximates the root. In practice this theorem is used to determine the number of iterations needed in order to achieve a certain precision for the solution. The result on the stability of the process will help with efficiency issues as it allows the use of an approximation rather than an exact real.

We do not present here the proofs of the theorems, we just give a few elements of these proofs that are needed in understanding the next section. For details on the proofs we refere the reader to [START_REF] Démidovitch | Éléments de calcul numérique[END_REF]. The central element of the proof is an induction process that establishes a set of properties for each element of the Newton sequence. The proof introduces the auxiliary sequences {A n } n∈N , {B n } n∈N and {µ n } n∈N :

A n = 2A n-1 (2)
B n = A n-1 B 2 n-1 C = 1 2 µ n-1 B n-1 (3)
µ n := 2A n B n C = µ 2 n-1 (4)
For each element of the Newton sequence, we are able to verify properties that are similar to those for x (0) . Reasoning by induction we get the following:

• f ′ (x (n) ) = 0 and | 1 f ′ (x (n) ) | ≤ A n • |f (x (n) )/f ′ (x (n) )| ≤ B n ≤ ε • µ n ≤ 1
Notice that hypothesis 3. is a property of the function and it does not depend on the elements of Newton's sequence. From the above relations we get the convergence, unicity and speed of convergence for the sequence.

For Theorem 4 (local stability) we prove that the new initial approximation x ′(0) satisfies similar hypotheses as those for x (0) . The new constants are A ′ = 4 3+µ0 A 0 and B ′ = 3+µ0 4µ0 B 0 . This makes that µ ′ = 2A ′ B ′ C = 1 and we can verify that

• f ′ (x ′(0) ) = 0 and | 1 f ′ (x ′(0) ) | ≤ A ′ • |f (x ′(0) )/f ′ (x ′(0) )| ≤ B ′ • µ ′ ≤ 1
We are thus in the hypotheses of Theorem 1 and by applying this theorem we conclude that the process converges to the same root x * .

Notice, however, that for the new constants we get µ ′ = 1. If we do a Newton iteration, we would get the new µ ′′ = µ ′ 2 = 1 (cf. equation ( 4)) and we would not be able to do an approximation again, because Theorem 4 requires µ ′′ < 1.

To correct this, we impose a finer approximation |x 0 -x ′ 0 | ≤ (1-µ0) 4µ0 B 0 . This new approximation yields the following formulas for the constants:

A ′ = 8 7 + µ 0 A 0 (5)
B ′ = µ 2 0 + 46µ 0 + 17 8(7 + µ 0 )µ 0 B 0 (6)
this makes that

µ ′ = µ 2 0 + 46µ 0 + 17 (7 + µ 0 ) 2 < 1 (7)
We summarize these results in:

Corollary 1 If the conditions of Theorem 1 are satisfied and if, additionally, 0 < µ 0 < 1 and [x (0) -2 µ0 B 0 , x (0) + 2 µ0 B 0 ] ⊂]a, b[, then for any initial approximation x ′(0) that satisfies |x ′(0) -x (0) | ≤ 1-µ0 4µ0 B 0 the associated Newton's process converges to the root x * .

Newton's method with rounding

We now have all the necessary tools to state and prove a theorem on the behavior of Newton's method if we consider rounding at each step. The rounding we do is just good enough to ensure the convergence. This theorem is particularly interesting for computations in arbitrary or multiple precision, as it relates number of iterations with the precision of the input and that of the result. This means that for the first iterations we need a lower precision, as we are not close to the root. We will later increase the precision of our input with the desired precision for the result.

Theorem 5 We consider a function f :]a, b[→ R and an initial approximation x (0) satisfying the conditions in Theorem 1. We also consider a function rnd : N × R → R that models the approximation we will make at each step in the perturbed Newton sequence:

t (0) = x (0) and t (n+1) = rnd n+1 (t (n) -f (t (n) )/f ′ (t (n) )) If 1. ∀n∀x, x ∈]a, b[⇒ rnd n (x) ∈]a, b[ 2. 1 2 ≤ µ 0 < 1 3. [x (0) -3B 0 , x (0) + 3B 0 ] ⊂]a, b[ 4. ∀n∀x, |x -rnd n (x)| ≤ 1 3 n R 0 , where R 0 = 1-µ 2 0 8µ0 B 0 then a. the sequence {t (n) } n∈N converges and lim n→∞ t (n) = x * where x * is the root of the function f given by Theorem 1 b. ∀n, |x * -t (n) | ≤ 1 2 n-1 B 0
The first hypothesis makes sure that the new value will also be in the range of the function. The second and third hypotheses come from the use of the stability property of the Newton sequence (see Corollary 1). The fourth hypothesis controls the approximation we are allowed to make at each iteration. The conclusion gives us the convergence of the process to the same limit as Newton's method without approximations. Also we give an estimate of the distance from the computed value to the root at each step.

Proof. Our proof is based on those for theorems 1 -4 and corollary 1. To give the intuition behind the proof, we decompose Newton's perturbed process t (n) as follows:

1. set t (0) := x (0) 2. do a Newton iteration to get x (1)

:= t (0) -f (t (0) ) f ′ (t (0) )
3. do an approximation of the result to get t (1) := rnd(x (1) ) 4. set t (0) := t (1) and go to step 2.

Now let's look at these steps individually:

• At step 1. we start with the initial x (0) that satisfies the conditions in Theorem 1. This means that Newton's method from this initial point converges to the root x * (cf. Theorem 1). • At step 2. we consider a Newton sequence starting with x (1) . This sequence is the same as the sequence at step 1. except that we "forget" the first element of the sequence and start with the second. It is trivial that this sequence converges to the root x * . We note that (cf. proof of Theorem 1) we can associate the constants A 1 , B 1 to the initial iteration of this sequence and get the corresponding hypotheses from Theorem 1.

• At step 3. we consider Newton's sequence starting from t (1) . This initial point is just an approximation of the initial point of the previously considered sequence. From Corollary 1 we get the convergence of the new sequence to the same root x * . Moreover, the proof of Corollary 1 gives us the constants A ′ , B ′ associated to the initial point that also satisfy the hypotheses of Theorem 1. This means we can start the process over again.

If we take x (0) and then all the initial iterations of the sequences formed at step 3. we get back our perturbed Newton's sequence. But decomposing the problem as we did gives the intuition of why this sequence should converge. However, just having a set of sequences that all converge to the same root does not suffice to prove that the sequence formed with all initial iterations of these sequences will also converge to the same root. The reason is simple, the approximation at step 3. could bring us back to the initial point x (0) which would still yield a convergent Newton's sequence, but which would not make the new element of the perturbed sequence any closer to the root than the previous one. To get the convergence of the perturbed sequence we need to control the approximation we make. We will see in what follows that hypothesis 4. suffices to ensure the convergence of the new process.

To make the intuitive explanation more formal we consider the sequence of sequences of real numbers {Y p } p∈N defined as follows:

Y n 0 = x (n) is the original Newton's sequence; Y 1 is given by Y 0 1 = rnd 1 (x (1) ); Y n+1 1 = Y n 1 -f (Y n 1 )/f ′ (Y n 1 )
is the Newton's sequence associated to the initial iteration Y 0 1 ; we continue in the same manner and for an arbitrary p we define Y p as follows

Y 0 p+1 = rnd p+1 (Y 1 p ); Y n+1 p+1 = Y n p+1 -f (Y n p+1 )/f ′ (Y n p+1
). We notice that taking the first element in each of these sequences forms our perturbed Newton's process:

Y 0 0 = x (0) = t (0) and Y 0 n+1 = rnd n+1 (Y 0 n -f (Y 0 n )/f ′ (Y 0 n )) = rnd n+1 (t (n) -f (t (n) )/f ′ (t (n) )) = t (n+1)
Following our plan, we now show that for each p the sequence {Y n p } n∈N converges to x * and ensures a certain bound in the error.

• We start with sequence {Y n 0 } n∈N . Since it coincides with the initial sequence, the properties from Theorem 1 are trivially satisfied. For the initial point Y 0 0 we have the associated constants A 0 , B 0 . Applying Theorem 1 we get that lim Remarks. Independent of certification of exact computations, this proof has an interest from a proof engineering point of view. We were able to come up with the proof because we had formalized theorems 1 -4 inside a proof assistant. Such a formalization forces the user to understand the structure of the proof on one hand and to handle details with care on the other. Thus, an assisted proof is usually more structured and more detailed than a paper proof (especially in domains where automatic techniques are difficult to implement, like real analysis).

n→∞ Y n 0 = x * and |x * -Y 0 0 | ≤ 2B 0 . • Before considering {Y n 1 } n∈N ,
For example, while on paper the auxiliary sequences {A n } n∈N , {B n } n∈N appear during the proof, on the computer they are defined appart from the proof, allowing the user to better understand their importance and use similar sequences in the new proof. A proof assistant is also helpful with syntactic aspects like properly constructing the induction hypothesis and doing the bookkeeping to make sure all needed details are taken into consideration.

A Coq library for exact real arithmetic

The exact real library we are considering represents a real in the interval [-1, 1] as a lazy infinite sequence of signed digits of an arbitrary integer base. The signed digits of a base β are the integers in [-β + 1, β -1]. We denote s 1 ::s the infinite sequence beginning by the digit s 1 and followed by the infinite sequence s. The real number r represented by such an infinite sequence s in base β is :

r = s β = s 1 ::s 2 ::s 3 :: . . . β = ∞ i=1 s i β i .
A real number represented by a stream and for which we know the first digit can be written as: r = s 1 ::s β = s1+ s β β . Having signed digits makes our representation redundant. For example we can represent 1 3 as 3::3::3::3 . . . 10 but also as 4:: -7::4:: -7 . . . 10 . For each digit k the set of real numbers that admit a representation beginning by this digit is:

[ k-1 β , k+1 β ].
The sets associated to consecutive digits overlap with a constant magnitude of 2 β . The main benefit of this redundancy is that we are able to design algorithms for which we can decide a possible first digit of the output. Without redundancy this is in general undecidable. Take the example of addition: 0::3 . . . 10 + 0::6 . . . 10 may need infinite precision to decide whether the first digit is 0 or 1. In the case of signed digits we give 1 as a first digit knowing we can always go back to a smaller number by using a negative digit. We also note that in our example it was sufficient to know two digits of the input to decide the first digit of the output and this is true for addition in general.

Designing an algorithm therefore requires approximating the result to a precision that is sufficient to determine a possible first digit. In the library this is supported by the function make_digit and the required precision is β-2 2β 2 . Also, since our real numbers are infinite streams, the algorithms need to be designed in such a way that we are always able to provide an extra digit of the result. This is done by co-recursive calls on our co-inductive streams.

In Coq, co-induction [START_REF] Giménez | Codifying guarded definitions with recursive schemes[END_REF] provides a way to describe potentially infinite datatypes as our infinite sequences of digits. It offers both efficient lazy evaluation and nice proof schemes. The type of infinite sequences of objects of some type A is define as follows

CoInductive stream (A : Set) : Set := | Cons : A → stream A → stream A.
Cons should not be understood as a way to construct an infinite stream from another since we cannot build an initial infinite stream, but as a way to decompose an infinite stream into a finite part and an infinite part that could be described again with a new Cons and so on.

Our real numbers will be streams of signed digits, so we also need to create a model for the digits. They are abstracted with respect to the base and the implementation of integers, so both the base and the type of integers can be chosen by the user. Here we will denote their type by digit.

We can define new streams using co-recursive functions, for instance the stream of 0s, which obviously represents the real number 0.

CoFixpoint zero : stream digit := Cons 0 zero.

To prove the correctness of the algorithms on streams of digits we first define a relation between these streams and the axiomatic reals of Coq. This relation is based on the relation between the real value of a sequence, its first digit and the real value of the following sequence as noted previously. We formalize this relation as a co-inductive predicate :

CoInductive represents (β : Z) : stream digit → R → Prop := | rep : ∀ s r k, -β < k < β → -1 ≤ r ≤ 1 → represents β s r → represents β (Cons k s) k+r β .
This relation also makes sure that streams only represent reals in [-1, 1] and that the digits are in the set of the allowed signed digits. The correctness of our algorithms is verified when we manage to express a represents relation between our implementation and the standard in the Coq library. For instance the proof that the multiplication is correct is formulated in this way :

Theorem mult correct : ∀ x y vx vy, represents x vx → represents y vy → represents (x ⊗ y) (x * y).

In means that every time we have an exact real (i.e. a stream of digits) x that represents an axiomatic real vx and an y that represents a vy than our multiplication of streams x and y (here denoted ⊗) will represent the multiplication of axiomatic reals vx and vy.

For further details on algorithms and proofs for this library we refer the reader to [START_REF] Julien | Certified exact real arithmetic using co-induction in arbitrary integer base[END_REF].

4 Newton's method on exact reals

Correctness of Newton's method

We want to prove correctness of computation with Newton's method on exact reals in the same manner we proved correctness of multiplication in section 3. We code Newton's algorithm for both exact reals and axiomatic reals. For simplification we use a function g on exact reals to represent the ratio f (x) f ′ (x) of axiomatic reals. The relation between elements of the same rank in the two sequences:

∀ n, represents (EXn g EX0 n) (Xn X0 f f' n)
is almost trivial, if we have a represents relation for the initial iteration and for the function.

Theorem EXn correct :

∀ g ex0 f f' x0 n, represents ex0 x0 → (∀ x vx, represents x vx → represents (g x) ( f vx / f ' vx)) → (∀ n, -1 ≤Xn x0 f f' n ≤ 1) → represents (EXn g ex0 n) (Xn x0 f f' n).
The proof follows from the correction of the subtraction on streams with respect to the subtraction on axiomatic reals. This theorem allows us to transfer properties proved for Newton's method on axiomatic reals to the method implemented on exact reals. If we satisfy the conditions of Theorem 1 for the function f and the initial iteration X0, then we can compute the root of the function at an arbitrary accuracy, given by Theorem 3 (speed of convergence). From the same theorem we get the rank to which we need to compute for a given accuracy to be obtained. However, if we wanted to increase this accuracy, we would need to redo all the computation for the new rank. We want to avoid this and take advantage of the lazy evaluation characteristic for streams: we can design an algorithm that uses Newton's method to compute an arbitrary number of digits for the root of a given function, under certain conditions for this function.

Remark

In the implementation we use tail recursive version of the method to improve efficiency. The equivalent definitions given above help in better understanding the problem.

An algorithm for exact computation of roots

We consider a function f : [-1, 1] → R with x * the root of f and a suitable initial approximation x (0) for Newton's process. We have to find a possible first digit of the result x * in base β. For this we use make_digit which requires a precision of β-2 2β 2 of the result to make the appropriate choice of the first digit.

To determine the number of Newton iterations that ensures this precision we use Theorem 3 (speed of convergence), which gives us n s.t.

|x (n) -x * | ≤ β-2 2β 2 .
We choose as a first digit for x * the first digit d 1 of a representation of x (n) . This gives us

x * = d1+x * 1 β
, where x * 1 is the number formed from the remaining digits of x * . Since f (x * ) = 0, we get f ( 1 . We repeat the previous steps for function f 1 and we take as the initial approximation the remaining digits of x (n) , given by x (n) = βx (n) -d 1 . Now we have a co-recursive process to produce the digits of the root of our function one by one. If we simplify our algorithm by using g = f f ′ , when we transform g in g 1 we get

g 1 (x) := f 1 (x) f ′ 1 (x) = f ( d1+x β ) 1 β f ′ ( d1+x β ) = β × g( d 1 + x β )
For the exact real implementation in Coq we express the algorithm on streams of digits, so we remind that for the stream d 1 ::x, we have d 1 ::

x β = d1+ x β β
CoFixpoint exact newton (g: stream digit → stream digit) ex0 n:= match (make digit (EXn g ex0 n) with |d1::x' ⇒ d1::exact newton (fun x ⇒ (β ⊙ g (d1::x))) x' n end.

We note that the multiplication by the base is done by a specific function, for efficiency.

The formal certification of this algorithm means we have to prove that the output of this algorithm represents the root of the function f . For this we use Theorems 1 -3 (see section 2) on axiomatic reals and the theorem EXn_correct (section 4.1) that links Newton's method on exact reals to Newton's method on streams. We need to show that if the initial function f satisfies the hypotheses of Theorem 1 then the function f 1 built at the co-recursive call will also satisfy these hypotheses, thus yielding a correct algorithm.

The hypotheses of Theorem 1 impose that

1. f ∈ C (1) (] -1, 1[) 2. ∀x, y ∈] -1, 1[, |f ′ (x) -f ′ (y)| ≤ C|x -y| 3. f ′ (x (0) ) = 0 and | 1 f ′ (x (0) ) | ≤ A 0 ; 4. | f (x (0) ) f ′ (x (0) ) | ≤ B 0 ≤ ε 2 ; 5. µ 0 = 2A 0 B 0 C ≤ 1. We analyze f 1 (x) := f ( d1+x β ) for which we have f ′ 1 = 1 β f ′ and the new initial iteration x (n) = βx (n) -d 1
1. the class of the function is obviously the same, so f ∈ C (1)

(] -1, 1[) 2. |f ′ 1 (x) -f ′ 1 (y)| = | 1 β f ′ ( d1+x β ) -1 β f ′ ( d1+y β )| ≤ 1 β C| d1+x β -d1+y β | = 1 β 2 C|x -y| 3. f ′ 1 (x (n) ) = f ′ (x (n) ) = 0 and | 1 f ′ 1 (x (n) ) | = |β 1 f ′ (x (n) ) | ≤ βA n ; 4. | f1(x (n) ) f ′ 1 (x (n) ) | = |β f (x (n) ) f ′ (x (n) ) | ≤ βB n ; 5. µ n = 2βA n βA n 1 β 2 C = 2A n B n C ≤ 1.
Relations 3. -5. are given by the proof of Theorem 1. We are now able to prove by co-induction the following correctness theorem Theorem exact newton correct:

∀ g ex0 f f ' x0 n, ( * hypotheses on f , f ', x0 from Theorem 1 * ) ( * hypothesis on the number of iterations n * ) (∀ x vx, represents x vx → represents (g x) ( f vx / f ' vx)) → represents ex0 x0 → represents (exact newton g ex0 n) x * .

Improvements of the algorithm

Though short, elegant and certified, the algorithm presented in this section is not usable in practice as it is very slow. There are two main reasons for this:

1. The certified computations from the library require a precision of the operands higher than that of the result. We saw that in the case of addition on extra digit is required, but for other operations and function this precision can be higher. When we have an expression where we perform several operations, the precision demanded for each individual operand is a lot higher than the precision of the output. In the case of Newton's method, each iteration only brings a certain amount of information, so using a higher precision will not improve the result. 2. This approach relies on the higher-order capabilities of the functional programming language: the first argument of the exact_newton function is itself a function that becomes more and more complex as exact_newton calls itself recursively. The management of this function is somehow transparent to the programmer, but it has a cost: a new closure is built at every recursive call to exact_newton and when the function g is called, all the closures built since the initial call have to be unraveled to obtain the operations that really need to be performed. This cost can be avoided by building directly a first older data structure.

We discuss two possible improvements of this algorithm, dealing with these two issues. For the first point the solution is simple, just use the significant digits in the stream. Determining which are these significant digits and certifying the result is still possible thanks to Theorem 5. We implement a truncate function that given a stream s returns the stream containing the first n digits of s and sets the rest to zero. This function represents the rnd function on axiomatic reals (see Theorem 5). The perturbed Newton's method becomes: The function φ controls the approximation we can make at each iteration and follows the constrains imposed by Theorem 5. The exact_newton algorithm will work in the same way with this sequence as with the original method.

CoFixpoint exact newton rnd (g: stream digit → stream digit) ex0 n:= match (make digit (Etn g ex0 n) with |d1::x' ⇒ d1::exact newton rnd (fun x ⇒ (β ⊙ g (d1::x))) x' n end.

Though the proof for this new algorithm is not finalized yet, we feel there is no real difficulty in obtaining it as both the algorithm and the optimization we make are certified.

To tackle the second point in our list of possible improvements we make explicit the construction of the new function g in the co-recursive call. Definition exact newton2 (g : stream digit → stream digit) (X0 : stream digit) n := exact newton aux g X0 0 n.

The function make_k_digits takes three arguments: two streams x and y and an integer k and produces k + 1 digits of y by copying the first k digits in x and computing the digit k + 1 by using make_digit. For the function to perform correctly we must ensure that the first k digits in y can indeed be the same as those in x. In our case this results from the theorem on the speed of convergence of Newton's method, which make sure that a certain element is close enough to the root. The way the algorithm works is that it does iterations always for the same function g. It produces digits one at a time. Once it reached enough precision to certify an extra digit, the (k +1)th, it gets this digit by using the function nth and it continues to compute where it left of. This algorithm performs better than the previous one, but the optimizations performed in this case seem more difficult to certify. At the time of writing this paper we have the good properties on make_k_digit and the proof of correctness of the algorithm is in progress.

Applications to the square root

Newton's method is commonly used for the implementation of nth root function or division. We discuss the example of the square root to illustrate the behaviour of our algorithms. The square root of a positive real number a is the root of the function

f sqrt (x) = x 2 -a. The corresponding function g sqrt is fsqrt(x) f ′ sqrt (x) = x 2 -a 2x .
Due to restrictions about implementing the inverse function of exact reals, the library provides functions of the family x → 1 β n x where n > 0. So we chose instead the function f sqrt (x) = β 2 x 2 -a which corresponds to g sqrt (x) = x 2 -a 2β 2 x . The root of this function is √ a β . So a final multiplication by the base will give the expected result. We apply the algorithm to this function g sqrt and the user provide a suitable initial approximation. The process will actually converge for any positive initial approximation. We prove in Coq that the resulting function actually computes a representation of the square root function on axiomatic reals divided by the base.

Definition Ssqrt (a : stream digit) ex0 n := exact newton (g sqrt a) ex0 n. Theorem sqrt correct : ∀ (a : stream digit) (va : R), represents a va → represents (Ssqrt a) (( sqrt va)/β).

The original algorithm is slow. For example the computation of the first digit of 1 2 in base 2 124 using the original algorithm blocks the system, while for the same algorithm improved with approximations we get the equivalent precision of 37 decimal digits in 12 seconds. The second algorithm exact_newton2 brings an improvement at each new digit we want to obtain making the algorithm run in average twice as fast. We should also take into consideration that using f (x) = a x 2 -1 can improve our execution times considerably as there is only one division involved. Nevertheless, our intention here was not to implement an efficient square root, but to test the capabilities of the previous presented algorithms.

Related work

This work presents different angles in the formal verification of a numerical algorithm. For the moment such developments are not very popular. A lot of work is being done concerning formally verified exact real arithmetic libraries. Besides the library presented here, the development [START_REF] Lester | Real Number Calculations and Theorem Proving[END_REF] for PVS [START_REF] Shankar | The PVS Proof Checker: A Reference Manual[END_REF] and [START_REF] Russell | Certified Exact Transcendental Real Number Computation in Coq[END_REF] also for Coq are two of the most recent such implementations. These two libraries have computations that are certified with respect to the real analysis formalizations in PVS and C-CoRN [START_REF] Cruz-Filipe | C-CoRN: The Constructive Coq Repository at Nijmegen[END_REF], respectively. A significant part of the work presented here could be reproduced in any of these libraries. In the case of [START_REF] Russell | Certified Exact Transcendental Real Number Computation in Coq[END_REF] the exact reals operations and functions are certified via an isomorphism between the exact reals and the C-CoRN real structure; there is also an isomorphism between C-CoRN reals and Standard Library reals (see [START_REF] Kaliszyk | Computing with classical real numbers[END_REF]), so in theory it should be possible to certify computations by using the presented proofs and the two isomorphisms.

Concerned with exact real arithmetic and also with co-inductive aspects we mention the work of Niqui [START_REF] Niqui | Coinductive formal reasoning in exact real arithmetic[END_REF]. This works aims to obtain all field operations on real numbers via the Edalat-Potts algorithm for lazy exact arithmetic.

Results of the convergence of Newton's method with rounding have been proved for some special cases like the the inverse and the square root [START_REF] Brent | Modern Computer Arithmetic[END_REF]. Of course, in these cases the speed of convergence is better than in the general case.

The certification of a square root algorithm has been the subject of several formal developments. We mention [START_REF] Bertot | A Proof of GMP Square Root[END_REF] for the certification of the GMP square root algorithm, [START_REF] Harrison | Formal verification of square root algorithms[END_REF] for an Intel architecture square root algorithm and [START_REF] Sawada | Mechanical verification of a square root algorithm using taylor's theorem[END_REF] for the verification of the square root algorithm in an IBM processor. A general algorithm using Newton's method was developped by Hur and Davenport [START_REF] Hur | A generic root operation for exact real arithmetic[END_REF] on a different representation of exact reals but not in a certified setting.

Conclusions and perspectives

As a case study of theorem proving in numerical analysis, this work tries to underline three aspects of such a development: how do design and formalize the necessary proofs from "paper" mathematics, how to prove correct numerical methods implemented on exact reals and provide certified computations, how to design and verify specific algorithms for an implementation of exact reals. The Coq development can be found at http://www-sop.inria.fr/marelle/ Exact_Newton.

To the best of the authors' knowledge, the result and proof of Theorem 5 are new, though the authors are not experts in numerical analysis. Using only a predetermined precision for our computation makes it that our formalization can be seen as an (imperfect) model of computation in multiple or arbitrary precision, thus validating Newton's method in such a context. The proof of Theorem 5 was motivated by the need to improve the algorithm discussed in section 4.2. The contribution of proof assistants in obtaining this proof is twofold: the proof was motivated by a formal development and the proof was constructed inside the proof assistant, following the pattern of existing proofs.

The algorithms presented in section 4 are also new. The certified algorithm, though it is not of practical use, it can serve as a model in obtaining proofs for our optimized algorithms. The next step is to put together the two proofs we presented here and get a formally verified algorithm for computing roots in a (more) efficient manner. With the results presented here we see no difficulties in obtaining this proof.

The axiomatic formalization on Newton's method contains the multivariable version of the theorems 1 -4. This means we can solve systems of (non-)linear equations using this method. Exact real arithmetic libraries do not yet treat such cases, so it would be an interesting experiment to see to what extent the results presented here can be obtained in the multivarite setting. We note that the proof of Theorem 5 has the same structure for the multivarite case. We presented here the real case to make it easier for the reader to follow and to show the correspondence with results from section 4.2.

  we note that the sequence Y n 0 = Y n+1 0 (i.e. the previously considered sequence where we start from the second element) also satisfies the conditions, with initial point Y 0 0 = Y 1 0 and constants A 0 = 2A 0 and B 0 = A 0 B 2 0 C. The laws for these constants are deduced from relations

Fixpoint

  EXn g ex0 n {struct n}: stream digit:= match n with | 0 ⇒ ex0 | S n ⇒ let exn:= (EXn g x0 n) in exn ⊖ g exn end. Fixpoint Xn f f' x0 n {struct n}: R:= match n with | 0 ⇒ x0 | S n ⇒ let xn:= (Xn x0 f f' n) in xn -f xn / f' xn end.

d1+x * 1 β

 1 ) = 0. This means we can define a new function f 1 (x) := f ( d1+x β ), and x * 1 is the root of f 1 . Determining the second digit of x * is equivalent to determining the first digit of x *

Fixpoint

  truncate s n {struct n} := match n with | 0 ⇒ zero | S n ⇒ match s with | d :: s' ⇒ d :: truncate s' n end end.

Fixpoint

  Etn g ex0 (n : nat) {struct n} : stream digit := match n with | 0 ⇒ ex0 | S n ⇒ let tn := (Etn g ex0 n) in (truncate (tn ⊖ (g tn)) (φ n)) end.

CoFixpoint

  exact newton aux (g : stream digit → stream digit) (Xn : stream digit) k n := let Xn' := make k digits x0 (EXn g x0 n) k in (nth k Xn') :: exact newton aux g Xn' (S k) n.

Acknowledgments

We thank Yves Bertot for his help and constructive suggestions.

(2), [START_REF] Brent | Modern Computer Arithmetic[END_REF]. We get that lim

). We are in the situation of Corollary 1, where we have a converging sequence ( {Y n 0 } n∈N ) and we introduce an approximation in the initial iteration. To be able to apply this corollary we need to verify 0

We will show later on that under our hypotheses these three conditions are indeed verified. From Corollary 1 we get the new constants according to relations ( 5), [START_REF] Démidovitch | Éléments de calcul numérique[END_REF]. This makes that we find ourselves again in the conditions of Theorem 1 and we can deduce that lim

We are in the appropriate conditions to start this process again and explain in the same manner the properties for {Y n 2 } n∈N , {Y n 3 } n∈N , etc. The auxiliary sequences are given by the following relations:

Using the above reasoning steps, we get by induction that |Y 0 n -x * | ≤ 2B ′ n and we also manage to show ∀n,

The latter relations is deduced from the above formulas by basic manipulations. It trivially implies the convergence of the perturbed sequence to the root x * .

We need some auxiliary results to ensure that Corollary 1 is applied in the appropriate conditions each time we make a rounding. These results are as follow:

We do not discuss all the details as they are elementary reasoning steps concerning inequalities, second degree equations or geometric series. All these results have been formalized in Coq to ensure that no steps are overlooked.


Robert Wipperfürth
email: robert.wipperfuerth@ils.uni-stuttgart.de

Thorben Hoffmann

Christoph Kurz

Tim Belschner

Reinhard Reichel

Automated Generation of Requirements for the Highly Fault-Tolerant System Behaviour of a Distributed and Integrated Avionics Platform

Keywords: Flexible Avionics Platform, AAA process, platform-based development, model-driven development, automatic requirements instantiation, requirements reuse network App. F sensors, A/C-systems sensors, actuators

Fully autonomous Unmanned Aerial Vehicles, Remotely Piloted Aircraft, Air Taxis, as well as advanced CS-23 aircraft require numerous complex and safety-critical system functions, such as vehicle management and utility functions, automatic take-off and landing or flight control. The development and qualification of the related avionics systems are characterised by a very high effort. The Institute of Aircraft Systems at the University of Stuttgart, in close cooperation with Aviotech GmbH, aims at a highly automated development and verification process for such fault-tolerant avionics systems to significantly reduce development effort, time, and risk and thus costs. For this reason, the Flexible Avionics Platform was developed. It enables the implementation of integrated fly-by-wire platform instances and is characterised by the following key aspects. (1) A platform-based development approach featuring an integrated, distributed, and highly redundant avionics architecture. (2) The platform management, a high-level abstraction layer providing a full abstraction towards integrated applications regarding the distribution, fault-tolerance, and redundancy of a fly-by-wire platform instance including redundant peripherals. (3) The AAA process, a comprehensive automation process for the highly automated generation of development and qualification artefacts, such as an instance of the Platform Management, the corresponding specification at the system and software level, and related test cases and test scripts. This paper presents the basics for the automated requirements generation at the system level with a focus on the specification of the highly fault-tolerant system behaviour of fly-by-wire platform instances based on the Flexible Avionics Platform.

I. INTRODUCTION

A. Motivation

Future aircraft require numerous complex and safety-critical system control functions. This is especially true for fully autonomous Unmanned Aerial Vehicles (UAVs) and Remotely Piloted Aircrafts (RPAs) that are certified and operated in nonsegregated airspace. Such aircraft must be able to react in a semi-or fully-automated manner to all critical situations as, for instance, the loss of the command and control data link or the This research was funded by the German Federal Ministry for Economic Affairs and Energy (BMWi) within the LuFo V-2 and LuFo V-3 program. loss of an engine. Furthermore, standard operational functions like take-off and landing or the entire vehicle management and utility functions must be automated as well.

Accordingly, the implementation of the related avionics systems is characterised by a very high effort. An implementation based on avionics platforms with highly integrated architectures is a first step to reduce system costs. While this approach enables the integration of a high number of systems within a single instance of such an avionics platform, adequate safety, up to failure rates of 10 -9 /h, has to be ensured. To enable an affordable usage of such integrated avionics platforms, especially within the CS-23 domain, a new approach is required that reduces development and qualification effort significantly while maintaining a high safety level.

B. State of the Art

In the avionics domain, Integrated Modular Avionics (IMA) represents the state of the art regarding platform-based development approaches as well as integrated and distributed architectures [START_REF] Itier | A380 integrated modular avionics-the history, objectives and challenges of the deployment of ima on a380[END_REF], [START_REF] Annighöfer | Large-scale model-based avionics architecture optimization methods and case study[END_REF], [START_REF] Gaska | Integrated modular avionics-past, present, and future[END_REF]. The hardware is based on standardised modules connected via an Avionics Data Communication Network (AFDX ® ). Concerning the software architecture, the hardware and communication are abstracted towards integrated applications (see Fig. 1). This includes inter-partition communication, even if the partitions are allocated to different hardware modules. There are comprehensive automation approaches for the automated instantiation of these IMA abstraction layers [START_REF] Kornek-Percin | New ima architecture approach based on ima resources[END_REF], [START_REF] Halle | Evaluation of the ashley seamless tool-chain on a real-world avionics demonstrator[END_REF], [START_REF] Annighoefer | Holistic ima platform configuration using web-technologies and a domain-specific model query language[END_REF], [START_REF] Yin | Application of model based system engineering to ima development activities[END_REF].

Due to these features, IMA represents a significant advance in the realisation of avionics systems, their development, and their qualification. However, despite all process automation approaches, the development and qualification of avionics systems based on IMA still require a high effort. The reason for this is the low abstraction level provided by IMA. IMA does not provide an abstraction of system management aspects such as the management of redundant sensors, redundant actuators, and the failure and redundancy management of distributed modules ensuring consistency in a distributed architecture. Thus, this extremely complex part of the system management, especially with highly redundant avionics systems, has to be implemented as part of the integrated applications. Consequently, the most challenging tasks of the system management are not part of the IMA development automation. This is the key difference to our approach of the Flexible Avionics Platform with its associated process automation.

C. The Flexible Avionics Platform [START_REF] Görke | Eine flexible Plattform für Fly-by-Wire-Systeme-Spezialisierbarkeit als Schlüssel zur effizienten Entwicklung sicherheitskritischer Avionik[END_REF] The Flexible Avionics Platform (apf) is a platform-based development approach in the sense of Di Natale et al. [START_REF] Natale | Moving from federated to integrated architectures in automotive: The role of standards, methods and tools[END_REF] and features an integrated, distributed, and highly redundant architecture. It consists of standardised hardware components as well as a library of generic software components, i.e. a Real Time Operating System (RTOS), drivers, and small software bricks called basic services. Each specific avionics system is generated as an instance of this Flexible Avionics Platform.

The apf is characterised by a high-level abstraction layer realised as a middleware, the so-called Platform Management (plama) (see Fig. 2). It covers the entire system management for all distributed and redundant modules (internal and external) as well as redundant peripherals, for example, redundant sensors and redundant actuators. Thus, it manages tasks such as fault-tolerant intra-module and inter-module communication, communication to other systems, the redundancy of all modules and peripherals, and reconfigurations in the event of failure. Furthermore, it controls the system-wide operation phases such as normal operation, pre-flight built-in test, and interactive system operation during maintenance. These system management tasks are handled by plama in a distributed manner and are executed on all modules of a Flexible Avionics Platform Instance (apfi). Each plama instance is implemented as a composition of specialised basic services.

Due to the high degree of abstraction provided by plama, integrated applications are executed in a failure-free virtual simplex environment and are not required to perform any system management tasks. Hence, applications are reduced to their cybernetic control law.

D. The AAA Process

The apf is complemented by a comprehensive automation process for the development and qualification of an apfi, the AAA process. It consists of the following subprocesses:

• Axx subprocess -Automated design and parameter instantiation [START_REF] Kraus | Verfahren zur weitgehend automatisierten Erzeugung der Middleware für hoch ausfallsichere, integrierte Avioniksysteme mittels Model-Integrated Computing[END_REF]: Based on a high-level system specification a high-level system design model is implemented manually. It is expressed with a domain-specific modelling language developed by the Institute of Aircraft Systems (ILS). This model describes the basic hardware structure, connected sensors and actuators, interfaces to other systems, a placeholder for the applications, the degree of redundancy, the basic reconfiguration strategy, and the scheduling of the apfi-wide operation phases.

In a first automation step, the implemented system design model is refined by synthesis rules into a software architecture model containing the key software components and their coupling. In a subsequent automation step, the software architecture model is further refined into a model of the software components' Parameter Data Items (PDIs). The PDI model defines the selection of suitable basic service, their functional specialisation, and their data and control coupling. In addition, it defines the configuration data for all drivers and the RTOS. As a last step, this model is automatically transformed into source code. This PDIs source code together with the source code of the selected basic services, drivers, and the RTOS as well as the hardware modules form an apfi. • xAx subprocess -Automated document generation [START_REF] Belschner | A Method for the Automated Generation of Requirements and Traceability for a Distributed Avionics Platform[END_REF]:

The approach of the automatic generation of requirements is based on requirement classes describing characteristic behaviour that can be realised with the apf. Requirement classes are modelled once in terms of characteristic patterns, defining aspects such as their instantiation condition, representation, and the structure of possible instances. The corresponding models are automatically transferred into synthesis rules. Executing these synthesis rules, the xAx tool suite automatically analyses the apfi design models, generated in the Axx subprocess, with regard to the characteristic patterns of each requirement class. The match of a single or a group of patterns leads to the automatic generation of a requirement instance, i.e. the specialisation of the related requirement class with the apfi specific information of this match. In this way, all apfi requirements are generated automatically for system-level, software high-level and software low-level. In general, a requirement instance is expressed in the form of a natural language representation and a formal representation. The natural language representations are human-readable descriptions of the requirements and include information on traceability and versioning.

They conform to the relevant aeronautical standards ARP4754A and DO-178C and represent a large part of the entire apfi specification documents that are used for an apfi certification process. The formal representations feature corresponding and consistent models of the apfi behaviour and are further processed by the xxA subprocess.

• xxA subprocess -Automated generation of verification artefacts [START_REF] Müller | Automated Test Artifact Generation for a Safety-Critical Integrated Avionics Platform[END_REF], [START_REF] Block | Automated test case generation for the verification of system and high-level software requirements for fly-by-wire platforms[END_REF]: Based on the formal representations the xxA tool suite automatically generates associated test cases and test procedures respectively test scripts using a dedicated test oracle. During the integration and verification processes for an apfi, these test scripts can be automatically executed on an apfi-in-the-loop testrig.

E. Automated Requirements Generation for Plama's High-Level Management Layer

A first approach for the automated generation of requirements focused on plama's communication layer (low-level management) which manages the fault-tolerant intra-module and inter-module communication as well as the monitoring and data fusion [START_REF] Belschner | A Method for the Automated Generation of Requirements and Traceability for a Distributed Avionics Platform[END_REF].

This paper presents the enhancement of the approach for the system specification of the high-level management layer of plama, i.e. the layer managing reconfigurations and the operation moding of an apfi. The strategy for an automated generation of requirements is based on the following considerations. The automatically generated instances of the requirement classes have to enable a meaningful apfi specification that can be used for validation processes and that is comparable to a manual specification. In addition, the set of existing requirement classes has to cover the entire usage domain of the apf. Especially at the system level, these requirement classes should describe the main characteristics. Furthermore, the effort considering the manual implementation of requirement classes must be justifiable.

For this reason, the behaviour of an apfi at the system level must be characterised by a limited number of generic requirement classes valid for all apfis. The central question resulting from this is how these requirement classes are to be defined. This is the focus of our article.

F. Paper Structure

First, we set the context by showing central architectural and operational aspects of an apfi in section II. While section III analyses what must be specified for an apfi at the system level, section IV elaborates on how the system-level behaviour is specified using requirement classes. Finally, section V summarises the key results and provides an outlook on our ongoing and future research.

II. FLEXIBLE AVIONICS PLATFORM

The section is intended to clarify the framework of the apf. For this purpose, the architecture of the apf is presented and important operation principles are explained.

A. Architecture

Figure 3 shows the hardware structure of an exemplary instance of the apf consisting of input output modules (ioms), core processing modules (cpms), smart actuator modules (sams), as well as the networks (net). An iom provides necessary input/output interfaces to connect system-specific peripheral units such as sensors, actuators, human-machine interfaces, or other systems. Measured Signals are preprocessed and transmitted to the cpms. A cpm is a dual-lane module. Each lane operates cyclically and all tasks are executed in parallel and frame synchronously with the other lane. A cpm features a fail/passive behaviour. This is realised by the crosscomparison mechanisms of plama, which ensure the required consensus [START_REF] Hadzilacos | A modular approach to fault-tolerant broadcasts and related problems[END_REF] between the lanes. Cpms have two main tasks. First, they plan and execute the central management decisions within an apfi. Second, they execute the laws of integrated applications, i.e. integrated system function laws. Control commands for the operation of the control surfaces of an aircraft are transmitted to the sams. A sam operates and monitors a control surface. It features a dual-lane architecture including the power electronics for an electric actuator with an optional clutch. All modules communicate via two independent networks, which can provide further internal redundancy. As shown, each module is logically assigned to one network side red S (R) or blue S (B) . For example, cpm (R,1) with module ID 1 is assigned to network side S (R) .

B. Apfi Operation

The apfi including connected peripherals and all integrated system functions must operate correctly in numerous operation phases as well as numerous apfi configurations. Here, an apfi configuration describes the state of an apfi regarding the dynamic configuration of the resources taking part in the apfi operation. It is not to be confused with the PDI generated by the Axx tool suite. If the apfi operation is affected by a failure, apfi reconfiguration measures are required. Likewise, the operation phase must be adjusted if the apfi operation conditions change. The decision making regarding such actions is designed strictly hierarchically [START_REF] Hoffmann | Enabling the automated generation of the failure and redundancy management for distributed and integrated fly-by-wire avionics[END_REF], [START_REF] Cake | Supervisor für eine komplexe verteilte Avionikplattform[END_REF]. The corresponding decision hierarchy is as follows:

1) Determination of the membership (membership determination). 2) Allocation of multi-application (mapp allocation).

3) Allocation of the master-slave engagement (master-slave allocation).

4) Scheduling of the operation phases (operation moding).

In general all apfi modules, as well as the connected peripheral units, are considered within this hierarchy. However, the following sections focus on the apfi core which comprises all cpms of the distributed apfi.

1) Membership Determination: The basis for consistent distributed decisions of the cpms is the so-called membership. It ensures that only non-faulty cpms participate in the apfi operation.

The membership determination is a two-step process. First, each cpm determines the membership of its own module locally (module membership). Based on this, each cpm determines the membership of the other cpms (inter-cpm membership). For the inter-cpm membership consensus between all correct cpms is required.

2) Mapp Allocation: The apfi features a dynamic in-flight reallocation of integrated system function laws (sfls) between cpms thus allowing for an efficient use of the cpm hardware. For this, several sfl of the same criticality level are grouped to a multi-application (mapp). Mapps are prioritised according to their criticality. For example, mapp (1) contains the absolute safety-critical system functions flight control, braking, and steering while mapp [START_REF] Annighöfer | Large-scale model-based avionics architecture optimization methods and case study[END_REF] , with the lower priority, comprises functions such as flight guidance or flight management. Although each cpm has loaded the software for all mapps, it executes only a single mapp at a time.

The assignment of which cpm executes which mapp is called mapp allocation. Mapps are allocated only to such cpms for which membership is given. The mapp allocation is based on apf generic mapp allocation rules. If the rules are met, the mapp allocation is correct. If the rules are violated, the corresponding incorrect mapp allocation is changed to a new, correct mapp allocation. This mapp reconfiguration may take place in flight. For the mapp allocation, consensus is required between all cpms with a given membership.

3) Master-Slave Allocation: If the same mapp is allocated to multiple cpms, i.e. if there are multiple replicas of a mapp, an active-hot-standby replication strategy is applied. Only data provided by the active mapp-replica, i.e. the mapp engaged as master, is processed by other mapps, ioms, or sams. The data provided by the hot-standby mapp-replica, i.e. the mapp engaged as slave, is transmitted via the network but is ignored by all recipients 1 . If there are further mapp-replicas, these are operated as cold-standby replicas. In our article, this so-called shadow engagement is not considered any further.

The selection of which mapp-replica is to be operated as master or slave is called master-slave allocation. As with the mapp allocation, the master-slave allocation is also based on an apf generic ruleset. These rules ensure that the mappreplica with the best performance execution level2 , regarding the implemented sfls of a mapp, is selected as the master. For the master-slave allocation, consensus between all replicas of a mapp is required.

4) Operation Moding: During a mission, the system of integrated systems, i.e. the apfi with all its integrated system functions including connected peripheral units, undergoes various operation phases. For each operation phase, the required behaviour can change. Examples are the normal operation during flight, the execution of all test steps of a pre-flight built-in test before dispatch, or the interactive activation of built-in tests during maintenance.

Each operation phase is associated with an apfi specific set of hierarchically structured operation modes that can be specified in the high-level system design model for the Axx subprocess. These operation modes define the behaviour of the entire system of integrated systems. The scheduling of the operation modes, which mainly depends on the apfi operation conditions, is performed centrally by the master replica of mapp (1) (mapp (1,ma) ). Other replicas of mapp (1) simply adopt the current operation modes determined by mapp (1,ma) which ensures consensus.

5) Examplary Apfi Reconfiguration:

To provide an insight into the apfi operation, a failure induced mapp and masterslave reconfiguration is presented exemplarily. The initial state is shown in Fig. 4(a). The module membership of each cpm, as well as the inter-cpm membership on all other cpms, is set to ON. Thus, membership is given for all cpms. The shown mapp and master-slave allocation is correct.

Starting from this state, there is a failure in one lane of cpm (R,1) . Due to the dual-lane architecture, this failure is detected by the other correct lane of cpm (R,1) , which then passivates the cpm. To do this, the correct lane changes its module membership to OFF and stops the transmission of messages over the network.

The passivation of cpm (R,1) which executed mapp (1,ma) affects the other cpms of the apfi. They cannot communicate with cpm (R,1) any more. Hence, the remaining correct cpms consistently set the inter-cpm membership about cpm (R,1) to OFF. However, the mapp and master-slave allocation of the cpms with given membership violate the allocation rules:

1) Although the priority of mapp (1) is higher than the priority of mapp [START_REF] Annighöfer | Large-scale model-based avionics architecture optimization methods and case study[END_REF] , it is allocated to only one cpm. 2) There is no master replica of mapp [START_REF] Itier | A380 integrated modular avionics-the history, objectives and challenges of the deployment of ima on a380[END_REF] . Consequently, the mapp allocation and the master-slave allocation have to be reconfigured. In a first step, cpm (B,1) reconfigures from mapp (1,sl) to mapp (1,ma) . In a second step, cpm (R,2) reconfigures from mapp (2,sl) to mapp (1,sl) . The state illustrated in Fig. 4(b) represents the resulting, correct allocation. Since the apfi operation condition did not change, the new mapp (1,ma) maintains the operation modes adopted from the previous master-replica.

III. OVERVIEW OF THE SPECIFICATION OF AN APFI AT SYSTEM LEVEL

This section aims to illustrate what must be specified at the system level. For this purpose, the classification of the specification is explained and details on each specification domain are provided.

A. Basics

Most of the time, the apfi operates in a steady-state. A steady-state is characterised by a steady apfi configuration and a steady operation phase. Hence, all allocation rules are met and the required behaviour of the system of integrated systems is stationary. However, failures or changes in the aircraft operation condition can lead to the transition of one steady-state to another. Based on this, the apfi specification at the system level is divided into the following specification domains:

1) The specification of the steady-state operation.

2) The specification of transitions between steady-states.

B. Specification of the Steady-State Operation

The requirements of this domain specify the correct operation of an apfi for all steady-states. A correct operation of a steady-state is characterised by

• the data flow,

• the operation features. Considering the data flow, data required for the execution of a system function must be correctly transferred from the input of the apfi (e.g. sensors) to the application programming interface of the sfls integrated on each cpm. Furthermore, data must be transferred between sfls and from an sfl to the output of the apfi (e.g. actuators).

Regarding the operation, key features such as the cyclic operation, synchronicity, and consensus, have to be ensured.

C. Specification of Transitions between Steady-States

This specification domain defines the system-level transitions from one steady-state to a new steady-state, due to failures or changes in the aircraft operation condition. Thus, the requirements of this domain specify the reconfigurations and operation moding of an apfi at the system level. Based on the decision hierarchy presented in section II-B, the specification domain is further divided into subdomains.

• The intra-module subdomain specifies the reconfiguration behaviour of single modules. • The inter-module subdomain specifies the reconfiguration of sets of modules. This includes reconfigurations of the inter-cpm membership, the mapp allocation, or the master-slave allocation. • The peripheral subdomain specifies reconfigurations affecting the operation of sensors and actuators as part of the execution of system functions. • The operation moding subdomain specifies the scheduling of operation modes for the system of integrated systems. For each of these specification subdomains, there is a dedicated set of requirement classes, which together cover all possible aspects of that subdomain. This facilitates a focused and expressive specification of the related behaviour. The sum of all requirement classes covers the overall reconfiguration and operation moding behaviour for all possible apfis. In the following, exemplary requirement classes for an apfi reconfiguration are presented.

IV. REQUIREMENT CLASSES AT SYSTEM LEVEL

This section exemplarily describes how the requirement classes of apfi reconfigurations at the system level are defined. For this, the basic reconfiguration principle of the apf is shown. This is followed by exemplary requirement classes covering different aspects of a reconfiguration. domain of the apf, in general, only a subset of all possible categorical indications is needed for a specific apfi 3 .

A. Basic Reconfiguration Principle

Necessary reconfiguration steps for the current apfi configuration s apf i are planned exclusively based on these categorical indications. The steps are executed over a short period until the overall reconfiguration is completed, i.e. until a new steadystate of the apfi configuration is re-established. As each apfi reconfiguration is associated with a categorical indication, the set of all possible reconfigurations is generic for the apf as well. In the following, the requirement class for the fusion of particular indications is introduced, which enables the specification of the categorical indications as the basis for each apfi reconfiguration 4 . Then, the requirement class for the mapp reconfiguration is presented.

B. Requirement Class for the Fusion of Particular Indications

The requirement class related to the fusion of particular indications describes transformations of the type

f f usion : {z I,i } → {z CI,x } (1)
within a single module. Using an if-then-else construct, the requirement class can be expressed as follows 5 . Values that need to be specialised during instantiation are coloured and marked with #.

REQ -fusion of particular indications

Let Z I,#nameCI#,(#M (x)#) := {z I,#nameI# } (#M (x)#) .
If there is a z

I,i,(#M (x)#) ∈ Z I,#nameCI#,(#M (x)#) with z I,i,(#M (x)#) = true for #confirmTime# ms, then z CI,#nameCI#,(#M (x)#) = true. Else, z CI,#nameCI#,(#M (x)#) = f alse. EndOfREQ
Here, Z I,#nameCI#,(#M (x)#) is the set of all particular indications z I,#nameI#,(#M (x)#) that are mapped to the categorical indication z CI,#nameCI#,(#M (x)#) within a specific module #M (x) #.

The basic pattern for the instantiation condition related to the requirement class is illustrated in Fig. 6(a) using an UML syntax 6 . The pattern corresponds to the generic structure of f f usion extended by the confirm time. Specific instances of this pattern are searched for in the generated apfi design models, which result from the Axx subprocess. These models comprise the information about every existing instance of f f usion for a specific apfi.

C. Basics of the Reconfiguration Requirement Classes

Compared to the requirement class of the fusion of particular indications, the following has to be considered for the reconfiguration requirement classes. While all reconfigurations are based exclusively on categorical indications, these categorical indications are only software-based quantities. However, states such as a power-off of all lanes of a module cannot be detected by the affected module and thus cannot be expressed by its categorical indications. For this reason, the physical health state z s of each apfi hardware resource is introduced. Within the scope of the specification, the categorical indications are extended with these physical health states to so-called extended categorical indications. The vector of the extended categorical indications is defined as z ECI := (z s , z CI ) T ECI . Based on the presented reconfiguration principle and the extended categorical indications, all possible system-level reconfigurations of each apfi can be generically described by the transformation:

f reconf ig :    s apf i z s z CI ECI    → {s apf i }. (2)
Consequently, f reconf ig is the basis for all reconfiguration requirement classes at the system level. As an example, the requirement class related to the mapp reconfigurations of apfis with two mapps and up to four cpms is presented in the following section.

D. Requirement Class for the Mapp Reconfiguration

The requirement class in Fig. 7 describes mapp reconfigurations due to the passivation or activation of cpms 9 . Therefore, it enables the specification of each transition from a mapp allocation for q correct cpms to the mapp allocation for r correct cpms. A correct cpm implies that the membership is given for this cpm. For a passivation transition, there is q ∈ {2, 3, 4} and r = q-1. In contrast to this, for an activation transition q ∈ {1, 2, 3} and r = q + 1.

To express the requirement class based on f reconf ig , the vectors s xcpm,mapp,q and s xcpm,mapp,r as well as the vector z ECI,xcpm,mapp,q →r are introduced.

• s xcpm,mapp,q describes the initial steady-state apfi configuration, i.e. the apfi-wide mapp allocation for q correct cpms.

• Starting from q correct cpm, z ECI,xcpm,mapp,q →r describes the apfi wide view of the passivation or activation of an arbitrary cpm to r correct cpms. • s xcpm,mapp,r describes the resulting steady-state mapp allocation for r correct cpms. Using these vectors, the mapp reconfiguration requirement class is illustrated in Fig. 7. The used variables can be described as follows:

• s mapp,(cpm(i)) describes the mapp currently allocated to an arbitrary cpm (i) , with s mapp,(cpm(i)) ∈ {mapp [START_REF] Itier | A380 integrated modular avionics-the history, objectives and challenges of the deployment of ima on a380[END_REF] , mapp (2) , nil}. N il is a state in which cpm (i) failed passive and thus no mapp is allocated. • z s,(cpm(j)) is the physical health state of an arbitrary cpm (j) . It applies that z s,(cpm(j)) ∈ {c, f p }, where c is a correct state of cpm (j) and f p is a state in which cpm (j) failed-passive. Accordingly, z s,(cpm(j)) is used to describe the passivation or activation of a cpm (j) . • Such a passivation or activation can be monitored by other, correct cpm (i) using the categorical indication z CI,comm,(cpm(i),cpm(j)) . It describes the opinion of cpm (i) about cpm (j) regarding their overall communication, with z CI,comm,(cpm(i),cpm(j)) ∈ {ok, ¬ok}. For example, if a cpm (j) failed-passive no messages are transmitted via any communication network to other cpm (i) which thus set z CI,comm,(cpm(i),cpm(j)) = ¬ok. For the indices that define the assignment of these variables to the cpms the following applies.

• Considering s xcpm,mapp,q , the network side indices

x, y ∈ {R, B}, with x ̸ = y. For the corresponding module ID indices, there is i, j, k, l ∈ {1, 2}, with i ̸ = j and k ̸ = l. • Analogously, considering z ECI,xcpm,mapp,q →r and s xcpm,mapp,r , the network side indices a, b ∈ {R, B}, REQ -Mapp reconfiguration due to a change from #q# to #r# correct cpms #s xcpm,mapp,q # #z ECI,xcpm,mapp,q →r # → (#s xcpm,mapp,r #)

=                
# s mapp,(cpm(S(x),i)) s mapp,(cpm(S(x),j)) s mapp,(cpm(S(y),k)) s mapp,(cpm(S(y),l)) q # There is a major difference between the instantiation of the requirement class for the fusion of particular indications and the requirement class for the mapp reconfiguration. Here, the aforementioned mapp allocation rules for apfis with two mapps and up to four cpms are a part of the requirement class. All correct cpms have to meet these rules, which are as follows:

#                 z s,(
                q →r #                 → # s mapp
1) The number of replicas of mapp (i) per network side is at most 1: i ∈ {1, 2}, x ∈ {R, B} : N mapp(i),(S(x)) ≤ 1.

2) The number of replicas of mapp (1) is equal to or at most greater than 1 compared to the number of replicas of mapp [START_REF] Annighöfer | Large-scale model-based avionics architecture optimization methods and case study[END_REF] :

N mapp(1) -1 ≤ N mapp(2) ≤ N mapp(1)
. The first rule is based on a design decision related to the communication architecture of the apf. The second rule ensures that each mapp is executed for as long as possible while taking into account the mapp prioritisation.

Using these rules, the requirement class itself generically describes each mapp reconfiguration due to a passivation or activation. Consequently, the number of mapps and cpms is the only characteristic required for the generation of the requirement instances. The associated basic instantiation pattern is shown in Fig. 8(a). If an does show this characteristic, all requirement instances of this class are generated, i.e. one requirement instance for each possible specific activation and passivation transition for the apfi specific number of cpms and mapps. The instantiation is illustrated in the following.

The apfi design model contains the information about the number of mapps and cpms of an apfi. An exemplary model for an apfi with two mapps and four cpms is illustrated in Fig. 8(b). The depicted mapp to cpm relation results in a single match for the class's instantiation pattern. Accordingly, requirement instances for the activation transitions q → r ∈ {1 → 2, 2 → 3, 3 → 4} have to be generated. Furthermore, requirement instances for the passivation transitions q → r ∈ {4 → 3, 3 → 2, 2 → 1} have to be generated. In the following, the instantiation steps carried out for each requirement instance are described using the example of a passivation transition from q = 4 to r = 3 correct cpms.

First, the value of s xcpm,mapp,q is determined based on q = 4 and the apf generic mapp allocation rules. The resulting correct mapp allocation for four correct cpms is

s xcpm,mapp,4 = mapp (1) mapp (2) mapp (1) mapp (2) 4
Fig. 9. Requirement instance for the mapp reconfiguration due to the passivation of an arbitrary cpm, from q = 4 to r = 3 correct cpms.

Third, with r = q -1 the value of s xcpm,mapp,r is determined based on the aforementioned mapp allocation rules, i.e.

s xcpm,mapp,3 = mapp (1) mapp (2) mapp (1) nil 3 . (5)
The resulting requirement instance for the passivation of an arbitrary cpm from one of q = 4 correct cpms is shown in Fig. 9.

Note that a single requirement instance specifies the passivation transition from q = 4 to r = 3 correct cpms for all possible permutations. Here, a permutation is a specific configuration of how the mapps are allocated to the cpms of an apfi as well as of the cpm that failed-passive. Thus, a permutation is a specific selection of the indices that define the assignment to the cpms 10 .

Regarding the verification of such a requirement instance, the following has to be considered. First, the transition must be verified for all specific permutations for a complete verification of the required behaviour. Second, to our understanding, performing the related tests based on the stimulation of the categorical indications is not sufficient for a verification at the system level. In order to verify the entire end-to-end system behaviour, the composed transformation

f moni • f f usion • f reconf ig (6)
is considered, with f moni : {ev i } → {z I,i }. This means that to verify a reconfiguration, not the categorical indication is stimulated but an actual exemplary failure event associated with the categorical indication. In the given example, such a failure event could be the power interruption of a cpm.

V. CONCLUSION

For a significant reduction of the costs related to the development of fault-tolerant real-time avionics systems, the Flexible Avionics Platform (apf) and an associated comprehensive automation process, the AAA process, were developed. The apf is characterised by a high-level abstraction layer, the Platform Management, providing a full abstraction of distribution, fault-tolerance, and redundancy towards integrated system functions. The associated AAA process combines the high flexibility of this platform-based approach with a high degree of automation. Therefore, the generation of the development 10 The passivation transition illustrated in Fig. 4 and qualification artefacts of each Flexible Avionics Platform Instance (apfi), such as the system-level specification and the verification artefacts, is largely automated.

This paper focused on the automatic generation of the system-level specification for the high-level Platform Management. The presented approach with its specification subdomains is made possible by the systematic and clear structuring of the apf [START_REF] Hoffmann | Enabling the automated generation of the failure and redundancy management for distributed and integrated fly-by-wire avionics[END_REF]. Each of the named subdomains is dedicated to specific apfi behaviour. These are the intra-module reconfigurations, inter-module reconfigurations, peripheral reconfigurations, and an apfi's entire operation moding. Our article describes the definition of the requirement classes for the apfi reconfigurations which can be expressed based on an apf generic set of categorical indications that classify all possible failure events of an apfi. On this basis, a limited number of requirement classes were defined. They are sufficiently generic to cover the apf's entire usage domain while still being expressive and comprehensible. This facilitates a manual validation as part of a certification process. In addition to the presented actual requirement text of a requirement class, other attributes can of course be added according to the applied requirements standard. The developed requirement classes for the high-level Platform Management were integrated into the AAA tool suite and thus enable the automatic instantiation of reconfiguration and operation moding requirements. This further completes our overall approach for a cost-efficient development and qualification of fault-tolerant, distributed and integrated avionics systems such as fly-by-wire systems.

The apf approach was successfully demonstrated within multiple projects up to an in-flight demonstrator featuring automatic take-off and landing [START_REF] Dalldorff | A full-authority automatic flight control system for the civil airborne utility platform s15-lapaz[END_REF], [START_REF] Kueke | Fly-by-wire for cs23 aircraft-core technology for general aviation and rpas[END_REF], [START_REF] Görke | Flexible platform approach for fly-by-wire systems[END_REF]. Our ongoing research in the LuFo V-3 research project Secured System for Manned Multicopter (SESYMM) focuses on optimising the generated artefacts with regard to DAL A conformity. Moreover, the AAA tool suite is used for the development of a fly-by-wire platform for a remotely piloted aircraft system based on a CS-23 aircraft for operation in the non-segregated airspace without an onboard safety pilot.

GLOSSARY apf

The Flexible Avionics Platform is a platform-based development approach featuring an integrated, distributed, and highly redundant architecture. It is characterised by a high-level abstraction layer, the Platform Management, enabling integrated applications to be executed in a failure-free virtual simplex environment. Thus, applications can be reduced to their cybernetic control law. apfi An instance of the Flexible Avionics Platform. cpm Core processing modules plan and execute the central management decision within an apfi. In addition, they execute the applications for the integrated system function laws.

mapp A multi-application comprises several integrated system function laws of the same criticality level. A dynamic in-flight mapp reallocation between cpms enables an efficient use of the cpm hardware.

Fig. 1 .

 1 Fig. 1. Integrated Modular Avionics architecture.

Fig. 2 .

 2 Fig. 2. Flexible Avionics Platform architecture.

Fig. 3 .

 3 Fig. 3. Hardware structure of an exemplary instance of the apf.

Fig. 4 .

 4 Fig. 4. Mapp and master-slave reconfiguration due to a failure in cpm (R,1) .

Figure 5 Fig. 5 .

 55 Figure5illustrates the basic reconfiguration principle valid for each apfi. An apfi features a large number of possible failure events such as a power interruption, CPU failures, or sensor failures. If a failure event ev i is monitored by a dedicated failure detection mechanism, the corresponding particular indication z I,i is set. Particular indications are then fused to so-called categorical indications z CI,x which are confirmed in time. While the events and the particular indications are mostly apfi specific, the set of possible categorical indications is generic for the apf. Because of the large usage

Fig. 6 .

 6 Fig. 6. (a) Basic instantiation pattern for the requirement class of the fusion of particular indications as well as (b) the relevant part of an exemplary apfi design model.

  cpm(S(a),m)) z CI,comm,(cpm(S(a),m),cpm(S(a),n)) z CI,comm,(cpm(S(a),m),cpm(S(b),o)) z CI,comm,(cpm(S(a),m),cpm(S(b),p)) (cpm(S(a),n)) z CI,comm,(cpm(S(a),n),cpm(S(a),m)) z CI,comm,(cpm(S(a),n),cpm(S(b),o)) z CI,comm,(cpm(S(a),n),cpm(S(b),p)) (cpm(S(b),o)) z CI,comm,(cpm(S(b),o),cpm(S(a),m)) z CI,comm,(cpm(S(b),o),cpm(S(a),n)) z CI,comm,(cpm(S(b),o),cpm(S(b),p)) (cpm(S(b),p)) z CI,comm,(cpm(S(b),p),cpm(S(a),m)) z CI,comm,(cpm(S(b),p),cpm(S(a),n)) z CI,comm,(cpm(S(b),p),cpm(S(b),o))

EndOfREQFig. 7 .

 7 Fig. 7. Requirement class for the mapp reconfiguration due to the passivation or activation of cpms.

Fig. 8 .

 8 Fig. 8. (a) Basic instantiation pattern for the requirement class of the mapp reconfiguration as well as (b) the relevant part of an exemplary apfi design model.

  is a specific permutation of this requirement instance, with x = R, y = B, i = k = 1, j = l = 2, a = B, b = R, m = p = 1, and n = o = 2.

If the master-slave allocation changes, this enables a transient-free usage of data from the new master by the recipients.

The performance level accounts for the state of sensors and actuators being part of the execution of the system functions.

The apfi specific subset is defined in the high-level system design model for the Axx subprocess.

Although, strictly speaking, this requirement class does not describe a reconfiguration, it serves to clarify basic mechanisms.

In addition to the actual requirement text, a requirement class comprises further attributes, such as a rationale, assumptions or the allocation to apfi functions assigned to a specific Design Assurance Level (DAL).

For the implementation into the xAx tool suite, the patterns are modelled using a dedicated domain-specific language. Details can be found in[START_REF] Belschner | A Method for the Automated Generation of Requirements and Traceability for a Distributed Avionics Platform[END_REF].

The formal representation of the requirement classes is not considered in this paper but will be part of future publications.

z CI,BIT leads to the execution of a module built-in test (BIT). If a fatal failure is found during this BIT, the module is passivated for the rest of the mission.

Note that the temporal aspects of this requirement class are neglected in the context of the paper.