Thierry Klein

Agnès Lagnoux

Pierre Petit

Large deviation results for triangular arrays of semiexponential random variables

Keywords: large deviations, triangular arrays, semiexponential distribution, Weibull-like distribution, Gärtner-Ellis theorem, contraction principle, truncated random variable. AMS subject classification: 60F10, 60G50

 derived deviation results at logarithmic scale with shorter proofs relying on classical tools of large deviation theory and expliciting the rate function at the transition. In this paper, we exhibit the same asymptotic behaviour for triangular arrays of semiexponentially distributed random variables, no more supposed absolutely continuous.

Introduction

Moderate and large deviations of the sum of independent and identically distributed (i.i.d.) real-valued random variables have been investigated since the beginning of the 20th century. Kinchin [START_REF] Kinchin | Über einer neuen Grenzwertsatz der Wahrscheinlichkeitsrechnung[END_REF] in 1929 was the first to give a result on large deviations of the sum of i.i.d. Bernoulli distributed random variables. In 1933, Smirnov [START_REF] Smirnov | On the probabilities of large deviations[END_REF] improved this result and in 1938 Cramér [START_REF] Cramér | Sur un nouveau théorème-limite de la théorie des probabilités[END_REF] gave a generalization to sums of i.i.d. random variables satisfying the eponymous Cramér's condition which requires the Laplace transform of the common distribution of the random variables to be finite in a neighborhood of zero. Cramér's result was extended by Feller [START_REF] Feller | Generalization of a probability limit theorem of Cramér[END_REF] to sequences of non identically distributed bounded random variables. A strengthening of Feller's result was given by Petrov in [START_REF] Petrov | Generalization of Cramér's limit theorem[END_REF][START_REF] Petrov | Large deviations for sums of independent non identically distributed random variables[END_REF] for non identically distributed random variables. When Cramér's condition does not hold, an early result is due to Linnik [START_REF] Linnik | On the probability of large deviations for the sums of independent variables[END_REF] in 1961 and concerns polynomial-tailed random variables. The case where the tail decreases faster than all power functions (but not enough for Cramér's condition to be satisfied) has been considered by Petrov [START_REF] Petrov | Generalization of Cramér's limit theorem[END_REF] and by S.V. Nagaev [START_REF] Nagaev | An integral limit theorem for large deviations[END_REF]. In [START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF], A.V. Nagaev studied the case where the commom distribution of the i.i.d. random variables is absolutely continuous with respect to the Lebesgue measure with density p(t) ∼ e -|t| 1-as |t| tends to infinity, with ∈ (0, 1). He distinguished five exact-asymptotics results corresponding to five types of deviation speeds. In [START_REF] Borovkov | Large deviation probabilities for random walks with semiexponential distributions[END_REF][START_REF] Borovkov | Asymptotic analysis of random walks[END_REF], Borovkov investigated exact asymptotics of the deviations probability for random variables with semiexponential distribution, also called Weibull-like distribution, i.e. with a tail writing as e -t 1-L (t) , where ∈ (0, 1) and L is a suitably slowly varying function at infinity. In [START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF], the authors consider the following setting. Let ∈ (0, 1) and let X be a real-valued random variable with a density p with respect to the Lebesgue measure verifying: p(x) ∼ e -x 1-, as x → +∞.

(

) 1
and ∃γ ∈ (0, 1]

ρ := E[|X| 2+γ ] < ∞. (2)
For all n ∈ N * , let X 1 , X 2 , ..., X n be i.i.d. copies of X and set S n = X 1 + • • • + X n and P n (x) = P(S n x). According to the asymptotics of x n , three logarithmic asymptotic ranges then appear. In the sequel, the notation x n y n (resp. x n y n , x n y n , and

x n = Θ(y n )) means that y n /x n → 0 (resp. x n /y n → 0, lim sup |x n /y n | < ∞, and y n x n y n ) as n → ∞. Maximal jump range [4, Theorem 1] When x n n 1/(1+ ) , log P n (x n ) ∼ log P(max(X 1 , . . . , X n ) x n ). Gaussian range [4, Theorem 2] When x n n 1/(1+ ) , log P n (x n ) ∼ log(1 -φ(n -1/2 x n )),
φ being the cumulative distribution function of the standard Gaussian law.

Transition [START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF]Theorem 3] The case x n = Θ(n 1/(1+ ) ) appears to be an interpolation between the Gaussian range and the maximal jump one.

In the present paper, we exhibit the same asymptotic behaviour for triangular arrays of random variables (Y n,i ) 1 i Nn satisfying the following weaker assumption: there exists q > 0 such that, if

y n → ∞, log P(Y n y n ) ∼ -qy 1-ε n , (3)
together with similar assumptions on the moments.

