Pierre L'ecuyer

Paul Wambergue
email: paul.wambergue@gmail.com

Erwan Bourceret
email: ebourceret@hotmail.fr

Spectral Analysis of the MIXMAX Random Number Generators

Keywords: Random number generators, matrix linear congruential generators, lattice structure, spectral test, simulation

We study the lattice structure of random number generators of the MIXMAX family, a class of matrix linear congruential generators that produce a vector of random numbers at each step. The design of these generators was inspired by Kolmogorov K-systems over the unit torus in the real space, for which the transition function is measure-preserving and produces a chaotic behavior. In actual implementations, however, the state space is a finite set of rational vectors, and the MIXMAX has a lattice structure just like linear congruential and multiple recursive generators. Its matrix entries were also selected in a special way to allow a fast implementation and this has an impact on the lattice structure. We study this lattice structure for vectors of successive and non-successive output values in various dimensions. We show in particular that for coordinates at specific lags not too far apart, in three dimensions, or if we construct points of k + 2 or more successive values from the beginning of an output vector of size k, all the nonzero points lie in only two hyperplanes. This is reminiscent of the behavior of lagged-Fibonacci and AWC/SWB generators. And even if we skip the output coordinates involved in this bad structure, other highly structured projections often remain, depending on the choice of parameters. We show that empirical statistical tests can easily detect this structure.

Introduction

A matrix linear congruential generator (matrix LCG) of order k with modulus m evolves according to a linear recurrence of the form

x i = Ax i-1 mod m (1)
in which x i = (x i,0 , . . . , x i,k-1 ) t is a k-dimensional column vector (the t means transposed ) with coordinates in Z m = {0, 1, . . . , m -1}, and A is a k × k matrix with elements in Z m . The vector x i ∈ Z k m is the state of the generator at step i. The total number of possible states is m k , and since we must avoid the absorbing state 0, the period of the recurrence cannot exceed m k -1. This period is attained if and only if m is a prime number and the characteristic polynomial of A is a primitive polynomial modulo m [START_REF] Niederreiter | A pseudorandom vector generator based on finite field arithmetic[END_REF]. The output at step i is the following k-dimensional vector of random numbers u i,j ∈ [0, 1):

u i = (u i,0 , . . . , u i,k-1 ) = x i /m ∈ [0, 1) k .
(2)

Matrix LCGs have been discussed and studied in [START_REF] Tahmi | Contribution aux Générateurs de Valeurs Aléatoires[END_REF], [START_REF] Niederreiter | A pseudorandom vector generator based on finite field arithmetic[END_REF], [START_REF] Grothe | Matrixgeneratoren zur Erzeugung Gleichverteilter Pseudozufallsvektoren[END_REF], and L' Ecuyer (1990Ecuyer ( , 1994)), for example.

The MIXMAX generators are matrix LCGs with special choices of A. They were introduced by [START_REF] Akopov | Matrix generators for pseudorandom numbers[END_REF] and [START_REF] Savvidy | On the Monte Carlo simulation of physical systems[END_REF], and further developed in [START_REF] Savvidy | The MIXMAX random number generator[END_REF] and [START_REF] Savvidy | Spectrum and entropy of C-systems MIXMAX random number generator[END_REF]. The original version proposed by [START_REF] Akopov | Matrix generators for pseudorandom numbers[END_REF] had

A = A(k, d) =              1 1 1 1 • • • 1 1 1 2 1 1 • • • 1 1 1 3 + d 2 1 • • • 1 1 1 4 3 2 • • • 1 1 . . . . . . 1 k k -1 k -2 • • • 3 2              , (3)
in which the integer d in the third row and second column is a parameter that can be chosen in addition to the dimension k and the modulus m. We shall call it the MIXMAX-(m, k, d).

The u i 's also follow the recurrence

u i = Au i-1 mod 1, (4)
which does not involve m, and this recurrence is actually defined over the entire unit hypercube [0, 1) k ⊂ R k . When the coordinates of u 0 are all rational as in (2), this recurrence necessarily has a finite period, but with irrational coordinates the sequence can be aperiodic and completely fill the space in [0, 1) k . The original MIXMAX was designed based on an analysis in this aperiodic continuous-space case, and then it was argued that for a large enough m, the periodic (discrete) implementation is a very close approximation of the aperiodic (continuous) system. The matrix A in (3) was selected to satisfy the following two conditions: (1) the determinant of A is 1 and (2) the eigenvalues λ 1 , . . . , λ k of A are away from the unit circle. The first condition implies that the linear transformation (4) maps any region R ⊆ [0, 1) k into another region of the same volume. The second condition ensures (roughly) that trajectories that start from states very close to each other and evolve according to this transformation in the real space diverge as Θ(e hi ), where i is the number of steps and h is the Kolmogorov entropy defined as

h = k j=1 I[|λ j | > 1] • log |λ j |,
in which I is the indicator function. For more precise statements and further details, see [START_REF] Savvidy | Spectrum and entropy of C-systems MIXMAX random number generator[END_REF]. [START_REF] Savvidy | The MIXMAX random number generator[END_REF] provides lower bounds on h that depend only on k for A = A(k, d), and shows that h is reasonably large. In particular, h is much larger than for the AWC and SWB generators of [START_REF] Marsaglia | A new class of random number generators[END_REF]. [START_REF] Savvidy | The MIXMAX random number generator[END_REF] also shows that the maximal period for these generators is (m k -1)/(m -1), which is m -1 times shorter than the maximal possible period for matrix LCGs. This limitation stems from the requirement that det(A) = 1. He provides a table of parameters (k, d) for m = 2 61 -1

where k ranges from 10 to 3150, d ranges from -11 to 15, and the period is (m k -1)/(m -1) divided by a small integer (which is 1 in some cases). Even with k = 8, this already gives a period near 2 427 . He finally provides an efficient implementation that uses only 2k additions and one multiplication by d to compute the next vector x i at each step.

To increase the flexibility and eventually permit a larger entropy and potentially better behavior, [START_REF] Savvidy | Spectrum and entropy of C-systems MIXMAX random number generator[END_REF] defined a MIXMAX variant with an additional integer parameter c, with

A = A(k, d, c) =                 1 1 1 1 • • • 1 1 1 2 1 1 • • • 1 1 1 c + 2 + d 2 1 • • • 1 1 1 2c + 2 c + 2 2 • • • 1 1 1 3c + 2 2c + 2 c + 2 • • • 1 1 • • • 1 (k -2)c + 2 (k -3)c + 2 (k -4)c + 2 • • • c + 2 2                 , (5)
which we call MIXMAX-(m, k, d, c), and another variant with five parameters (m, k, d, c, b), with

A = A(k, d, c, b) =                 1 1 1 1 • • • 1 1 1 2 1 1 • • • 1 1 1 3c + d + b 2 1 • • • 1 1 1 4c + b 3c + b 2 • • • 1 1 1 5c + b 4c + b 3c + b • • • 1 1 • • • 1 kc + b (k -1)c + b (k -2)c + b • • • 3c + b 2                 , (6)
which we denote by MIXMAX-(m, k, d, c, b). These generators also satisfy the conditions (1) and ( 2) above and have the same maximal possible period as the MIXMAX-(m, k, d). Note that in those papers, the parameters m, k, d, c are named p, N, s, m instead. A user's guide with specific parameters and pointers to downloadable code is available in [START_REF] Savvidy | MIXMAX Manual[END_REF]. This code is part of the ROOT library available at the CERN, in Geneva.

Examining the eigenvalues of A and the entropy h is one type of spectral analysis for matrix LCGs. A different type of spectral analysis is the spectral test that examines the lattice structure of vectors of successive or non-successive output values produced by LCGs [START_REF] Coveyou | Fourier analysis of uniform random number generators[END_REF][START_REF] Knuth | The Art of Computer Programming[END_REF][START_REF] L'ecuyer | An implementation of the lattice and spectral tests for multiple recursive linear random number generators[END_REF]. The purpose of this paper is to show how this spectral test applies to MIXMAX generators and see what kind of lattice structure we can find.

The remainder is organized as follows. In Section 2, we recall the lattice structure of matrix LCGs and how the spectral test works for these generators. In Section 3, we prove various properties of the lattice structure of the MIXMAX generators. We show that certain coordinates of the successive output points are linked by very simple linear relations, which implies that these points belong to a small number of parallel hyperplanes in the unit hypercube. In Section 4, we show that undesirable structures remain even if we skip certain output values to break the most problematic linear relations. In Section 5, we illustrate this with specific MIXMAX generators proposed in [START_REF] Savvidy | MIXMAX Manual[END_REF]. What we find is reminiscent of the types of bad structures found in the Lagged-Fibonacci, AWC/SWB, and some other types of multiple recursive generators [START_REF] Tezuka | On the add-with-carry and subtract-with-borrow random number generators[END_REF], L'Ecuyer 1997[START_REF] L'ecuyer | On the Deng-Lin random number generators and related methods[END_REF][START_REF] L'ecuyer | On the lattice structure of a special class of multiple recursive random number generators[END_REF].

For general background on uniform random number generators (RNGs), we refer the reader to the tutorial chapter of L 'Ecuyer (2012), the recent survey of L 'Ecuyer et al. (2017), and the detailed historical account of L 'Ecuyer (2017).

Lattice Structure of Matrix LCGs

