Roxana Dumitrescu
email: roxana@ceremade.dauphine.fr.

Céline Labart
email: celine.labart@univ-savoie.fr

Reflected scheme for doubly reflected BSDEs with jumps and RCLL obstacles

Keywords: Double barrier reflected BSDEs, Backward stochastic differential equations with jumps, numerical scheme MSC 2010 classifications : 60H10, 60H35, 60J75, 34K28

, which also depends on the penalization parameter). We prove the convergence of the scheme, and give some numerical examples.

Introduction

Non-linear backward stochastic differential equations (BSDEs in short) have been introduced by Pardoux and Peng in the Brownian framework in their seminal paper [START_REF] Pardoux | Adapted solution of a backward stochastic differential equation[END_REF] and then extended to the case of jumps by Tang and Li [START_REF] Tang | Necessary conditions for optimal control of stochastic systems with random jumps[END_REF]. BSDEs appear as a useful mathematical tool in finance (hedging problems) and in stochastic control. Moreover, these stochastic equations provide a probabilistic representation for the solution of semilinear partial differential equations. BSDEs have been extended to the reflected case by El Karoui et al in [START_REF] Karoui | Reflected solutions of Backward SDE's and related obstacle problems for PDE's[END_REF]. In their setting, one of the components of the solution is forced to stay above a given barrier which is a continuous adapted stochastic process. The main motivation is the pricing of American options especially in constrained markets. The generalization to the case of two reflecting barriers has been carried out by Cvitanic and Karatzas in [START_REF] Cvitanic | Backward stochastic differential equations with reflection and Dynkin games[END_REF]. It is well known that doubly reflected BSDEs (DRBSDEs in the following) are related to Dynkin games and to the pricing of Israeli options (or Game options). The extension to the case of reflected BSDEs with jumps and one reflecting barrier with only inaccessible jumps has been established by Hamadène and Ouknine [START_REF] Hamadène | Reflected Backward Stochastic Differential Equation with jumps and random obstacle[END_REF]. Later on, Essaky in [START_REF] Essaky | Reflected backward stochastic differential equation with jumps and RCLL obstacle[END_REF] and Hamadène and Ouknine in [START_REF] Hamadène | Reflected Backward SDEs with general jumps[END_REF] have extended these results to a right-continuous left limited (RCLL) obstacle with predictable and inaccessible jumps. Results concerning existence and uniqueness of the solution for doubly reflected BSDEs with jumps can be found in [START_REF] Crépey | Reflected and doubly reflected BSDEs with jumps: a priori estimates and comparison[END_REF], [START_REF] Dumitrescu | Double barrier reflected BSDEs with jumps and generalized Dynkin games[END_REF], [START_REF] Hamadène | BSDEs with two reacting barriers driven by a Brownian motion and an independent Poisson noise and related Dynkin game[END_REF], [START_REF] Hamadène | BSDEs with two RCLL Reflecting Obstacles driven by a Brownian Motion and Poisson Measure and related Mixed Zero-Sum Games[END_REF] and [START_REF] Essaky | Backward stochastic differential equation with two reflecting barriers and jumps[END_REF].

Numerical schemes for DRBSDEs driven by the Brownian motion have been proposed by Xu in [START_REF] Xu | Numerical algorithms and Simulations for Reflected Backward Stochastic Differential Equations with Two Continuous Barriers[END_REF] (see also [START_REF] Mémin | Convergence of solutions of discrete Reflected backward SDE's and Simulations[END_REF] and [START_REF] Peng | Numerical algorithms for BSDEs with 1-d Brownian motion: convergence and simulation[END_REF]) and, in the Markovian framework, by Chassagneux in [START_REF] Chassagneux | A discrete-time approximation for doubly reflected BSDEs[END_REF]. In this paper, we are interested in numerically solving DRBSDEs driven by a Brownian motion and an independent Poisson process in the case of RCLL obstacles with only totally inacessible jumps. More precisely, we consider equations of the following form:

   (i) Y t = ξ T + T t g(s, Y s , Z s , U s )ds + (A T -A t ) -(K T -K t ) - T t Z s dW s - T t U s d Ñs , (ii) ∀t ∈ [0, T ], ξ t ≤ Y t ≤ ζ t a.s., (iii)
T 0 (Y t -ξ t )dA t = 0 a.s. and T 0 (ζ t -Y t )dK t = 0 a.s.

(1.1) {W t : 0 ≤ t ≤ T } is a one dimensional standard Brownian motion and { Ñt := N t -λt, 0 ≤ t ≤ T } is a compensated Poisson process. Both processes are independent and they are defined on the probability space (Ω, F T , F = {F t } 0≤t≤T , P). The processes A and K have the role to keep the solution between the two obstacles ξ and ζ. Since we consider that the jumps of the obstacles are totally inaccessible, A and K are continuous processes.

In the non-reflected case, some numerical methods have been provided: in [START_REF] Bouchard | Discrete-time approximation of decoupled Forward-Backward SDE with jumps[END_REF], the authors propose a scheme for Forward-Backward SDEs based on the dynamic programming equation and in [START_REF] Lejay | Numerical approximation of Backward Stochastic Differential Equations with Jumps[END_REF], the authors propose a fully implementable scheme based on a random binomial tree. In the reflected case, a fully implementable numerical scheme has been recently provided by Dumitrescu and Labart in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF]. Their method is based on the approximation of the Brownian motion and the Poisson process by two random walks and on the approximation of the reflected BSDE by a sequence of penalized BSDEs.

The aim of this paper is to propose an alternative scheme to [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF] to solve (1.1). The scheme proposed here takes the following form:

     y n j = E[y n j+1 |F n j ] + g(t j , E[y n j+1 |F n j ], z n j , u n j )δ + a n j -k n j , a n j ≥ 0, k n j ≥ 0, a n j k n j = 0, ξ n j ≤ y n j ≤ ζ n j , (y n j -ξ n j )a n j = (y n j -ζ n j )k n j = 0.
(1.

2)

It generalizes the scheme proposed by [START_REF] Xu | Numerical algorithms and Simulations for Reflected Backward Stochastic Differential Equations with Two Continuous Barriers[END_REF] to the case of jumps. Compared to the scheme proposed in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF], the scheme proposed here -called reflected scheme in the following -is based on the direct discretization of (1.1). In particular, there is no penalization step. Then, this method only depends on one parameter of approximation (the number of time steps n), contrary to the scheme proposed in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF] (which also depends on the penalization parameter). We provide here an explicit reflected scheme and an implicit reflected scheme and we show the convergence of both schemes. We illustrate numerically the theoretical results and show they coincide with the ones obtained by using the penalized scheme presented in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF], for large values of the penalization parameter.

The paper is organized as follows: in Section 2 we introduce notations and assumptions. In Section 3, we precise the discrete time framework and present the numerical schemes. In Section 4 we provide the convergence of the schemes. Numerical examples are given in Section 5 .

Notations and assumptions

In this Section we introduce notations and assumptions. We recall the result on existence and uniqueness of solution to (1.1). We also introduce some assumptions on the obstacles ξ and ζ specific to this paper (Assumption 2.5).

Let (Ω, F, P) be a probability space, and P be the predictable σ-algebra on [0, T ] × Ω. Let W be a onedimensional Brownian motion and N be a Poisson process with intensity λ > 0. Let F = {F t , 0 ≤ t ≤ T } be the natural filtration associated with W and N .

For each T > 0, we use the following notations:

• L 2 (F T ) is the set of F T -measurable and square integrable random variables.

• H 2 is the set of real-valued predictable processes φ such that φ 2

H 2 := E T 0 φ 2 t dt < ∞. • B(R 2 ) is the Borelian σ-algebra on R 2 .
• S 2 is the set of real-valued RCLL adapted processes φ such that φ 2

S 2 := E(sup 0≤t≤T |φ t | 2 ) < ∞. • A 2 is the set of real-valued non decreasing RCLL predictable processes A with A 0 = 0 and E(A 2 T ) < ∞.
Definition 2.1 (Driver, Lipschitz driver). A function g is said to be a driver if

• g : Ω × [0, T ] × R 3 → R (ω, t, y, z, u) → g(ω, t, y, z, u) is P ⊗ B(R 3 )-measurable, • g(., 0, 0, 0) ∞ < ∞.
A driver g is called a Lipschitz driver if moreover there exists a constant C g ≥ 0 and a bounded, nondecreasing continuous function Λ with Λ(0) = 0 such that dP⊗dt-a.s. , for each (s 1 , y 1 , z 1 , u 1 ), (s 2 , y 2 , z 2 , u 2 ), Let us now introduce an additional assumption on g, which ensures the comparison theorem for BSDEs with jumps (see [START_REF] Quenez | BSDEs with jumps, optimization and applications to dynamic risk measures[END_REF]Theorem 4.2]). The comparison theorem plays a key role in the proof of the convergence of the penalized scheme (see [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF]), which is useful to prove the convergence of the reflected scheme (see Section 4). Assumption 2.4. A Lipschitz driver g is said to satisfy Assumption 2.4 if the following holds : dP ⊗ dt a.s. for each (y, z, u 1 , u 2 ) ∈ R 4 , we have