The first main contribution of this paper is the generalization of [START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF] to triangular arrays. Such a setting appears naturally in some combinatorial problems, such as those presented by [START_REF] Janson | Asymptotic distribution for the cost of linear probing hashing[END_REF], including hashing with linear probing. Since the eighty's, laws of large numbers have been established for triangular arrays (see, e.g., [START_REF] Gut | Complete convergence for arrays[END_REF][START_REF] Gut | The weak law of large numbers for arrays[END_REF][START_REF] Hu | Strong laws of large numbers for arrays of rowwise independent random variables[END_REF]). Lindeberg's condition is standard for the central limit theorem to hold for triangular arrays (see, e.g., [START_REF] Billingsley | Convergence of probability measures[END_REF]Theorem 27.2]). Dealing with triangular arrays of light-tailed random variables, Gärtner-Ellis theorem provides moderate and large deviation results. Deviations for sums of heavy-tailed i.i.d. random variables are studied by several authors (e.g., [START_REF] Borovkov | Large deviation probabilities for random walks with semiexponential distributions[END_REF][START_REF] Borovkov | Asymptotic analysis of random walks[END_REF][START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF][START_REF] Linnik | On the probability of large deviations for the sums of independent variables[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Large deviations of sums of independent random variables[END_REF][START_REF] Petrov | Generalization of Cramér's limit theorem[END_REF]) and a good survey can be found in [START_REF] Mikosch | Large deviations of heavy-tailed sums with applications in insurance[END_REF]. Here, we focus on the particular case of semiexponential tails (treated in [START_REF] Borovkov | Large deviation probabilities for random walks with semiexponential distributions[END_REF][START_REF] Borovkov | Asymptotic analysis of random walks[END_REF][START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF] for sums of i.i.d. random variables) generalizing the results to triangular arrays. See [START_REF] Klein | Deviation results for hashing with linear probing[END_REF] for an application to hashing with linear probing. Another contribution is the fact that the random variables are not supposed absolutely continuous as in [START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF]. Assumption (3) is analogue to that of [START_REF] Borovkov | Large deviation probabilities for random walks with semiexponential distributions[END_REF][START_REF] Borovkov | Asymptotic analysis of random walks[END_REF], but there the transition at x n = Θ(n 1/(1+ ) ) is not considered. Hence, up to our knowledge, Theorem 3 is the first large deviation result at the transition which is explicit.

The paper is organized as follows. In Section 2, we state the main results, the proofs of which can be found in Section 3. In Section 4, a discussion on the assumptions is proposed. Section 5 is devoted to the study of the model of a truncated random variable which is a natural model of triangular array. This kind of model appears in many proofs of large deviations. Indeed, when one wants to deal with a random variable, the Laplace transform of which is not finite, a classical approach consists in truncating the random variable and in letting the truncation going to infinity. In this model, we exhibit various rate functions, especially nonconvex rate functions.

Main results

For all n 1, let Y n be a centered real-valued random variable, let N n be a natural number, and let (Y n,i ) 1 i Nn be a family of i.i.d. random variables distributed as Y n . Define, for all k ∈ 1, N n ,

T n,k := k i=1 Y n,i .
To lighten notation, let T n := T n,Nn .

Theorem 1 (Maximal jump range). Let ε ∈ (0, 1), q > 0, and α > (1 + ε) -1 . Assume that:

(H1) for all N αε n y n N α n , log P(Y n y n ) ∼ -qy 1-ε n ; (H2) E[Y 2 n ] = o(N α(1+ε)-1 n ).
Then, for all y 0,

lim n→∞ 1 N α(1-ε) n log P(T n N α n y) = -qy 1-ε .
As in [START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF][START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF][START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF], the proof of Theorem 1 immediately adapts to show that, if

x n N (1+ε) -1 n , if, for all x ε n y n x n (1 + δ) for some δ > 0, log P(Y n y n ) ∼ -qy 1-ε n , and if Var(Y n ) = o(x (1+ε) n /N n ), then log P(T n x n ) ∼ -qx 1-ε n .
In this paper (see also Theorems 2 and 3), we have chosen to explicit the deviations in terms of powers of N n , as it is now standard in large deviation theory.

In addition, the proof of Theorem 1 immediately adapts to show that, if L is a slowly varying function such that, for all

N αε n /L(N α n ) y n N α n , log P(Y n y n ) ∼ -L(y n )y 1-ε n
and if assumption (H2) holds, then, for all y 0,

lim n→∞ 1 L(N α n )N α(1-ε) n log P(T n N α n y) = -y 1-ε .
The same is true for Theorem 2 below whereas Theorem 3 below requires additional assumptions on L to take into account the regularly varying tail assumption.

Moreover, if an analogous assumption as (H1) for the left tail of Y n is also satisfied, then T n satisfies a large deviation principle at speed N α (1-ε) n with rate function -q |y| 1-ε (the same remark applies to Theorems 2 and 3).

Theorem 2 (Gaussian range). Let ε ∈ (0, 1), q > 0, and 1/2 < α < (1 + ε) -1 . Suppose that (H1) holds together with:

(H2') E[Y 2 n ] → σ 2 ; (H2+) there exists γ ∈ (0, 1] such that E[|Y n | 2+γ ] = o(N γ(1-α) n ).
Then, for all y 0,

lim n→∞ 1 N 2α-1 n log P(T n N α n y) = - y 2 2σ 2 .
Theorem 3 (Transition). Let ε ∈ (0, 1), q > 0, and α = (1 + ε) -1 . Suppose that (H1), (H2'), and (H2+) hold. Then, for all y 0,

lim n→∞ 1 N (1-ε)/(1+ε) n log P(T n N 1/(1+ε) n y) = -inf 0 θ 1 qθ 1-ε y 1-ε + (1 -θ) 2 y 2 2σ 2 =: -I(y). (4)
Let us explicit a little the rate function

I. Let f (θ) = qθ 1-ε y 1-ε + (1 -θ) 2 y 2 /(2σ 2
). An easy computation shows that, if y y 1+ε) , f is increasing and its minimum y 2 /(2σ 2 ) is attained at θ = 0. If y > y 0 , f has two local minima, at 0 and at θ(y): the latter corresponds to the greatest of the two roots in [0, 1] of f (t) = 0, equation equivalent to

0 := ((1 -ε 2 )(1 + 1/ε) ε qσ 2 ) 1/(
(1 -θ)θ = (1 -ε)qσ 2 y 1+ε . ( 5
) If y 0 < y y 1 := (1 + ε) (qσ 2 /(2ε) ε ) 1 1+ε , then f (θ(y)) f (0). And if y > y 1 , f (θ(y)) < f (0). As a consequence, for all y 0, I(y) =    y 2 2σ 2 if y y 1 qθ(y) 1-ε y 1-ε + (1-θ(y)) 2 y 2 2σ 2 if y > y 1 .

Proofs

Proof of Theorem 1 (Maximal jump regime)

Let us fix y > 0. The result for y = 0 follows by monotony. First, we define

P(T n N α n y) = P(T n N α n y, ∀i ∈ 1, N n Y n,i < N α n y) + P(T n N α n y, ∃i ∈ 1, N n Y n,i N α n y) =: P n,0 + R n,0 . ( 6
)
Lemma 4. Under (H1) and (H2), for α > 1/2 and y > 0,

lim n→∞ 1 N α(1-ε) n log R n,0 = -qy 1-ε . Proof of Lemma 4. Using (H1), lim sup n→∞ 1 N α(1-ε) n log R n,0 lim n→∞ 1 N α(1-ε) n log(N n P(Y n N α n y)) = -qy 1-ε . ( 7
)
Let us prove the converse inequality. Let δ > 0. We have,

R n,0 P (T n N α n y, Y n,1 N α n y) P (T n,Nn-1 -N α n δ) P(Y n N α n (y + δ)).
By Chebyshev's inequality, observe that

P(T n,Nn-1 -N n α δ) 1 - Var(Y n ) N 2α-1 n δ 2 → 1,
using (H2). Finally, by (H1), one gets

lim inf n→∞ 1 N α(1-ε) n log R n,0 lim n→∞ 1 N α(1-ε) n log P(Y n N α n (y + δ)) = -q(y + δ) 1-ε .
We conclude by letting δ → 0.

To complete the proof of Theorem 1, it remains to prove that, for α >

(1 + ε) -1 , lim sup n→∞ 1 N α(1-ε) n log P n,0 -qy 1-ε , ( 8
)
and to apply the principle of the largest term (see, e.g., [6, Lemma 1.2.15]). Let q ∈ (0, q).

Using the fact that 1 x 0 e x , we get

P n,0 e -q (N α n y) 1-ε E e q (N α n y) ε Yn 1 Yn<N α n y Nn . If we prove that E e q (N α n y) ε Yn 1 Yn<N α n y 1 + o(N α(1-ε)-1 n ), then log P n,0 -q (N α n y) 1-ε + o(N α(1-ε) n )
and the conclusion follows by letting q → q. Write

E e q (N α n y) ε Yn 1 Yn<N α n y = E e q (N α n y) ε Yn 1 Yn<(N α n y) ε + E e q (N α n y) ε Yn 1 (N α n y) ε Yn<N α n y .
First, by a Taylor expansion and (H2), we get

E e q (N α n y) ε Yn 1 Yn<(N α n y) ε E 1 + q (N α n y) ε Y n + (q ) 2 e q 2(N α n y) 2ε Y 2 n 1 Yn<(N α n y) ε 1 + (q ) 2 e q 2 • E[Y 2 n ] (N α n y) 2ε = 1 + o(N α(1-ε)-1 n ).
To bound above the second expectation, we need the following simple consequence of (H1). Lemma 5. Under (H1), for all y > 0,

∀q < q ∃n 0 ∀n n 0 ∀u ∈ [(N α n y) ε , N α n y] log P(Y n u) -q u 1-ε .
Proof of Lemma 5. By contrapposition, if the conclusion of the lemma is false, we can construct a sequence (u n ) n 1 such that, for all n 1,

u n ∈ [(N α n y) ε , N α n y] and log P(Y n u n ) > -q u 1-ε n , whence (H1) is not satisfied.
Now, integrating by parts, we get

E e q (N α n y) ε Yn 1 (N α n y) ε Yn<N α n y = N α n y (N α n y) ε e q (N α n y) ε u P(Y n ∈ du) = -e q (N α n y) ε u P(Y n u) N α n y (N α n y) ε + q (N α n y) ε N α n y (N α n y) ε e q (N α n y) ε u P(Y n u)du e q P(Y n (N α n y) ε ) + q (N α n y) ε N α n y (N α n y) ε e q (N α n y) ε u-q u 1-ε du (1 + q (N α n y) 1-ε )e q -q (N α n y) ε(1-ε) = o(N α(1-ε)-1 n )
for n large enough, using (H1) and Lemma 5 with q ∈ (q , q), and the supremum of

u → q (N α n y) -ε u -q u 1-ε over [(N α n y) ε , N α n y].
The proof of Theorem 1 is now complete.

Proof of Theorem 2 (Gaussian regime)

Let us fix y > 0. The result for y = 0 follows by monotony. For all m ∈ 0, N n , we define

Π l,m (x) = P T n,l x, ∀i ∈ 1, l -m Y n,i < (N α n y) ε , ∀i ∈ l -m + 1, l (N α n y) ε Y n,i < N α n y ,
and we denote Π Nn,m (N α n y) by Π n,m , so that

P n = P n,0 + R n,0 = Nn m=0 N n m Π n,m + R n,0 . (9)
By Lemma 4 and the fact that, for α >

(1 + ε) -1 , 2α -1 > α(1 -ε), we get lim n→∞ 1 N 2α-1 n log R n,0 = -∞. ( 10
)
Lemma 6. Under (H1), (H2'), and (H2+), for 1/2 < α (1 + ε) -1 and y > 0,

lim n→∞ 1 N 2α-1 n log Π n,0 = - y 2 2σ 2 . ( 11
)
Proof of Lemma 6. For all n 1, we introduce the variable

Y < n distributed as L(Y n | Y n < (N α n y) ε ). Let T < n = Nn i=1 Y < n,i
where the Y < n,i are independent random variables distributed as

Y < n . Then Π n,0 = P(T < n N α n y)P(Y n < (N α n y) ε ) Nn .
On the one hand, P(Y n < (N α n y) ε ) Nn → 1 by (H1). On the other hand, in order to apply the unilateral version of Gärtner-Ellis theorem (see [START_REF] Plachky | A theorem about probabilities of large deviations with an application to queuing theory[END_REF], and [START_REF] Brosset | Probabilistic proofs of large deviation results for sums semiexponential random variables and explicit rate function at the transition[END_REF] for a modern formulation), we compute, for u 0,

Λ n (u) = N 2(1-α) n log E e u N 1-α n Y < n .
Now, there exists a constant c > 0 such that, for all t uy ε , |e t -

(1 + t + t 2 /2)| c |t| 2+γ , whence e u N 1-α n Y < n -1 - u N 1-α n Y < n - u 2 2N 2(1-α) n (Y < n ) 2 cu 2+γ N (2+γ)(1-α) n |Y < n | 2+γ , ( 12
)
by the definition of Y < n and α(1

+ ε) 1. Now, E e u N 1-α n Y < n -e u 2 σ 2 2N 2(1-α) n E e u N 1-α n Y < n -E 1 + u N 1-α n Y < n + u 2 2N 2(1-α) n (Y < n ) 2 + E 1 + u N 1-α n Y < n + u 2 2N 2(1-α) n (Y < n ) 2 -e u 2 σ 2 2N 2(1-α) n . ( 13
)
The first term of ( 13) is bounded above by

cu 2+γ N (2+γ)(1-α) n E[|Y < n | 2+γ ] = o(N -2(1-α) n ), (14)
by assumptions (H1) and (H2+), and an integration by parts. Using a Taylor expansion of order 2 of the exponential function, the second term of ( 13) is equal to

u N 1-α n E[Y < n ] + u 2 2N 2(1-α) n (E[(Y < n ) 2 ] -σ 2 ) + o(N -2(1-α n ) . ( 15
)
By (H1) and the fact that

E[Y n ] = 0, E[Y < n ] is exponentially decreasing, whence E[Y < n ] = o(1/N 1-α n )
; similarly, by (H1), (H2'), and (H2+), E[(Y < n ) 2 ] → σ 2 ; hence, we get

Λ n (u) = u 2 σ 2 2 + o(1),
and the proof of Lemma 6 is complete.

Theorem 2 stems from ( 10), [START_REF] Janson | Asymptotic distribution for the cost of linear probing hashing[END_REF] and the fact that, for 1/2

< α < (1 + ε) -1 , lim sup n→∞ 1 N 2α-1 n log Nn m=1 N n m Π n,m - y 2 2σ 2 , ( 16
)
the proof of which is given now. We adapt the proof in [17, Lemma 5] and focus on the logarithmic scale. Let

m n = N α(1-ε) 2 2y (1-ε) 2 n .
In particular, for all m > m n ,

m(N α n y) ε(1-ε) m(N α n y) ε(1-ε) 2 + (N α n y) 1-ε . ( 17
)
Lemma 7. Under (H1), for α > 1/2, y > 0, and q < q, lim sup

n→∞ 1 N α(1-ε) n log Nn m=mn+1 N n m Π n,m -q y 1-ε .
Proof. For n large enough, using Lemma 5 and inequality [START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations Into Account When Cramér's Condition Does Not Hold[END_REF],

Nn m=mn+1 N n m Π n,m Nn m=mn+1 N n m P(∀i ∈ 1, m Y n,i (N α n y) ε ) Nn m=mn+1 N n m e -mq (N α n y) ε(1-ε) e -q (N α n y) 1-ε Nn m=mn+1 N n m e -mq (N α n y) ε(1-ε) /2 e -q (N α n y) 1-ε 1 + e -q (N α n y) ε(1-ε) /2 Nn .
Here, as α(1 -ε) > 2α -1, we conclude that

lim n→∞ 1 N 2α-1 n log Nn m=mn+1 N n m Π n,m = -∞. (18)
Now, for m ∈ 1, m n , let us bound above Π n,m . Let us define

f m (u 1 , . . . , u m ) := Π Nn-m,0 N α n y - m i=1 u i ,
which is nondecreasing in each variable. For q < q < q and n large enough,

Π n,m = P(T n N α n y , (N α n y) ε Y n,1 , . . . , Y n,m < N α n y , Y n,m+1 , . . . , Y n,n < (N α n y) ε ) = [(N α n y) ε ,N α n y] m f m (u 1 , . . . , u m ) dP Yn (u 1 ) • • • dP Yn (u m ) = (k 1 ,...,km) i (k i -1,k i ] f m (u 1 , . . . , u m ) dP Yn (u 1 ) • • • dP Yn (u m ) (k 1 ,...,km) f m (k 1 , . . . , k m ) i P(Y n ∈ (k i -1, k i ]) (k 1 ,...,km) f m (k 1 , . . . , k m )e -q m i=1 (k i -1) 1-ε [(N α n y) ε ,N α n y+2] m f m (u 1 , . . . , u m ) e -q m i=1 u 1-ε i du 1 • • • du m = I 1,m + I 2,m ,
where, for j ∈ {1, 2},

I j,m := A j,m f m (u 1 , . . . , u m ) e -q sm(u 1 ,...,um) du 1 • • • du m ( 19
)
with

A 1,m := (u 1 , . . . , u m ) ∈ [(N α n y) ε , N α n y + 2] m m i=1 u i N α n y , A 2,m := (u 1 , . . . , u m ) ∈ [(N α n y) ε , N α n y + 2] m m i=1 u i < N α n y ,
and

s m (u 1 , . . . , u m ) := m i=1 u 1-ε i . Lemma 8. For α > 1/2 and y > 0, lim sup n→∞ 1 N α(1-ε) n log mn m=1 N n m I 1,m -q y 1-ε .
Proof. Since s m is concave, s m reaches its minimum on A 1,m at the points with all coordinates equal to (N α n y) ε except one equal to N α n y -(N α n y) ε (m -1). Moreover, using the fact that f m (u 1 , . . . , u m ) 1 in [START_REF] Nagaev | Large deviations of sums of independent random variables[END_REF], it follows that, for n large enough, for all m ∈ {1, . . . , m n },

I 1,m (N α n y) m e -q (m-1)(N α n y) ε(1-ε) -q (N α n y-(m-1)(N α n y) ε ) 1-ε (N α n y) m e -q (N α n y) 1-ε e -q (m-1)((N α n y) ε(1-ε) -1) .
Finally,

mn m=1 N n m I 1,m e -q (N α n y) 1-ε mn m=1 N n m (N α n y) m e -q (m-1)((N α n y) ε(1-ε) -1) e -q (N α n y) 1-ε N 1+α n y mn m=1 N 1+α n ye -q ((N α n y) ε(1-ε) -1) m-1
, and the conclusion follows, since the latter sum is bounded.

As

α(1 -ε) > 2α -1, we conclude that lim n→∞ 1 N 2α-1 n log mn m=1 N n m I 1,m = -∞. ( 20
)
Lemma 9. Under (H2') and (H2+), for 1/2 < α (1 + ε) -1 , y > 0, n large enough, and m ∈ {1, . . . , m n },

I 2,m (N α n y) m e -q (m-1)(N α n y) ε(1-ε) exp sup m(N α n y) ε u<N α n y φ m (u)
where

φ m (u) := - (N α n y -u) 2 2σ 2 (N n -m)(1 + c n ) -q (u -(m -1)(N α n y) ε ) 1-ε .
Proof. Here, we use Chebyshev's exponential inequality to control

f m (u 1 , . . . , u m ) = Π Nn-m,0 (N α n y- u 1 -• • • -u m ) in I 2,m
. For all l ∈ N * , for all x ∈ R, and for all λ 0, Π l,0 (x) exp -λx + l log E e λYn 1 Yn (N α n y) ε . Let M > y/σ 2 . There exists c > 0 such that, for all s M , we have e s 1 + s + s 2 /2 + c|s| 2+γ . Hence, as soon as

λ M/N 1-α n M/N α n , E e λYn 1 Yn (N α n y) ε 1 + λ 2 2 E[Y 2 n ] + cλ 2+γ E[|Y n | 2+γ ] 1 + λ 2 σ 2 2 (1 + c n ), ( 21
)
where

c n := E[Y 2 n ] -σ 2 + 2cM γ σ 2 N -γ(1-α) n E[|Y n | 2+γ ] = o(1),
by (H2') and (H2+). Thus, for

λ M/N 1-α n , Π Nn-m,0 (N α n y -u) exp -λ(N α n y -u) + (N n -m) λ 2 σ 2 2 (1 + c n ) .
For n large enough and m ∈ {1, . . . , m n }, the infimum in λ of the last expression is attained at

λ * := N α n y -u (N n -m)σ 2 (1 + c n ) M N 1-α n , and is equal to -(N α n y -u) 2 /(2σ 2 (N n -m)(1 + c n ))
. So, for n large enough:

Π Nn-m,0 (N α n y -u) exp - (N α n y -u) 2 2σ 2 (N n -m)(1 + c n ) . ( 22
)
Since s m is concave, s m reaches its minimum on

A 2,m,u := (u 1 , . . . , u m ) ∈ [(N α n y) ε , N α n y + 2] m m i=1 u i = u
at the points with all coordinates equal to (N α n y) ε except one equal to u -(m -1)(N α n y) ε , whence, for n large enough and m ∈ {1, . . . , m n },

I 2,m (N α n y) m sup m(N α n y) ε u<N α n y exp - (N α n y -u) 2 2σ 2 (N n -m)(1 + c n ) -q (u -(m -1)(N α n y) ε ) 1-ε -q (m -1)(N α n y) ε(1-ε) (N α n y) m e -q (m-1)(N α n y) ε(1-ε) exp sup m(N α n y) ε u<N α n y φ m (u) . Now, for 1/2 < α < (1 + ε) -1 , n large enough, and m ∈ {1, . . . , m n }, the function φ m is decreasing on [m(N α n y) ε , N α n y). So, I 2,m (N α n y) m exp -q m(N α n y) ε(1-ε) - (N α n y -m n (N α n y) ε ) 2 2N n σ 2 (1 + c n ) . It follows that mn m=1 N n m I 2,m e - (N α n y-mn(N α n y) ε ) 2 2Nnσ 2 (1+cn) mn m=1 N 1+α n ye -q (N α n y) ε(1-ε) m .
Since the latter sum is bounded, we get lim sup

n→∞ 1 N 2α-1 n log mn m=1 N n m I 2,m - y 2 2σ 2 (23)
as m n (N α n y) ε = o(N α n ) and c n = o [START_REF] Billingsley | Convergence of probability measures[END_REF]. By ( 18), [START_REF] Petrov | Generalization of Cramér's limit theorem[END_REF], and (23), we get the required result. Remark 10. Notice that, using the contraction principle, one can show that, for all fixed m, lim sup

n→∞ 1 N (1-ε)/(1+ε) n log Π n,m = - y 2 2σ 2 .

Proof of Theorem 3 (Transition)

Here, we assume (H1), (H2'), and (H2+), and we deal with the case α

= (1 + ε) -1 , so that α(1 -ε) = 2α -1 = (1 -ε)/(1+ ε).
Let us fix y > 0. The result for y = 0 follows by monotony. We still consider the decomposition [START_REF] Gut | The weak law of large numbers for arrays[END_REF]. By Lemmas 4 and 6, and the very definition of I in (4), we have

lim n→∞ 1 N (1-ε)/(1+ε) n log R n,0 = -qy 1-ε -I(y) and lim n→∞ 1 N (1-ε)/(1+ε) n log Π n,0 = - y 2 2σ 2 -I(y).
To complete the proof of Theorem 3, it remains to prove that lim inf

n→∞ 1 N (1-ε)/(1+ε) n log Π n,1 -I(y) (24)
lim sup

n→∞ 1 N (1-ε)/(1+ε) n log Nn m=1 Π n,m -I(y) (25)
and to apply the principle of the largest term.

Proof of (24). For all t ∈ (0, 1), 1

N (1-ε)/(1+ε) n log Π n,1 1 N (1-ε)/(1+ε) n log P T n,Nn-1 N α n ty, ∀i ∈ 1, N n -1 Y n,i < (N α n y) ε + 1 N (1-ε)/(1+ε) n log P N α n (1 -t)y Y n,Nn < N α n y ---→ n→∞ - t 2 y 2 2σ 2 -q(1 -t) 1-ε y 1-ε ,
by Lemma 6 and by (H1). Optimizing in t ∈ (0, 1) provides the conclusion.

Proof of (25). We follow the same lines as in the proof of [START_REF] Nagaev | Integral Limit Theorems Taking Large Deviations into Account when Cramér's Condition Does Not Hold[END_REF]. By Lemma 7, letting q → q, we get lim sup

n→∞ 1 N (1-ε)/(1+ε) n log Nn m=mn+1 N n m Π n,m -qy 1-ε -I(y). (26)
Let η = 1 -q /q ∈ (0, 1). By Lemma 8, lim sup

n→∞ 1 N (1-ε)/(1+ε) n log mn m=1 N n m I 1,m -q y 1-ε -(1 -η)I(y). ( 27
)
Now, recall that Lemma 9 provides I 2,m (N α n y) m e -q (m-1)(N α n y) ε(1-ε) e Mn , for n large enough, where

M n = sup m(N α n y) ε u<N α n y - (N α n y -u) 2 2σ 2 (N n -m)(1 + c n ) -q (u -(m -1)(N α n y) ε ) 1-ε N (1-ε)/(1+ε) n sup m(N α n y) -1+ε θ<1 - (1 -θ) 2 y 2 2σ 2 (1 + c n ) -q θ 1-ε y 1-ε 1 - (m -1)(N α n y) -1+ε θ 1-ε .
For n large enough, for all m ∈ {1, . . . , m n },

inf m(N α n y) -1+ε θ<η    (1 -θ) 2 y 2 2σ 2 (1 + c n ) + q θ 1-1 - (m -1)(N α n y) -1+ε θ 1-    (1 -η) 2 y 2 2σ 2 (1 -η) (1 -η) 3 I(y) and inf η θ<1    (1 -θ) 2 y 2 2σ 2 (1 + c n ) + q θ 1-1 - (m -1)(N α n y) -1+ε θ 1-    inf η θ<1 (1 -θ) 2 y 2 2σ 2 + q θ 1-y 1-ε (1 -η) (1 -η) 2 I(y). So M n -N (1-ε)/(1+ε) n (1 -η) 3 I(y) and lim sup n→∞ 1 N (1-ε)/(1+ε) n log mn m=1 n m I 2,m -(1 -η) 3 I(y) + lim sup n→∞ 1 N (1-ε)/(1+ε) n log mn m=1 n m N α n ye -q (N α n y) ε(1-ε) m = -(1 -η) 3 I(y). ( 28
)
Transition 2 When α = β, for all y 0,

lim n→∞ 1 N α(1-ε) n log P(T n N α n y) = -I 2 (y) := -q y/c c 1-ε + (y -y/c c) 1-ε .
Here, as in all cases where α β, we adapt the definitions ( 6) and ( 9) as:

P(T n N α n y) = P(T n N α n y, ∀i ∈ 1, N n Y n,i < N β n c) =: P n,0 (29)
(R n,0 = 0) and, for all m ∈ 0, N n ,

Π n,m = P T n N α n y, ∀i ∈ 1, N n -m Y n,i < (N β n c) ε , ∀i ∈ N n -m + 1, N n (N β n c) ε Y n,i < N β n c . ( 30
)
For all t > 0,

Π n,0 = P(T n N α n y, ∀i ∈ 1, N n Y n,i < (N α n c) ε ) e -tyN α(1-ε) n E e tN -αε n Yn 1 Yn<(N α n c) ε Nn = e -tyN α(1-ε) n (1+o(1)) ,
(see the proof of Theorem 1), whence Lemma 6 with L(Y

< n ) = L(Y n | Y n < N α n c) updates into 1 N α(1-ε) n log Π n,0 ---→ n→∞ -∞.
So, by the contraction principle, for all fixed m 0,

1 N α(1-ε) n log Π n,m ---→ n→∞    -∞
if m y/c -1 -q ( y/c c 1-ε + (y -y/c c) 1-ε ) otherwise, that provides a minoration of the sum of the Π n,m 's. To obtain a majoration, let us introduce

m n = N α(1-ε) 2 n 2k
where k = y/c c 1-ε + (y -y/c c) 1-ε . Lemma 7 remains unchanged while Lemmas 8 and 9 requires adjustments. The integration domains defining I 1,m and I 2,m become

A 1,m = (u 1 , . . . , u m ) ∈ [(N α n c) ε , N α n c + 2] m m i=1 u i N α n y , A 2,m = (u 1 , . . . , u m ) ∈ [(N α n c) ε , N α n c + 2] m m i=1 u i < N α n y ,
Further, the concave function s m attains its minimum at points with all coordinates equal to (N α n c) ε except y/c n coordinates equal to N α n c n and one coordinate equal to

N α n (y -y/c n c n )- (N α n c) ε (m -1 -y/c n ) with c n = c + 2N -α n .
Then following the same lines as in the proof of Lemmas 8 and 9, we get, for j ∈ {1, 2},

lim n→∞ 1 N 2α-1 n log mn m=1 N n m I j,m = -q y/c c 1-ε + (y -y/c c) 1-ε .
Truncated maximal jump range When β < α < β + 1 and y 0, or α = β + 1 and y < c, the proof of Theorem 1 adapts and provides

lim n→∞ 1 N α-βε n log P(T n N α n y) = -qyc -ε .
As in the previous case, we use the decomposition given by ( 29) and (30). To upper bound P n,0 , we write

P n,0 e -qyc -ε N α-βε n E e yc -ε N -βε n Yn 1 Yn<(N β n c) ε + 1 (N β n c) ε Yn<N β n c
Nn and follow the same lines as in the proof of Theorem 1. To lower bound P n,0 , we write, for c < c,

log P n,0 log P(∀i ∈ 1, N α-β n y/c Y n,i N β n c ) ∼ -N α-β n y(c ) -1 q(N β n c ) 1-ε = -N α-βε n qy(c ) -ε ,
and we recover the upper bound, when c → c.

Trivial case When α = β + 1 and y c, or α > β + 1, we obviously have P(T n N α n y) = 0.

Case

β < (1 + ε) -1
Here, Theorem 2 applies for α < (1 + ε) -1 . The notable fact is that the Gaussian range is extended: it spreads until α < 1 -βε.

Gaussian range When α < 1 -βε, the proof of Theorem 2 adapts and, for all y 0, lim

n→∞ 1 N 2α-1 n log P(T n N α n y) = - y 2 2σ 2 .
As we said, the result for α < (1 + ε) -1 is a consequence of Theorem 2. Now, suppose α (1 + ε) -1 > β. We use the decomposition given by ( 29) and (30). Lemma 6 works for α

< 1 -βε, with L(Y < n ) = L(Y n | Y n < (N β n c) ε ). Then, we choose m n = N α-2βε+βε 2 n 2yc -ε . We obtain the equivalent of Lemma 7: lim sup n→∞ 1 N α-βε n log Nn m=mn+1 N n m Π n,m -q yc -ε . with N α-βε n N 2α-1 n
. Finally, Lemmas 8 and 9 adapt as well, with

A 1,m = (u 1 , . . . , u m ) ∈ (N β n c) ε , N β n c + 2 m m i=1 u i N α n y , A 2,m = (u 1 , . . . , u m ) ∈ (N β n c) ε , N β n c + 2 m m i=1 u i < N α n y .
Transition 3 When α = 1 -βε, the proof of Theorem 3 adapts and, for all y 0,

lim n→∞ 1 N 1-2βε n log P(T n N 1-βε n y) = -I 3 (y) := -inf 0 t 1 q(1 -t)yc -ε + t 2 y 2 2σ 2 = -    y 2 2σ 2 if y y 3 qy c ε -q 2 σ 2 2c 2ε
if y > y 3

with y 3 := qσ 2 c -ε .

Figure 1 :

 1 Figure1: Representation of the rate functions. Here, q = 1, σ 2 = 2, = 1/2, and c = 1. Left -Gaussian range. The typical event corresponds to the case where all the random variables are small but their sum has a Gaussian contribution. Center -Maximal jump range. The typical event corresponds to the case where one random variable contributes to the total sum (N α n y), no matter the others. We recover the random variable tail. Right -Truncated maximal jump range. The typical event corresponds to the case where N α-β n y/c variables take the saturation value N β n c, no matter the others.

Figure 2 :

 2 Figure 2: Representation of the rate functions. Here, q = 1, σ 2 = 2, = 1/2, and c = 1. Left -Transition 1. The typical event corresponds to the case where one random variable is large (N α n θ(y)y) and the sum of the others has a Gaussian contribution (two competing terms). Center -Transition 2. The typical event corresponds to the case where y/c random variables take the saturation value N β n c and one completes to get the total sum. Right -Transition 3. The typical event corresponds to the case where some random variables (a number of order N 1-β(1+ε) n ) take the saturation value N β n c, and the sum of the others has a Gaussian contribution (two competing terms).

Figure 3 : 0 α 1 / 2 ( 1 +

 30121 Figure 3: Representation of the rate functions. Here, q = 1, σ 2 = 2, = 1/2, and c = 1. Left -Transition 1-for c c 0 . The typical event corresponds to the case where k 3 (c) variables take the saturation value N β c, and the sum of the others has a Gaussian contribution. Right -Transition 1-for c c 0 . The typical event corresponds to the case where k 2 (c) variables take the saturation value N β c, one is also large (N β n θ(y -k 2 (c)c)(y -k 2 (c)c)) and the sum of the others has a Gaussian contribution.

T r a n s i t i o n 2 I 2 T r a n s i t i o n 3 I 3 Figure 4 :

 22334 Figure 4: Rate function transition diagram.

Π n,m -(1 -η) 3 I(y), and (25) follows, letting q → q, i.e. η → 0.

Remark 11. Notice that, using the contraction principle, one can show that, for all fixed m, lim sup

About the assumptions

Looking into the proof of Theorem 1, one can see that assumption (H1) can be weakened and one may only assume the two conditions that follow.

Theorem 12. The conclusion of Theorem 1 holds under (H2) and:

Lemma 13. (H1a) is equivalent to:

First extract a convergent subsequence; then, again extract a subsequence such that N -α n y n is convergent and use (H1a) to show that N -α(1-ε)

Lemma 14. (H1b) is equivalent to the conclusion of Lemma 5:

(H1b') ∀y > 0 ∀q < q ∃n 0 ∀n n 0 ∀u ∈ [(N α n y) ε , N α n y] log P(Y n u) -q u 1-ε . Proof. See the proof of Lemma 5.

Theorem 15. The conclusion of Theorem 1 holds under assumptions (H1a), (H1b), and

Proof. The only modification in the proof is the minoration of R n,0 : R n,0 P(T n,Nn-1 0)P(Y n N α n y). Now Lyapunov's theorem [START_REF] Billingsley | Convergence of probability measures[END_REF]Theorem 27.3] applies and provides P(T n,Nn-1 0) → 1/2.

As for Theorem 2, assumption (H1) can be weakened and one may only assume (H1b), or even the following weaker assumption.

Theorem 16. The conclusion of Theorem 2 holds under (H2'), (H2+), and: Theorem 3, assumption (H1) can be weakened and one may only assume (H1a) and (H1b).

Application: truncated random variable

Let us consider a centered real-valued random variable Y , admitting a finite moment of order 2 + γ for some γ > 0. Set

). Such truncated random variables naturally appear in proofs of large deviation results.

If Y has a light-tailed distribution, i.e. Λ Y (λ) := log E[e λY ] < ∞ for some λ > 0, then (the unilateral version of) Gärtner-Ellis theorem applies:

Note that we recover the same asymptotics as for the non truncated random variable Y . In other words, the truncation does not impact the deviation behaviour.

Now we consider the case where log P(Y y) ∼ -qy 1-ε for some q > 0 and ε ∈ (0, 1). In this case, Gärtner-Ellis theorem does not apply since all the rate functions are not convex as usual (as can be seen in Figures 1 to 3). Observe that, as soon as y n → ∞,

] are exponentially decreasing to zero. Therefore, our theorems directly apply for α < max(β, (1 + ε) -1 ), and even for α = (1 + ε) -1 < β. For α max(β, (1 + ε) -1 ), the proofs easily adapt to cover all cases. To expose the results, we separate the three cases β > (1 + ε) -1 , β < (1 + ε) -1 and β = (1 + ε) -1 and provide a synthetic diagram at the end of the section (page 18) and the graphs of the exhibited rate functions (pages 17 and 18).

Case β > (1 + ε) -1

Gaussian range When α < (1 + ) -1 , Theorem 2 applies and, for all y 0,

Transition 1 When α = (1 + ) -1 , Theorem 3 applies and, for all y 0,

Maximal jump range When (1 + ) -1 < α < β, Theorem 1 applies and, for all y 0,

Truncated maximal jump range When 1 -βε < α < 1 + β and y 0, or α = 1 + β and y < c, as before, the proof of Theorem 1 adapts and

Trivial case When α = β + 1 and y c, or α > β + 1, we obviously have P(T n N α n y) = 0.

Case β

Gaussian range When α < (1 + ε) -1 = β, Theorem 2 applies and, for all y 0, lim

Transition T 0 As in Section 2 after the statement of Theorem 3, we define θ(y) and y 1 for the function f (θ) = qθ 1-ε y 1-ε + (1 -θ) 2 y 2 /(2σ 2 ). Define θ(y) := 1 y y 1 θ(y) and notice that θ is increasing on [y 1 , ∞) (and θ(y) → 1 as y → ∞). Set c 0 := θ(y 1 )y 1 = (2εqσ 2 ) 1/(1+ε) .

• When α = (1 + ε) -1 = β and c c 0 , then

where

where Remark: For all c < c 0 , y 0,1 (c) > y 1 : so the Gaussian range in the nontruncated case (which stops at y 1 ) is extended. Moreover, y 0,1 (c 0 ) = y 1 = y 0,2 (c 0 ), and, for c = c 0 , I 0,1 = I 0,2 (since I 1 (y) = y 2 /(2σ 2 ) for y y 1 ).

Truncated maximal jump range


Kehinde G Samuel

Oumar Maïga
email: oumary.maiga@usttb.edu.ml

Mamadou K Traoré
email: mamadou-kaba.traore@u-bordeaux.fr

A DEVS-based pivotal modeling formalism and its verification and validation framework

Keywords: High Level Language for Systems Specification (HiLLS), Discrete Event System Specification (DEVS), formal verification, temporal logic, model transformation, UPPAAL

System verification is an ever-lasting system engineering challenge. The increasing complexity in system simulation requires some level of expertise in handling the idioms of logic and discrete mathematics to correctly drive a full verification process. It is recognized that visual modeling can help to fill the knowledge gap between system experts and analysis experts. However, such an approach has been used in one hand to specify the behavior of complex systems, and on the other hand to specify complex requirement properties, but not simultaneously. This paper proposes a framework that is unique in supporting a full system verification process based on the graphical modeling of both the system of interest and the requirements to be checked. Patterns are defined to transform the resulting models to formal specifications that a model checker can manipulate. A real-time crossing system is used to illustrate the proposed framework.

Introduction

The continuous growth of systems of various kinds through human activities and the increasing complexities of the activities themselves lead to the continuous development of formal techniques to ensure safe and secure systems. The evolution of a system's functional requirements is often inevitably accompanied by a corresponding evolution of its complexities in structure and behavior, hence more efforts are required to monitor this evolution process to ensure that the resulting system is reliable and safe. This may involve a combination of scientific techniques such as simulation, prototyping and formal analysis to carefully investigate the model before the implementation of the emerging system. Significant efforts and advances have been made towards making these techniques accessible individually. However, not much success has been recorded in unifying the various formalisms, thus, different models of different aspects of a system have to be treated. This is characterized by communication gaps between the different experts and consequently reduced efficiency of the entire process.

Simulation models are usually represented by different domain specific modeling languages (DSML) most of which have no precise semantic definition. The semantics of simulation models are left to model simulators and translators; these are defined by general-purpose programming languages, which is unacceptable for formal analysis [START_REF] Bryant | Challenges and Directions in Formalizing the Semantics of Modeling Languages[END_REF]. Although the syntax of some recent DSML is formally described with metamodel, generally, the lack of formal model transformations contributes to the challenges of formal analysis at the model level. It is, therefore, a challenge to describe simulation models and its requirement specification formally to improve formal verification and analysis of models.

The High-Level Language for System Specification (HiLLS) has been proposed to fill such a gap [START_REF] Aliyu | The High-Level Language for Systems Specification: A Model-Driven Approach to Systems Engineering[END_REF]. HiLLS is a scalable visual modeling language that serves as a one-stop reference point through a harmonious combination of modeling paradigms from system theory and software engineering to integrate the different aspects of a system in one coherent whole. As such, it is a pivotal visual language that allows model simulation, enactment, and formal analysis. In order to ensure these combined features, concepts have been borrowed from three formalisms that are universal, each in one of these three analysis domains, and seamlessly integrated through formalism weaving techniques, namely DEVS, UML and first-order logic. DEVS, which is recognized as a universal simulation modeling formalism [START_REF] Zeigler | Theory of Modeling and Simulation[END_REF], provides the semantic domain for HiLLS-specified models simulation. Similarly, a UML-specified pattern provides the architecture for HiLLS-specified models enactment [START_REF] Aliyu | A Framework for Discrete Event Systems Enactment[END_REF], while first-order logic is used as the semantic domain for formal verification of HiLLS-specified models [START_REF] Samuel | Formal Verification with HiLLS-Specified Models: A Further Step in Multi-Analysis Modeling of Complex Systems[END_REF].

However, while the objectives of having a highly communicable graphical concrete syntax and multiple semantic domain mappings for simulation, enactment, and accessibility to formal analysis, have been achieved, there is a major concern in making such an approach effectively and easily usable. As illustrated by Figure 1, such a concern stands for each of the analysis methods (i.e., simulation, enactment, and model checking) in that a complete framework is needed to allow users to drive a whole process from visual modeling of a system to its analysis. Indeed, while a DEVS model can be automatically derived from a HiLLS specification, the full simulation process of such a model entails the specification of additional aspects (such as the experimental frame, simulation initialization, parameter tuning, etc.). Similarly, the full enactment process of the HiLLS-derived model entails the definition of additional aspects (such as realtime concerns, human-in-the-loop interface, etc.). And so does the full formal verification process of the HiLLS-derived model. The latter is the focus of this paper, and we aim at achieving a supporting framework for such a process.

Figure 1. From pivotal visual modeling to multiple analyses of complex systems

The paper is organized as follows. Section 2 discusses related works. Section 3 presents the HiLLS formalism and its editor. Section 4 introduces patterns that will serve as the building blocks for defining HiLLS semantics in a way that it is amenable to formal checking. Section 5 extends HiLLS to the specification of system requirements and provides semantics for such an extension. Section 6 shows how both the HiLLS-based system modeling and HiLLS-based requirements specification fall within a full formal verification framework. Section 7 illustrates the application of the framework with a well-known study case. Section 8 concludes the paper, by summarizing the work done and by giving perspectives for future work.

Related Works

Related works have addressed the formal analysis of DEVS models. These proposals range from formal model-checking of sub-classes of DEVS, the transformation of DEVS into formal methods for verification purposes, generation of traces from DEVS models for testing, or introducing clock constraints to DEVS to conform to formal methods. We present some notable works in this area:

• Hong and Kim [START_REF] Hong | DEVSpecL: DEVS Specification Language for Modeling, Simulation, and Analysis of Discrete Event Systems[END_REF] proposed a method of verification of DEVS models in the DEVSim++ environment. The approach was to specify the model in DEVS and use temporal logic to specify the properties and time constraints of the system. The authors use a projection technique to reduce the state space. The lifetimes of the states are not taken into account, but the temporal logic allows expressing constraints on sequences of states. The technique used by the authors is very similar to the technique of model-checking using Buchi automata [START_REF] Büchi | On a Decision Method in Restricted Second-Order Arithmetic[END_REF]. • Zeigler et al. [START_REF] Zeigler | Combining DEVS and Model-Checking: Concepts and Tools for Integrating Simulation and Analysis[END_REF] used a subclass of DEVS models having finite sets of states, inputs, and outputs, named FD-DEVS [START_REF] Zeigler | Guide to Modeling and Simulation of Systems of Systems[END_REF] to map the system representation onto a non-deterministic automaton that is subject to model checking using the SPIN/PROMELA model checker.

• Several related works align on the principle combining DEVS with Timed Automata, and the use of the UPPAAL model checker [START_REF] Furfaro | A Development Methodology for Embedded Systems Based on RT-DEVS[END_REF][START_REF] Saadawi | Verification of Real-Time DEVS Models[END_REF][START_REF] Madlener | Verification of Dynamically Reconfigurable Embedded Systems by Model Transformation Rules[END_REF][START_REF] Maïga | An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems[END_REF].

Our work differs from all of the above in that we use a pivotal visual notation at both sides: one that has equivalent DEVS representation for system behavior and the other that has equivalent temporal logic representation for system requirements. Moreover, by building a full framework based on these visual notations, we provide a systematic verification approach, which most of the related works don't, as they require to add a suitable verification component for checking specific properties of interest.

HILLS-Based System Modeling

HiLLS can be seen as a visual language for DEVS (see in annex a brief recall of DEVS), with specific features for formal analysis and direct prototyping [START_REF] Aliyu | The High-Level Language for Systems Specification: A Model-Driven Approach to Systems Engineering[END_REF], [START_REF] Aliyu | A Framework for Discrete Event Systems Enactment[END_REF], [START_REF] Maler | From timed to hybrid systems[END_REF]. This is the point of view adopted here, although any of the two other formalisms and their underlying paradigms could be used as the entry point.

HiLLS Syntax

A template of how HiLLS represents a DEVS model is shown in Figure 2. A HiLLS-specified system is represented by an HSystem, which is denoted by a box similar to the UML class with an additional horizontal compartment and two vertical compartments. The left (respectively right) hand side vertical compartment has input (respectively output) ports attached to it. The concept of a port is defined as in DEVS. All declarations in HiLLS (whether ports or any other variables or functions) are done in first-order logic. The top horizontal compartment contains the name of the model and the declaration of its parameters. The immediate compartment below contains the declaration of state variables. The third compartment from the top contains the definitions of operations that use and manipulate all variables, including parameters and ports. Therefore, while a message received on some given input port causes a change of the internal state of the model, a call to some given modifier operation causes a change of the value of some given parameter. The bottom compartment contains the system's behavior described by the configuration transition diagram (i.e., the HiLLS automaton), an automaton in which nodes are configurations and which edges are configuration-to-configuration transitions that can occur in the system. A configuration is defined by the assignment of specific values or constraints to state variables. One can notice that the assignment of a specific value to each of the state variables gives a state in the sense of DEVS (i.e., a particular configuration), while the assignment of constraints (rather than specific values) to some or all of the state variables gives a configuration that corresponds in DEVS to a family of states (instead of a single one). As such, a configuration depicts a set of properties that several states share. Configurations are a way to cluster a DEVS state set (whether finite or not) into a finite partition [START_REF] Samuel | Formal Verification with HiLLS-Specified Models: A Further Step in Multi-Analysis Modeling of Complex Systems[END_REF]. Figure 3 shows how the syntactic elements are visually captured by graphical elements.

A configuration has three visual representations: finite, passive and transient configurations. A finite configuration (Figure 3.a) is a 4-compartments box, which respectively contains the label of the configuration, the logic specification of its properties (such as the assignment of values and constraints to state variables), its sojourn time (which corresponds in DEVS to the value of the time advance function at states falling within this configuration), and the description of activities to be carried out when the system is in this configuration (which has no equivalence in DEVS but serves for the purpose of enactment). An infinite configuration (Figure 3.b) is a configuration in which sojourn time is +∞; therefore, its visual representation is reduced to a 3-compartments box, the compartment related to sojourn time being replaced by a double line at the right-hand edge of the box. A transient configuration (Figure 3.c) is the one in which sojourn time is 0; therefore, its visual representation is reduced to a 3-compartments circle. A black circle (Figure 3.g) allows to make reference to the initial configuration of the model.

The three kinds of configuration transitions are denoted by different labeled arrows with the operations accompanying the transitions (for the update of state variables, when needed) as part of the labels. For internal transition (Figure 3.d), the value sent on the output port is also part of the label. For external transition (Figure 3.e), the label includes the triggering condition on the receipt of a value on a port and the time elapsed by the model in its current configuration. The label for confluent transition (Figure 3.f) is similar, except that there is no condition on the elapsed time (since it is known to be the sojourn time in this case). Decision nodes (Figure 3.h) can be used to define various possible routes during a transition, depending on conditions to be met by state variables.

An HClass (Figure 3.j) denotes a software component that does not represent the model of a dynamic system, as opposed to an HSystem (Figure 3.i). As such, it is a simple resource manipulated by model components and corresponds to a "regular" class in UML with attributes and methods specified by logical predicates. Both HSystem and HClass can be parameterized. The HSystem and HClass components can be linked by relationships such as aggregation, composition, generalization, and reference, with cardinalities attached to, as described by the UML metamodel (indeed HClass and HSystem are specializations of the UML Classifier mother class).

HiLLS Editor

An editor has been developed for HiLLS modeling, using the Graphical Modeling Framework (GMF) of the Eclipse IDE. As HiLLS model specification requires both graphical and textual representations, Xtext was used to capture the textual aspects of the model (such as labels, properties, and activities) and EuGENia, a plugin that overlays GMF, was used to process the geometric shapes that compose the model. The HiLLS Editor allows the drag and drop modeling of complex systems, as shown in

HiLLS-DEVS Relation

Details of the correspondence between a DEVS model and a HiLLS automaton are given in [START_REF] Samuel | Formal Verification with HiLLS-Specified Models: A Further Step in Multi-Analysis Modeling of Complex Systems[END_REF]. The idea of HiLLS automaton is that a DEVS model (whether with finite or infinite state set) can be represented graphically with a finite HiLLS automaton for the purpose of formal analysis, without any loss of behavioral property, while still being adequate for simulation and enactment. Multiple states of an atomic DEVS model are mapped onto a single configuration in the corresponding HiLLS automaton. A Coupled DEVS model is mapped onto a composed HiLLS automaton, which uses its configuration(s) to specify the coupling information between the sub-components of the corresponding DEVS model. The focus of this paper not being the HiLLS-DEVS relation, we avoid here the provision of unnecessary details and refer interested readers to [START_REF] Samuel | Formal Verification with HiLLS-Specified Models: A Further Step in Multi-Analysis Modeling of Complex Systems[END_REF] for more on that aspect. We rather focus on providing a full formal verification framework to HiLLS. However, Figure 5 shows a DEVS model (a patient) and its HiLLS counterpart. A larger illustration of the concepts introduced in this section is given through the application presented in Section 7. As the application is meant to demonstrate the entire methodology proposed in the paper, it is presented after all theoretical aspects of the methodology are introduced. However, at this stage, in order to get an illustration of HiLLS modeling on the application, the reader can get the application presentation in Section 7, and the expression of the corresponding system models in Section 7.1 (which refers to Annex D for complements). Going to Section 7's introduction and Section 7.1, and then coming back to Section 4 is a way to match Section 3 with the application and possibly improve the readability of this section, while keeping the general structure of the paper from theory and methodology to application.

DEVSPatient = X, Y, S, δint, δext, λ, ta, with X = {(in, x) / x ∈ Viruses} Y = {(out, x) / x ∈ Viruses}∪ {(status, y) / y ∈ {S, E, I, D} S = {1, 2, 3, 4, 5} × ℜ0 +∞ ta : S → ℜ0 +∞ ta(s, σ) = σ ∀ s ∈ {1, 2, 3, 4, 5} δint : S → S δint(2, σ) = (3, tINC) ∀ σ ∈ ℜ0 +∞

HiLLS-to-UPPAAL Patterns

Timed automata are among the most widely used models for the verification of real-time systems. To semantically map HiLLS to one of the formal method tools available (namely UPPAAL), we define patterns that provide building blocks to building the HiLLS formal method-based semantics. The subsequent subsections present these patterns.

Similar to matching Section 3 with the application presented in Section 7, reader can switch between subsections of Section 4 at one hand, and Section 7.1 and Annex E at the other hand, to better match the concepts introduced in Section 4 with the application.

Semantic pattern for configuration

The pattern shown in Figure 6 expresses the formal semantics of a HiLLS model in a given configuration, using a Timed Automaton (TA) composed of four types of locations, namely Ccurse, Cend, Cinterrupt and Cdilemma, and a unique clock.

In this pattern, the lifetime of a configuration C starts at Ccurse, where the property of the configuration is (e < ta) AND (mail =∅), with mail representing the input bag of the system. To overcome the fact that model checking tools often restraint on time representation as limited to integer values only, we represent a realtime value, such as e (elapsed time) and ta (time advance), as a pair of integer values (tint, tdec), where tint is the integral part of the time value, and tdec is its decimal part. That way, t = t' is translated into ((tint-t'int=0) AND (tdec-t'dec=0)), while t < t' translates to ((tint-t'int<0) OR ((tint-t'int=0) AND (tdec-t'dec<0))), with AND (respectively OR) being the conjunction (respectively disjunction) logical operator. Pairs of integer values (tint, tdec) are implemented in UPPAAL as 2D arrays, where t[0] implements tint, and t [START_REF] Bryant | Challenges and Directions in Formalizing the Semantics of Modeling Languages[END_REF] implements tdec. Such a representation of time is one of the possible forms of superdense time as introduced in [START_REF] Nutaro | Toward a Theory of Superdense Time in Simulation Models[END_REF] and brought to discrete event simulation in [START_REF] Jouault | ATL: a model transformation tool[END_REF] within a very formal framework.

When the system enters the Ccurse location, e is set to 0.0 (hence e[0] = 0, and e[1] = 0), and ta is determined by update(ta). Ccurse means that the system is in the curse of C, and no input has been received yet by the system, nor the lifetime of C has elapsed yet. The TA takes a transition from Ccurse to Cend when (e = ta) AND (mail = ∅), but if before that condition is met, a message ?x is received at elapsed time e, the TA transits to Cinterrupt(x). There are as many locations Cinterrupt(x) as the number of possible values of x that the system can receive in the C configuration. From each Cinterrupt(x), the TA will do as many external transitions as the number of possible values for e. From a theoretical point of view, there is a potential of combinatorial explosion for the number of locations of type Cinterrupt(x), as well as for the number of external transitions that can be taken from each location Cinterrupt(x). However, in practice, models have very limited number of different cases for an external transition. In any case, this aspect is intrinsically a limitation of our approach.

at the Cend location, an internal transition takes place and an output !y is sent, unless a message is received exactly at that moment, leading then to a transition to Cdilemma(X) where a confluent transition takes place and an output !y is sent. Internal, external and confluent transitions taken from any location of the C configuration lead, each to the location corresponding to the curse of another configuration. Then the same pattern applies to that new configuration, and so on. Figure 7 illustrates how the semantics of a HiLLS model is given by a TA, using the pattern. Figure 7a shows the HiLLS automaton, and Figure 7b shows how its semantics is built in TA (but only the translation for the C1 configuration is shown).

Pattern variants

From the general configuration pattern previously presented, we derive the variants presented by Figure 8.

Patterns for Hierarchical Composition

None of the patterns defined in the previous section takes care of the case of HiLLS composed automata.

In order to handle this case, we proceed as follows:

(1) A feedback loop location transition is used in UPPAAL to semantically translate the DEVS simulation protocol, according to which, when a HiLLS component sends a message, the composed model is the one to first receive that message, before it forwards it to the appropriate recipients of the message. (2) Messages are systematically labeled in UPPAAL with the name of the sender/receiver components.

That way, when a message is sent by a HiLLS component, its encapsulating HiLLS model identifies the origin of the message, and with the composition information, transforms it to be a message tagged with the name of the recipient.

The composition steps described above is illustrated in Figure 9. The interruptless passive configuration pattern corresponding to a composed HiLLS model translates into a single location in UPPAAL, in conformance with the pattern of Figure 8e. Assuming this composed model has a component named sender (therefore, all messages sent from or received by any location that corresponds to a configuration of the sender component is tagged in UPPAAL with <sender>), and a component named receiver (therefore, all messages sent from or received by any location that corresponds to a configuration of the receiver component is tagged in UPPAAL with <receiver>). The location of the composed HiLLS has a feedback loop such that if a message is sent by the sender component, it is intercepted by this location, which in turn will emit a message with the same content but tagged with the identity of the receiver component (we know that the composition information is defined in the configuration's property).

Figure 9. Semantic pattern of message transmission between two components by the composed model

Another way to address the case of HiLLS composed automata is to apply the "closure under composition" property of DEVS, which establishes that any coupled DEVS model has a corresponding atomic model. That way, any coupled model can be translated into an equivalent atomic model, and doing this would avoid the need to use the pattern introduced here. However, such an approach can be error-prone if not automated, as well as time-consuming for very complex systems hierarchies. In a given situation, the choice of either using the pattern introduced here or flattening the HiLLS composed automata before translating it into UPPAAL depends on how practical would be the application of the closure under composition property.

HiLLS to UPPAAL Transformation with Atlas Transformation Language (ATL)

We automate the HiLLS-to-UPPAAL transformation by implementing the general configuration pattern and its variants as ATL (Atlas Transformation Language) rules. ATL [START_REF] Baier | Principles of Model Checking[END_REF] is a model transformation language specified as both a metamodel and a textual concrete syntax. ATL follows the model transformation process that takes a source model in a specific form as inputs and outputs another form of the target model according to a set of predefined rules. ATL snippets of HiLLS-to-UPPAAL rules are detailed in Annex B.

HILLS-Based Requirement Specification

In the context of a HiLLS-based systems engineering, the sequence of configurations visited during execution describes the behavior of a system. Hence, a temporal logic can be used for the specification of, and reasoning with, the behavior of an ideal system. This behavior of the ideal system can serve as the metamodel that specifies the required behavioral properties of the real system. Therefore, with the help of verification techniques such as model checking [START_REF] Pnueli | The Temporal Logic of Programs[END_REF], we can verify whether or not a given model of the real system satisfies the required properties.

Good candidates for the description of temporal property requirements exist, such as Linear Temporal Logic -LTL [START_REF] Clarke | Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications[END_REF], or Computation Tree Logic (CTL) also known as branching temporal logic [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF]. However, it is common knowledge that dealing with such formalism is usually non-trivial. It takes some level of expertise in handling the idioms of logic and discrete mathematics to correctly read and/or write complex requirement properties. Lack of this expertise has been widely acknowledged by formal methods researchers as one of the main inhibitors to the wide adoption of formal verification tools.

In an effort to proffer a solution to this problem, Dwyer et al. [START_REF] Ferro | AMC: ACTL Model Checker. Reference Manual[END_REF] hypothesized that the experience base of experts in specification formalisms could be captured in parameterized patterns in formalism-independent formats to allow for systematic mapping to equivalent representations in some known specification formalism. They argued that this could be an easy way to transfer the experiences of experts in the domain to emerging practitioners and potential users.

Dwyer et al. were inspired by the successes that had been recorded with the use of design patterns to provide guidance on the best ways to language features to solve recurring problems by documenting tested solutions to such problems in patterns that can be easily reused to solve similar problems. With this, they envisioned the success of a pattern-based approach to the formal specification of properties of finite-state systems for verification. The output of their research was the recognition of some commonly occurring requirement property patterns from a collection of over five hundred property specifications they collected about thirtyfive sources comprising academia and industry. They then proposed parameterized templates for the recognized property patterns in five property specification formalisms, including LTL, CTL, and LCTL, which some other researchers later reproduced in additional formal methods' languages [START_REF] Kozen | Results on the Propositional μ-Calculus[END_REF][START_REF] Meyers | ProMoBox: A Framework for Generating Domain-Specific Property Languages[END_REF].

We propose to use variants of the elements of HiLLS for expressing graphically the templates suggested by [START_REF] Ferro | AMC: ACTL Model Checker. Reference Manual[END_REF]. We believe that uniformity of notations in both system and requirement models, due to the use of a pivotal language, will aid the user's specification and understanding of required temporal properties for complex systems. Similar benefits have motivated Meyers et al. [START_REF] Klein | Joint Structural and Temporal Property Specification Using Timed Story Scenario Diagrams[END_REF] and Klein & Giese [START_REF] Behrmann | Developing UPPAAL over 15 years[END_REF] to propose a framework to support the use of domain-specific notations for specifying properties in Domain-Specific Languages (DSLs).

To express the temporal properties, we propose basic notations (Figure 10) as the building blocks to specify temporal properties based on Dwyer's property patterns:

• The universal existence configuration notation (Figure 10.a) is a generic representation for any configuration that matches the set of information given by the notation (name, or/and predicates).

In addition, this pattern specifies that all configurations visited during the lifetime of a system within a given scope (to be defined) must match the set of information given by the pattern. • The eventual existence configuration notation (Figure 10.b) is a similar generic representation, with the difference that it only requires at least one of the configurations visited within a given scope (to be defined) must match the set of information given by the pattern. • The absence configuration notation (Figure 10.c) is also defined similarly, with the difference that it requires that any of the configurations visited within a given scope (to be defined) must match the set of information given by the pattern. • The bounded configuration notation (Figure 10.d) is defined the same generic way, with the difference that it requires the configurations visited within a given scope (to be defined) must match the set of information given by the pattern only a bounded number of times. The lower (respectively upper) bound is indicated in the lower (respectively upper) compartment of the circle at the righthand side of the generic configuration. The default value (i.e., when not indicated) for the lower (respectively upper) bound is 1 (respectively +∞).

Property Scope Notations

Table 1 presents the graphical notations introduced in HiLLS to support the property scopes defined in [START_REF] Ferro | AMC: ACTL Model Checker. Reference Manual[END_REF]. Since a temporal property specification is an abstract assertion on a segment of the execution of a system; we denote the entire execution by the elements between the initial configuration (solid ball) and final configuration (bull's eye) symbols. Each of the scopes describes the segment of the entire execution within which the specified property pattern (represented by dotted lines) must hold. Thus, to use any of the scope templates, we replace the dotted lines with the property pattern to be checked.

The scopes are:

• "Globally" scope, as the name implies, specifies that a property should hold throughout the execution of a system.

• "Before R" (respectively "After R") scope specifies that a given property must hold before (respectively after) the occurrence of a specified property R. • "Between Q and R" implies that a given property must hold after the occurrence of Q and before R where it is certain that R will eventually occur. • "After Q until R" has a similar implication with "Between Q and R" except that, in the former, it is not certain whether R will occur or not.

Note that the transitions between the generic configurations are abstract transitions without specific operations, triggers or output events. Hence, they do not specifically indicate any of the three kinds of configuration transition.

Table 1. Property scope notations in HiLLS Property scope notations Descriptions

Globally

The property pattern (to replace the dotted lines) must be satisfied in every configuration throughout the execution between the initial and final configuration.

Before R

The property pattern (to replace the dotted lines) must be satisfied before a transition into a configuration matching R.

After R

The property pattern (to replace the dotted lines) must be satisfied after a transition into a configuration matching R.

Between Q and R

The property pattern (to replace the dotted lines) must be satisfied after a transition into a configuration matching Q and before a transition into a configuration matching R.

After Q until R

The property pattern (to replace the dotted lines) must be satisfied after a transition into a configuration matching Q, and continue to hold until a configuration matching R occurs. If R does not occur, then the scope of the specified pattern continues until the end of execution.

Property Pattern Notations

Dwyer et al. have classified property patterns into two categories: occurrence and order, to describe properties on the occurrences or non-occurrence of properties, and relative order of properties respectively within the segment of execution defined by the associated scopes.

Occurrence patterns include:

• Absence (which specifies properties that must never occur within the specified scope);

• Universality (which specifies properties that must continuously occur within the specified scope);

• Existence (which specifies properties that must occur at least once within the specified scope); and

• Bounded existence (which specifies the maximum possible number of occurrences of certain properties within the specified scope).

Order patterns include:

• Precedence (which specifies a cause and effect relationship between two properties such that the occurrence of one must always have been preceded by the occurrence of the other within the specified scope); • Response (which specifies a stimulus and response relationship between two properties such that the occurrence of one must always eventually be followed by the occurrence of the other within the specified scope); • Chain precedence (which specifies a variant of the precedence pattern with m-cause to n-effect where m, n ∈N); and • Chain response (which specifies a variant of the response pattern with m-stimulus to n-response where m, n ∈N).

Table 2 presents graphical notations introduced in HiLLS to support these patterns. The basic notations support directly the Absence, Universality, Existence and Bounded existence patterns. They are combined with additional symbols to support the remaining property patterns. Notice that the circle used in the precedence patterns can be seen as a mnemonic indication of the required property in an implication relationship (e.g., in S precedes R, S is required anytime R occurs, while in R responds to S, R is required anytime S occurs).

Table 2. Property pattern notations in HiLLS

Patterns and Scopes for Composed Models

In order to extend these notations to composed HiLLS models, we allow the requirements specification of such models to make reference to the generic configurations of their components by tagging them with the name of the corresponding components, as indicated by Figure 11. The relationships defined in Table 2 still hold for the elements of Figure 11. Consequently, requirements can be specified for HiLLS composed models, either by using generic configuration notations derived from its configuration transition diagram or by using the ones derived from the configuration transition diagrams of its component models.

Mapping to TCTL

The requirements specifications can be mapped onto TCTL (and many other temporal formalisms), such that once the user has a HiLLS-specified requirement model, the corresponding logic-based queries can be generated. There exist tools to automatically check such queries against the system model. We use the UPPAAL tool for that purpose [START_REF] Behrmann | UPPAAL 4.0[END_REF][START_REF] Alpern | Defining Liveness[END_REF]. Annex C gives for each of the property patterns, the corresponding TCTL/CTL specifications in the context of the scope patterns.

HILLS-Based Verification Framework

Systems properties can be expressed at different levels of abstraction. At higher levels, requirements resemble general principles and global expectations, for which there is no tool for automated verification. At the lower levels, requirements are detailed such that formal tools can be used, but this entails mathematical skills that are not commonly shared. We suggest a layered approach to bridge the gap between these extremes, as shown by Figure 12's right-hand side. In this organization, properties at a given level can be expressed in terms of properties at the immediate lower level. We consider three levels of abstraction:

(1) At the higher level are conceptual properties, such as fairness (also known as starvation-freedom), deadlock-freedom (also known as progress), termination, real-time correctness… (2) The medium level is where the user needs to reduce a higher-level property to either a safety property, or a liveness property, or a combination of both properties. In a generic way, Safety specifies that "Something bad will never happen", while Liveness specifies that "Something good will eventually happen" [START_REF] Callahan | Automated Software Testing Using Model Checking[END_REF]. For example, deadlock-freedom can be expressed either as repeated liveness [START_REF] Maandag | Experiments in Unifying Model-Checking Approaches[END_REF] or safety [START_REF] Yang | Model Checking Concurrent and Real-Time Systems: The Pat Approach[END_REF]; termination can be expressed as liveness to some desired end [START_REF] Akhtar | Formal Verification and Model Transformations of an Agent-based System: A Case Study[END_REF][32], and fairness can be expressed either as repeated liveness or safety [START_REF] Pnueli | The Temporal Logic of Programs[END_REF] -e.g., in the mutual exclusion property, having always at most one process in its critical section is a typical safety property, where the bad thing is that more than one process is in its critical section. (3) The lowest level is where Safety and Liveness are expressed as Reachability properties. A reachability property states that some particular situations can be reached. If P is the something in Safety, then "Something bad will never happen" translates to "Never P". If Q is the something in Liveness, then "Something good will eventually happen" translates to "Eventually P".

Consequently, both are reachability problems. The user needs to place them within a given scope (e.g., the entire lifetime of the system, or a given lifetime window). The resulting requirement can be graphically captured using the notations we have introduced and automatically translated to logic queries that a formal tool can check.

Application

To illustrate the application of our framework, let us capitalize on the well-known automated unmanned railway level crossing system described in Figure 13.

Figure 13. Automated unmanned railway level crossing system

The crossing is guarded by a gate, which is used to close the road when a train is crossing. Two sensors, one located upstream of the crossing, and the other downstream, are used to detect the arrival and exit of a train. The two sensors communicate the entrance and the exit of a train to the controller. The control system receives remote signals from the sensors, and remotely closes and opens the gate.

HiLLS-based System Modeling

Figure 14 shows the HiLLS model of the Crossing system as drawn in HGE. The entire system is a composition of 5 system components. These components are individually detailed in Annex D.

The entire system has a unique passive configuration labeled Network which depicts the relationships between components, and which translates the static nature of the composition. The predicate of the Network configuration provides the coupling information between the components, i.e., the Train's output port "Out" is connected to both the sensors' and the Controller's input ports "In", while the Controller's output port "Out" is connected to the Gate's input ports "In".

HiLLS-based Requirements Specification

Our high-level requirements knowledge is that such a system has security concerns (among others), as regards to vehicles and pedestrians crossing the level by the road. We do not want users to be crushed by a high-speed train. We then reduce this security concern to "something bad will never happen" (mid-level Safety requirement), where something bad is "gate open while train crossing". The corresponding low-level requirements (i.e., scope and properties elucidated) are given by Figure 16. As shown by Figure 16, three cases can be considered:

(1) The requirement is expressed as a specific configuration of a model. While Figure 16.a requires that the gate must eventually open, Figure 16.b requires that the train must never cross the level. (2) The requirement is expressed as a predicate that one or more configurations can satisfy. Figure 16.c requires that the gate must be in a passive configuration at least twice, while Figure 16.d requires that whenever a train approaches, it crosses eventually. (3) The requirement is defined over multiple components of a composed model. Figure 16.e requires that always the gate must be closed when a train is crossing, while Figure 16.f requires that always the crossing of a train must be preceded by the closing of the gate.

HiLLS-based System Verification and Validation

Figure 17 shows how the requirement "Whenever a train is crossing, the gate is closed" translates to UPPAAL query, and the failure of the checking. This result reveals that the system is not safe since there exist cases where the train is crossing and the gate is open, which violates the safety property. A known solution to this crossing system is to protect the crossing level by a traffic light that receives information to turn red or green from the controller. The controller also controls the opening and the closing of the gate. This solution has easily been modelled, verified and validated in the HiLLS framework.

Conclusion

This paper proposes a framework to support a full system verification process, using the High Level Language for Systems Specification (HiLLS) as a visual pivotal formalism. The process comprises the specification of both the discrete-event behavior of the system of interest and the temporal requirements to be checked against it. As HiLLS provides a graphical concrete syntax to the well-known DEVS formalism, the latter provides the semantic domain for the discrete-event simulation of HiLLS-specified models. To extend HiLLS capabilities to requirements specification, we adopted concepts from a pattern-based classification of Temporal Logic specifications of commonly occurring temporal requirements, for which we provided graphical notations using HiLLS syntactical elements. Well-defined transformation patterns allow to make HiLLS specifications amenable to UPPAAL checking, where at one side the system model is turned to a UPPAAL Timed Automaton and the requirements model is turned to UPPAAL queries.

We agree with the belief that the definition and use of high-level abstractions in writing formal specification is an important factor in making automated formal methods, specifically finite-state verification tools, more suitable. Therefore, providing graphical notations to describe systems and their requirements is a step towards bridging the gap between system experts and analysis experts. Moreover, having a highly communicable concrete syntax and multiple semantic domain mappings achieves the aim of providing a pivotal formalism for multiple analysis approaches, including the formal analysis of system properties without the need to run time-consuming experiments.

The proposed framework is unique in supporting a full system verification process based on the graphical modeling of both the system of interest and the requirements to be checked, using a drag and drop editor.

Much remains to be done for large-scale adoption, which we target as future work, including:

• The distribution of the HiLLS editor as an Eclipse plugin;

• The development of automated transformation engines for more temporal logic formalisms (other than TCTL), in order to allow the use of model checking tools other than UPPAAL; and • The development of connectors from the HiLLS editor to existing DEVS tools (see http://www.sce.carleton.ca/faculty/wainer/standard/tools.htm, last accessed on 28/02/2020).

Figure 2 .

 2 Figure 2. Template for HiLLS representation of a DEVS model

Figure 3 .

 3 Figure 3. HiLLS concrete syntax

Figure 4 .

 4 The editor displays a workspace, with a central area where the model is drawn. To the left of the workspace is the Model view, where appears the hierarchy tree of the model, which provides easy navigation throughout the model components. On the right side of the workspace, are three panels for modeling. The upper palette contains all the basic elements of the HiLLS concrete syntax (Configuration, Declaration, Activity, HSystem, etc.). The middle panel displays all connectors (Transition, Aggregation, Reference, and Composition). The bottom panel displays the temporal logic items for requirement specification.

Figure 4 .

 4 Figure 4. HiLLS Graphical Editor

  Prob(δint(4,σ)=(5,+∞))=σFAT and Prob(δint(4,σ)=(1,+∞))=1-σFAT, ∀ σ ∈ [0, tINF] Prob(δint(3,σ)=(3,tINC))=σINF and Prob(δint(3,σ)=(1,+∞))=1-σINF, ∀ σ ∈ [0, tINC] λ : S → Y λ(2, σ) = (status, E), ∀ σ ∈ ℜ0 +∞ Prob(λ(3,σ)={(status,I),(out,vir)})=σINF and Prob(λ(3,σ)=(status,S))=1-σINF, ∀ σ∈[0,tINC] Prob(λ(4,σ)=(status,D)) = σFAT and Prob(λ(4,σ)=(status,S)) = 1-σFAT, ∀ σ ∈ [0, tINF] δext : Q × X → S, with Q = {((s,σ), e) / (s,σ) ∈ S, 0 ≤ e< σ} δext((1, σ), e, (in, vir)) = (2, 0) ∀ σ ∈ ℜ0 +∞ ∀ e ∈ [0, σ) δext((3, σ), e, (in, vir)) = (3, σ-e) ∀ σ ∈ [0, tINC] ∀ e ∈ [0, σ) δext((4, σ), e, (in, vir)) = (4, σ-e) ∀ σ ∈ [0, tINF] ∀ e ∈ [0, σ)

Figure 5 .

 5 Figure 5. DEVS model example and its HiLLS counterpart

Figure 6 .

 6 Figure 6. Semantics pattern for HiLLS active configuration

Figure 7 .

 7 Illustration of (partial) semantics mapping from HiLLS to UPPAAL From C1curse of Figure7b, two types of external transitions are possible based on the type of message received. If ?start is received then a transition to C1interruptStart (for C1interrupt(Start)) will happen and if ?stop is received, then a transition to C1interruptStop (for C1interrupt(Stop)) will happen. The external transition from each of the C1interrupt(x) can go to different other configurations' curses, depending on the elapsed time, as stated by the HiLLS model.

Figure 8 .

 8 Figure 8. Variants of the semantics pattern for HiLLS configurations These variants, together with the general pattern, form the building blocks for a complete translation of any HiLLS model into its UPPAAL TA counterpart: • Figure 8a presents the interruptless configuration pattern, where only internal and confluent transitions are possible, as no input is received by the corresponding HiLLS model in the corresponding configuration (therefore no external transition happens).

•Figure 10 .

 10 Figure 10. Building blocks for property patterns representation in HiLLS

Figure 11 .

 11 Figure 11. Generic configuration specification of a HiLLS composed model

Figure 12

 12 Figure 12 depicts the full process of HiLLS-based visual modeling and the UPPAAL-based verification framework. On one side, HiLLS offers visual modeling means to capture the structure and behavior of the system. The patterns defined allow us to translate such a model into a UPPAAL TA. On the other side, the user can start with a high-level elicitation of requirements, then reduce it to an intermediate level of property analysis, and then a low level of reachability. Then the extended notations to HiLLS offer a visual means to capture the resulting requirements model. Rules defined in Annex translate such a model into TCTL statements, which can directly be expressed as UPPAAL queries. The UPPAAL tool allows to check the queries against the TA model.

Figure 12 .

 12 Figure 12. HiLLS-based formal verification framework

Figure 14 .

 14 Figure 14. HiLLS model of the crossing system Figure15presents the corresponding UPPAAL Timed Automata, using the semantic pattern defined in Figure9. Semantic translations of all the HiLLS component models into corresponding UPPAAL automata using the configuration pattern variants previously defined are displayed in Annex E.

Figure 15 .

 15 Figure 15. UPPAAL Timed Automata of the Crossing System

Figure 16 .

 16 Figure 16. HiLLS-based requirements specifications for the crossing system

Figure 17 .

 17 Figure 17. "Whenever a train is crossing, the gate is closed": Not satisfied

  The composed system, while in its unique location Networkcurse, receives signals from some components and translates them into signals to other components:• If approachTRAIN is received from Train, then approachENTRANCESENSOR is sent to Entrance_Sensor and approachCONTROLLER is sent to Controller. • If openCONTROLLER is received from Controller, then openGATE is sent to Gate. • If closeCONTROLLER is received from Controller, then closeGATE is sent to Gate. • If exitTRAIN is received from Train, then exitEXITSENSOR is sent to Exit_Sensor and exitCONTROLLER is sent to Controller.

ANNEX A: DEVS formalism

An atomic DEVS model is defined by the n-uple: X, Y, S, δint, δext, δconf, λ, ta, where

• X, Y, and S are respectively the input set, output set, and state set (at any time, the system modeled is in one of the possible states) • ta : S → ℜ0 +∞ is the time advance function (i.e., it gives the lifespan of each state), with ℜ0 +∞ designating the set of non-negative real numbers, including +∞ • δint : S → S is the internal transition function (i.e., it is triggered only when the elapsed time in the system's current state scurr has reached ta(scurr) without the system being disturbed by any receipt of input) • λ : S → Y is the output function (i.e., it computes the output of the system, each time an internal transition is occurring) • δext : Q × X → S is the external transition function (i.e., it is triggered only when the system receives an input, while the elapsed time in the system's current state scurr has not reached ta(scurr)), and Q = {(s,e) / s ∈ S, 0 ≤ e < ta(s)} is called the total state • δconf : S × X → S is the confluent transition function (i.e., it is triggered only when the system receives an input at exactly the time that the elapsed time in the system's current state scurr has reached ta(scurr))

The operational semantics of an atomic DEVS model is informally described as follows: at the start, the systems are in an initial state and remain there until the time specified by ta is exhausted or until input event is received. In the former case, an internal transition function occurs then the system switches to another state after sending output event as defined by the output function λ. In the latter case if an input event is received before the specified time, then the external transition function is applied. When a collision occurs i.e., an external event is received concurrently with the elapsed time equal to the time specified by the time advance function, the confluent function is applied in such a way that the system sends output value and changes to a new state.

A coupled DEVS model is a structure: Xself, Yself, {Md}d∈D, {Id}d∈D, {Zi,j}i∈D∪{self},j∈Ii, where • Xself and Yself are defined the same way X and Y are for atomic models (self being here a reference to the coupled model, while component models are referred to using indices such as i, j or d)

ANNEX C: TCTL/CTL templates for occurrence property patterns

Variables p, q, and r, are user-defined properties. The ◊, □, and ○ operators are respectively the eventually, always and next operators. The w operator is the weak until operator which may be related to the strong until operator (Y) using any of the following equivalences:

In addition to the logical and temporal operators used in LTL, CTL supports the use of the existential path quantifier ∃ (resp. universal path quantifier ∀) for the specification of properties that must be satisfied by some (resp. all) computations starting in a state of interest. For example, ∀◊p requires that ◊p holds in all paths of executions starting from the state of interest, while ∃◊p requires that ◊p holds in at least one path of executions starting from the state of interest.

Readers may refer to [START_REF] Pnueli | The Temporal Logic of Programs[END_REF] for more details on basic temporal operators, as well as a good introduction to LTL and CTL.

Absence (p is false) Globally ∀□(¬p) Before r ∀[(¬p∨ ∀□(¬r))w r] After q ∀□( q ⇒ ∀□ (¬p)) Between q and r ∀□(q∧¬r⇒ ∀ [(¬p∨ ∀□(¬r)) w r]) After q until r ∀□(q∧¬r⇒

Between q and r ∀□