Suppose a matrix LCG produces s uniform random numbers u 0 , . . . , u s-1 as follows. Starting from some initial state x 0 , we generate u 0 , . . . , u ν as in (2) where ν satisfies s = kν + r and 0 ≤ r < k, and we put u ki+j = u i,j for all i = 0, . . . , ν and j = 0, . . . , k -1 for which 0 ≤ ki + j < s. Let Ψ s be the set of all vectors (u 0 , . . . , u s-1 ) obtained in this way, from all the m k possible initial states x 0 of the matrix LCG, including the zero vector. In case the generator does not have full period m k -1, the set Ψ s considered here contains all vectors produced over all cycles of the generator. An important requirement of good RNGs is that this set Ψ s covers the unit hypercube [0, 1) s very evenly, at least when s is not too large (L 'Ecuyer 1994'Ecuyer , 2006)). This requirement captures uniformity and independence of the successive random numbers; that is, it measures the quality of the approximation of the theoretical concept of independent uniform random variables [START_REF] Knuth | The Art of Computer Programming[END_REF][START_REF] Ecuyer | Uniform random number generation[END_REF]. Note that for s = k, Ψ s contains all the m k points of Z k m /m = {0, 1/m, . . . , (m -1)/m} k exactly once. For s < k, Ψ s is a multiset that contains all points Z s m /m exactly m k-s times each. This is the best that one can achieve, given m and k.

We also consider the following generalized form of this notion, as in [START_REF] Couture | On the lattice structure of certain linear congruential sequences related to AWC/SWB generators[END_REF], L 'Ecuyer (1997), L 'Ecuyer and Couture (1997), and L' Ecuyer and Simard (2014). For any finite set of integers I = {i 1 , . . . , i s } where 0 ≤ i 1 < • • • < i s , consider the multiset Ψ s (I) of all s-dimensional output vectors (u i 1 , . . . , u is ) obtained by the method described earlier, from all possible initial states x 0 :

Ψ s (I) = {(u i 1 , . . . , u is ) ∈ [0, 1) s | x 0 ∈ Z k m }.
If x 0 is selected randomly and uniformly from Z k m , then (u i 1 , . . . , u is ) has the uniform distribution over the finite multiset Ψ s (I). The ideal, on the other hand, would be that this vector has the uniform distribution over [0, 1) s . Obviously, we can have a good approximation of this ideal only if Ψ s (I) covers [0, 1) s very evenly, or at least not too unevenly. This multiset Ψ s (I) is actually the projection of the set Ψ s over the selected coordinate indices i 1 , . . . , i s , with s = i s + 1. The set Ψ s is just a special case of this with I = {0, ..., s -1}. For s < k, it is not always true that Ψ s (I) contains all of Z s m /m; for some sets I it can contain only a small proportion.

It is known that any projection Ψ s (I) of some Ψ s over a subset of s coordinates, is the (finite) intersection of a lattice L s (I) in the real space R s with the unit hypercube [0, 1) s [START_REF] Afflerbach | The lattice structure of pseudo-random vectors generated by matrix generators[END_REF]Grothe 1988, L'Ecuyer and[START_REF] L'ecuyer | An implementation of the lattice and spectral tests for multiple recursive linear random number generators[END_REF]. One consequence of this is that there are families of equidistant parallel hyperplanes in R s such that each family contains all the points of Ψ s (I). We want to make sure that none of these families has just a few widelyspaced hyperplanes, because this would imply that the points would not cover the space very well. The spectral test introduced by [START_REF] Coveyou | Fourier analysis of uniform random number generators[END_REF] for LCGs and further discussed in [START_REF] Knuth | The Art of Computer Programming[END_REF] and L 'Ecuyer and Couture (1997), for example, computes the distance d s (I) between successive hyperplanes for the family for which this distance is largest. Let n = min(m k , m s ), which is the largest number of distinct points that we can have in Ψ s (I). A standardized measure that takes values in (0, 1] regardless of n and s can be defined as S s (I) = d * s (n)/d s (I), where the normalizing constant d * s (n) is the smallest distance between hyperplanes that can be achieved by a general s-dimensional lattice having n points per unit of volume. One can write

d * s (n) = γ 1/2
s n -1/s where the γ s are the Hermite constants, which depend only on s [START_REF] Conway | Sphere Packings, Lattices and Groups[END_REF]Sloane 1999, L'Ecuyer 1999). These constants are known exactly only for s ≤ 8 and s = 24. For the other values of s, we replace d * s (n) in the definition of S s (I) by the value of d s (I) achieved by the best known lattice of density n in s dimensions. In other words, we approximate γ 1/2 s by the smallest value of n 1/s d s (I) that has been achieved by a known lattice construction in s dimensions. These values can be found in Chapter 6 of [START_REF] Conway | Sphere Packings, Lattices and Groups[END_REF]. We need them only for s < 20. Thus, S s (I) can be arbitrarily close to 1 in general. Very small values of S s (I) are bad and should be avoided.

It is known that d s (I) = 1/ s (I) where s (I) is the (Euclidean) length of the shortest nonzero vector in the dual lattice

L * s (I) = {w ∈ R s : w t v mod 1 = 0 for all v ∈ L s (I)}.
To find a shortest vector, one first constructs a basis of the dual lattice. Then a shortest vector and its length are a solution and the optimal value of a quadratic integer optimization problem that can be solved by a branch-and-bound procedure [START_REF] Fincke | Improved methods for calculating vectors of short length in a lattice, including a complexity analysis[END_REF]Pohst 1985, L'Ecuyer and[START_REF] L'ecuyer | An implementation of the lattice and spectral tests for multiple recursive linear random number generators[END_REF]).

If we compute a shortest nonzero vector in the dual lattice with the L 1 norm defined by

w 1 = (w 1 , . . . , w s ) 1 = |w 1 | + • • • + |w s | instead
of the Euclidean norm, the length of the shortest vector minus one gives the minimal number of hyperplanes that cover all the lattice points in [0, 1) s [START_REF] Marsaglia | Random numbers fall mainly in the planes[END_REF][START_REF] Knuth | The Art of Computer Programming[END_REF].

The lattice bases can be constructed as follows. Suppose s = kν + r and for any k × k matrix M, let [M] r denote the r × k matrix formed by the first r rows of M. Let I be the identity matrix. Consider the s × s matrices

V =           I/m A t /m • • • (A ν-1 ) t /m ([A ν ] r ) t /m 0 I 0 . . . I 0 I           (7)
and

W =           m • I 0 0 -A I . . . . . . -A ν-1 I -[A ν ] r 0 I           (8)
in which the identity I at the bottom right of each matrix is r × r and the other I's are k × k.

Then the rows of V form a basis of the lattice L s [START_REF] Afflerbach | The lattice structure of pseudo-random vectors generated by matrix generators[END_REF]) and, since VW t = I, the rows of W form the corresponding dual basis, which is a basis of the dual lattice L * s . Any integer linear combination of the rows of W belongs to the dual lattice. For the case of lacunary indices, a set of generating vectors for L s (I) can be obtained by projecting the basis vectors of L s over the s retained coordinates in I. That is, we build V with s columns and then we keep only the columns of V whose indices are in I, and discard the other ones. The s rows of the resulting matrix give a set of s vectors that can be turned into a set of s independent vectors that form a basis of L s (I), using the approach described in L' Ecuyer and Couture (1997). The corresponding dual basis can then be obtained by inverting this basis matrix modulo 1. (Note that projecting the vectors of the original dual basis on the retained lacunary coordinates does not provide vectors that belong to the dual basis of L s (I) in general.)

Ideally, we want to make sure that no S s (I) is very small, at least for a selected class of subsets I. We cannot verify this for all possible subsets I of arbitrary size, because there are too many. The idea is to limit ourselves to a finite class of subsets I and make sure that the smallest S s (I) (the worst-case) over that class is not too small. One way to define this class is to select an integer s > 0 and consider all subsets I ⊆ {0, . . . , s -1}. This gives the worst-case figure of merit M s = min I⊆{0,...,s -1}

S s (I), which we will use in the rest of this paper. We will always take s > k, because for s ≤ k all the projections contain all the points of Z s m /m. If s is taken very large, for example s > 100, it may be impossible to have M s very close to 1, because an excessively large number of subsets I are considered and it may be impossible to have S s (I) close to 1 for all of them simultaneously. We do not know what is the best achievable M s as a function of s . But empirically, we find that for large m and moderate k, with random choices of the matrix A, it is rare to find a matrix LCG with a very small value of M s . The following example illustrates this situation.

Example 1. Consider a multiple recursive generator (MRG), defined via:

x i = (a 1 x i-1 + • • • + a k x i-k ) mod m, u i = x i /m,
which is in fact equivalent to a matrix LCG of order k with matrix

A =        0 1 • • • 0 . . . . . . . . . 0 0 • • • 1 a k a k-1 • • • a 1        k .
For k = 7 and m = 2 63 -52425 (a prime), we made a random search for 10,000 parameter vectors a = (a 1 , . . . , a k ) that give a full period ρ = m k -1 ≈ 2 441 , and we then computed M 10 and M 12 for each. Their values of M 10 ranged from 0.53858 (the best) to 0.13221 (the worst), and M 12 ranged from 0.40807 to 0.10540. Clearly, values of M 10 or M 12 smaller than say 0.1 are very rare. In Section 5, we will find that the corresponding values for the MIXMAX are several orders of magnitude smaller. 2 Although computing S s (I) for a large class of sets I can be expensive, by looking at the structure of the generator, one can sometimes identify specific subsets I for which S s (I) is very small for some s not too large, due to an unfortunate design. This is what we do for the MIXMAX in this paper. For excellent generators, such systematic structural defects should not happen. Note that for any two sets I ⊂ I of sizes s < s , any vector in L * s (I) can be extended to a vector of the same length in L * s (I ) by adding zero coordinates. Therefore s (I ) ≤ s (I), or equivalently d s (I) ≤ d s (I ). This means that if d s (I) is large for some set I of small cardinality s, then d s (I ) must be at least as large for all sets I that contain I. For this reason, when S s (I) is extremely small, it is often the case that d s (I ) = d s (I) for a very large number of supersets I that contain I, and S s (I ) will typically be also very small for most of them. Conversely, this same inequality implies that if d s (I ) is large for some set I , then for any set I ⊂ I , it cannot be small.