|g(ω, s 1 , y 1 , z 1 , u 1 ) -g(ω, s 2 , y 2 , z 2 , u 2 )| ≤ Λ(|s 2 -s 1 |) + C g (|y 1 -y 2 | + |z 1 -z 2 | + |u 1 -u 2 |).
g(t, y, z, u 1 ) -g(t, y, z, u 2 ) ≥ θ(u 1 -u 2 ), with -1 ≤ θ ≤ θ 0 .
We also assume the following hypothesis on the barriers. 3 Discrete time framework and numerical scheme

Assumption 2.5. ξ and ζ are Itô processes of the following form

ξ t = ξ 0 + t 0 b ξ s ds + t 0 σ ξ s dW s + t 0 β ξ s -d Ñs (2.1)
ζ t = ζ 0 + t 0 b ζ s ds + t 0 σ ζ s dW s + t 0 β ζ s -d

Discrete time framework

For the numerical part of the paper, we adopt the framework of [START_REF] Lejay | Numerical approximation of Backward Stochastic Differential Equations with Jumps[END_REF] and [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF], presented below.

Random walk approximation of (W, Ñ )

For n ∈ N, we introduce δ := T n and the regular grid (t j ) j=0,...,n with step size δ (i.e. t j := jδ) to discretize [0, T ]. In order to approximate W , we introduce the following random walk

W n 0 = 0, W n t = √ δ [t/δ] i=1 e n i , (3.1)
where e n 1 , e n 2 , ..., e n n are independent identically distributed random variables with the following symmetric Bernoulli law:

P(e n 1 = 1) = P(e n 1 = -1) = 1 2 .
To approximate Ñ , we introduce a second random walk

Ñ n 0 = 0, Ñ n t = [t/δ] i=1 η n i , (3.2)
where η n 1 , η n 2 , ..., η n n are independent and identically distributed random variables with law

P(η n 1 = κ n -1) = 1 -P(η n 1 = κ n ) = κ n ,
where κ n = e -λδ . We assume that both sequences e n 1 , ..., e n n and η n 1 , η n 2 , ..., η n n are defined on the original probability space (Ω, F, P). The (discrete) filtration in the probability space is F n := {F n j : j = 0, ..., n} with F n 0 = {Ω, ∅} and F n j = σ{e n 1 , ..., e n j , η n 1 , ..., η n j } for j = 1, ..., n. The following result states the convergence of (W n , Ñ n ) in the J 1 -Skorokhod topology. We refer to [START_REF] Lejay | Numerical approximation of Backward Stochastic Differential Equations with Jumps[END_REF]Section 3] for more results on the convergence in probability of F n -martingales .