There is one important difference between the lattice structure of matrix LCGs and that of ordinary LCGs and MRGs. In the latter, the point set Ψ s (I) and its lattice structure are shift-invariant with respect to coordinate numbers, in the sense that Ψ s (I) for I = {i 1 , . . . , i s } is the same as Ψ s (I ) for I = {i 1 + j, . . . , i s + j} for any integer j ≥ 0, whereas for the matrix LCG, apart from special cases, this is true only if j is a multiple of k. That is, the lattice structure we analyze is for points whose coordinates are numbered from the beginning of an output vector.

Lattice Structure of MIXMAX

When a MIXMAX generator has maximal period, it has m -1 cycles of length (m k -1)/(m -1), and the initial state determines which cycle we are in. In this paper, we study the lattice L s or L s (I) generated by all the points produced over all the cycles of the MIXMAX generator. When a generator has many disjoint cycles, one cannot rule out a priori that the lattice generated by a single cycle is a strict sublattice of the full lattice generated by all the points produced over all the cycles. Analyzing the lattice generated over a single cycle is beyond the scope of the present paper. It could be done using the ideas and methodology of [START_REF] Couture | Orbits and lattices for linear random number generators with composite moduli[END_REF].

By writing the matrix -A = -A(k, d) explicitly in rows k + 1 to 2k of the definition of W, we find that for the MIXMAX-(m, k, d), of W, which we denote by w 1 , . . . , w s , form a basis of the dual lattice, so any integer linear combination of these vectors belongs to the dual lattice L * s . In particular, if k ≥ 2, we have w k+1 = (-1, -1, -1, . . . , -1,1, 0, . . . , 0)

W =                                       m • I 0 0 • • • 0 -1 -1 -1 • • • -1 -1 -2 -1 • • • -1 -1 -3 -d -2 • • • -1 -1 -4 -3 • • • -1 I 0 • • • 0 • • • -1 -k -(k -1) • • • -2 -A 2 0 I . . . . . . . . . -A ν-1 -[A ν ] r 0 I                                       .
w k+2 = (-1, -2, -1, . . . , -1,0, 1, . . . , 0) ↑ coordinate k + 1
and therefore w = w k+1 -w k+2 = (0, 1, 0, . . . , 0,1, -1, 0, . . . , 0)

↑ coordinate k + 1
is in the dual lattice L * s for any s ≥ k + 2. (Here, the index i of output values and the coordinates of u i start at 0 as usual, but we start the coordinates of vectors v and w at 1, which is also standard.) This vector w has Euclidean length √ 3 and L 1 norm equal to 3. Its presence in the dual lattice implies that if we take all k output values at each step, the successive output values satisfy (u 1 + u k -u k+1 ) mod 1 = 0. And since 0 ≤ u i < 1 for all i, one must have u 1 + u k -u k+1 = q for q ∈ {0, 1}. This means that if we take I = {1, k, k + 1}, all the points of Ψ 3 (I) are in only two planes, determined by this equation. Also, the dual lattice to L 3 (I) contains the vector (1, 1, -1), whose Euclidean length is √ 3. This argument holds in exactly the same way for the MIXMAX-(m, k, d, c) andMIXMAX-(m, k, d, c, b) as well, because they have the same first two rows of A. We have just proved the following.

Proposition 1. For the three MIXMAX variants, with k ≥ 2, whenever I = {1, k, k + 1} ⊆ I , all the points of Ψ 3 (I ) are in two equidistant parallel planes, which are at distance 1/ √ 3 apart, in the three dimensional unit hypercube.

This result shows not only that the lattice structure is very bad for Ψ 3 (I), but also that it is bad for a very large number of projections on subsets I of coordinates that contain I. This is the same type of problematic structure as for the lagged-Fibonacci and AWC/SWB generators [START_REF] Couture | On the lattice structure of certain linear congruential sequences related to AWC/SWB generators[END_REF], L'Ecuyer 1997[START_REF] Tezuka | An analysis of add-with-carry and subtract-with-borrow generators[END_REF][START_REF] Tezuka | On the add-with-carry and subtract-with-borrow random number generators[END_REF], which are known to fail simple statistical tests because of this structure (L 'Ecuyer and Simard 2007). We will see in Section 5 that the MIXMAX also fails simple tests because of this structure.

The next proposition unveils another structure of the MIXMAX-(m, k, d). If k ≥ 5, by taking w = w 2k -w 2k-1 -w k+1 = (1, 0, . . . , 0, -1, 0, . . . , 0, -1, 1, 0, . . . , 0)

↑ coord. k + 1
in which we have -1 at coordinates k + 1 and 2k -1, we find with a similar reasoning: 5 equidistant parallel hyperplanes at distance 1/ √ 6 apart. These 5 hyperplanes are not the same as the 4 hyperplanes in the first part.

Proof. For the first part, take w = w k+4+j -2w k+5+j + w k+6+j = (0, . . . , 0, -1, 0, . . . , 0, 1, -2, 1, 0, . . . ) ↑ coord. 6 + j in which the -1 is at position 6 + j and the -2 is at position k + 5 + j. This shows that we have the relationship -u 5+j + u k+3+j -2u k+4+j + u k+5+j = q for q ∈ {-2, -1, 0, 1}. These are the equations of four hyperplanes that contain all the points of Ψ s (I) when I contains the coordinates involved in this linear relationship. In this case, the lattice L s (I) contains a dual vector with L 1 -norm of 5 and Euclidean length √ 7. For the second part, take w = w k+4+j -w k+5+j -w k+6+j + w k+7+j = (0, . . . , 0, -1, -1, 0, . . . , 0, 1, -1, -1, 1, 0, . . . ).

↑ coord. 6 + j in which the first -1 is at position 6 + j and the first 1 is at position k + 4 + j. This dual basis vector indicates the relationship -u 5+j -u 6+j + u k+3+j -u k+4+j -u k+5+j + u k+6+j = q for q ∈ {-3, -2, -1, 0, 1}, which involves only retained coordinates if I satisfies the condition in the second part of the proposition. Then the lattice L s (I) contains a dual vector with L 1 -norm of 6 and Euclidean length √ 6, and the conclusion follows. Since the condition of the second part implies that of the first part, the result of the first part also holds here. The two sets of hyperplanes are different.

2 By taking for w the same combination of dual vectors as in the first part of the previous proposition, we obtain the following two results for the MIXMAX with four and five parameters. In all the propositions that follow, will denote the length of a short vector in the dual lattice, but not necessarily the shortest length. (m,k,d,c) generator with c ≥ 1, if k ≥ 6, 0 ≤ j ≤ k -6, and {4 + j, 5 + j, k + 3 + j, k + 4 + j, k + 5 + j} ⊆ I, then there is a set of c + 3 equidistant parallel hyperplanes that contain all the points of Ψ s (I). These hyperplanes are at distance 1/ apart, where 2 = (c -1) 2 + 7.

Proof. The dual basis contains the vector w = w k+4+j -2w k+5+j + w k+6+j = (0, . . . , 0, 1 -c, -1, 0, . . . , 0, 1, -2, 1, 0, . . . ), ↑ coord. 5 + j in which the 1-c is at position 5+j and the -2 is at position k +5+j. Thus we have the relationship (1 -c)u 4+j -u 5+j + u k+3+j -2u k+4+j + u k+5+j = q where q ∈ {-c -1, -c, . . . , 0, 1}. Also, the square Euclidean length of w is (c -1) 2 + 7. The result follows.

2

Proposition 5. For the MIXMAX-(m, k, d, c, b) generator with c ≥ 1 and b ≥ 0, if k ≥ 6, 0 ≤ j ≤ k -6, and {3 + j, 4 + j, 5 + j, k + 3 + j, k + 4 + j, k + 5 + j} ⊆ I, then there is a set of 5c + 2b -1 equidistant parallel hyperplanes that contain all the points of Ψ s (I). These hyperplanes are at distance 1/ apart, where 2 = (2c + b -2) 2 + (3c + b -3) 2 + 7.

Proof. The dual lattice contains w = w k+4+j -2w k+5+j + w k+6+j = (0, . . . , 0, 2c + b -2, -3c -b + 3, -1, 0, . . . , 0, 1, -2, 1, 0, . . . )

↑ coord. 4 + j in which the -2 is at position k + 5 + j. Thus, ((2c + b -2)u 3+j -(3c + b -3)u 4+j -u 5+j + u k+3+j -2u k+4+j + u k+5+j
) mod 1 = 0. If I contains the coordinates involved in this linear relationship, the lattice L s (I) contains a dual vector with L 1 -norm of 5c + 2b and square Euclidean length

(2c + b -2) 2 + (3c + b -3) 2 + 7.
2 Propositions 4 and 5 tell us that the MIXMAX- (m,k,d,c) has a bad structure when c is small, and the MIXMAX- (m,k,d,c,b) has a bad structure when both c and b are close to 0, respectively. The next proposition emphasizes the fact that a large value of c is not sufficient to guarantee good quality. It shows that if the modulus m is near a small multiple of c, there is also a bad structure. Proposition 6. For the MIXMAX-(m, k, d, c) generator with c ≥ 1, suppose m = qc + r where q > 0 and |r| are small integers (r can be negative).

If k ≥ 6, 0 ≤ j ≤ k -6, and {4 + j, 5 + j, k + 3 + j, k + 4 + j, k + 5 + j} ⊆ I, then there is a set of 5q + |q + r| -1 equidistant parallel hyperplanes that contain all the points of Ψ s (I). These hyperplanes are at distance 1/ apart, where 2 = 7q 2 + (q + r) 2 .

Under the stronger conditions that k ≥ 7, 0 ≤ j ≤ k -7, and {4 + j, 5 + j, 6 + j, k + 3 + j, k + 4 + j, k + 5 + j, k + 6 + j} ⊆ I, Ψ s (I) is covered by another family of equidistant parallel hyperplanes at distance 1/ apart, where 2 = 5q 2 + r 2 + (q + r) 2 . This last bound is smaller than the bound in the first part if and only if 2q 2 > r 2 .

In both cases, if d = 0, one can also take j = -1 and reduce the lower bound on k by 1.

Proof. For the first part, take w = q(w k+4+j -2w k+5+j + w k+6+j ) mod m = q(0, . . . , 0, 1 -c, -1, 0, . . . , 0, 1, -2, 1, 0, . . . ) mod m = (0, . . . , 0, q + r, -q, 0, . . . , 0, q, -2q, q, 0, . . . ), in which the q + r is at position 5 + j and the -2q is at position k + 5 + j. Thus we have the relationship ((q + r)u 4+j -qu 5+j + qu k+3+j -2qu k+4+j + qu k+5+j ) mod 1 = 0. So if I satisfies the condition, we have a dual vector whose L 1 length at most 5q + |q + r| and squared Euclidean length 7q 2 + (q + r) 2 .

For the second part, we have w = q(w k+4+j -w k+5+j -w k+6+j + w k+7+j ) mod m = q(0, . . . , 0, 1 -c, -c, -1, 0, . . . , 0, 1, -1, -1, 1, 0, . . . ) mod m = (0, . . . , 0, q + r, r, -q, 0, . . . , 0, q, -q, -q, q, 0, . . . ), in which the q + r is at position 5 + j and the first q is at position k + 4 + j. If I satisfies the condition in the first part, we have a vector in the dual of L s (I) whose only nonzero coordinates correspond to the nonzero coordinates of w. This vector has L 1 length of 5q + |r| + |q + r| and squared Euclidean length 5q 2 + r 2 + (q + r) 2 . When d = 0, one can easily verify that this development also works for j = -1. 2 We have seen so far that the MIXMAX always produces a bad lattice structure if we keep the first two coordinates of each vector. If we skip these two coordinates, there is still always a bad lattice structure for the MIXMAX-(m, k, d), as seen in Proposition 3, and for the MIXMAX with four or five parameters, the lattice structure is always bad if the parameters c and b are too small (e.g., if b = 0 and c is close to a divisor of m). Moreover, even if c is large and we skip the first three values of each vector, there are situations where the lattice structure is also bad, depending on the choices of parameters c and b. In other situations, the lattice structure can be explored by applying the spectral test numerically to specific MIXMAX instances. That is, for s = k + 1, k + 2, . . . , we construct a basis of the dual lattice for I = {0, . . . , s -1} as explained in Section 3, then we compute the length s of the shortest nonzero vector in that lattice using the methodology described in L' Ecuyer and Couture (1997).

Testing of some proposed MIXMAX generators