Lemma 3.1. ([15, Lemma3, (III)]

The couple (W n , Ñ n ) converges in probability to (W, Ñ ) for the J 1 -Skorokhod topology.

We recall that the process ξ n converges in probability to ξ in the J 1 -Skorokhod topology if there exists a family (ψ n ) n∈N of one-to-one random time changes from

[0, T ] to [0, T ] such that sup t∈[0,T ] |ψ n (t)-t| ----→ n→∞ 0 almost surely and sup t∈[0,T ] |ξ n ψ n (t) -ξ t | ----→ n→∞ 0 in probability.

Martingale representation

Let y j+1 denote a F n j+1 -measurable random variable. As pointed out in [START_REF] Lejay | Numerical approximation of Backward Stochastic Differential Equations with Jumps[END_REF], we need a set of three strongly orthogonal martingales to represent the martingale difference m j+1 := y j+1 -E(y j+1 |F n j ). We introduce a third martingale increment sequence {µ n j = e n j η n j , j = 0, • • • , n}. In this context there exists a unique triplet (z j , u j , v j ) of F n j -random variables such that

m j+1 := y j+1 -E(y j+1 |F n j ) = √ δz j e n j+1 + u j η n j+1 + v j µ n j+1 ,
and

       z j = 1 √ δ E(y j+1 e n j+1 |F n j ), u j = E(yj+1η n j+1 |F n j ) E((η n j+1 ) 2 |F n j ) = 1 κn(1-κn) E(y j+1 η n j+1 |F n j ), v j = E(yj+1µ n j+1 |F n j ) E((µ n j+1 ) 2 |F n j ) = 1 κn(1-κn) E(y j+1 µ n j+1 |F n j ). (3.3)
The computation of conditional expectations is done in the following way:

Remark 3.2. (Computing the conditional expectations) Let Φ denote a function from R 2j+2 to R. We use the following formula

E(Φ(e n 1 , • • • , e n j+1 , η n 1 , • • • , η n j+1 )|F n j ) = κ n 2 Φ(e n 1 , • • • , e n j , 1, η n 1 , • • • , η n j , κ n -1) + κ n 2 Φ(e n 1 , • • • , e n j , -1, η n 1 , • • • , η n j , κ n -1) + 1 -κ n 2 Φ(e n 1 , • • • , e n j , 1, η n 1 , • • • , η n j , κ n ) + 1 -κ n 2 Φ(e n 1 , • • • , e n j , -1, η n 1 , • • • , η n j , κ n ).

Reflected schemes

The barriers ξ and ζ given in Assumption 2.5 are approximated in the following way: for all k ∈ {1, • • • , n}

ξ n k = ξ 0 + k-1 i=0 b ξ ti δ + k-1 i=0 σ ξ ti √ δe n i+1 + k-1 i=0 β ξ ti η n i+1 , (3.4
)

ζ n k = ζ 0 + k-1 i=0 b ζ ti δ + k-1 i=0 σ ζ ti √ δe n i+1 + k-1 i=0 β ζ ti η n i+1 . ( 3
(i) sup n max j E(|ξ n j | r ) + sup n max j E(|ζ n j | r ) + sup t≤T E(|ξ t | r ) + sup t≤T E(|ζ t | r ) ≤ C ξ,ζ,T,λ (ii) ξ n (resp. ζ n ) converges in probability to ξ (resp. ζ) in J 1 -Skorokhod topology.
Proof. (i) ensues from Burkhölder-Davis-Gundy and Rosenthal inequalities, and (ii) ensues from [14, Theorem 6.22 and Corollary 6.29].

In the following Section we introduce the implicit reflected scheme, which is an intermediate scheme useful to prove the convergence of the reflected scheme (1.2).

Implicit reflected scheme

After the discretization of the time interval, our discrete reflected BSDEs with two RCLL barriers on small interval [t j , t j+1 [, for 0 ≤ j ≤ n -1 is

y n j = y n j+1 + g(t j , y n j , z n j , u n j )δ + a n j -k n j -z n j √ δε n j+1 -u n j η n j+1 -v n j µ n j+1 , a n j ≥ 0, k n j ≥ 0, a n j k n j = 0, ξ n j ≤ y n j ≤ ζ n j , (y n j -ξ n j )a n j = (y n j -ζ n j )k n j = 0. (3.6)
with terminal condition y n n = ξ n n . By taking the conditional expectation in (3.6) w.r.t. F n j , we get

(S 1 )          y n n = ξ n n , y n j = E[y n j+1 |F n j ] + g(t j , y n j , z n j , u n j )δ + a n j -k n j , a n j ≥ 0, k n j ≥ 0, a n j k n j = 0, ξ n j ≤ y n j ≤ ζ n j , (y n j -ξ n j )a n j = (y n j -ζ n j )k n j = 0. Lemma 3.4. For δ small enough, (S 1 ) is equivalent to (S 2 )          y n n = ξ n n , y n j = Ψ -1 (E[y n j+1 |F n j ] + a n j -k n j ), a n j = (E[y n j+1 |F n j ] + g(t j , ξ n j , z n j , u n j )δ -ξ n j ) -, k n j = (E[y n j+1 |F n j ] + g(t j , ζ n j , z n j , u n j )δ -ζ n j ) + ,
where Ψ(y) := y -g(t j , y, z n j , u n j )δ.

Proof. For δ small enough, Ψ is invertible because the Lipschitz property of g leads to (Ψ(y)-Ψ(y ))(y-y ) ≥ (1 -δC g )(y -y ) 2 > 0 for any y = y . We first prove that (S 1 ) implies (S 2 ). Let us firstly assume that ∀j ≤ n -1, ξ n j < ζ n j . On the set {y n j = ξ n j } we have k n j = 0, then

a n j = Ψ(ξ n j ) -E[y n j+1 |F n j ] = (E[y n j+1 |F n j ] -Ψ(ξ n j )) -(since E[y n j+1 |F n j ] -Ψ(ξ n j ) = Ψ(y n j ) -Ψ(ξ n j ) -a n j ≤ 0) and on {y n j > ξ n j } we have a n j = 0, (E[y n j+1 |F n j ] -Ψ(ξ n j ) = Ψ(y n j ) -Ψ(ξ n j ) + k n j > 0 (thanks to the monotonicity of Ψ)). Then, a n j = (E[y n j+1 |F n j ] -Ψ(ξ n j )) -.
The same type of proof leads to the fourth line of (S 2 ). If there exists j ≤ n-1 such that ξ n j = ζ n j , we get ξ n j = ζ n j = y n j . Then, we have a n j = 0 or k n j = 0. If both are null, we get Ψ(

y n j ) = E[y n j+1 |F n j ] = Ψ(ξ n j ) = Ψ(ζ n j
). This coincides with the definitions of a n j and k n j given in (S 2 ). If a n j > 0, k n j = 0 and we get

a n j = Ψ(y n j ) -E[y n j+1 |F n j ] = Ψ(ξ n j ) -E[y n j+1 |F n j ], then a n j = (E[y n j+1 |F n j ] -Ψ(ξ n j )) -. Conversely, assume (S 2 ), let us prove a n j k n j = 0, (y n j -ξ n j )a n j = (y n j -ζ n j )k n j = 0 and ξ n j ≤ y n j ≤ ζ n j . If a n j > 0, we get Ψ(ζ n j ) ≥ Ψ(ξ n j ) > E[y n j+1 |F n j ], then k n j = 0. Let us prove that (y n j -ξ n j )a n j = 0. If a n j > 0, Ψ(y n j ) = E[y n j+1 |F n j ] + a n j = Ψ(ξ n j ).
Since Ψ is a one to one map, we get y n j = ξ n j . The same argument holds to prove (y n j -ζ n j )k n j = 0. Let us prove that ξ n j ≤ y n j . To do so, assume that y n j < ξ n j . In this case

a n j = k n j = 0, which gives Ψ(ξ n j ) ≤ E[y n j+1 |F n j ], by definition of a n j . Then Ψ(y n j ) = E[y n j+1 |F n j ] ≥ Ψ(ξ n j )
. Ψ being a non decreasing function, this leads to absurdity.

We also introduce the continuous time version (Y n t , Z n t , U n t , A n t , K n t ) 0≤t≤T of (y n j , z n j , u n j , a n j , k n j ) j≤n :

Y n t := y n [t/δ] , Z n t := z n [t/δ] , U n t := u n [t/δ] , A n t := [t/δ] i=0 a n i , K n t := [t/δ] i=0 k n i . (3.7)
In the following

Θ n := (Y n , Z n , U n , A n -K n ).

Explicit reflected scheme

The explicit reflected scheme is introduced by replacing y n j by E[y n j+1 |F n j ] in g. We obtain

     y n j = y n j+1 + g(t j , E[y n j+1 |F n j ], z n j , u n j )δ + a n j -k n j -z n j √ δε n j+1 -u n j η n j+1 -v n j µ n j+1 , a n j ≥ 0, k n j ≥ 0, a n j k n j = 0, ξ n j ≤ y n j ≤ ζ n j , (y n j -ξ n j )a n j = (y n j -ζ n j )k n j = 0. (3.8)
with terminal condition y n n = ξ n n . By taking the conditional expectation in (3.8) with respect to F n j , we derive that:

(S 1 )      y n n = ξ n n , y n j = E[y n j+1 |F n j ] + g(t j , E[y n j+1 |F n j ], z n j , u n j )δ + a n j -k n j a n j ≥ 0, k n j ≥ 0, a n j k n j = 0, ξ n j ≤ y n j ≤ ζ n j , (y n j -ξ n j )a n j = (y n j -ζ n j )k n j = 0.
As for the implicit reflected scheme, we get that (S 1 ) is equivalent to (S 2 )

(S 2 )          y n n = ξ n n , y n j = E[y n j+1 |F n j ] + g(t j , E[y n j+1 |F n j ], z n j , u n j )δ + a n j -k n j , a n j = (E[y n j+1 |F n j ] + g(t j , E[y n j+1 |F n j ], z n j , u n j )δ -ξ n j ) -, k n j = (E[y n j+1 |F n j ] + g(t j , E[y n j+1 |F n j ], z n j , u n j )δ -ζ n j ) + .
We also introduce the continuous time version (Y

n t , Z n t , U n t , A n t , K n t ) 0≤t≤T of (y n j , z n j , u n j , a n j , k n j ) j≤n : Y n t := y n [t/δ] , Z n t := z n [t/δ] , U n t := u n [t/δ] , A n t := [t/δ] i=0 a n i , K n t := [t/δ] i=0 k n i . (3.9)
In the following Θ

n := (Y n , Z n , U n , A n -K n ) and α n := A n -K n .

Implicit penalization scheme

In this Section we recall the implicit penalization scheme introduced in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF]. The penalization is represented by the parameter p. As the implicit reflected scheme, this scheme will be useful to prove the convergence of the explicit reflected scheme. For all j in {0, • • • , n -1} we have

     y p,n j = y p,n j+1 + g(t j , y p,n j , z p,n j , u p,n j )δ + a p,n j -k p,n j -(z p,n j √ δe n j+1 + u p,n j η n j+1 + v p,n j µ n j+1 ), a p,n j = pδ(y p,n j -ξ n j ) -, k p,n j = pδ(ζ n j -y p,n j ) -, y p,n n := ξ n n .
(3.10) Following (3.3), the triplet (z p,n j , u p,n j , v p,n j ) can be computed as follows

     z p,n j = 1 √ δ E(y p,n j+1 e n j+1 |F n j ), u p,n j = 1 κn(1-κn) E(y p,n j+1 η n j+1 |F n j ), v p,n j = 1 κn(1-κn) E(y p,n j+1 µ n j+1 |F n j ).
Taking the conditional expectation w.r.t. F n j in (3.10), we get

           y p,n j = (Ψ p,n ) -1 (E(y p,n j+1 |F n j )), a p,n j = pδ(y p,n j -ξ n j ) -; k p,n j = pδ(ζ n j -y p,n j ) -, z p,n j = 1 √ δ E(y p,n j+1 e n j+1 |F n j ), u p,n j = 1 κn(1-κn) E(y p,n j+1 η n j+1 |F n j ),
where Ψ p,n (y) = y -g(jδ, y, z p,n j , u p,n j )δ -pδ(y -ξ n j ) -+ pδ(ζ n j -y) -. We also introduce the continuous time version (Y p,n t , Z p,n t , U p,n t , A p,n t , K

E T 0 |Y p,n s -Y s | 2 ds + E T 0 |Z p,n s -Z s | r ds + E T 0 |U p,n s -U s | r ds = 0. (3.12) Moreover, Z p,n (resp. U p,n ) weakly converges in H 2 to Z (resp. to U ) and for 0 ≤ t ≤ T , α p,n ψ n (t) converges weakly to α t in L 2 (F T ) as n → ∞ and p → ∞, where (ψ n ) n∈N is a one-to-one random map from [0, T ] to [0, T ] such that sup t∈[0,T ] |ψ n (t) -t| ----→ n→∞ 0 a.s..

Convergence result

We prove in this Section that Θ n converges to Θ := (Y t , Z t , U t , A t -K t ) 0≤t≤T , the solution to the DRBSDE (1.1). The main result is stated in the following Theorem.

Theorem 4.1. Suppose that Assumption 2.5 holds and g is a Lipschitz driver satisfying Assumption 2.4.

Then we have

lim n→∞ E T 0 |Y n t -Y t | 2 dt + T 0 |Z n t -Z t | 2 dt + T 0 |U n t -U t | 2 dt = 0.
Moreover, α n ψ n (t) converges weakly to α t in L 2 (F T ).

Proof. To prove this result, we split the error in three terms. The first one is the error Θ n -Θ n , the second one is Θ n -Θ p,n , where Θ p,n := (Y p,n , Z p,n , U p,n , A p,n -K p,n ) represents the solution given by the implicit penalization scheme (see (3.11)), and the third error term is Θ p,n -Θ, whose convergence has already been proved in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF]. The result on the convergence of Θ p,n to Θ is recalled in Theorem 3.5.

We have the following inequality for the error on Y (the same inequality holds for the errors on Z and U )

E[ T 0 |Y n t -Y t | 2 dt] ≤ 3E[ T 0 |Y n t -Y n t | 2 dt] + 3E[ T 0 |Y n t -Y p,n t | 2 dt] + 3[ T 0 |Y p,n t -Y t | 2 dt].
For the increasing processes, we have:

E[|α n ψ n (t) -α t | 2 ] ≤ 3 E[|α n ψ n (t) -α n ψ n (t) | 2 ] + E[|α n ψ n (t) -α p,n t | 2 ] + E[|α p,n t -α t | 2 ] . ( 4
N 0 := 4T (1 + C g + C 2 g + C 2 g e 2λT λ
). The rest of the Section is organized as follows: Section 3.3 recalls the implicit penalization scheme introduced in [START_REF] Dumitrescu | Numerical approximation of doubly reflected BSDEs with jumps and RCLL obstacles[END_REF] and the convergence of Θ p,n -Θ, we give some intermediate results in Section 4.1 and we prove the convergence of Θ n -Θ n (see Proposition 4.5) and the convergence of Θ n -Θ p,n (see Proposition 4.6) in Section 4.2.

Intermediate results

In this Section we state two intermediate results useful for Section 4.2.

Lemma 4.3. Under Assumption 2.5 we have

sup j E[|y n j | 2 ] + E   δ n-1 j=0 |z n j | 2 + κ n (1 -κ n ) n-1 j=0 |u n j | 2 + 1 δ n-1 j=0 |a n j | 2 + 1 δ n-1 j=0 |k n j | 2   ≤ c.
Proof. Since ξ n j ≤ y n j ≤ ζ n j , Assumption 2.5 gives sup j E(|y n j | 2 ) ≤ c. Let us deal with z n j and u n j . To do this, we apply Lemma B.1 with i 0 = i and i 1 = i + 1 to the process y n and we sum the equality from i = j to i = n. We get:

E[|y n j | 2 ]+δ n-1 i=j E[|z n i | 2 ] + κ n (1 -κ n ) n-1 i=j E[|u n i | 2 ] ≤E[|ξ n n | 2 ] + 2δ n-1 i=j E[y n i g(t i , y n i , z n i , u n i )] + 2 n-1 i=j E[y n i a n i ] -2 n-1 i=j E[y n i k n i ], ≤E[|ξ n n | 2 ] + δ n-1 i=j g(t i , 0, 0, 0) 2 + δ 1 + 2C g + 2C 2 g + 2C 2 g δ κ n (1 -κ n ) n-1 i=j E[|y n i | 2 ] + δ 2 n-1 i=j E[|z n i | 2 ] + κ n (1 -κ n ) 2 n-1 i=j E[|u n i | 2 ] + 2δ α n-1 i=j E(|y n i | 2 ) + α δ n-1 i=j E(|a n i | 2 ) + α δ n-1 i=j E(|k n i | 2 ). Since ξ n i ≤ y n i ≤ ζ n i , we get a n i ≤ E(ξ n i+1 |G n i ) + δg(t i , ξ n i , z n i , u n i ) -ξ n i -= δ(b ξ ti + g(t i , ξ n i , z n i , u n i )) -, (4.2)
k n i ≤ E(ζ n i+1 |G n i ) + δg(t i , ζ n i , z n i , u n i ) -ζ n i + = δ(b ζ ti + g(t i , ζ n i , z n i , u n i )) + .
Then, using the Lipschitz property of g gives

α δ n-1 i=j E(|a n i | 2 ) ≤ 5αδ n-1 i=j E[|b ξ i | 2 + |g(t i , 0, 0, 0)| 2 + C 2 g (|ξ n i | 2 + |z n i | 2 + |u n i | 2 )], (4.3)
and the same result holds for

α δ n-1 i=j E(|k n i | 2 )
. By Using Assumption 2.5 and the inequality sup i E(

|y n i | 2 ) ≤ c, we get δ n-1 i=j E[|z n i | 2 ] + κ n (1 -κ n ) n-1 i=j E[|u n i | 2 ] ≤ c + δ 1 2 + 10αC 2 g n-1 i=j E(|z n i | 2 ) + κ n (1 -κ n ) 1 2 + 10αC 2 g δ κ n (1 -κ n ) n-1 i=j E(|u n i | 2 ). Since δ (1-κn)κn = 1 λ λδ
(1-e -λδ )e -λδ and e x ≤ xe 2x e x -1 ≤ e 2x , we get

δ (1-κn)κn ≤ 1 λ e 2λT . Then, by taking α = 1 40C 2 g (λe -2λT ∧ 1), we get δ n-1 i=j E[|z n i | 2 ] + κ n (1 -κ n ) n-1 i=j E[|u n i | 2 ] ≤ c. Plugging this result in (4.3) ends the proof.
The same type of proof gives the following Lemma Lemma 4.4. Under Assumption 2.5, we have

sup j E[|y n j | 2 ] + E   δ n-1 j=0 |z n j | 2 + κ n (1 -κ n ) n-1 j=0 |u n j | 2 + 1 δ n-1 j=0 |a n j | 2 + 1 δ n-1 j=0 |k n j | 2   ≤ c.

Proof of the convergence of Θ

n -Θ n and Θ n -Θ p,n Proposition 4.5. Assume that Assumption 2.5 holds and g is a Lipschitz driver. We have

lim n→∞ sup 0≤t≤T E[|Y n t -Y n t | 2 ] + E[ T 0 |Z n s -Z n s | 2 ds] + E[ T 0 |U n s -U n s | 2 ds] = 0. (4.4) Moreover, lim n→∞ (α n t -α n t ) = 0 in L 2 (F t ), for t ∈ [0, T ].
Proof. Let us consider y n j , the solution of the discrete implicit reflected sheme (3.6) and y n j , the solution of the explicit reflected scheme (3.8). We compute |y n j -y n j | 2 , we take the expectation and we get:

E[|y n j -y n j | 2 ] ≤E[|y n j+1 -y n j+1 | 2 ] -δE[|z n j -z n j | 2 ] -κ n (1 -κ n )E[|u n j -u n j | 2 ] + 2δE[(y n j -y n j )(g(t j , y n j , z n j , u n j ) -g(t j , E[y n j+1 |F n j ], z n j , u n j ))] -E δ(g(t j , y n j , z n j , u n j ) -g(t j , E[y n j+1 |F n j ], z n j , u n j )) + (a n j -a n j ) -(k n j -k n j ) 2 + 2E[(y n j -y n j )(a n j -a n j )] -2E[(y n j -y n j )(k n j -k n j )], ≤ E[|y n j+1 -y n j+1 | 2 ] -δE[|z n j -z n j | 2 ] -κ n (1 -κ n )E[|u n j -u n j | 2 ] + 2δE[(y n j -y n j )(g(t j , y n j , z n j , u n j ) -g(t j , E[y n j+1 |F n j ], z n j , u n j ))].
The last inequality comes from (y n j -y n j )(a n j -a n j ) ≤ 0 and (y n j -y n j )(k n j -k n j ) ≥ 0 (this ensues from the third and fourth lines of (S 1 ) and (S 1 )). Taking the sum from j = i to n -1 we get

E[|y n i -y n i | 2 ]+δ n-1 j=i E[|z n j -z n j | 2 ] + κ n (1 -κ n ) n-1 j=i E[|u n j -u n j | 2 ] ≤ 2δ n-1 j=i E[(y n j -y n j )(g(t j , y n j , z n j , u n j ) -g(t j , E[y n j+1 |F n j ], z n j , u n j ))], ≤ 2δC g n-1 j=i E |y n j -y n j ||y n j -E[y n j+1 |F n j ]| + 2δC 2 g 1 + δ κ n (1 -κ n ) n-1 j=i E[|y n j -y n j | 2 ] + δ 2 n-1 j=i E[|z n j -z n j | 2 ] + κ n (1 -κ n ) 2 n-1 j=i E[|u n j -u n j | 2 ]. (4.5)
Since

y n j -E[y n j+1 |F n j ] = y n j -y n j + y n j -E[y n j+1 |F n j ] = y n j -y n j + δg(t j , E[y n j+1 |F n j ], z n j , u n j ) + a n j -k n j , we get 2δC g E |y n j -y n j ||y n j -E[y n j+1 |F n j ]| ≤ (2C g + 1)δE[|y n j -y n j | 2 ] + C 2 g δE j , E[y n j+1 |F n j ], z n j , u n j )| + |a n j | + |k n j | 2 .
Plugging the previous inequality in (4.5) and using Lemma 4.4 gives

E[|y n i -y n i | 2 ] + δ 2 n-1 j=i E[|z n j -z n j | 2 ]+ κ n (1 -κ n ) 2 n-1 j=i E[|u n j -u n j | 2 ] ≤ 1 + 2C g + 2C 2 g + 2C 2 g δ κ n (1 -κ n ) δ n-1 j=i E[|y n j -y n j | 2 ] + cδ 2 .
Let n be bigger than N 0 , then δ 1 + 2C g + 2C (4.4). The convergence of (

A n -K n ) -(A n -K n ) ensues from A n t -K n t = Y n 0 -Y n t - t 0 g(s, Y n s , Z n s , U n s )ds + t 0 Z n s dW n s + t 0 U n s d Ñ n s , A n t -K n t = Y n 0 -Y n t - t 0 g(s, Y n s , Z n s , U n s )ds + t 0 Z n s dW n s + t 0 U n s d Ñ n s ,
from the Lipschitz property of g and from (4.4).

Proposition 4.6. Assume that Assumption 2.5 holds and g is a Lipschitz driver. For n ≥ N 0 , we get

sup 0≤t≤T E[|Y n t -Y p,n t | 2 ] + E[ T 0 |Z n s -Z p,n s | 2 ds] + E[ T 0 |U n s -U p,n s | 2 ds] ≤ c √ p . (4.6) Moreover, ∀ t ∈ [0, T ], E[|α n t -α p,n t | 2 ] ≤ c √ p .
Proof. Let us first prove (4.6). From (3.6), (3.10) and Lemma B.1 applied to the process (y n -y p,n ) following the beginning of the proof of Lemma 4.3, we get

E|y n j -y p,n j | 2 + δ n-1 i=j E|z n i -z p,n i | 2 + (1 -κ n )κ n n-1 i=j E[|u n i -u p,n i | 2 ] + (1 -κ n )κ n n-1 i=j E[|v n i -v p,n i | 2 ] = 2 n-1 i=j E[(y n i -y p,n i )(g(t i , y n i , z n i , u n i ) -g(t i , y p,n i , z p,n i , u p,n i ))δ] + 2 n-1 i=j E[(y n i -y p,n i )(a n i -a p,n i )] -2 n-1 i=j E[(y n i -y p,n i )(k n i -k p,n i )].
Let us deal with the last two terms

(y n i -y p,n i )(a n i -a p,n i ) = (y n i -ξ n i )a n i -(y p,n i -ξ n i )a n i -(y n i -ξ n i )a p,n i + (y p,n i -ξ n i )a p,n i ≤ (y p,n i -ξ n i ) -a n i .
By using same computations, we derive

(y n i -y p,n i )(k n i -k p,n i ) ≥ -(y p,n i -ζ n i ) + k n i .
By using the Lipschitz property of g, we get

E[|y n j -y p,n j | 2 ] + 1 2 δE[|z n j -z p,n j | 2 ] + κ n (1 -κ n ) 2 E[|u n j -u p,n j | 2 ] ≤ 2C g + 2C 2 g + 2C 2 g δ κ n (1 -κ n ) δ n-1 i=j E[(y n i -y p,n i ) 2 ] + 2 n-1 i=j E[(y p,n i -ξ n i ) -a n i + (y p,n i -ζ n i ) + k n i ].
Using Cauchy-Schwarz inequality gives

E[|y n j -y p,n j | 2 ] + 1 2 δE[|z n j -z p,n j | 2 ] + κ n (1 -κ n ) 2 E[|u n j -u p,n j | 2 ] ≤ 2C g + 2C 2 g + 2C 2 g δ κ n (1 -κ n ) δ n-1 i=j E[(y n i -y p,n i ) 2 ] + 2   δ n-1 i=j E (y p,n i -ξ n i ) -2   1 2   1 δ n-1 i=j E[(a n i ) 2 ]   1 2 + 2   δ n-1 i=j E (y p,n i -ζ n i ) + 2   1 2   1 δ n-1 i=j E[(k n i ) 2 ]   1 2 , ≤ 2C g + 2C 2 g + 2C 2 g δ κ n (1 -κ n ) δ n-1 i=j E[(y n i -y p,n i ) 2 ] + 2 √ p   1 pδ n-1 i=j E[(a p,n i ) 2 ]   1 2   1 δ n-1 i=j E[(a n i ) 2 ]   1 2 + 2 √ p   1 pδ n-1 i=j E[(k p,n i ) 2 ]   1 2   1 δ n-1 i=j E[(k n i ) 2 ]   1 2
.

Since n ≥ N 0 , Lemma 4.3, Lemma A.1 and Gronwall inequality give (4.6). Concerning α n t -α p,n t we have

α n t -α p,n t =(Y n t -Y p,n t ) -(Y n 0 -Y p,n 0 ) - t 0 g(s, Y n s , Z n s , U n s ) -g(s, Y p,n s , Z p,n s , U p,n s )ds + t 0 (Z n s -Z p,n s )dW n s + t 0 (U n s -U p,n s )d Ñ n s .
It remains to take the square of both sides, then the expectation, and to use the Lipschitz property of g combining with (4.6) to get the result.

Numerical simulations

We consider the simulation of the solution of a DRBSDE with obstacles and driver of the following form:

ξ t := (W t ) 2 +2(1-t T ) Ñt + 1 2 (T -t), ζ t := (W t ) 2 +(1-t T )(( Ñt ) 2 +1)+ 1 2 (T -t), g(t, ω, y, z, u) := -5|y +z|+6u.
Table 1 gives the values of Y 0 with respect to n. We notice that the algorithm converges quite fast in n. Moreover, the computational time is low. are almost the same when n = 400 and p = 20000. The CPU times are also of the same order. The main advantage of the reflected scheme is that there is only one parameter to tune (n).

A Technical result for the implicit penalized scheme

In this Section, we use N 0 and c introduced in Definition 4.2.

Lemma A.1. Suppose Assumption 2.5 holds and g is a Lipschitz driver. For each p ∈ N and n ≥ N 0 we have

sup j E[|y p,n j | 2 ] + δ n-1 j=0 E[|z p,n j | 2 ] + κ n (1 -κ n ) n-1 j=0 E[|u p,n j | 2 ] + 1 pδ n-1 j=0 E[|a p,n j | 2 ] + 1 pδ n-1 j=0 E[|k p,n j | 2 ] ≤ c.
Proof. By applying Lemma B.1 to the process y p,n between i and i + 1 and by suming the equality from

B Some results on discrete stochastic calculus

In this section we present two lemmas which are used throughout the paper.

Lemma B.1. Consider two integers i 0 and i 1 in 0, ..., N and (y n ) n a discrete process. We have

y 2 i1 = y 2 i0 + 2y i0 (y i1 -y i0 ) + (y i1 -y i0 ) 2 .
The proof comes from the computation of ((b -a) + a) 2 , we omit it. A proof of this lemma can be found in [17, Lemma 2.2], so we omit it.

. 1 )Definition 4 . 2 (

 142 Then, combining Propositions 4.5, 4.6 and Theorem 3.5 yields the result. Definition of c and N 0 ). In this Section and in the Appendix, c denotes a generic constant depending on C g , g(•, 0, 0, 0) ∞ and C ξ,ζ,λ,T . N 0 is defined by

Figure 1 :

 1 Figure 1: One path of the Brownian motion for n = 400.

Figure 2 :Figure 3 :

 23 Figure 2: One path of the compensated Poisson process for λ = 5 and n = 400.

Finally, by taking| 2 ]

 2 α = β = 4C and by applying the Gronwall inequality (we recall n ≥ N 0 ), we get that: ≤ c.

Lemma B. 2 .

 2 (A discrete Gronwall lemma) Let a, b and α be positive constants, δb < 1 and a sequence (v j ) j=1,...n of positive numbers such that for every jv j + α ≤ a + bδ j i=1 v i .Then sup j≤n v j + α ≤ ae bT .

Definition 2.2 (

  Mokobodzki's condition). Let ξ, ζ be in S 2 . There exist two nonnegative RCLL supermartingales H and H in S 2 such that ∀t ∈ [0, T ], ξ t ≤ H t -H t ≤ ζ t a.s.

	The following Theorem states existence and uniqueness of solutions to (1.1) (see for e.g. [3, Proposition
	5.1]).

Theorem 2.3. Suppose

  ξ and ζ are RCLL adapted processes in S 2 such that for all t ∈ [0, T ], ξ t ≤ ζ t , Mokobodzki's condition holds and g is a Lipschitz driver. Then, DRBSDE (1.1) admits a unique solution (Y, Z, U, α) in S 2 × H 2 × H 2 × S 2 , where α := A -K, A and K in A 2 .

Table 1 :

 1 The solution y n at time t = 0

	n	10	20	50	100	200	300	400
	y n 0	1.2191	1.3238	1.3953 1.4167 1.4293 1.4332 1.4352
	CPU time 2.14 × 10 -4 1.5 × 10 -3 0.0211 0.1622 1.4230 5.2770 12.5635
	When we use the explicit penalized scheme introduced in [5], we get y p,n 0	= 1.4353 for n = 400 and
	p = 20000. The CPU time is 12.85s.
	Figures 1, 2 and 3 represent one path the Brownian motion, one path of the compensated Poisson process
	(with λ = 5) and the corresponding path of (y n i , ξ n i , ζ n i ) 1≤i≤n . We notice that for all i, y n i stays between the two obstacles. The values of y n 0 and y p,n 0

  i = i to i = n, we get E[|y p,n j | 2 ] + δ | 2 ] + κ n (1 -κ n ) | 2 ] + κ n (1 -κ n )

			n-1	E[|z p,n i n-1	E[|u p,n i n-1	E[|v p,n i | 2 ]
			i=j								i=j	i=j
												n-1	n-1
								≤ E[|ξ n n | 2 ] + 2		E[|y p,n i ||g(t i , y p,n i , z p,n i , u p,n i )δ|] + 2E[	(y p,n i a p,n i	-y p,n i k p,n i )].
													i=j	i=j
	Note that y p,n i a p,n i	= -1 pδ (a p,n i ) 2 + ξ n i a p,n i	and y p,n i k p,n i	= 1 pδ (k p,n i ) 2 + ζ n i k p,n i . We have that:
		E[|y p,n j | 2 ] +	δ 2	n-1 i=j	E[|z p,n i | 2 ] +	κ n (1 -κ n ) 2	n-1 i=j	E[|u p,n i | 2 ] +	1 pδ	n-1 i=j	E[|a p,n i | 2 ] +	1 pδ	n-1 i=j	E[|k p,n i | 2 ]
			≤ E[|ξ n n | 2 ] + δE[	n-1 i=j	|g(t i , 0, 0, 0)| 2 ] + 2δ 1 + 2C g + 2C 2 g +	2C 2 g δ κ n (1 -κ n )	n-1 i=j	E[|y p,n i | 2 ]
							n-1					n-1
			+ 2	E[(ξ n i )a p,n i ] -2	E[(ζ n i )k p,n i ].
							i=j					i=j
	We get 2	n-1 i=j E[(ξ n i )a p,n i ] ≤ αE(sup i |ξ n i | 2 ) + 1 α E	n-1 i=j a p,n i	2	and 2	n-1 i=j E[(ζ n i )k p,n i ] ≤ βE(sup i |ζ n i | 2 ) +
	1 β E	n-1 i=j k p,n i	2	. Following the same type of proof as [16, Lemma 2], we get
		 n-1	 2		 n-1			
	E		a p,n i			+ E		k p,n i	
			i=j					i=j

2 ≤ C(c + E[ n-1 i=j δ(|y p,n i | 2 + |z p,n i | 2 ) + κ n (1 -κ n )(|u p,n i | 2 + |v p,n i | 2 )].


Arbi El

Ileana Aboussoror
email: el-arbi.aboussoror@irit.fr

Iulian Ober
email: ileana.ober@irit.fr

Ober

Significantly Increasing the Usability of Model Analysis Tools through Visual Feedback

A plethora of theoretical results are available which make possible the use of dynamic analysis and model-checking for software and system models expressed in high-level modeling languages like UML, SDL or AADL. Their usage is hindered by the complexity of information processing demanded from the modeler in order to apply them and to effectively exploit their results. Our thesis is that by improving the visual presentation of the analysis results, their exploitation can be highly improved. To support this thesis, we define a trace analysis approach based on the extraction of high-level semantics events from the low-level output of a simulation or model-checking tool. This extraction offers the basis for new types of scenario visualizations, improving scenario understanding and exploration. This approach was implemented in our UML/SysML analyzer and was validated in a controlled experiment that shows a significant increase in the usability of our tool, both in terms of task performance speed and in terms of user satisfaction.

Introduction

A plethora of theoretical results are available which make possible the use of dynamic analysis and model-checking for software and system models expressed in high-level modeling languages UML [START_REF]Object Management Group: Unified Modeling Language[END_REF], SDL [2] or AADL [START_REF]SAE International: SAE Architecture Analysis & Design Language (AADL) AS5506 Rev.B[END_REF]. These results have the virtue of allowing reasoning at the level of models instead of code, making possible early verification and validation, while taking advantage of the abstract nature of modeling languages. Unfortunately, the use of these advanced techniques is not as widespread as their capabilities could justify. One reason for this is that such techniques are often inaccessible to modelers with a basic software engineer training, as it demands advanced knowledge of these techniques and a high investment in learning the specificities of tools in order to apply them and to effectively exploit their results. Our thesis is that by improving the visual presentation of the analysis results, their exploitation by regular users can be highly improved. To support this thesis, we defined a trace analysis approach and we integrated it in Metaviz, a model-driven framework for simulation trace visualization introduced earlier in [START_REF] Aboussoror | Seeing Errors: Model Driven Simulation Trace Visualization[END_REF].

The typical functioning of a model-based formal analysis tool, consists in mapping the semantics of the high-level modeling language into a simpler language, more well-suited for formal analysis. Most of the time this language has a sound formal semantics that allows reasoning on the model and on its properties, using analysis tools. It is the case of vUML [START_REF] Lilius | vUML: A tool for verifying UML models[END_REF] that uses Promela [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF], of IFx-OMEGA [START_REF] Ober | OMEGA2 -A new version of the profile and the tools[END_REF], that uses IF [START_REF] Bozga | The IF toolset[END_REF], etc. This change of context is in general not supported by a bi-directional mapping to and from the formal language, since the goal is to represent a complex modeling language with a limited set of primitives available in the formal language. Thus, the structure of a model may be very different between the two levels, and analysis results such as execution traces obtained from the lower-level model may be hard to interpret by a user whose knowledge is limited to the upper-level language and model. The trace analysis method is based on the extraction of high-level semantics events from basic events of the underlying semantics. It offers the basis for new types of scenario visualizations, improving the model execution understanding and exploration.

In order to validate these assertions we set up a controlled experiment that shows a significant increase in our model checking tool usability, both in terms of task performance speed and in terms of user satisfaction.

The rest of this paper is organized as follows: we start by an overview of existing methods for executable UML/SysML analysis, and by discussing why exploiting analysis results is challenging. Then we present the typical analysis tool integration pattern and finally describe our approach for extending the verification platform with trace analysis support. The evaluation of the new tool is detailed and discussed in Section 3.

Translational Semantics Approaches to Model Analysis

To be useful (not only descriptive) models need to have a well defined semantics. Among other advantages, formal definition of semantics provides the possibility to do analysis earlier in the design process. For example non-functional properties such as performance, schedulability or safety can be analyzed. For this purpose, mature formalisms and associated analysis techniques and tools already exist (Petri nets, queuing networks, Markov chains, etc.).

For Model Driven Engineering, the approach usually followed is to:

1. annotate the original models (e.g. UML [START_REF] Espinoza | Annotating UML Models with Non-Functional Properties for Quantitative Analysis[END_REF]), 2. generate input artifacts for a formal analysis tool, and finally 3. perform analysis activities on the generated artifacts.

Target analysis formalisms can be process algebra, timed automata, queuing networks etc. Some examples of tools working in this way are IFx-OMEGA [START_REF] Conquet | Formal Model Driven Engineering for Space Onboard Software[END_REF], vUML [START_REF] Lilius | vUML: A tool for verifying UML models[END_REF] or OPTIMUM [START_REF] Mraidha | Optimum -a MARTE-based Methodology for Schedulability Analysis at Early Design Stages[END_REF].

Even if these model analysis techniques, called translational semantics approaches, are widely adopted in the industry they still suffer from limitations. Translational semantics approaches to model analysis bring a new complexity to the end user. The analysis results (e.g. model checking counterexamples) are not easily understood by the domain user. This is due to the gap between the two semantic levels: the original one and the target analysis formalism. Those results necessitate expertise in the low level analysis semantics. To enable a usable approach to model analysis a translation of the low level results to a more user friendly abstraction should take place in the process.

General Schema for Analysis Tool Integration

Analyzing models is assessing some properties of them. For example UML offers an extension mechanism, namely profiles that enable building a language to express non-functional properties. This approach offers a clear advantages like the reuse of the tools and techniques available for UML. Two well known examples are SPT and MARTE profiles. UML Profiles are integrated with analysis tools using the basic architecture described in Fig. 1. In this architecture model transformations are used to fill the gap between UML modeling technical space and the analysis technical space. This semantic gap is at the heart of the diagnostic problem described in the previous section1.1.

Extending a Verification Platform with Trace Analysis Support

IFx-OMEGA1 platform integrates a compiler, a simulator and model-checker for a rich subset of UML and SysML [START_REF] Ober | OMEGA2 -A new version of the profile and the tools[END_REF]. The toolset relies on the automatic translation of models into a lower-level language (named IF) based on asynchronous communicating extended timed automata, and on the use of the extensive toolset available for this language [START_REF] Bozga | The IF toolset[END_REF]. The validation acts on a UML or SysML model, which is first translated to an IF model, and then compiled2 to an executable program that will be used for automatic verification and interactive simulation.

Fig. 2. Generic architecture for extracting high-level events from analysis results using a Result Converter. It is composed of an Event Adapter for generating relevant events from an operational semantics and an Event Processor Agent that translates those events to user level events.

The IFx validation approach has been applied to several industry-grade models such as Ariane-5 [START_REF] Ober | Modeling and Validation of a Software Architecture for the Ariane-5 Launcher[END_REF], MARS [START_REF] Ober | Timing Analysis and Validation with UML -the case of the embedded Mars bus manager[END_REF] and SGS [START_REF] Conquet | Formal Model Driven Engineering for Space Onboard Software[END_REF], and has proven to be very effective in discovering design issues. As an application to this approach we propose to extend the IFx-OMEGA platform. The extension transforms low-level semantics analysis result. Figure 2 shows the architecture of this extension. The automatic verification and the simulation activities generates execution scenarios as analysis results. Those scenarios are expressed using the low-level semantics used by the IF model checker. The extension we propose translates the relevant information from the scenarios into a high-level like formalism syntax. To extend the IFx-OMEGA platform with result analysis facility we follow the generic architecture proposed in [START_REF]Official reference MARTE Tutorial[END_REF] and depicted in Fig. 1.

Extracting Execution Events Using Model Differences

The generic architecture has to be refined to enable a flexible and extensible implementation. We choose to take an event based approach to report the analysis results. The design rationale behind this choice is the decoupling introduced by this approach and its adequacy to our context. Indeed an event reports changes in monitored states [START_REF] Etzion | Event Processing in Action[END_REF] and since we are in the context of translating UML models to an operational semantics we have this notion of state changes within the execution model. Those state changes are captured using a model difference mechanism [START_REF] Lin | DSMDiff -a differentiation tool for domain-specific models[END_REF] and the difference model is then transformed into a set of events by an event generator. Those events report what has occurred in the analysis results (e.g. state changes, message passing, . . . ). An example is shown in Fig. 3. This figure shows an original trace on the left (an XML file loaded in an tree-based view) alongside the extracted event. The event showed on the right correspond to the computed difference between two configurations of the system in the trace. In the example the difference between the system configurations (from step 15 to 16) is a state change of the Model_EVC instance from Waiting status to Started.

Fig. 3. Extracting execution events using model differences. State changes are captured using a model difference mechanism, the difference model is transformed into a set of events by an event generator.

Abstracting Execution Events to High-Level Semantics Events

Once the relevant execution events are extracted we have a clear view on what has changed in the execution semantics. But still, we needed a translation step to make the analysis results expressed in the high-level semantics. For this step we use an Event Processor Agent [START_REF] Etzion | Event Processing in Action[END_REF] implemented as a model transformation from low-level analysis results to a high-level set of events. Those events can be easily understood by the user and embed relevant concepts from the high-level design model. High-level events can constitute a base for reporting the analysis results directly into the user models or for animating a part of the original specification.

The two transformation rules in Listings 1.1 and 1.2 show an excerpt of the ATL transformation that abstracts execution events to high level events. The first rule transforms each IF process state change event into an OMEGA state enter event.

The second rule extracts OMEGA send events from IF enqueue events.

Interpreting High-Level Semantics Events

After abstracting execution events we get a set of high-level semantics events. High-level events gather state changes that can be easily understood by the user. The last step in the proposed process is the visual interpretation of the analysis results that is now transformed into high-level events. End user visualizations has to be carefully designed to help the user grasping the event information without visual effort. More on this point can be found in our previous work [START_REF] Aboussoror | Seeing Errors: Model Driven Simulation Trace Visualization[END_REF]. Figure 4 shows graphical rendering of OMEGA state enter event extracted from IF process state change event.

Evaluation

In order to assess the advantages and limitations of the new visualization, we need to evaluate its usage. Several techniques can be used for such an evaluation. Some of these are purely subjective, while others use an objective and quantitative approach [START_REF] Dix | Human-Computer Interaction[END_REF]. Moreover, evaluation techniques can be categorized according to the stakeholders: techniques such as cognitive walk-through or heuristic evaluation involve human factors experts, while observational or experimental techniques rely on user participation.

The premier goal in our study is to make our model analysis tool more accessible to a wider audience. Today, the overwhelming majority of modelers are not familiar with analysis techniques such as model checking. In order to assess whether we have achieved our premier goal, we need to evaluate the approach on a sample of users compliant with this profile. Therefore, due to its objective and quantitative orientation, we decided to use a controlled experiment that involves user participation. However, since this technique does not provide a detailed user impression and satisfaction overview, we complement our validation with a subjective approach, by means of a questionnaire technique based on the System Usability Scale [START_REF] Brooke | SUS -A quick and dirty usability scale[END_REF].

Defining Formal Methods Usability

Before defining the hypothesis and designing an experiment, we need to understand the notion of usability in the context of formal analysis techniques. The ISO standard definition [START_REF]1998 Ergonomic requirements for office work with visual display terminals (vdts) part 11 -Guidance on usability[END_REF] for usability, defines it as: "the extent to which a system, product or service can be used by specified users to achieve specified goals with effectiveness, efficiency and satisfaction in a specified context of use."

To customize the usability definition in our context, we need to set its three characteristics -effectiveness, efficiency and satisfaction -in the context of formal methods:

-Effectiveness is the ability of users to understand, find and correct errors reported by the analysis process. -Efficiency is the time and cognitive effort needed to perform each of the three above-mentioned tasks. -Satisfaction is the subjective impression the users get after using the integrated tool suite that supports the three task.

Hypotheses Formulation

As mentioned above, our goal is to increase analysis tools usability. To achieve this goal, we propose to enhance tools with visualization techniques. Thus we can formulate the following hypothesis: H. Effectively supporting the user in understanding model analysis results, will increase the analysis tool usability.

The notion of analysis tool usability was defined in the previous section. Based on this, our hypothesis H can be further refined: H1. Participants using the new tool extension will spent less time understanding the trace. H2. Participants using the new tool extension will have a better understanding of the trace. H3. Participants using the new tool extension will spent less time locating the error in the trace. H4. Participants using the new tool extension will locate the error in the trace with more precision. H5. Participants using the new tool extension will spent less time understanding the error cause(s). H6. Participants using the new tool extension will have better understanding of the error cause(s).

These refined hypothesis will allow more insights into the experiment results.

Experiment Design

In this section we will go further with the experiment design, by defining several of its characteristics. The terminology used in this section is the one defined in [START_REF] Juzgado | Basics of Software Engineering Experimentation[END_REF].

Participants. Participants were chosen from Master and PhD students from the University of Toulouse. The experiment was conducted with 10 subjects distributed in two groups, the experimental group (group A in next sections) and the control group (group B). All the participants were already familiar with UML, two of them have already used a formal analysis tool, but none of them has used ours. In order to assess their adequacy with the user population, participants were asked to fill a questionnaire. The questionnaire has 7 parts and 12 questions such as education level, experience with modeling, and verification techniques abilities. In the first group technical experience median is 4, mean is 4,4 and standard deviation is 1.67. In the second group mean is 4.6 with a median 4, the standard deviation is 1.52.

Experimental Unit. Participants were asked to visualize the execution trace of a small OMEGA UML model representing an Electronic Valve Controller.

A timed constraint was set on the model. The OMEGA model is then used as input for the IF Model Checker. Since the model was intentionally violating the constraint, the model checker generated a counterexample. The model was built to get a representative counterexample of what a modeler would get from using the IFx-OMEGA toolbox. Participants will explore this counterexample and perform some well defined tasks.

Experimental Variable. It corresponds to the software product used by the participant to explore the analysis results. We consider the Metaviz [START_REF] Aboussoror | Seeing Errors: Model Driven Simulation Trace Visualization[END_REF] tool being the experimental unit. It offers support for IF traces exploration alongside with elaborate visualizations. Figure 5 presents a screen shot of the trace analysis support. The right panel contains the error trace browser, which is similar to what is available in other analysis tools. The middle panel contains the trace visualization feature that we added.

Factors. Also called independent variables, are those we are going to manipulate in the participants environment to see how other variables (response variables) are affected. Our experiment has the goal to analyze how a better support for the users would affect their understanding of the model analysis results. Thus we run the experiment with a two-level factor: Metaviz with elaborate trace visualization support activated and deactivated. Consequently we have the following levels: level 1: only basic Metaviz views are activated level 2: advanced visualization is activated

Response Variables. They correspond to the experimental aspects impacted.

To investigate their quantitative values we have designed a set of user tasks distributed in three categories. Each category corresponding to a response variable. The categories are related to the following cognitive tasks: For each category we assess two characteristics: the speed and the quality.

Tasks. The set of tasks each participant has to perform was designed to cover the understanding of the trace, the error and its cause. Each participant was given a set of 7 tasks to perform using the trace analysis tool. Additionally, the time spent by each participant performing a task is monitored with an external stopwatch application. We do not take into account the time spent by the participant writing down the answers. The table 1 gives an overview of the tasks.

Results

The goal of our experiment is to see whether extending an analysis tool with the event-based visualization mechanism described previously would improve analysis results exploitation. Figures 6 and7 show the results for each task, in terms of time and success rate. Participants that use the Metaviz extension belong to the group A (experimental group) , while group B (control group) corresponds to participants using the basic version of the tool (i.e. without the Metaviz extension).

Time Spent in Each Task. Results for tasks T1 and T2 show that participants in the group A perform 5 times faster than the group B participants.

For task T3 they perform 8 times faster, while for the last set of tasks T5 to T7 they perform 2 times faster. The overall unbalanced improvement rate is therefore of 400%. This important increase in task performance speed is due to the cognitive nature of each task category. For instance, one can notice that the experimental group group A was 8 times faster in performing the task T3. This task is the most demanding in cognitive workload for the participants. Indeed, it asks participants to find the step in the trace where a certain instance enters a particular state. The participant has to recall the instance and state names while he goes step by step through the whole trace. This is where we can see the power of having a visualization that presents only what has changed in the trace. The Metaviz visualizations focus on the state change of the relevant instance and filter other irrelevant information. Figure 5 shows the basic visualization alongside the elaborate one. The visual vocabulary used is highly intuitive and thus enabled the control group to perform the task T3 8 times faster.

Quality. Concerning success rates, results revealed an increase of the participant's answers quality. Results for understanding the trace (task T1 to T3 ) show that understanding of the instances interactions (i.e. message passing) is 25% better. For locating the error (task T4 ) the improvement is about 9%. For the last cognitive category, namely understanding the cause the improvement is of 40%. Figure 7 shows the success rate for each task. To complement our analysis we have run a questionnaire based evaluation. This evaluation assessed the user satisfaction. For this purpose we relied on the System Usability Scale test [START_REF] Brooke | SUS -A quick and dirty usability scale[END_REF]. We have chosen this analysis method since it is lightweight and reliable [START_REF] Stanton | Human Factors Methods -A Practical Guide for Engineering and Design[END_REF]. Results for user satisfaction are slightly higher for 2 show an increase of about 11% of the user satisfaction.

Hypothesis Tests

The null hypothesis corresponding to each hypothesis formulated previously can be summarized by there is no difference between participants that use the elaborate visualization and those who use the basic one in performing the tasks from the category CTx. Were CTx is one of the three cognitive task categories listed in 1. As mentioned previously task performance is measured with the speed and quality of three cognitive task types (i.e. understanding a trace, locating an error, understanding its causes). As we describe in section 3.

Threats to Validity

Threats related to the conclusion. We have used statistical test, namely Student's t test. Our samples has the same number of individuals and similar variances which ensure the soundness of the test conclusions. Construct threats. The role of the trace abstractions is to reduce the amount of data to a relevant set of information for a specific user task, this avoid the cognitive overload. The visualization has a different role. It brings to the user these relevant information in a domain oriented way, that is, in terms of concepts already known by the user. No additional effort is needed from the user to understand the notations and semantics of the visualization constructs (perception overload). The visualization alone is not enough, this is why the control group (that uses a basic visualization of the low-level traces) has the worst results. The huge amount of data gathered to the user in a basic view (without abstraction) is cognitively demanding and time consuming. Internal threats: The statistics shown in the section 3.3 ensures that there's is no significant difference in the participants technical level. External threats: While used with a small model, the technique is more likely to accelerate user exploring and understanding for bigger models. We think that for experts, the results may not be as significant as for users with average technical background. But we should be careful of this generalization, the expertise reversal effect as coined by Sweller [START_REF] Sweller | Evolution of human cognitive architecture[END_REF] may arise. Thus, further experiments should be conducted to assess the results for expert users.

Related Work

Early work in analyzing UML models like [START_REF] Bozga | The IF toolset[END_REF][START_REF] Espinoza | Annotating UML Models with Non-Functional Properties for Quantitative Analysis[END_REF] set among others the foundations of model-driven analysis. Recent work on the MARTE profile [START_REF] Mraidha | Optimum -a MARTE-based Methodology for Schedulability Analysis at Early Design Stages[END_REF] introduces the use of user feedback in an integrated MDE approach. Results of MARTE [START_REF]The UML Profile for MARTE[END_REF] models analysis is used to annotate back the original user models. The RT-Simex research project [START_REF] Deantoni | RT-SIMEX -Retro-analysis of execution traces[END_REF] tackles the problem of user feedback with an elaborate user interface. This is very similar to our approach but the work focuses on clock reconciliation between independent traces and no controlled experiment is conducted to assess the effectiveness of the user feedback. In the work of [START_REF] Yokoyama | User-friendly GUI in Software Model Checking[END_REF] an emphasis is put on the lack of user friendly interfaces in model checkers. They effectively address the problem of understanding analysis results but directly at the low level semantics. A broader view to the issue of designing SE notations is addressed by Moody [START_REF] Moody | The "Physics" of Notations: Toward a scientific basis for constructing visual notations in software engineering[END_REF]. He emphasizes the lack of foundational work on the syntax of software engineering visual notation. Combemale et al. adressed the problem of extracting high-level traces from low-level executions in [START_REF] Combemale | A Generic Tool for Tracing Executions Back to a DSML's Operational Semantics[END_REF]. They show how to extract high level trace from low level traces. They also assume an existing execution model for the high-level formalism and editors. Our work emphasize the importance and the effectiveness of the user feedback but go further by validating the added value in a controlled experiment.

Conclusion and Future Work

Today's integrated development environments offer many debugging facilities, that allow the developer to follow closely the code execution, to debug it and to understand it. While modeling languages aim at raising the level of abstraction in software development and could support much more powerful analysis techniques, the tools existing to support them are still difficult to use [START_REF] Hutchinson | Empirical Assessment of MDE in Industry[END_REF]. Using languages such as UML, SysML, SDL, to model the software, performing model-based analysis on these models and understanding the analysis results is still a challenging task. Improving the existing tools and mechanisms for exploring and understanding model based analysis results is greatly needed for a larger adoption of formal methods. This paper presents our contribution in this direction. Our approach provides a semi-automatic technique to implement a feedback mechanism in a SysML/UML translational semantics approach. Based on an existing SysML/UML tool that offers the possibility to perform verification, we develop an advanced and flexible trace analysis support mechanism. As described in this paper, this mechanism allows the analyst to reason at model level on the model execution, in terms of easily understandable high-level events. The pertinence of our approach is assessed through an evaluation, based on well established evaluation mechanisms (Usability Scale System, ISO notion of usability, etc). In order to perform such an evaluation, we needed to adapt the notion of usability to the context of formal methods usability, and to adapt the evaluation process to our setting. The goal of this experiment was to see whether extending analysis tools with a well designed event-based visualization would improve analysis results exploitation and the results are meeting our expectations. Several directions could be taken for future work. Beyond improving the existing approach/toolset, we intend to add new visualization techniques, based on specific tasks to be performed during the analysis (variable change impact, queue size evolution, etc), to identify new kinds of user profile based visualizations that may assist the user, depending on its level of expertise, to perform new experiments with different user profiles, etc. We strongly believe that by facilitating the access to analysis tools by regular users, the interest in using modeling techniques could significantly increase and the much advertised advantages of these techniques could finally get accessible to a larger panel of users.

Fig. 1 .

 1 Fig. 1. Generic approach for analysis results exploitation. The annotated model is translated to a formal model for analysis. Results are then showed to the end user in a visual interpreter.

Fig. 4 .

 4 Fig. 4. Graphical rendering of high-level events. The Event Visual Interpreter executes a model transformation to generate the input model for the visual renderer.

Fig. 5 .

 5 Fig. 5. Metaviz with the full support for trace analysis

Fig. 6 .

 6 Fig. 6. Time (in secondes) to perform each task. Participants that use an elaborate visualization perform tasks 4 times faster. A: experimental group, uses an elaborate visualization B: control group, uses a basic visualization

Fig. 7 .

 7 Fig. 7. Success rate for each task.Participants that use an elaborate visualization produce task outputs of a better quality. A: experimental group, uses an elaborate visualization B: control group, uses a basic visualization

  Listing 1.2. ATL rule for extracting OMEGA message sending events

	StateChangeE vt2State E nte rE vent extends TraceEvent2OmegaEvent {
	from
	sEvt : IFTraceEB ! StateChangeEvt
	to
	tEvt : OmegaTraceEB ! S t a t e E n t e r E v e n t (
	className <-sEvt . i n s t a n c e . type ,
	name <-sEvt . i n s t a n c e . p i d . name ,
	stateName <-sEvt . newState . name ,
	oldStateName <-sEvt . o l d S t a t e . name
	)
	}
	Listing 1.1. ATL rule for extracting OMEGA object state entering events
	rule EnqueueEvt2SendEvent extends TraceEvent2OmegaEvent {
	from
	sEvt : IFTraceEB ! EnqueueEvt
	u s i n g {

mes : IFTraceEB ! Message = sEvt . m e s s a g e s -> f i r s t ( ) ; } to tEvt : OmegaTraceEB ! SendEvent ( s i g n a l <-mes . s i g n a l T y p e , by <-thisModule . p i d 2 O b j e c t ( mes . " from " ) . . . }

Table 1 .

 1 Task per each cognitive category. Participants were asked to perform a set of tasks that spans three cognitive task types.

	Cognitive Types	Tasks
	Trace Understanding 1. What are the instances created during
		this execution and at what step
		2. What are the exchanged messages,
		at what step and between which instances
		3. At which step of the trace, the instance
		Model_Valve enters the state Closed
	Error Locating	4. Find in which step the property is
		violated
	Cause Understanding 5.Which diagram should be modified to
		satisfy the property ?
		6. Explain informally (in English) what
		modification you want to do
		7. Fix the error in the model (syntax is free).

Table 2 .

 2 Statistical results by cognitive category. Results show means and Student's t hypothesis tests for each cognitive category of tasks.

		Trace	Error	Cause
		Understanding Understanding Understanding
		(T1 to T3)	(T4)	(T5 to T7)
		Success Timing Success Timing Success Timing
	Group A	5	44.33	5	18	5	35
		5	27.33	5	21	4.33	55.67
		5	27	5	59	5	30.67
		5	8.33	5	51	3.33	62.67
		5	29.67	4	55	3.67	110
	Group B	5	103	5	20	3	100
		3.17	325	5	540	0	600
		5	183.33	5	27	5	90.33
		5	120.67	5	32	5	23.33
		1.67	238	2	267	2.33	94.33
	t	0.16	0.004	0.54	0.22	0.26	0.28

  3 the standard deviation can be considered equal and we can test the null hypothesis using the Student's t test. We applied a two-tailed Student's t test to the six null hypothesis. The results are showed in table 2. The experiment was run with five participants in each group, that gives us 8 degrees of freedom and a value for t 0.99 of 3,355. All the values of t are under the value of t 0.99 , we can then reject the null hypothesis. For the user satisfaction results showed in table 3 are also statistically sound (t value of 0,7) and shows that the null hypothesis corresponding to user satisfaction can also be rejected. Initial hypotheses are thus accepted, meaning that effectively supporting the user in understanding analysis results increases analysis tool usability.

Table 3 .

 3 Usability tests using the System Usability Scale[START_REF] Brooke | SUS -A quick and dirty usability scale[END_REF]. Results show an increase of 11% in usability for the experimental group (group A). Results are statistically sound according to the Student's t test.

		System Usability Scale
	Group A	67.7
	Group B	61.0
	t	0.71

http://www.irit.fr/ifx

In some cases, the model can be first simplified using automatic abstraction techniques.

Acknowledgments. We thank Anke Brock and Antonio Serpa for their support, the volunteer participants to the experiment, and the reviewers for their valuable suggestions.