We now apply our results to specific MIXMAX generators proposed by [START_REF] Savvidy | MIXMAX Manual[END_REF]. We also give empirical results for two simple empirical statistical tests that detect the bad structures, namely the collision test and the birthday spacings tests. These tests are studied in details in L 'Ecuyer and Simard (2001) and L 'Ecuyer et al. (2002); here we just summarize their definitions. For the collision test, we split the interval [0, 1) into d equal parts. This partitions the unit cube [0, 1) s into d s cubic boxes. Then we generate n random vectors in s dimensions by taking n non-overlapping blocks of s successive output values produced by the generator, and we count the number C of times a point falls in a box that already had a point before (the number of collisions). We repeat this N times independently and let C tot be the total number of collisions (the sum of the N realizations of C). This C tot should have approximately a Poisson distribution with mean λ c = N n 2 /(2d s ). We compute and report the right p-value, defined as the probability that a Poisson random variable with mean λ c takes a value larger or equal to the observed realization of C tot . A very small pvalue indicates that the points tend to fall in the same boxes (or same regions in the unit To see if simple tests can detect this structure, we implemented a version of the generator that skips the first 3 values and keeps the next 5, in each block of 8, and we applied the birthday spacings test in s = 10 dimensions with d = 64, n = 10 7 , and N = 10. The expected number of collisions was 2168 and we observed C tot = 4220. This gives a p-value smaller than 10 -300 . 2

Example 3. We now look at the larger MIXMAX-(m, k, d, c) with m = 2 61 -1, k = 17, d = 0, and c = 2 36 + 1, proposed by [START_REF] Savvidy | MIXMAX Manual[END_REF] and widely adopted in software. For I = {1, 17, 18} and any superset of this I, all the points of Ψ 3 (I) are in two parallel planes at distance 1/ √ 3. With subsets of successive coordinates starting at 0, we find d s = 1/ √ 18 with S s ≈ 1.115 × 10 -17 for s = 18, and d s = 1/ √ 3 with S s ≈ 3.656 × 10 -17 for s = 19, which are again very small.

Here m = 2 25 c -2 25 -1, so q = 2 25 and r = -2 25 -1 in Proposition 6, which yields a dual vector of length = (7 × 2 50 + 1) 1/2 ≈ 8.878 × 10 7 for I = {4, 5, 11, 12, 13} gives Ψ 5 (I) = 3.127 × 10 -11 . With I = {4, 5, 6, 11, 12, 13, 14}, we get a dual vector of length ≈ 8.219 × 10 7 , which gives S 7 (I) ≈ 2.648 × 10 -11 .

We applied the birthday spacings test to this generator with s = 20, d = 8, n = 10 7 , and N = 10. Each block of 20 successive output values was formed by taking all 17 values of one block and the first three values of the next block, and the remaining values of the second block were not used. The expected number of collisions was 2168.4 and we observed 5863, for a p-value smaller than 10 -300 . 2

Example 4. This MIXMAX-(m, k, d, c) example was also proposed (and highly recommended) by [START_REF] Savvidy | MIXMAX Manual[END_REF]. It has m = 2 61 -1, k = 240, d = 487013230256099140, and c = 2 51 + 1. Proposition 1 tells us that for I = {1, 240, 241}, all the points of Ψ 3 (I) are in only two parallel planes and similarly for any set I that contains I. As in the previous example, some bad projections appear even if we skip the first three coordinates of each output vector. Here we have m = 1024c -1025, so Proposition 6 applies with q = 1024 and r = -1025. The proposition tells us that for I = {4, 5, 243, 244, 245}, Ψ s (I) is contained in at most 5q + |q + r| -1 = 5120 equidistant parallel hyperplanes at distance 1/ apart, where 2 = 7q 2 + (q + r) 2 = 7340033, i.e., ≈ 2709.245, for s = 5. This turns out to be the exact length of the shortest vector for this I. The corresponding normalized figure of merit is S s (I) ≈ 9.5436 × 10 -16 .

For the larger index set I = {4, 5, 6, 243, 244, 245, 246}, the points of Ψ s (I) all belong to another family of parallel hyperplanes at distance 1/ apart, where 2 = 5q 2 + r 2 + (q + r) 2 = 6293506, i.e., ≈ 2508.686, in s = 7 dimensions. This is again the length of the shortest vector for this I and we have S s (I) ≈ 8.0836 × 10 -16 , which is again very small. This means that the distance between successive hyperplanes that contain all the points is much larger than what one should expect with m = 2 61 -1 in 7 dimensions. Note that changing d would have no impact on these results, because d does not appear in the bounds. 2

Conclusion

We have examined the lattice structure of the vectors (or points) of successive output values produced by the MIXMAX generator. We showed that the projections of those points over certain subsets of coordinates have bad structures, in which all the points belong to a small number of parallel hyperplanes, much smaller than what one would expect given the size of the modulus. In particular, for a very large number of projections (all those that contain three specific indices), all the points are in only two hyperplanes. One can get rid of these bad structures by skipping some output values, but we saw that other structures then show up, due to linear relationships between other subsets of coordinates. These relationships come from the special structure of the matrix A. One can alleviate this weak behavior by skipping more coordinates in the output vectors (those that are involved in the bad linear relationships), but this would slow down the generator. What is the practical impact of these bad structures on simulation results if we do not skip coordinates, or if we skip just a few? The results of simple empirical tests given here provide a partial answer: the tests easily detect the structure. For most applications there may be no visible impact, but for some applications the poor structures may introduce significant bias if there is some kind of alignment or synergistic effect between the poor lattice structure and the way the random numbers are used in the application, as exemplified in our statistical tests. This type of effect is not easy to predict in general, but it has been observed in the past for RNGs that have a poor lattice structure similar to the one that we have unveiled here; see [START_REF] Ferrenberg | Monte Carlo simulations: Hidden errors from "good" random number generators[END_REF], [START_REF] Tezuka | On the add-with-carry and subtract-with-borrow random number generators[END_REF]L'Ecuyer (1997), for example. Therefore, it is important for the MIXMAX users to be aware of these structural properties and be cautious about them.

For

  the MIXMAX-(m, k, d, c) and MIXMAX-(m, k, d, c, b), it suffices to replace the explicit submatrix -A = -A(k, d) in W by -A(k, d, c) and -A(k, d, c, b), respectively. The rows

Proposition 4 .

 4 For the MIXMAX-

Acknowledgments

This work has been supported by an NSERC-Canada Discovery Grant, a Canada Research Chair, and an Inria International Chair to P. L'Ecuyer. Marc-Antoine Savard helped doing spectral test computations and Théo Guillaumot ran the statistical tests. P. L'Ecuyer wants to thank G. K. Savvidy for inviting him to the MIXMAX Network Meeting at the CERN, in Geneva, in July 2016, which triggered his interest in the MIXMAX generator. We thank the reviewers, the Associate Editor, and the Area Editor B. Tuffin, whose comments helped improving the paper.

Proposition 2. For the MIXMAX-(m, k, d) with k ≥ 5, if {0, k, 2k -2, 2k -1} ⊆ I, then all the points of Ψ s (I) are in the three equidistant parallel planes with equations u 0 -u ku 2k-2 + u 2k-1 = q for q ∈ {-1, 0, 1}, which are at distance 1/2 apart.

Note that in contrast to the previous one, this relationship does not involve the second coordinate of the state vectors of size k. One can find other undesirable relationships like this and we will give a few more in what follows.

Skipping Coordinates

The simplest way to eliminate the bad structure exhibited in the previous propositions is to skip some coordinates of the k-dimensional vector u i when producing the output. This idea was already proposed by [START_REF] Lüscher | A portable high-quality random number generator for lattice field theory simulations[END_REF] for the AWC/SWB generators and implemented by [START_REF] James | RANLUX: A Fortran implementation of the high-quality pseudorandom number generator of Lüscher[END_REF]. Instead of taking all k coordinates at each step, one can retain only a subset J ⊂ {0, . . . , k -1} of the k coordinates, to produce a block of |J| random numbers at each step. For example, if we skip the second coordinate of each vector, i.e., if we take J = {0, 2, 3, . . . , k -1}, the relationship u 1 + u k -u k+1 = 0 or 1 is not harmful anymore, because u 1 and u k+1 are no longer used. But other relationships can be found that do not involve these removed coordinates (Proposition 2 gives one), and some of these relationships may correspond to short vectors in the dual of the corresponding projected lattice L s (I), where I contains only coordinates that are retained. To find such a relationship, we need to find a vector w ∈ L * s whose coordinates that correspond to the output values that are skipped are zero. (In the notation used in this paper, the indices of the u i 's when we skip coordinates remain the same as when we take all k values at each step; we find this less confusing than making them depend on I or J.)

If the set J of coordinates that we keep includes the first two coordinates, then the relationship u 1 + u k -u k+1 = 0 or 1 still involves coordinates that are all retained and the bad lattice structure remains. To remove this structure, one must skip at least one of the first two coordinates. For the MIXMAX-(m, k, d), if we skip only the second coordinate of each u i , the problem remains, because the relationship in Proposition 2 does not involve u 1 , u k+1 , u 2k+1 , . . . , so we still have the bad hyperplane structure pointed out in this proposition.

The next proposition shows that even if we skip the first two (and even the first three) coordinates of each u i , for the MIXMAX-(m, k, d) we still get bad relationships among the other coordinates, and therefore a bad structure. In all our propositions, the bad structure also holds for all sets I that contain I. Proposition 3. For the MIXMAX-(m, k, d), if k ≥ 6, 0 ≤ j ≤ k -6, and {5 + j, k + 3 + j, k + 4 + j, k + 5 + j} ⊆ I, then Ψ s (I) is contained in at most 4 equidistant parallel hyperplanes at distance 1/ √ 7 apart. If k ≥ 7, 0 ≤ j ≤ k -7, and the stronger condition {5 + j, 6 + j, k + 3 + j, k + 4 + j, k + 5 + j, k + 6 + j} ⊆ I holds, then Ψ s (I) is also contained in cube) much more often that they should. The birthday spacings test is similar, except that we number the d s boxes in some natural order, sort the box numbers of the n points by increasing order, compute the first-order differences between the successive box numbers, and count the number of collisions in these differences. The total number of collisions B tot over the N replications should be approximately Poisson with mean λ b = N n 3 /(4d s ) and we can use this to compute the right p-value.

Example 2. Consider the small MIXMAX-(m, k, d, c) proposed in the MIXMAX implementation of [START_REF] Savvidy | MIXMAX Manual[END_REF], for which m = 2 61 -1, k = 8, d = 0, and c = 2 53 + 1. If we take all k coordinates of each vector, Proposition 1 tells us that for I = {1, 8, 9}, all the points of Ψ 3 (I) are in only two parallel planes, and this is also true for any set I that contains I. For this particular I, this gives S 3 (I) = 6.69 × 10 -19 = M 10 , and therefore M s ≤ 6.69 × 10 -19 for all s ≥ 10. This value is much smaller than the worst measure we were able to find by random search in Example 1. If we insist on taking only subsets of successive coordinates starting at 0, i.e., I = {0, 1, . . . , s -1}, we find d s = 1/3 with S s ≈ 1.009 × 10 -16 for s = 9, and d s = 1/ √ 3 with S s ≈ 2.463 × 10 -15 for s = 10, which are again very small. We checked that d s = 1/ √ 3 for s ≥ 10 up to at least s = 48. We applied the collision test in s = 16 dimensions, with d = 8, n = 4 × 10 7 , and N = 10. The expected total number of collisions was about 28 and we observed C tot = 314. This gives the p-value p ≈ 6 × 10 -206 . The birthday spacings test with s = 16, d = 16, n = 3 × 10 7 , and N = 10, gave a p-value smaller than p < 10 -300 . We also tried a collision test in s = 6 dimensions by taking only the first 3 values of each block of 8, with d = 128, n = 4 × 10 7 , and N = 10. We expected about 1,818 collisions and we observed 116,218; this gives p < 10 -300 . We see that these simple tests easily detect the bad structure.

To avoid the structure given in Proposition 1, we may skip one (or both) of the two coordinates involved in this linear relation. But Propositions 4 and 6 still apply, even if we skip the first three coordinates of each vector. Given the large value of c, the matrix A has many large entries, so one might have hoped for a good lattice structure if we skip some coordinates. But here, m = 256c -257, and Proposition 6 applies with q = 256 and r = -257.

The first part of the proposition (with j = 0) says for example that for I = {4, 5, 11, 12, 13}, Ψ s (I) is contained in at most 5q + |q + r| -1 = 1280 equidistant parallel hyperplanes at distance 1/ apart, where 2 = 7q 2 + (q + r) 2 = 458753, i.e., ≈ 677.31, for s = 5. By applying the spectral test numerically, we found that this is also the exact length s (I) of the shortest vector for this particular I (and also for I = {0, 1, . . . , 13}), and it gives S s (I) ≈ 2.386×10 -16 .

The second part of the proposition tells us that for I = {4, 5, 6, 11, 12, 13, 14}, the points of Ψ s (I) are also all covered by another family of equidistant parallel hyperplanes at distance 1/ apart, where 2 = 5q 2 + r 2 + (q + r) 2 = 393730, i.e., ≈ 627.48, in s = 7 dimensions. This is also the exact length s (I) of the shortest vector for this I. The corresponding normalized figure of merit is S s (I) ≈ 2.022 × 10 -16 , again a much smaller value than the worst we could find in Example 1.


J Christian Attiogbé
email: christian.attiogbe@univ-nantes.fr

Building Correct SDN Components from a Global Event-B Formal Model

Keywords: SDN, Correct Design, Event-B, Refinement, Decomposition

  L'archive ouverte pluridisciplinaire

Introduction

An essential constituent of distributed applications is the physical network behind them. Distributed applications very often, build on existing middlewares which embody services provided by the network level. Thus the reliability of distributed applications depends not only on their own development but also on the reliability of the network. Due to the involvment of many physical devices, the network level has been for many years a source of severe complexities and constraints leading very often to the adoption of rigid solutions in the deployment of applications.

Fighting the lack of flexibility of physical networks has resulted in the Software-Defined Networking (SDN) initiative [START_REF] Kreutz | Software-Defined Networking: A Comprehensive Survey[END_REF][START_REF][END_REF][START_REF]Software-Defined Networking: The New Norm for Networks[END_REF]. Software-Defined Networking now provides the opportunity to go deeper in modelling and reasonning on networks, since it enables to define and manage more easily the networks at software level. Indeed a Software-Defined Network is made of a controller and switches which are abstractly defined before being implemented at software level. In this context an user application does not consider a physical network or a specific middleware but it is rather built on top of a virtual or open network.

Even if Software-Defined networking makes it possible to control an entire network with software, through programs that tailor network behavior to suit specific applications and environments, programmers still have many difficulties to write correct SDN programs. This is due to the unpredictability of the SDN as a distributed asynchronous system, and the lack of correctly developped SDN frameworks or formally verified SDN frameworks. Many works have been undertaken around SDN; they address different aspects: building simulators and analysers for SDN, building SDN controllers, verifying the controller component of an Software-Defined Network, etc.

However SDN deployment is still at its beginning and programmers or administrators still need trustworthy materials and frameworks. Such materials may come from rigorously founded models and related reasonning and engineering tools. Besides, considering the keen and the demands for the deployment of SDN as a flexible infrastructure for specific applications, clouds applications, IoT, etc, which all require security, it is of tremendous importance to have at the disposal of developpers trustworthy development, analysis and simulation frameworks. Formal models taking into account several of these aspects are then necessary. That is the challenges that motivates of our work.

The main contributions of this paper are: i) capturing the SDN as a discreteevent system to foster its modelling with an event-based approach; ii) a statebased core model for rigorous analysis, development and simulation frameworks dedicated to SDN applications. It is a global Event-B [START_REF] Attiogbé | Modeling in Event-B: System and Software Engineering[END_REF] formal model, designed as the basis of the stepwise construction of the various components of a SDN; iii) the systematic derivation of correct components (SDN controller and switches) from the global model which is previously proved to have some required properties.

The article is organised as follows. Section 2 gives an overview of the Software-Defined Networking, related works and main issues. In Section 3 we introduce the main concepts for modelling SDN, an overview of Event-B method and then our approach to build the global abstract model by stepwise refinements. Section 4 shows how one can derive the construction of a correct SDN controller from the global formal model. Section 5 gives the first experimental results related to simulation and verification of global safety/liveness properties. We conclude in Section 6 and stress some challenges for future work.

Overview of SDN: Concepts and Architecture

The SDN architecture consists of three layers: User-application, Control and Data forwarding. Control and Data are the most relevant ones when studying the SDN. Figure 1 depicts how the SDN is viewed from the user side as a single global switch which denotes an abstraction of an entire network. User applications can directly exploit an abstraction of the network. Network services are solicited directly from host machines linked to a physical device: a switch assumed to be under the SDN control. In Software-Defined Networking there is a physical separation between the control-plane (the management of the network and definition of rules to forward data packets) and the data-plane (how packets are forwarded according to control-plane) [START_REF][END_REF][START_REF] Kreutz | Software-Defined Networking: A Comprehensive Survey[END_REF]. Indeed the network control (the high level or controlplane) is now separated from the packet forwarding (the low level or data-plane) activity and, physical devices inside the low level may be designed more easily; the network control is independent from device providers, the control is brought closer to software controllers and administrators. Traditional network services such as routing, access control, traffic engineering, security, etc can be implemented via various API provided by the SDN, instead of being vendordependent. The control and data levels are linked by an open communication interface. OpenFlow [START_REF] Foundation | OpenFlow Switch Specification[END_REF][START_REF]Software-Defined Networking: The New Norm for Networks[END_REF] is representative of such communication interfaces. OpenFlow is a standard communication interface, that moves the control of the network from the physical switches to logically centralized control software.

SDN has been used in variety of implementations, for example [START_REF] Mahmud | Exploitation of openflow in wireless sensor networks[END_REF] is dedicated to the implementation of wireless networks, while in [START_REF] Al-Shaer | FlowChecker: Configuration Analysis and Verification of Federated Openflow Infrastructures[END_REF] the authors describe a tool, FlowChecker, which identifies any intra-switch misconfiguration within a FlowTable of a switch. RouteFlow [START_REF] Rothenberg | When open source meets network control planes[END_REF] is a controller which implements virtualized IP routing over OpenFlow infrastructure.

Concepts and Components

We distinguish in Figure 2, the main components of an SDN. Switches and controller are network devices that interact using packets and messages on data channel and message channel.

Switch.

A switch is a device responsible of forwarding packets, to perform a hopby-hop transfer of information through the network. A switch is configurable by the controller with which it interacts with the controller via a secure message channel. A switch interacts with other switches via a data channel. Controller. A controller is a device responsible of controlling a whole network (a local or medium area network). It is used by the network administrator to dynamically configure, in an evolutive way, the switches with adequate forwarding information; it maintains the connectivity of the switches, etc. The controller initiates the switches behaviour, maintains them and instructs the switches with respect to specific actions. Packets not treated by the switches are sent to the controller via messages emitted on the secure channel. The controller does not use the data channel.

Packet. A packet contains information related to various protocols (Ethernet, IP, etc). A packet has a header related to Data, Networkand layers and a body. Inside the header we have for instance: the destination and source addresses for each layer, the type of protocol, ...

Message.

A message contains a control or management information addressed by the controller to a switch. The control information is for instance: which packet to drop, the indication of a port on which the switch may forward a data packet. A switch can also emit a message to a controller. In this case either the message contains a response to a control order (for instance the controller asked for the status of a switch) or a packet for which the switch does not have an entry in its table for forwarding the packet to its destination. Flow Table . A flow table is a part of a switch. It describes the switch elementary behaviour. A flow table is made of several entries sent by the controller. Each entry has a header information and a body. The header may contain a message priority set by the controller. The body of the message can be a data packet, or a rule to process the incoming packets.

Interaction between switches and controller. A properly configured switch has routes to forward received packets coming from other network services. If the switch lacks of forwarding information, it sends the received packets to the controller. The controller is linked to the available switches and manages them directly with orders sent via messages on a secure reliable channel. These messages are used to configure and maintain the switches, defining for each one the rules to forward packets it receives. At this stage we have a simple interaction between application level, and the provided high level network services. But this interaction is more complex if we look at it in details. Consider for this purpose a detailed view of the interaction with the SDN network depicted by Figure 2.

OpenFlow: a Standard Interface

OpenFlow is a standard communications interface, supported by the Open Network Foundation [START_REF] Foundation | OpenFlow Switch Specification[END_REF][START_REF][END_REF][START_REF]Software-Defined Networking: The New Norm for Networks[END_REF]. OpenFlow has been precisely defined but not formally.

As such, OpenFlow provides a means for specifying data level or control-plane logic and also protocols. However there is no mandatory formal specification or formal requirements; accordingly the network systems resulting from OpenFlow may be incorrect or not satisfying safety conditions.

The OpenFlow semantics being unformal, tool builders may assume particular behaviour and functioning for the network devices, leading to inconsistencies and incorrect behaviours; that is the case for the order in which packets are processed inside a switch.

Issues and Related Works

There is a keen for SDN, justifying several works both from industry and academy. Important efforts are devoted to the implementation of SDN [START_REF] Rothenberg | When open source meets network control planes[END_REF][START_REF] Mahmud | Exploitation of openflow in wireless sensor networks[END_REF][START_REF] Raza | A Comparison of Software Defined Network (SDN) Implementation Strategies[END_REF]. SDN provides flexible network systems and distributed systems development but there is no guarantee that these systems are safe or correct. SDN as an asynchronous system undergoes the impact of time passing and non-determinism or concurrency of events. Packets may be received and distributed in any order causing for instance inconsistent interpretation in the switches when a forwarding route arrives after the related packet is sent. One of the main issues in SDN is the inconsistent packet forwarding during a network update which results in an update inconsistency [START_REF] El-Hassany | Sdnracer: Concurrency analysis for software-defined networks[END_REF]. Update consistency requires that packets are either forwarded by an old version of the forwarding table or by the new version of the table (after an update), but not by an interleaving of the old and the new version.

These issues require efforts to build robust tools and protocols on the basis of thoroughly studied SDN models. Several works have been devoted to various aspects of SDN among which the modelling and reasoning on the SDN controller [START_REF] Guha | Machine-verified Network Controllers[END_REF], the analysis of the SDN traffic [START_REF] El-Hassany | Sdnracer: Concurrency analysis for software-defined networks[END_REF][START_REF] Khurshid | VeriFlow: Verifying Network-wide Invariants in Real Time[END_REF].

According to the state of the art [START_REF] Kreutz | Software-Defined Networking: A Comprehensive Survey[END_REF][START_REF] Horvath | A Literature Review on Challenges and Effects of Software Defined Networking[END_REF][START_REF] Akhunzada | Secure and dependable software defined networks[END_REF][START_REF] Alsmadi | Security of Software Defined Networks: A survey[END_REF] most investigations address the implementation issue as an important challenge; some of the aspects taken into account in these works are: scalability, performance, security, simulation. The correction of the implementations has received less attention.

In [START_REF] Hu | FLOWGUARD: Building Robust Firewalls for Software-defined Networks[END_REF] the authors address the challenge of building robust firewalls for protecting OpenFlow-based networks where network states and traffic are frequently changed. They propose the FlowGuard framework for the detection and the resolution of firewall policy violation. They use an algorithmic approach.

VeriFlow is a verification tool proposed in [START_REF] Khurshid | VeriFlow: Verifying Network-wide Invariants in Real Time[END_REF] for checking in real-time network invariants and policy correctness in OpenFlow networks. This work is based on direct implementation of the forwarding rules and an algorithmic approach, that monitors the update events occurring on the network.

SDNRacer [START_REF] El-Hassany | Sdnracer: Concurrency analysis for software-defined networks[END_REF] is a network analyzer which can ensure that a network is free of harmful errors such as data races or per-packet inconsistencies. The authors provide a formal semantics enriched with a happens-before model, to capture when events can happen concurrently.

The work in [START_REF] Guha | Machine-verified Network Controllers[END_REF] is devoted to the verification of an SDN controller; the authors provide an operational model for OpenFlow and formalize it in the Coq proof assistant. This model is then used to develop a verified compiler and a run-time system for a high-level network programming language.

To sum up, there is the preliminary steps towards making SDN networks more reliable; but much works remain to be done:

making it easier for developers the construction and verification of controllers from various existing well-researched models, enhancing machine-assisted configuration of controllers and OpenFlow-based switches, promoting the reuse of correct SDN components in the deployment of new SDN (that is interoperability).

The goal of our work is to serve these purposes by contributing with a global, extensible, refinable formal model. It is the first event-based one, making it easy to derive simulators and also to prove safety and liveness properties. It is provided as a reusable formal basis for any one interested, avoiding hence to repeat the efforts through the chains of works.

Unlike in the case dedicated to implementations, we follow an approach similar to those addressing modelling and reasoning on controllers, by defining for the SDN a global formal model from which the models of the components can be derived and then correctly implemented.

Stepwise Refinement-based Modelling of SDN

We use Event-B [START_REF] Attiogbé | Modeling in Event-B: System and Software Engineering[END_REF] and adopt a correct-by-construction approach.

An overview of Event-B

Event-B [START_REF] Attiogbé | Modeling in Event-B: System and Software Engineering[END_REF][START_REF] Hoang | Developing topology discovery in Event[END_REF] is a modelling and development method where components are modelled as abstract machines which are composed and refined into concrete machines. An abstract machine describes a mathematical model of a system behaviour 1 . In an Event-B modelling process, abstract machines constitute the dynamic part whereas Contexts are used to describe the static part. A Context is seen by machines. It is made of carrier sets and constants. It may contain properties (defined on the sets and constants), axioms and theorems. A machine is described, using named clauses, by a state space made of typed variables and invariants, together with several event descriptions.

State Space of a Machine

The variables constrained by the invariant (typing predicate, properties) describe the state space of a machine. The change from one state to the other is due to the effect of the events of the machine. Specific properties required by the model may be included in the invariant. The predicate I(x) denotes the invariant of machine, with x the state variables.

Events of an Abstract Machine Within Event-B, an event is the description of a system transition. Events are spontaneous and show the way a system evolves. An event e is modelled as a guarded substitution: e = eG =⇒ eB where eG is the event guard and eB is the event body or action. An event may occur only when its guard holds. The action of an event describes, with simultaneous generalised substitutions, how the system state evolves when this event occurs: disjoint state variables are updated simultaneously.

The effect of events are modelled with generalised logical substitution (S) using the global variables and constants. For instance a basic substitution x := e is logically equivalent to the predicate x' such that x' = e. This is symbolically written x : (x = e) where x corresponds to the state variable x after the substitution and e is an expression. In the rest of the paper, the variable x is generalised to the list of state variables.

Several events may have their guards held simultaneously; in this case, only one of them occurs. The system makes internally a nondeterministic choice. If no guard is true the abstract system is blocking (deadlock).

In Event-B Proof Obligations are defined to establish model consistency via invariant preservation. Specific properties (included in the invariant) of a system are also proved in the same way.

Refinement. An important feature of the Event-B method is the availability of refinement technique to design concrete system from its abstract model by stepwise enrichment of the abstract model. During the refinement process new variables (y) are introduced; the invariant is strengthened without breaking the abstract invariant, and finally the events guards are strengthened. In the invariant J(x, y) of the refinement, abstract variables (x) and concrete variables (y) are linked. The refinement is accompanied with proof obligations in order to prove their correctness with respect to the abstract model. Rodin Tool. Rodin2 is an open tool dedicated to building and reasoning on B models, using mainly provers and the ProB model-checker. Rodin is made of several modules (plug-ins) to work with B models and interact with related tools.

Abstractions for SDN Modelling

An SDN is made of a controller linked with several devices, which are the switches. The controller are linked to the switches via a secure message channel which conveys message flows between the controller and the switches. The switches are interconnected via a data channel which conveys data packets. Consequently, the elementary abstractions are the basic sets that represent: the switches (SW ID), the packets (PACKET), the messages (MESG), the packet headers (HEADER), the states of a switch (SW STATE). The messages have types and may contain packets:

mesgT ype ∈ M ESG → M ESGT Y P E, mesgP k ∈ M ESG → P ACKET .
A packet has several headers (MAC source address, MAC destination address, MAC type, IP source address, IP destination address, IP protocol, transport source port, transport destination port), for simplification we consider only one of such header: pHeader i ∈ P ACKET → HEADER. In the model these headers are specified like the function pHeader i . All the previous sets and constants are gathered in a CONTEXT, seen my a MACHINE which contains the variables and the previous typing predicate and properties respecrively in a VARIABLES and INVARIANT clauses.

The SDN is a set of components that work concurrently in an asynchronous manner; we build a first global abstract model that simulates the functioning of this asynchronous system. The global abstract model will be the basis for the development of the components.

To structure this abstract model, we consider the data model and the discretisation of the behaviour (a set of observed events) of each of its components as a family of events. This is important for mastering the interaction between components and the forthcoming decomposition of the model.

Switches.

Each switch has a flow table which contains the elementary behaviour of the switch according to the packets entering the switch. The behaviour of a switch is as follows: when it receives a message from the controller, it analyses the information inside the message and accordingly performs the instructions of the controller, for example updating its table, delivering a packet to a given port indicated in the message, dropping a packet or buffering a packet contained in the message. When a switch receives a packet from another switch, either it forwards the packet to another switch according to the rules in its current table, or it forwards the packet to the controller if there is no rule matching the packet headers. Accordingly, we have a set of switches: switches ⊆ SW ID.

Each switch has:

a flow table which may be empty or made of several entries: f lowT able ∈ EN T RY → switches.

Each entry has several headers (similar as for packets); each one is specified as follows: eHeader i ∈ EN T RY → HEADER dom(eHeader i ) = dom(f lowT able) a status: swStatus ∈ SW ID → SW ST AT E ∧ dom(swStatus) = switches a buffer swIncomingM sg containing all messages received by the switches:

swIncomingM sg ⊆ M ESG × switches a buffer swIP k for all packet received by a switch, before treatment: swIP k ∈ P ACKET ↔ switches; swIncomingP k is the set of packets such that swIncomingP k ⊆ P ACKET and swIncomingP k = dom(swIP k).

Each packet has a header: pHeader i ∈ P ACKET → HEADER a buffer swOM sg that contains messages to be sent to the controller: swOM sg ∈ M ESG ↔ switches; swOutgoingM sg is a set of messages such that swOutgoingM sg ⊆ M ESG ∧ swOutgoingM sg = dom(swOM sg) a buffer swOP k containing all packets to be sent to other switches or to the controller: swOP k ∈ P ACKET ↔ switches and swOutgoingP k the set of packets such that swOutgoingP k ⊆ P ACKET ∧ swOutgoingP k = dom(swOP k).

Behaviour of the switch. We capture the behaviour of the switch by considering how it is involved in the interaction with its environment. Each impact of the environment is considered as an event. The (re)actions of the switch are modelled as events that in turn impact or not the environment. We have then a set of events characterizing the switches; they are as follows.

sw rcv machingPkt: the condition for the occurrence of this event is that there is in the incoming packets of a switch sw, a packet pkt, received from another switch via the data channel ((pkt → sw) ∈ dataChan), which header (ahd = pHeader1(pkt)) is matched with one entry of the flow table of sw: (∃ee.(((ee ∈ EN T RY ) ∧ (ee ∈ dom(f lowT able))) ∧ (eHeader1(ee) = ahd))) ; the effect of the event is that the packet should be forwarded to another switch: swIP k := swIP k ∪ {pkt} sw rcv unmachingPkt: its occurs when a switch receives a packet (from another switch) which header does not match any entry of the flow table. sw sndPk2ctrl: occurs when a switch emits a message containing an unmached packet to the controller; sw sendPckt2sw: a switch sends a packet to another switch via the data channel; sw newFTentry: the occurrence of this event expresses that a new entry is added to the flow table.

• • •

Controller. A controller is the device that administrates the switches using control messages. It has buffers which contain messages or packets to be sent/received to/from switches: a buffer for incoming packets (ctlIncomingP k ⊆ P ACKET ); a buffer for outgoing packets (ctlOutgoingP k ⊆ P ACKET ).

The controller emits/receives messages on/from the secure channel. These messages contain either data packets or instructions to control the switches. Among the control message we have: the Add order to add an new entry into the table flow of a switch; Modf to modify an entry into the table flow of a switch; Del to delete an entry into the table flow of a switch.

Behaviour of the controller. As for the switch, the behaviour of the controller is captured and modelled as a set of events denoting how the controller interacts with its environment. Each impact of the environment is considered as an event; the (re)actions of the controller are modelled as events that in turn impact or not the environment.

As illustration, among the events of the controller we have the following:

ctl emitPkt: this event occurs when the controller emits to a switch sw, through a message, one of its pending packets; the condition for this occurrence is that there is some pending packets in the dedicated buffer (pkt ∈ ctlOutgoingP k).

The effect of the event is that a message containing the packet is added to the secure channel: secureChan := secureChan ∪ {msg → sw} and the buffer is updated: ctlOutgoingP k := ctlOutgoingP k\{pkt}. Figure 3 gives the Event-B specification of the event; all the remaining events are specified in a similar way. ctl rcvPacketIn: this event occurs when the controller receives a packet from a switch which previously received it but does not have an entry matching it. ctl askBarrier: the occurrence of this event specifies when the controller asks for a barrier; that means the controller orders the switch to perform some control with urgency and to send a barrier acknowledgement.

event ctl emitPkt // the controller emits a mesg conveying a packet any sw pkt msg where /* the guard */ sw ∈ switches // in destination to one of the switches pkt ∈ P ACKET pkt ∈ ctlOutgoingP k // one of the packet to be sent on the sw msg ∈ M ESG // a given message to convey the packet (msg → P KOut) ∈ mesgT ype // a packet of type OUT (msg → pkt) ∈ mesgP k // the message contains the packet then /* the substitution */ secureChan := secureChan ∪ {msg → sw} //emission on the channel ctlOutgoingP k := ctlOutgoingP k \ {pkt} end The global abstract model comprises in an EVENT clause, all the events characterizing the switches and the controller; the occurrence of each event is due to some conditions of the SDN and this occurrence has effect on the SDN. In Event-B a guard captures each condition; an Event-B substitution describes the effect of the event.

Interaction between Controller and Switches. The interaction is based on communications via channels; we distinguish a data packet channel and a control message channel. The channels are modelled with sets. A switch or a controller writes/reads messages on/from the channels according to their behaviour.

secureChan ⊆ M ESG × switches dataChan ⊆ P ACKET × switches A first abstract Event-B model is obtained by gathering all these abstractions on data and behaviour.

Model Construction Strategy: the Refinements

Despite the general development strategy in Event-B which consists to build an abstract global model of a system and then to use several refinements to make it precise, it is still challenging to determine the refinement steps according to the problem at hand. In this work we have considered as one of our targets, the main components of the SDN. That is, we tried to deal with details related to the targeted components (switches, controller). The questions are: what characterizes the switches and what are the impacts on their environments? what characterizes the controller behaviour and what are the impacts on its environments? By answering these questions we went out by introducing, for instance, that switches use various ports and they receive/emit messages on ports. Consequently the first abstract model of channels is impacted and then refined.

We focus on the architecture of the SDN, and then tried to list the details that will support actually the achievement of the network services. We have listed, the detailed structure of packets, the structure of messages, the fine-grained processing of packets inside the switches. Then we order these details and tried to handle them one by one. It follows that we have to detail in the refinements: the structure of packets with various headers and body parts; the structure of messages, and accordingly the refinement of the abstract channels; the behaviour of the events that specify the behaviour of both switches and controller. This guided us to master the gradual modelling. From the methodological point of view this is a recipe for Event-B adepts.

We also follow the basic recommendations of Event-B to consider small steps of refinement at time. Table 1 gives an overview of the refinement chains.

GblModel0

The first abstract model; all the events are specified at a high level; for instance we do not have yet information on ports, etc GblModel0 1 Refinement. Ports and headers are introduced in the state space thus refined; the related events are refined. GblModel0 2 Refinement. Priorities are introduced in the state space; messages are sent from the controller with a priority in their header. GblModel0 3 Refinement. The events guard are refined according to priority rules Table 1. The refinement steps

Data Refinement

The set of ports (PORTID ACTION) are introduced as data refinement details in the GblModel0 1 refined abstract model. Packets are sent on ports according to the actions defined in the entries of the flow table. One port (also called action) may be the destination of a set of packets. An entry may specify several actions or ports. The various fields in SDN packets are also introduced as data refinement with the functions: macSrc, macDst, IpSrc, IpDst, IpP roto, T pSrc, T pDst, T pSrcP t, T pDstP t.

actionsQueues ∈ ACT ION → P(P ACKET ) // packets targeting a port actions ∈ EN T RY → P(ACT ION ) // ports concerned by an entry dom(actions) = dom(f lowT able) // all entries have target ports

Behavioural Refinement

Explicit priority The controller (via a human administrator) can introduce priorities as an information contained in the messages. Priorities are comparable, they are numbers. Consequently, we introduced this refinement level where the messages are refined by adding to them a field which represents their priority. In Event-B, this is a function giving the priority of each message: msgP riority ∈ M ESG → M SG P RIORIT Y where M SG P Y is the set of priorities (a subset of naturals). Accordingly, the event ctl emitPkt for instance, is now refined in the model (GblModel0 2); its substitution sets the priority of the message which is sent.

Implicit priority We introduced implicit priorities via a partial order on messages to be sent; in the sequel the symbol ≺ denotes this partial order.

To avoid inconsistencies in the behaviour of switches, the messages they sent should be reordered. In practice, when for instance the flow table is modified by an instruction coming from the controller, the outgoing packet in a switch may be forwarded in a wrong destination due to the modification. Besides, the controller can use the barrier to impose a quick modification.

Accordingly the modification messages coming from the switch should have less priority compared with the the forwarding messages. A priority rule which reorder the events, is that: the add control messages are processed after the forwarding of all data packets. The involved events in the model are: sw newFTentry, sw sendPckt2sw, sw sendPckt2Ctrl. Therefore we have the following ordering: sw newFTentry ≺ sw sendPckt2sw sw sndPk2ctrl ≺ sw sendPckt2sw sw sndPk2ctrl ≺ sw newFTentry As far as the Del order is concerned, as lost packets in the network can be claimed, we use this hypothesis to consider that the Del order has priority on the forward packet. For the Add order, this does not present an inconsistency risk for outgoing packets. For this reason the Add order can be processed in any order. Barrier messages coming from the controller are the most priority ones. Unmatched packets to be returned to the controller are less priority than the packet to be forwarded to other switches: a rule is that packets to the controller are sent if there is no packet to be forwarded to other switches.

These priorities have been implemented (in GblModel0 3) as a refinement of our model. The guards of the involved events have been strengthen with this rules.

Deriving Correct Controller and Switch Components

The purpose is to derive SDN components from the global model resulting from the chain of refinements; such derivation is enabled with Event-B via the use of model decomposition techniques: the Abrial'style decomposition (called the Astyle decomposition) [START_REF] Abrial | Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B[END_REF] based on shared variables, and the Butler'style decomposition (called the B-style decomposition) [START_REF] Butler | Decomposition Structures for Event-B[END_REF][START_REF] Silva | Shared Event Composition/Decomposition in Event-B[END_REF] based on shared events. In the A-style decomposition, which we have used, events are first partitioned between Event-B sub-components and then, shared variables of these sub-components, but only modified by a sub-component, are used to introduce some external events in the sub-components which do not modify the variables. These external events simulate the behaviour of the events which modify the variables, in the components where the variables are not modified. To avoid inconsistency, external events should not be refined. In the B-style decomposition, variables are first partitioned between the sub-components and then shared events (which use the variables of both sub-components) are split between the sub-components according to the used variables. We used the A-style decomposition because it is more relevant when we consider that the events describe the behaviour of each specific component (controller, switch) of the SDN.

Decomposition into a controller and switches

According to our modelling approach (see Section 3.2) where events are gathered by family, it is straightforward to list the events that describe the behaviour of the controller in order to separate them from the events related to the switches. The controller component is made of all the events, already introduced as such and prefixed with ctrl, which simulate the behaviour of the controller (see Section 3.2): ctl emitPkt, ctl rcvPacketIn, ctl askBarrier, etc. Formally, the decomposition is as if a model M Σ composed of components S σ1 and C σ2 , such that M Σ P , is split into submodels C σ1 and S σ2 such that C σ1 P and S σ2 P , with Σ = σ 1 ∪ σ 2 the alphabet of M Σ and σ 1 (resp. sigma 2 ) the alphabet of C σ1 (resp. S σ2 ).

We experimented with the decomposition plugin of the Rodin toolkit using the A-Style decomposition approach.

A challenging issue here is the question of partitioning a set of identical behaviours; for instance if we would like to decompose the behaviours of the switches as a partition. This question is out of the scope of the existing decomposition techniques because of the non-determinism of data and event modelling.

Experimentations and Assessment

The global abstract model has been incrementally worked out by combining invariant verification, refinements and simulation. This is done with the Rodin platform 3 . In Table 2 we give the statistics (on proof obligations) of the performed proofs on the abstract model and its refinements; they were mostly automatically discharged by the Rodin prover. The complete model is available at http: //pagesperso.ls2n.fr/ ~attiogbe-c/mespages/nabla/sdn/SDN-WP2.pdf

Elt Name

Total Auto Manual Undischarged

SDN-WP2 210 202 8 0 GlModel0 97 94 3 0 GlModel0 1 63 59 4 0 GlModel0 1 1 2 2 0 0 GblModel0 2 2 2 0 0 GblModel0 3 0 0 0 0 Table 2. Proof statistics
The model of the last refinement level has been decomposed into a controller component and switches which preserve all the proved properties. One benefit of deriving components from a global formal model is the ability to study required properties involving the components and their environment. We have illustrated this study with a few properties expected from SDN. Both safety and liveness properties have been considered. This can be extended to other specific properties, following a similar approach.

We have expressed and proved several global properties on the model before its decomposition into components. For instance: The data packets received by any switch are sent by the controller or by the other switches.

Proof. Assume ctlSentP kts be the set of packets sent by the controller; we have to prove that ∀sw.(sw : switches ⇒ swIP s[{sw}] ⊆ ctlSentP ks). If swIncomingP ks is the union of the buffers of the switches, then it suffices to establish that swIncomingP ks ⊆ ctlSentP kts.

Several such safety properties (e.g. Table 3) have been proved on the model.

SPa Any packet in the data channel was sent by the controller or the switches SP b Any packet in the switches buffers was sent by the controller or the switches SPc The packets sent via the message channel are contained in ctl sentP kts Table 3. Proof statistics Similarly, liveness properties study is undertaken using stepwise checking of basic properties. For instance, we prove that, the data packets generated by the controller, are finally emitted by this later. The formula LP deliv (see Table 4) expresses this property. Literally it describes that after the occurrence of the event ctl havePacket we will fatally (F) observe the occurrence of ctl emitPkt. The other formula in Table 4 are similar; the X symbol stands for the next operator. Event-B provides, via the ProB tool integrated in the Rodin, the facilities to state and prove liveness properties. ProB supports LTL, its extension LTL[e] and CTL properties with the standard modal and temporal operators. Table 4. A few liveness properties in LTL/ProB

Conclusion

We have shown how to build correct controller and switches components from the refinement of a global formal model of an SDN system, using the decomposition of the global model into the target components. The global model was first built by a systematic construction using refinements. The construction of the abstract model itself was achieved so as to be reusable as a recipe for Event-B developers, following the steps we had identified. We overcame the challenging modelling in Event-B, of an SDN system, viewing it as a discrete events system, and thus as an interaction between its main components. We evaluated our model and components for their conformance to the properties required for SDN systems. We experimented the various aspect related to property proving and simulation, usig the Rodin tool. As far as we know, among the related work using formal approaches, this study is the first one proposing an event-based appoach for studying SDN systems. We provided a core event-based model to found frameworks dedicated to the development, analysis and simulation of SDN-based applications.

As future work, instead of a one-shot derivation of a specific code for the contoller, we are investigating a parametric environment to enable the construction of specific controllers targeting various languages. The same idea is relevant for the switches. In light-weight distributed applications requiering the deployment of adhoc SDN, it is desirable to build various specific SDN switches from a single abstract model. Consequently a process of generic refinement to codes, will be beneficial.

Fig. 1 .

 1 Fig. 1. The layered architecture of a SDN

Fig. 2 .

 2 Fig. 2. A detailed architecture

Fig. 3 .

 3 Fig. 3. Event-B specification of the event ctl emitPkt

  LPOKstatuse(ctl askStatusMsg) ⇒ F(e(ctl rcvStatus)) LP deliv e(ctl havePacket) ⇒ F(e(ctl emitPkt)) LP OKM ach e(ctl emitPkt) ⇒ X(e(sw rcv machingPkt))

A system behaviour is a discrete transition system

http://wiki.event-b.org/index.php/Main Page

http://wiki.event-b.org/index.php