Romain Delpoux

Laurentiu Hetel

Alexandre Kruszewski

Parameter Dependent Relay Control: application to PMSM

Keywords: Relay feedback control, Linear Matrix Inequalities, switched systems, PMSM

The article presents a novel relay control design strategy for some classes of nonlinear systems. The main idea of this work is to use an Linear Parameter-Varying (LPV) modeling to design nonlinear switching surfaces. This modeling is motivated by the fact that numerical tools such as LMI may be used by exploiting the quasi-linear structure of the system. Here we propose LMI formulation providing criteria for the design of switching surfaces. This design is seen as the synthesis of Parameter Dependent Relay (PDR). The second contribution of this article is the implementation of this relay strategy for Permanent Magnet Synchronous Motors (PMSM). Since the LPV framework can encompass the PMSM model, the obtained relay control depends on the motor speed variations. Experimental results on a PMSM are presented.

I. INTRODUCTION

The design of switching controller for nonlinear systems with input constraints represents a challenging area in control theory [START_REF] Tsypkin | Relay Control Systems[END_REF], [START_REF] Emel'yanov | Variable Structure Automatic Control Systems[END_REF], [START_REF] Flügge-Lotz | Discontinuous automatic control[END_REF], [START_REF] Saberi | Special Issue: Control of Linear Systems Subject to Hard Constraints[END_REF]. Among the class of systems with input constraints [START_REF] Tarbouriech | Control of uncertain systems with bounded inputs[END_REF], [START_REF] Zaccarian | Modern anti-windup synthesis: control augmentation for actuator saturation[END_REF], relay feedback control has been applied in a wide range of technical domains. It may be found for example in servos-mechanisms in mechanics or in hydraulic systems, in power-electronic actuators with Pulse-Width Modulation (PWM) etc. Such control systems have been used in variable structure control [START_REF] Tsypkin | Relay Control Systems[END_REF], [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF], [START_REF] Emel'yanov | Variable Structure Automatic Control Systems[END_REF], [START_REF] Utkin | Sliding modes in control optimization[END_REF], since they offer interesting robustness properties faced to particular perturbations. The design of relay control systems is a non-trivial issue: the control design procedure has to take into account complex phenomena such as zeno solutions [START_REF] Schumacher | Time-scaling symmetry and Zeno solutions[END_REF], limit cycles [START_REF] Boiko | Oscillations and transfer properties of relay servo systems -the locus of a perturbed relay system approach[END_REF], [START_REF] Johnson | Review of sensorless methods for brushless DC[END_REF], [START_REF] Gonc ¸alves | Global stability of relay feedback systems[END_REF] and sliding modes [START_REF] Utkin | Sliding modes in control optimization[END_REF], [START_REF] Tsypkin | Relay Control Systems[END_REF], [START_REF] Fridman | An averaging approach to chattering[END_REF]. In fact the system dynamics are inherently hybrid since to each control value we may associate a discrete state variable. Therefore, the synthesis of a relay feedback can be related with the design of switching surfaces in hybrid systems [START_REF] Van Der Schaft | An introduction to hybrid dynamical systems[END_REF], [START_REF] Liberzon | Switching in Systems and Control, ser. Systems & control. Systems & Control: Foundations & Applications[END_REF], [START_REF] Bolzern | Quadratic stabilization of a switched affine system about a nonequilibrium point[END_REF], [START_REF] Deaecto | Switched affine systems control design with application to DC-DC converters[END_REF].

Although relay feedback has been studied for a long time, there are still many unsolved issues. For the moment very few numerical tools exist for designing switching surfaces while optimizing the system performances or the size of the domain of attraction. Sliding mode control theory is well developed for generic nonlinear switching surfaces. However, for relay control, the exiting numerical optimization approaches can only handle switching surfaces described by affine hyperplanes [START_REF] Hetel | Sampled-data control of LTI systems with relay: a convex optimization approach[END_REF], [START_REF] Polyakov | On practical stabilization of systems with delayed relay control[END_REF].

The main idea of this work is to use a Linear Parameter-Varying (LPV) [START_REF] Biannic | Parameter varying control of a high performance aircraft[END_REF], [START_REF] Bara | Parameter-dependent state observer design for affine LPV systems[END_REF], [START_REF] Daafouz | Parameter dependent Lyapunov functions for discrete time systems with time varying parametric uncertainties[END_REF], [START_REF] Geromel | Robust stability of time varying polytopic systems[END_REF] modeling in order to design nonlinear switching surfaces. The LPV formulation has a long history in the automatic control literature. This modeling enables the use of well known linear design approaches to the case of nonlinear systems. The plant dynamics are rewritten in such a manner that the system nonlinearities are embedded in linear models as time-varying parameters. Powerful numerical optimization tools (such as LMI solvers [START_REF] Boyd | Linear Matrix Inequalities in System and Control Theory[END_REF]) can be applied in the design procedure by exploiting the quasi-linear system structure. The main theoretical contribution of the article is to provide criteria for the design of nonlinear switching surfaces by using an LMI formulation. From the point of view of LPV systems, the design of nonlinear switching surfaces is seen as the synthesis of Parameter Dependent Relay (PDR). For the sake of generality we consider a wide class of relays which is not only restricted to the classical sign controller (vector taking ± one as elements), but may take any values in the vertices of a time-varying convex polytope. Such a control can also encompass the simplex type variable structure control [START_REF] Bartolini | Simplex sliding mode control of multi-input systems with chattering reduction and mono-directional actuators[END_REF], [START_REF]Simplex methods for nonlinear uncertain sliding-mode control[END_REF], [START_REF] Bajda | Vector method of design of sliding motion and simplex algorithms[END_REF] for which few LMI design procedure exist. From a practical point of view, the second contribution of the article is the illustration of the proposed methodology for the control of a Permanent Magnet Synchronous Motor (PMSM). Indeed, PMSM are usually controlled by relays and thus only a finite set of control values is available. However in most of classical control design methods the use of averaging and PWM ignores the relay nature of the actuator [START_REF] Bodson | High performance nonlinear feedback control of a permanent magnet stepper motor[END_REF], [START_REF] Sira-Ramírez | A Passivity plus Flatness Controller for Permanent Magnet Stepper Motor[END_REF]. Here we propose a direct relay control which may use the advantages of the switching actuator in power electronics. The LPV framework encompasses the PMSM model. The obtained switching surfaces depend in a nonlinear manner on the motor speed. Preliminary results have been proposed in the conference version [START_REF] Delpoux | Permanent Magnet Synchronous Motor control via Parameter Dependent Relay Control[END_REF]. The article is divided into five sections. Section II presents the motivation of the article. An LPV representation is derived from the PMSM model and the relay nature of the actuators is exhibited. Section III is dedicated to the design of the PDR control for generic model of LPV systems. In Section IV, an LMI criterion is proposed for the stabilization problem. This section also provides tools for the estimation of the domain of attraction. The theory presented in this article is illustrated through an academic example in Section V. The last section, Section VI, is devoted to the real implementation of the control design procedure on a PMSM.

Notations: The identity (or null) matrix with appropriate dimension is denoted by I (or 0). For a real square symmetric matrix M, M > 0 (M < 0) indicates that M is positive (negative) definite. For a full rank square symmetric matrix M , M -1 denotes the inverse of M . In a symmetric matrix * denotes an element that may be inferred by symmetry.

For a matrix A ∈ R n×n , we denote the Hermitian of A by: He{A} = A + A T . We denote by I N the set {1, 2, . . . , N }. The symbol ∆ N denotes the unit simplex in R N defined by:

∆ N = µ ∈ R N : µ i ≥ 0, i ∈ I N , N i=1 µ i (t) = 1 .
For a given set S ∈ R n the symbol conv(S) denotes the closed convex hull of the set. For a symmetric positive definite matrix P ∈ R n×n and a positive scalar c we denote

E(P, c) = {x ∈ R n : x T P x ≤ c}. Let B(x, c) denotes the open ball centered on x ∈ R n with radius c > 0, B(x, c) = {y ∈ R n : |x -y| < c}.
Given a constant scalar U > 0, we define the finite set

Ψ m (U ) = {u ∈ R m : u i ∈ {-U, U }, i ∈ I m }.
Given a continuous function f : R n → R and a compact set S we denote by

argmin s∈S f (s) = {s ∈ S : f (s) ≤ f (r), ∀r ∈ S}. For a set S ⊂ R m , K ∈ R m×n , we denote C S (K) = {x ∈ R n : Kx ∈ conv(S)}.

II. MOTIVATION

In this section the speed model of the PMSM is presented and the practical problem that motivated our research is introduced. The equations [START_REF] Tsypkin | Relay Control Systems[END_REF] give the standard PMSM model in the phase (or winding) variables [START_REF] Marino | Nonlinear adaptive control of permanent magnet step motors[END_REF]:

                   L di α dt = v α -Ri α + KΩ sin(n p θ), L di β dt = v β -Ri β -KΩ cos(n p θ), J dΩ dt = K (i β cos(n p θ) -i α sin(n p θ)) -f v Ω -τ, (1)
where v α and v β are the voltages applied to the two phases of the PMSM, i α and i β are the two phase currents, L is the inductance of a phase winding, R is the resistance of a phase winding, K is the back-EMF constant (and also the torque constant), n p is the number of pole pairs (or rotor teeth), J is the moment of inertia of the rotor (including the load), f v is the coefficient of viscous friction and τ represents the load torque. The variable θ is the angular position of the rotor, Ω = dθ/dt is the angular velocity of the rotor. While for particular applications the variable θ can be included in the state vector, in this article we consider only the speed control, justifying the fact that θ is not in the state vector. We are interested in the stability of the velocity in a constant value. In this case the position θ is time varying. For this reason θ is not included in the state vector.

The non-linear state space representation of the system of equations ( 1) is given by:

ẋαβ (t) = f (x αβ , t) + Bv αβ (t) + D̟(t), (2)
where x T αβ = i α i β Ω , v T αβ = v α v β and ̟ = τ . The function f (x αβ , t) is defined by: f (x αβ , t) =           - R L i α (t) + K L Ω(t) sin(n p θ(t)) - R L i β (t) - K L Ω(t) cos(n p θ(t)) K J (i β (t) cos(n p θ(t)) -i α (t) sin(n p θ(t))) - f v J Ω(t)           , B =     1 L 0 0 1 L 0 0     and D =    0 0 1 J    .
Considering that each motor phase is actuated via commutation, the control vector v αβ belongs to the set Ψ 2 (V ), where V represents the maximal voltage.

V -V ] T [-V -V ] T [-V V ] T [V V ] T R(θ) 0 v α v β v d v q

Model in the rotating frame (d -q)

In the phases frame the signals i α and i β vary at n p times the frequency of rotation. This high frequency problem is alleviated by the use of the direct quadrature (d -q) transformation, also known as the Park transformation [START_REF] Park | Two-reaction theory of synchronous machines generalized method of analysis-part I[END_REF]. This transformation changes the frame of reference from the fixed phase axes to axes moving with the rotor. Equation ( 3) gives the transformation performed to obtain the rotating frame:

R(θ(t)) = cos(n p θ(t)) sin(n p θ(t)) -sin(n p θ(t)) cos(n p θ(t)) , i d (t) i q (t) = R(θ(t)) i α (t) i β (t) and v d (t) v q (t) = R(θ(t)) v α (t) v β (t) . (3)
The state space representation is then given by:

ẋdq (t) = A dq (Ω(t))x dq (t) + Bv dq (t) + D̟(t), (4)
where x T dq = i d i q Ω , v T dq = v d v q , and,

A dq (Ω(t)) =           - R L n p Ω(t) 0 -n p Ω(t) - R L - K L 0 K J - f v J           .
The matrices B and D remain unchanged. Consider that Ω(t) ranges between known extremal values Ω(t) ∈ [Ω, Ω]. In this frame the PMSM can be described using an LPV state space representation. The state space representation of the system depends linearly on a vector of time-varying parameters: Ω(t). The model may be represented as follows:

     ẋdq (t) = A(α(t))x dq (t) + Bv dq (t) + D̟(t), A(α(t)) = N A i=1 αi(t)Ai, ∀i, αi(t) ≥ 0, i αi(t) = 1, (5)
where

N A = 2, with A 1 = A dq (Ω), A 2 = A dq (Ω).
The controls v dq (t) are defined for all θ ∈ [0, 2π] by:

v dq (t) = k(x dq (t), θ(t)), ∀k ∈ R n × [0, 2π] → R m (6)
Note that the control v dq (t) is a PDR control which takes values in a finite set of vectors depending on θ:

{u ∈ R 2 : ∃v ∈ Ψ 2 (V ), u = R(θ(t))v}.
The input vector in the different frames is represented in Fig. 1. For a given V , the objective is to determine the switching surfaces in the state space, which ensure the closed loop stability of the system (5) with the control law ( 6). This represents one of the motivations for the theoretical developments in the paper.

III. PARAMETER DEPENDENT RELAY (PDR) CONTROL

In this section we will present a generic model of LPV systems. This LPV framework encompasses the PMSM model. Local stabilization results will be presented for this model.

A. Generic problem formulation

We consider the class of Linear Parameter-Varying (LPV) systems with the state-space realization:

ẋ = A(µ)x + B(µ)u, (7)
where x ∈ R n is the state vector and u ∈ R m is the control vector, the matrices A ∈ R n×n , B ∈ R n×m are polytopic matrices with the following form:

A(µ(t)) = N i=1 µ i (t)A i , B(µ(t)) = N i=1 µ i (t)B i , (8)
with A 1 , . . . , A N , B 1 , . . . , B N being known constant matrices. The vector

µ(t) = µ 1 (t) . . . µ N (t)
T is a vector of real and known parameters which evolves piecewise continuously in the unit simplex ∆ N . Such models are interesting since they can be useful for absorbing locally the behavior of more complex affine nonlinear systems [START_REF] Blanchini | Set-Theoretic Methods in Control, ser. Systems & Control: Foundations & Applications[END_REF], [START_REF] Rugh | Research on gain scheduling[END_REF]. Here we consider the LPV representation as a starting point. From now, the manner in which it is obtained from a nonlinear model is neglected (see [START_REF] Rugh | Research on gain scheduling[END_REF] for details).

We assume that for each µ ∈ ∆ N the control u may only take values in a finite set which depends on the parameter µ. We define this set of finite values V µ by:

V µ = {v i (µ), i ∈ I k }, v i : ∆ N → R m , ∀i ∈ I k . (9)
We consider that conv(V µ ) is a non empty bounded set containing the origin in its interior for any µ ∈ ∆ N . The objective is to find a PDR control u = K d (x, µ) which locally stabilizes the system (7):

K d : R n × ∆ N → V µ . (10)
Given that u is discontinuous, the closed loop vector field is discontinuous. System solutions are considered in the sense of Filippov [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides: Control Systems, ser. Mathematics and its Applications[END_REF]. We recall the definition of local asymptotic stability. One poses:

ẋ = f (t, x(t)), where f (t, x(t)) = A(µ(t))x(t) + B(µ(t))K d (x(t), µ(t)). (11)
Definition 1. [START_REF] Bacciotti | Liapunov Functions and Stability in Control Theory[END_REF] The equilibrium point x = 0 of (11) is

• stable if, for each ǫ > 0, there is δ = δ(ǫ, t 0 ) > 0 such that ||x(t 0 )|| < δ ⇒ ||x(t)|| < ǫ, ∀t ≥ t 0 ≥ 0,
• locally asymptotically stable at the origin if it is stable and there is c = c(t 0 ) > 0 such that x(t) → 0 as t → ∞, for all ||x(t 0 )|| < c.

B. Stabilization by PDR control

In this subsection we present a method for the construction of the PDR control [START_REF] Boiko | Oscillations and transfer properties of relay servo systems -the locus of a perturbed relay system approach[END_REF]. The main idea is to use the existence of any stabilizing control law (possibly continuous) in order to redesign a locally stabilizing relay control. The following proposition allows to use a previously designed control law to find a relay based one. Proposition 1. Consider system [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF] with the description [START_REF] Utkin | Sliding modes in control optimization[END_REF]. Consider Γ ⊂ R n be a domain containing x = 0. Assume that there exists a control u = K(x, µ), with K :

R n × ∆ N → R m such that K(x, µ) ∈ conv(V µ ), ∀µ ∈ ∆ N , x ∈ Γ \ {0}. Let V (x), V : Γ → R, be a continuously differentiable function such that W 1 (x) ≤ V (x) ≤ W 2 (x), ∂V ∂x (A(µ)x + B(µ)K(x, µ)) < -W 3 (x), ∀µ ∈ ∆ N , x ∈ Γ \ {0}, (12)
where W 1 (x), W 2 (x) and W 3 (x) are continuous positive definite functions on Γ. Then system [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF] with the control law:

u = K d (x, µ) ∈ argmin v∈Vµ ∂V ∂x B(µ)v, x ∈ Γ, (13)
is locally asymptotically stable when solutions are understood in the sense of Filippov. Furthermore, for any level set L V (c) = {x ∈ R n : V (x) ≤ c} such that L V (c) ⊆ Γ, the following relation is satisfied for any Filippov solution x(t) originating from the initial condition x 0 :

x 0 ∈ L V (c) ⇒ lim t→∞ ||x(t)|| = 0, (14)
i.e. L V (c) is an inner estimation of the domain of attraction.

Proof: In order to show the local stability of the closed loop system when solution are understood in the sense of Filippov [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides: Control Systems, ser. Mathematics and its Applications[END_REF] we consider the differential inclusion ẋ ∈ F (x, t), where

F (x, t) = conv A(µ(t))x + B(µ(t))ũ, ũ ∈ argmin v∈Vµ ∂V ∂x B(µ(t))v , µ(t) ∈ ∆ N , (15)
and show that:

max y∈F (x,t) ∂V ∂x y < -W 3 (x), ∀x ∈ Γ \ {0}, y ∈ F (x, t). (16)
This is a sufficient condition for local stabilization [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides: Control Systems, ser. Mathematics and its Applications[END_REF], since V (x) acts as a Lyapunov function. Furthermore [START_REF] Bolzern | Quadratic stabilization of a switched affine system about a nonequilibrium point[END_REF] implies that the level sets of V contained in Γ provide an inner estimation of the domain of attraction since they are invariant sets. Suppose that there exists a feedback u = K(x, µ), such that (12) holds, i.e. there exists a state feedback such that the equilibrium point x = 0 is locally asymptotically stable (see Theorem 4.9 p.152 [START_REF] Khalil | Nonlinear systems 3rd edition[END_REF]). Then one has:

∂V ∂x (A(µ)x + B(µ)K(x, µ)) < -W 3 (x), ∀x = 0, ∀µ ∈ ∆ N . ( 17
) Since ∀x ∈ Γ, µ ∈ ∆ N ⇒ K(x, µ) ∈ conv(V µ ), then for any x ∈ Γ and µ ∈ ∆ N there exist k scalars α i (x, µ) ≥ 0, i ∈ I k , with k i=1 α i (x, µ) = 1 such that: K(x, µ) = k i=1 α i (x, µ)v i (µ), (18)
holds. From ( 17) and ( 18) we have:

k i=1 α i (x, µ) ∂V ∂x (A(µ)x + B(µ)v i (µ)) + W 3 (x) < 0, ∀µ ∈ ∆ N and ∀x ∈ Γ \ {0}. (19)
Considering α i (x, µ) > 0, µ ∈ ∆ N and i ∈ I k , then for any x ∈ Γ \ {0} there must be at least one, x-dependent index,

i = i(x) ∈ I k such that: ∂V ∂x (A(µ)x + B(µ)v i (µ)) < -W 3 (x), ∀µ ∈ ∆ N . (20)
Consider the subset of control vectors in V µ minimizing the expression (20):

V min (x, µ) = argmin v∈Vµ ∂V ∂x (A(µ)x + B(µ)v) . (21)
Note that A(µ)x does not depend on v i , thus for a given x the subset V min (x, µ) can be rewritten as

V min (x, µ) = argmin v∈Vµ ∂V ∂x (B(µ)v) . (22)
Since there exists at least one index such that (20) holds, then for all x ∈ Γ \ {0} there exist at least one control v ∈

V min (x, µ) ⊂ V µ such that ∂V ∂x (A(µ)x + B(µ)v) < -W 3 (x), ∀µ ∈ ∆ N . (23)
When for some x ∈ Γ \ {0} there are several minimizers in V min (x, µ) (that is the cardinal of V min (x, µ) is greater than 1), then for any control vector ũ ∈ V min (x, µ)

∂V ∂x (A(µ)x + B(µ)ũ) < -W 3 (x), ∀µ ∈ ∆ N . (24)
In this case, given any two minimizers ∀ũ a , ũb ∈ V min (x, µ), ∀x ∈ Γ \ {0} one has

∂V ∂x (A(µ)x + B(µ)ũ a ) < -W 3 (x) and ∂V ∂x (A(µ)x + B(µ)ũ b ) < -W 3 (x). (25)
Therefore ∀x ∈ Γ \ {0}, ∀µ ∈ ∆ N and ∀ρ ∈ [0, 1] one has:

ρ ∂V ∂x (A(µ)x + B(µ)ũ a ) < -ρW 3 (x)
and

(1 -ρ) ∂V ∂x (A(µ)x + B(µ)ũ b ) < -(1 -ρ)W 3 (x). (26)
By summing the two inequalities in [START_REF]Simplex methods for nonlinear uncertain sliding-mode control[END_REF] ∀x ∈ Γ \ {0} and ∀µ ∈ ∆ N one has

∂V ∂x (A(µ)x + B(µ)ũ) < -W 3 (x), ∀ũ ∈ conv(V min (x, µ)), ∀µ ∈ ∆ N . (27)
Considering the differential inclusion [START_REF] Liberzon | Switching in Systems and Control, ser. Systems & control. Systems & Control: Foundations & Applications[END_REF] then from [START_REF] Bajda | Vector method of design of sliding motion and simplex algorithms[END_REF] we have that

∂V ∂x y < -W 3 (x), ∀x ∈ Γ \ {0}, ∀y ∈ F (x, t), (28)
which using ( 16) is sufficient for the local stability with the control function [START_REF] Fridman | An averaging approach to chattering[END_REF] when solutions are understood in the sense of Filippov.

Remark 1. The previous theorem uses the existence of any stabilizer K(x, µ) (possibly continuous) in order to redesign a PDR control K d (x, µ) which takes values only in the set V µ (x, µ). Comparing ( 17) with [START_REF] Bodson | High performance nonlinear feedback control of a permanent magnet stepper motor[END_REF] we have shown that the PDR has at least the same guaranteed decay of the Lyapunov function as K(x, µ). The result provides a general theoretical framework for the design of PDR. In the following section we will show how this result can be used in a constructive manner.

IV. LMI DESIGN CONDITION

In this section the LMI framework [START_REF] Boyd | Linear Matrix Inequalities in System and Control Theory[END_REF] is exploited to provide tractable and constructive conditions for the design of a PDR control. An estimation of the domain of attraction with the proposed control law is equally provided. Generally, when using a relay control law, only local stability may be ensured. Therefore, it is of interest to provide an estimation of the domain of attraction.

Considering that for all µ ∈ V µ , conv(V µ ) is non empty and contains the origin in its interior, remark that there exists a polytopic region:

Q = conv({q 1 , q 2 , . . . , q p }) = {z ∈ R m : h i z ≤ 1, i ∈ I N h }, such that Q ⊂ conv(V µ ), ∀µ ∈ ∆ N and 0 ∈ Int{Q}. (29)
Using the polytope Q one can adjust the design conditions to include an LMI based optimization of the domain of attraction. Proposition 2. Consider system [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF]. Consider Γ ⊂ R n be a domain containing x = 0. Assume that there exists Q = Q T > 0, Y i ∈ R m×n , i ∈ I N and a positive scalar δ such that:

He{(A i + A j )Q + B i Y j + B j Y i } < -2δQ, i, j ∈ I N , (30a)
1 h i Y j * Q > 0, i ∈ I N h , j ∈ I N , (30b)
eI I * Q > 0. ( 30c
) Let u = K d (x, µ) ∈ argmin v∈Vµ x T Q -1 B(µ)v, x ∈ Γ. (31)
Then the equilibrium point x = 0 of the closed-loop system (7)-( 31) is locally asymptotically stable. An estimation of the domain of attraction is provided by the ellipsoid

E(Q -1 , 1) containing the ball B(0, √ ǫ) with ǫ = 1 e , i.e. ∀x(0) ∈ E(Q -1 , 1), lim t→∞ ||x(t)|| = 0.
Proof: Assume that the set of LMI conditions (30) holds for system [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF] with the description [START_REF] Utkin | Sliding modes in control optimization[END_REF]. Multiplying the set of LMIs (30a) by µ i , µ j ∈ ∆ N , i, j ∈ I N and summing, followed by the multiplication of both side by Q -1 yields

2x T Q -1   N i=1 N j=1 µ i µ j A i + B i K j + A j + B j K i 2   < -2δx T Q -1 x, ∀x = 0, (32)
with

K i = Y i Q -1 . Then the function V (x) = x T Q -1 x, satisfies ∂V ∂x (A(µ)x + B(µ)K(x, µ)) < -2δV (x), ∀x ∈ R n \ {0}, ∀µ ∈ ∆ N , (33)
with

K(x, µ) = N i=1 µ i Y i Q -1 x. (34)
Then u = K(x, µ) is a global stabilizer for system [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF]. It will be used for re-designing a locally stabilizing PDR based on Proposition 1.

First we compute a domain Γ where K(x, µ) ⊂ conv(V µ ), ∀µ ∈ ∆ N . The set of LMI constraints (30b) ensures that

∀x ∈ E(Q -1 , 1) ⇒ K(x, µ) ∈ Q ⊂ conv(V µ ), ∀µ ∈ ∆ N . (35)
To prove this we use the Constrained Quadratic Lemma (given in the Appendix) as follows. Using [START_REF] Sira-Ramírez | A Passivity plus Flatness Controller for Permanent Magnet Stepper Motor[END_REF] with the definition of K(x, µ) in [START_REF] Rugh | Research on gain scheduling[END_REF], one can note that for the condition [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides: Control Systems, ser. Mathematics and its Applications[END_REF] to be true, it is sufficient that none of the hyperplanes h i Y j Q -1 x = 1, i ∈ I N h , j ∈ I N , crosses the ellipsoid E(Q -1 , 1). With Lemma 1, it leads to:

1 ≤ min hiYj Q -1 x=1 x T Q -1 x = min i∈IN h h i Y j Q -1 Q(Y j Q -1 ) T (h i ) T -1 . (36)
Using the Schur complement Lemma, the latter leads to (30b).

To guarantee that B(0, √ ǫ) is included in the domain of attraction E(Q -1 , 1), we add the constraints

x T x < ǫ ⇒ x T Q -1 x < 1. ( 37
) If x T Q -1 x < 1 ǫ
x T x then (37) holds, with e = 1 ǫ the LMI problem becomes (30c). Therefore if (30b) holds we obtain that

for K(x, µ) ∈ Q ⊂ conv(V µ ), ∀x ∈ E(Q -1 , 1), µ ∈ ∆ N . Applying Proposition 1, with Γ = L v (1) = E(Q -1 , 1), K(x, µ)
defined in [START_REF] Rugh | Research on gain scheduling[END_REF] and satisfying the constraint [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides: Control Systems, ser. Mathematics and its Applications[END_REF], allows to show that the control law [START_REF] Marino | Nonlinear adaptive control of permanent magnet step motors[END_REF] ensures the local stabilization in E(Q -1 , 1). Furthermore, using [START_REF] Khalil | Nonlinear systems 3rd edition[END_REF] we show that the domain of attraction contains the ball B(0, √ ǫ).

Remark 2. Proposition 2 is inspired by convex optimization arguments from [START_REF] Hu | Control Systems With Actuator Saturation: Analysis and Design[END_REF], [START_REF] Hindi | Analysis of Linear Systems with Saturation using Convex Optimization[END_REF], [START_REF] Tanaka | Fuzzy Control Systems Design and Analysis: A Linear Matrix Inequality Approach[END_REF]. The feasibility of the LMI optimization problem [START_REF] Delpoux | Permanent Magnet Synchronous Motor control via Parameter Dependent Relay Control[END_REF] with some matrix Q, guarantees that any solutions of the LPV system [START_REF] Edwards | Sliding mode control -Theory and applications[END_REF] with the control [START_REF] Fridman | An averaging approach to chattering[END_REF] originating from the invariant ellipsoid E(Q -1 , 1) is converging to the origin with a decay rate δ. By minimizing e, we increase the radius √ ǫ of the ball B(0, √ ǫ) included in E(Q -1 , 1). This allows to provide an inner ellipsoidal approximation E(Q -1 , 1) of the domain of attraction.

V. ACADEMIC EXAMPLE

In order to illustrate the results presented in this section, we propose to show simulations through a simple second order system so that the trajectories of the system can be plotted in a two dimensions phase portrait. We consider the system:

ẋ(t) = A 0 x(t) + B 0 (x 1 (t))u(t), (38)
with x = [x 1 x 2 ] T in R 2 , u ∈ R 2 , A 0 ∈ R 2×2 and B 0 ∈ R 2×2 defined by A 0 = 0 3 1 1
, B 0 (x 1 (t)) = 1 + 0.5 sin(x 1 (t)) 0 0 1 + 0.5 sin(x 1 (t)) .

For each x 1 (t), the control u(t) is constrained to switch among four different values in the set {R(x 1 (t))ρ, ρ ∈ Ψ 2 (V )}. The matrix R(x 1 (t)) is the rotation matrix defined by

R(x 1 (t)) = cos(x 1 (t)) sin(x 1 (t)) -sin(x 1 (t)) cos(x 1 (t)) . ( 39
)
The relay value V is equal to 10, leading to two inputs each taking values in {-V, V } which is a square of side length 2 × V . Considering as bounded time-varying parameter sin(x 1 ), cos(x 1 ), the system (38) may be rewritten as an LPV system of the form (7) defined by:

ẋ(t) = Ax(t) + B(µ(t))u(t) (40)
with

A = A 0 and B(µ(t)) = 2 i=1 µ i (t)B i = B 0 (x 1 (t)), where µ 1 (t) = 1 -sin(x 1 (t)) 2 , µ 2 (t) = 1 + sin(x 1 (t)) 2 and
B 1 = 0.5 0 0 0.5 , B 2 = 1.5 0 0 1.5 .
The control u takes values in the finite set (9) defined by

V µ(t) = {v i (µ(t)), i ∈ 1, . . . , 4} = {R(x 1 (t))ρ, ρ ∈ Ψ 2 (V )}. (41)
In order apply Proposition 2 we need to construct a polytopic region Q such that equation ( 29) is satisfied. Note that all squares defined by conv(V µ(t) ) are centered at 0 and have the same size thus the disc of radius V centered at 0 belong to all conv(V µ(t) ) (see Fig. 2). This disc can be approximated by the polytope Q represented in brown Fig. 2 for

v 2 (µ) = R(x 1 )[V -V ] T v 3 (µ) = R(x 1 )[-V -V ] T v 4 (µ) = R(x 1 )[-V V ] T v 1 (µ) = R(x 1 )[V V ] T v 1 v 2 q 1 q 2 q i q N R(x 1 ) h i 0 Fig. 2.
Representation of control sets Vmu for the system in the simulation example.

which the vertices q i are given by

q i+1 = V       cos 2iπ p sin 2iπ p       , i = 0, . . . , p -1. (42)
Each face of the polytope can be characterized by its normal:

h i+1 = q i + q i+1 1 + cos 2π p , i = 0, . . . , p -1. (43)
The simulations are realized using Matlab/Simulink and the LMI in the Proposition 2 are solved using SeDuMi ( [START_REF] Labit | SeDuMi Interface 1.02: a Tool for Solving LMI Problems with SeDuMi[END_REF]). In order to approximate the inscribed disc by the polytope Q we take p = 15. Choosing a decay rate δ = 4 and applying Proposition 2, the LMI solver returns the matrices Q and Y i , i ∈ I 2 matrices:

Q = 43.
The Q matrix defines the parameter dependent relay control [START_REF] Marino | Nonlinear adaptive control of permanent magnet step motors[END_REF] and thus the switching regions. These regions are plotted Fig. 3 as function of the states x 1 and x 2 . On this figure r 1 is the region for which the argument of the minimum is given for the

control input v 1 (µ(t)) = R (x 1 (t)) [V V ] T , r 2 for v 2 (µ(t)) = R (x 1 (t)) [V -V ] T , r 3 for v 3 (µ(t)) = R (x 1 (t)) [-V V ] T , r 4 for v 4 (µ(t)) = R (x 1 (t)) [-V -V ] T .
To illustrate the theoretical results, one proposes to compare the Continuous State Feedback (CSF) control law [START_REF] Rugh | Research on gain scheduling[END_REF] with the PDR control [START_REF] Marino | Nonlinear adaptive control of permanent magnet step motors[END_REF]. In the continuous case, the control input applied to the system denoted by ρ in the description of the system is in R 2 but it has elements saturated in the interval [-V, V ]. The phase portrait of the states x 1 and x 2 for both cases are plotted Fig. 4. On theses figures, we have plotted in red the ellipsoid E(Q -1 , 1), characterizing the domain of attraction of the system. The brown lines represent the hyperplanes h i Y j Q -1 = 1. In accordance with condition [START_REF] Filippov | Differential Equations with Discontinuous Righthand Sides: Control Systems, ser. Mathematics and its Applications[END_REF] it shows that none of the hyperplanes crosses the domain of attraction.

The first simulation is executed while taking initial conditions outside the attractive ellipsoid. On the figure, the initial condition is denoted by x 0,1 . One observes that outside the attraction domain, the closed-loop system does not converge to the origin. The second simulation is realized with the initial condition x 0,2 , near the domain of attraction, but outside. The figures show that in this case, the trajectories are converging to the origin. Finally, the initial condition x 0,3 is taken inside the domain of attraction. In this case the trajectories also converge to the origin. For this example the attractive ellipsoid contains the ball |x| < ǫ with ǫ = 1.28 and the initial condition x 0,3 with |x 0,3 | = 4.14. Note that |x 0,1 | = 7.07 and |x 0,2 | = 4.24, this gives an idea about the conservatism introduced in the estimation of the domain of attraction. In comparison with the static feedback proposed in [START_REF] Delpoux | Permanent Magnet Synchronous Motor control via Parameter Dependent Relay Control[END_REF], the same settings lead to ǫ equal to 0.58, the PDR enlarges considerably the ellipsoid estimation of the domain of attraction.

VI. PMSM APPLICATION

This section is devoted to the experimental application on the PMSM, to illustrate the proposed control design methodology on a concrete case.

A. Test-bench description

The experiments are realized using a stepper motor bench developed in LAGIS at École Centrale de Lille (see Fig. 5). The parameters of the motor with coils in series have been identified using the offline procedure described in [START_REF] Delpoux | Parameter estimation of permanent magnet stepper motors without mechanical sensors[END_REF], leading to L = 9mH, R = 3.01Ω, K = 0.27N.m.A -1 and J = 3.18.10 -4 kg.m 2 . The number of pole pairs is n p = 50. The input voltages v a and v b of each coil are delivered by two D/A outputs of the dSpace card and amplified by two linear power amplifiers (this means that the controls are directly applied to the coils without PWM implementation). The currents i a and i b are measured using Hall effect sensors with a precision of 1% of the nominal current I n = 3A. The power supply provides a maximum voltage v max = 20V and i max = 3A. The sampling period for this experiment is constant and equals to 10 -4 s for the control.

B. Experimental results

We design a control law where we consider that only four control inputs are available. In this article, the control design is considered with the assumption that there is no external torque (i.e. τ = 0). In the section tracking, an unknown torque will still be applied to the motor to show the disturbance rejection property of the new PDR control law. An integral action is implemented with ζ the ouput of the integrator (ζ(0) = 0)) [START_REF] Ogata | Modern Control Engineering, ser. Instrumentation and controls series[END_REF] to ensure tracking performance with respect to a reference Ω ref . The integral action given by:

ζ = Ω -Ω ref = Cx -Ω ref , C = [0 0 1], ( 45
)
where ζ is the output of the integrator (ζ(0) = 0). The combination of the state space representation (4) and the integral action without torque can be re-written as:

ẋdq ζ ż = A dq (Ω) 0 C 0 A(Ω) x dq ζ z + B 0 B u - 0 I I Ω ref ( 46
)
where u is constrained to switch among four different values in the set {R(θ)ρ, ρ ∈ Ψ 2 (V )}. The matrix R(θ) is defined by equation [START_REF] Flügge-Lotz | Discontinuous automatic control[END_REF]. In this section, two different control strategies are proposed to show the experimental behavior of the PDR control applied to PMSM. Firstly, we are interested in the motor stabilization starting from non-zero initial conditions, next a velocity tracking strategy is proposed. 1) Stabilization to the origin: In the same way as the simulations, the stabilization is realized on the PMSM starting from different initial conditions to the origin. Here the PDR control is proposed based on Proposition 2 applied to model (46) with To compare the experimental behavior of the PDR control with the classical Continuous State Feedback (CSF) control, [START_REF] Rugh | Research on gain scheduling[END_REF]) starting from non null initial velocity, we have plotted in Fig. 6 the velocity evolution for three different cases (Open Loop, CSF and PDR). This control law is applied to the system by using linear amplifiers, without any PWM module. Knowing that the PMSM is a stable system, it is important to show that the stabilization performance are better than the open loop performance. For this reason, the blue curve represents the open-loop stabilization. The red line represents the CSF while the green one represents the PDR. The figure shows that the closed loop performances are better than the open loop performances (better settling-times and transient responses). The closed loop strategies show similar settling time given that the PDR uses only 4 inputs control values.

Ω ref = 0. It leads to a control law of the form v αβ = argmin ρ∈Ψ2(V ) z T Q -1 R(-θ)ρ where Q =     29
v αβ = R(-θ)Y (Ω)Q -1 z, (obtained from
2) Velocity tracking: In this section we compare the behavior of the CSF and PDR for the tracking of a slowly varying velocity, although the proposed theoretical developments do not cover this case. The velocity profile is chosen according to industrial test trajectories [START_REF] Hamida | An Adaptive Interconnected Observer for Sensorless Control of PM Synchronous Motors With Online Parameter Identification[END_REF]. The robustness of the proposed approach is also tested by applying an external torque to the motor produced by a Electromagnetic Particle Brake.

Figure 7 exhibits the comparison between the CSF and the PDR when no external torque is applied to the motor. Without additional torque the velocity tracking is accurate in both cases: it shows that at steady state the desired trajectory is tracked with a precision around 1rad.s -1 for the PDR control. It must be noted that chattering phenomena appear in the PDR case leading to a sightly higher tracking error. However, in this case only four control inputs are used for the control.

Figure 8 shows the experimental result of the velocity tracking similarly to the previous figure. At time t = 7s an unknown external torque is applied to the motor using an Electromagnetic Particle Brake. On this figure, the plot of the tracking errors shows that in the presence of external torque, the PDR is more robust to disturbances than CSF. Indeed the perturbation is rejected only by the PDR control. This results is more clearly illustrated on Figure 9, where a focus on both trajectories tracking is represented. We can see that the PDR control (represented in red) provides a better velocity tracking performance. Moreover, for the CSF case, when the load torque is applied, the power amplifiers are in saturation.

Finally, the last figure, Figure 10 shows the PDR inputs control applied to the motor on a small time window. The figure shows that indeed, the PDR do not behave as a PWM with regular switching instant but it switches only when needed.

VII. CONCLUSION

In this article we have proposed a novel relay control strategy. The main idea of this work was to use LPV modeling to design nonlinear switching surfaces. This modeling has been motivated by the fact that powerful numerical tools such as LMI could be used. Here we have proposed an LMI formulation to provide criteria for the design of nonlinear switching surfaces. This design was referred as Parameter Dependent Relay (PDR). The second contribution of this article was the implementation of this relay strategy for Permanent Magnet Synchronous Motors (PMSM). Since the LPV framework encompasses the PMSM model, experimental results on a PMSM have been proposed. These results have shown that stabilization and good trajectory tracking was possible despite the finite set of control inputs. The load torque introduction has shown the good disturbance rejection properties of the PDR control. The analysis of disturbance rejection represents an interesting future work. APPENDIX Lemma 1. ( [START_REF] Hindi | Analysis of Linear Systems with Saturation using Convex Optimization[END_REF]). Let V (x) = x T Q -1 x, where Q = Q T > 0, C be a row vector in R n and r be a nonzero scalar. Then the minimum of V along the hyperplane {x|Cx = r} is given by α r = r 2 CQC T 6.5

  R. Delpoux is with Laboratoire des Sciences de l'Information et des Sytèmes (CNRS UMR 7296) INSM team, 8, Bd Louis XIV, 59046 Lille Cedex and Non-A Team, Inria Lille Nord Europe, France romain.delpoux@ensam.eu, L. Hetel and A. Kruszewski are with Laboratoire d'Automatique, Génie Informatique et Signal (CNRS UMR 8219), Ecole Centrale de Lille, 59651 Villeneuve d'Ascq cedex, France laurentiu.hetel@ec-lille.fr and alexandre.kruszewski@ec-lille.fr The research leading to these results has received funding from the European Community's 7th Framework Program (FP7/2007-2013) (grant agreement No 257462) HYCON2 Network of Excellence and the ANR project ROCC-SYS (grant agreement ANR-14-CE27-0008).

[

Fig. 1 .

 1 Fig. 1. Finite set of control in the fixed frame and in the rotating frame.

Fig. 3 .

 3 Fig. 3. Representation of the switching region, (the region r 1 in dark blue, r 2 in light blue, r 3 in yellow and r 4 in red).

2 Fig. 4 .

 24 Fig. 4. Characterization of the domain of attraction and simulation results of the PDR.

Fig. 5 .- 1 )Fig. 6 .

 516 Fig. 5. PMSM test-bench.

Fig. 7 .

 7 Fig. 7. CSF and PDR experimental results wihtout pertubations.

Fig. 8 .

 8 Fig. 8. CSF and PDR experimental results wiht pertubations.

Fig. 9 .

 9 Fig.9. Velocity zoom during the perturbation.

Fig. 10 .

 10 Fig. 10. Relay input.


Cédrick Lelionnais
email: cedrick.lelionnais@eseo.fr

Jérôme Delatour
email: jerome.delatour@eseo.fr

Matthias Brun
email: matthias.brun@eseo.fr

Olivier H Roux
email: olivier-h.roux@irccyn.ec-nantes.fr

Charlotte Seidner
email: charlotte.seidner@irccyn.ec-nantes.fr

Formal Synthesis of Real-Time System Models in a MDE Approach

Keywords: Real-time operating systems, Model Driven Engineering, Time Petri Nets, Multi-platform deployment, Formal model

The development of real-time embedded systems is quite complex because of the wide range of execution platforms and of the importance of non-functional requirements. Furthermore, Model Driven Engineering is particularly suitable for handling the diversity of implementation targets. Therefore, several real-time embedded systems development suites leverage Model Driven Engineering by automatically generating platform-specific code from high-level design models. Such tools may also take nonfunctional requirements into account by integrating verification activities. These activities typically rely on the generation of formal models from the same high-level design descriptions used for code generation. However, few tool suites support both code and formal model generation. Furthermore, among these, most overlook real-time operating systems mechanisms. Therefore, both code and formal models generated by these tool suites may not behave as specified in the high-level design descriptions. The present work extends the SExPIsTools code generator tool suite with a support for the generation of formal models. The proposed strategy relies on the composition of formal model fragments described using an extension of the classical Time Petri Nets. This paper presents a formalization of this composition that generically considers the behavior of platforms. As an illustration, we then give the formal model describing the behavior of an application on two different platforms (OSEK/VDX and VxWorks) and check a safety property on both models.

I. INTRODUCTION

Real-Time Embedded Systems (RTES) increasingly surround us in various domains (aircrafts, cars, cell phones, robotics, etc.). RTES engineers are confronted with the challenge of developing more complex, higher quality systems, with shorter development cycles at lower costs. Model Driven Engineering (MDE) helps engineers to develop tool suites that partially automate the development of RTES. Using model transformations, these tool suites mainly produce either executable code or formal models from high-level design descriptions of RTES. Some of these tool suites have both code and formal models generation processes. However, the mechanisms of Real-Time Operating Systems (i.e., executable software platforms supporting real-time applications, RTOS) are often ignored by these generation processes. As a result, generated code and generated formal models may not behave as specified in the high-level design description. Consequently, verification and validation activities applied on the RTES development could provide erroneous results. For instance, the detection of malfunctions (e.g., wrong treatments of critical data, or bad scheduling of real-time multitasking applications) could be compromised.

Nevertheless, among these tool suites, some consider realtime aspects in their generation processes. They thus take the deployment of real-time applications on RTOS (i.e., mapping of application concepts to execution platform services in order to execute them) into account. However, none of them satisfies the four criteria given below:

• Portability of real-time applications to adapt to the RTOS heterogeneity;

• Reusability of generation processes for a rapid migration of these applications in a multi-platform deployment case;

• Maintainability of RTES to help all stakeholders in their interventions;

• Correctness of generation processes in ordrer to have confidence in RTES development.

This work is part of an overall strategy of RTES development using a MDE approach. This strategy is supported by a tool suite called SExPIsTools (for Software Execution Platform Inside Tools). In order to satisfy the criteria previously given, SExPIsTools relies on the following approach:

• considering any RTOS as parameter of generation processes to achieve multi-platform deployment;

• writing more generic transformation rules to be independent from the considered RTOS;

• separating domain concerns (i.e., application deployment choice, RTOS consideration, transformation rules and verification and validation activities) to clarify interventions of each domain specialist;

• formalizing transformation rules to increase the correctness of generation processes.

In the present paper, we focus on the latter point. We need to construct RTES formal models, i.e., models of the whole system including the RTOS. For this purpose, our approach relies on a single transformation that does not depend on any specific RTOS. This transformation composes multiple formal model fragments independently of the target RTOS. Each of these fragments represents a part of the formal model that captures the behavior of the RTES.

As a basis of the construction, we use roles to generically identify connection points. These roles are used as a glue between the formal fragments. As a consequence, a new definition is presented to represent these formal fragments based on roles. The class of models we use is Time Petri Nets (TPN). The generic construction is then formalized as a basis of the transformation rules. Finally, an application example is proposed to illustrate a multi-platform deployment case, where two RTOS are considered. As a result of this experimentation, a scheduling safety property is verified on both resulting models. This paper extends our previous work [START_REF] Lelionnais | Formal Composition Based on Roles within a Model Driven Engineering Approach[END_REF] in which the fundamental rules of composition have been presented. An extension of these rules is given here to both 1) compose formal models of multitasking deployed applications with priority policy, and 2) provide a first validation of the generic construction.

Section II presents multi-platform deployment related works within a MDE approach [START_REF] Miller | Model Driven Architecture (MDA) Guide, version 1.0.1[END_REF]. A description of SEx-PIsTools is then given in Section III. Section IV gives the formal definition of the TPN fragments composition operator, which is based on roles. The application of this operator to the construction of whole RTES formal models is then described in Section V. Application examples are presented in Section VI. The benefits and limits of this approach are discussed in Section VII. Finally, we conclude in Section VIII.

II. RELATED WORKS

The following sub-sections present existing tool suites related to the multi-platform deployment problem.

Firstly, some code generators are introduced. Formal model generation tool suites are then presented, some of which are also capable of generating code. Finally, we will take a stand on the adopted approach.

A. Code generator tool suites

In order to promote the reuse of deployment tools within a single code generator, the genericity of processes has been at the heart of concerns. For instance, TransPI [START_REF] Maeng | Model-Driven Development of RTOS-Based Embedded Software[END_REF] relies on a two-step approach to generate specific code. A first phase considers a generic behavioral representation of the RTOS API (Application Programming Interface) in accordance with POSIX standard. In a second phase, the deployment is refined by configuring the process rules with the API of the targeted RTOS. However, the configuration of new rules does not fully satisfy the reuse of such a process since the tool must be modified.

A similar experimentation [START_REF] Kim | Platform dependent code generation of real-time embedded software[END_REF] improves reuse by specifying the RTOS concerned by the deployment without modification of the process. This orientation has been thought with the aim of porting real-time applications. This strategy relies on the transcription of code snippets by configuration of functions with RTOS information. Those information come from components of the targeted RTOS whose architecture was previously modeled by the generic modeling language AADL, which is dedicated to the real-time domain. The flexibility of this process meets the heterogeneous requirements of platforms.

Another approach [START_REF] Hajj Chehade | Contribution to Multiplatform Deployment of Multitasking Applications by High-Level Execution Services Behavioral Modeling[END_REF] also contributes to the multi-platform deployment problem. This fills the behavioral gap in the SRM package of the MARTE UML profile [START_REF] Omg | UML Profile for Modeling and Analysis of Real Time and Embbeded Systems (MARTE)[END_REF]. Before dealing with the RTOS behavior, a transformation process was developped [START_REF] Thomas | Software Real-Time Resource Modeling[END_REF] to generate a deployed application model by considering the targeted RTOS structure described with SRM. Descriptions of executable concepts (i.e., resources and services of the API) of the targeted platform required by the application are instantiated through the deployment process. This instantiation is completed by a refinement of descriptions depending on both application data and location of elements playing a generic role (e.g., a task priority or a counting semaphore capacity) within the considered platform. The integration of the behavioral aspect is also based on this notion of role. Code snippets are assigned to execution services (e.g., a task creation or a semaphore taking) in accordance with Java or C++/POSIX implementations.

The main interest of the two last contributions is the independence of specialists during their interventions regarding the tool suite. This criterion guarantees the quality of maintainability, which is added to the already mentioned reusability and portability. Despite this, these contributions present a major drawback that is inherent to all code generators. The formalization is indeed absent from the addressed processes. This weakness prevents specialists from applying verification activities on deployed applications.

B. Formal model generation tool suites

The tool suites presented in this section encourage the behavioral formalization of RTOS.

1) Without code generator:

An approach [START_REF] Kim | Formal synthesis of application and platform behaviors of embedded software systems[END_REF] has recently launched a formal synthesis for composing behavioral models of RTES. In order to achieve this, both application and platform are modeled with adequate modeling language. With the help of an Algebra of Communicating and Shared Resources (ACSR), behavior of the targeted platform is formalized. Behavior of the application is described by a Timed and Resource-oriented Statechart (TRoS) including both time annotations and resource constraints. A model of the deployed application is then composed with the obtained formal models and used for analysis. This synthesis provides a detailed design of RTES by formalizing their implementation with a complementary manner. Unfortunately, this process is complex to use, which forces stakeholders to have a good knowledge of formalization tools. Moreover, the composition requires a strong dependency of the application with respect to the platform.

Metropolis [START_REF] Pinto | Metropolis Design Guidelines[END_REF] supports both design and analysis of heterogeneous embedded systems on the basis of the platform-based methodology. The behavioral representation is illustrated by entities such as concurrent and communication activities. In addition, this environment offers the possibility to use formal languages in accordance with the LTL logic for verifying both functional and non-functional properties once the deployment reached by mapping of the system components with the platform entities is described. Similarly, GME [START_REF] Davis | GME: The Generic Modeling Environment[END_REF] includes use constraints on the representation of executable concepts thanks to the Platform Modeling Language (PML). This consideration mixed with the integration of formal languages to describe the behavior of platforms provides a deeper design of embedded systems. However, the genericity of modeling languages used for describing the platforms does not facilitate the treatment of particular domains such as real-time. Furthermore, transformation rules are not entirely clear. This leads to a less meaningful separation of domain skills and consequently to a maintainability decrease.

2) With code generator: More specifically to RTES, Ptolemy project [START_REF] Lee | Overview of the Ptolemy Project[END_REF] is further adapted for describing execution models. The definition of those models relies on the actor-oriented design and revolves around mechanisms of concurrency and communication implemented between RTES components. The behavior represented within those models is translatable into several execution semantics. This benefit offers a code-formal model duality of deployed applications. This approach thus achieves a wide coverage of software execution platforms. Nevertheless, the concepts of structural representation are only intended for the modeling of applications with this approach, and not for RTES themselves. Mechanisms such as RTES components synchronization must therefore be simulated with other verification tools. In spite of a very high completeness, the RTES maintainability with Ptolemy is once again called into question.

C. Positioning

In order to highlight both advantages and drawbacks of the works presented above, Table I classifies the tool suites according to their uses. Depending on whether a given tool suite addresses only code generation, only formal models generation, or both it will be in the first, second, or third column respectively. The first row is for tool suites that are not adapted to RTOS, while the second row is for tool suites that are adapted to RTOS.

Adapted to RTOS

TransPI 1 [3] ACSR+TRoS 2 [8] Ptolemy 3 [11] snippets+AADL [4] SRM [5]
1 Less suitable for both reusability and maintainability 2 Less suitable for reusability 3 Less suitable for maintainability Ptolemy seems to be the most versatile. Nevertheless, stakeholders distinction does not appear clearly, which does not facilitate maintainability.

Within MDE, alternative approaches were compared [START_REF] Brun | Contribution to the Software Execution Platform Integration during an Application Deployment Process[END_REF] to meet these requirements. The adopted strategy offers the possibility to capitalize most RTOS descriptions for multiplatform deployment in a generic way.

In conjunction with this objective, SExPIsTools integrates the Real-Time Embedded Platform Modeling Language (RTEPML) [START_REF] Brun | Contribution on the Software Execution Platform Integration During an Application Deployment Process[END_REF]. RTEPML was developed with the aim of representing executable platform concepts dedicated to the real-time domain. To further detail their representation, RTEPML [START_REF] Lelionnais | Formal Behavioral Modeling of Real-Time Operating Systems[END_REF] has been enriched to describe their behavior in TPN. However, the generation process used to take into account these behavioral descriptions needs to be formalized, which was started in [START_REF] Lelionnais | Formal Composition Based on Roles within a Model Driven Engineering Approach[END_REF], and is continued in the work presented in this paper (see Sections IV and V).

III. SEXPISTOOLS

This section presents SExPIsTools. Firstly, the modeling language RTEPML used to describe RTOS mechanisms is presented. Then, both deployment and formal models generation processes integrated in SExPIsTools are described. The role notion used as a generic basis of transformation rules is highlighted.

A. Modeling with RTEPML

RTEPML distinguishes the RTOS structural modeling from the behavioral RTOS modeling.

1) Structural description:

RTEPML is born from SRM package [START_REF] Thomas | Software Real-Time Resource Modeling[END_REF] mentioned in the previous section. SRM allows the description of a large number of RTOS [START_REF] Thomas | Towards a Framework for Explicit Platform-Based Transformations[END_REF] and had identified all concepts and their mechanisms present in RTOS. In SRM, these concepts are called resources (e.g., task, semaphore, etc.). RTEPML keeps the same taxonomy. In Figure 1, a small part of OSEK/VDX RTOS [START_REF] Group | OSEK/VDX Operating System Specification, version 2.2.3[END_REF] and VxWorks RTOS [START_REF] Windriver | VxWORKS Programmer's Guide, version 6.9[END_REF] descriptions in RTEPML are given. The task concept, called schedulable resource in RTEPML, is described for both RTOS. As depicted in Figure 1, thanks to the notion of roles (represented in bold between french quotation marks), we could specify the priority (an integer) of OSEKVDX Task or of VxWorks Task. This priority plays the role of priority element (<<priorityElement>>) for both tasks. Roles are thus used to identify both structures and features of each RTOS resource. As another example, on OSEK/VDX model, the <<terminateService>> role characterizes the terminate-Service of OSEKVDX Task in Figure 1.

Sometimes, certain concepts do inherently not exist on RTOS. As an example, the periodic task concept is missing on both OSEK/VDX and VxWorks platforms. With RTEPML, sets of concepts (i.e., identified with the DesignPrototype role in Figure 1) can be composed to translate this kind of concept. Thus, a PeriodicTask concept could be viewed at a composition of a Task and an Alarm for OSEK/VDX. As regards VxWorks, the PeriodicTask concept is differently composed of a Task and a Watchdog synchronizing with a Semaphore.

2) Behavioral description:

The behavioral description allows to represent the life cycle of RTOS concepts. Figure 2 extends the representation of OSEK/VDX concepts, given in Figure 1. The <<behavioralPrototype>> role leads to the assignation of a behavioral description to each concept, including services. Each behavioral description is translated into a Time Petri Net (TPN) [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] [19] whose definition is given Section IV. This class of model is used to describe both synchronism and parallelism, as well as time evolution. Therefore, TPN are well adapted to our concerns.

In the example given in Figure 2, the TPN describing OS-EKVDX AlarmBehavior represents the periodic activation of OSEKVDX Alarm. Informally, once a token is present in the ENABLE place, making it marked, one token is periodically distributed in the ACTIVATION place. Distribution of tokens is initially achieved once the left transition, represented as a black rectangle, is triggered (i.e., when ENABLE is marked and the transition clock has reached 0 time unit). The periodicity is then guaranteed by the right transition triggering (i.e., when LAPSE is marked and the transition clock has reached p time units). With clocks on transitions, we can consequently add as many time constraints as necessary, e.g., on the OSEKVDX TaskBehavior TPN, a delay between the READY and RUNNING places could represent the required time to start the task execution.

B. Model generation processes within SExPIsTools

SExPIsTools is designed for multi-platform deployment. Both code and formal model generations are performed in two steps. Figure 3 depicts these two steps. The first one concerns the deployment. This is common to both generations, which avoids to deploy twice. The application is deployed on a specific RTOS [START_REF] Brun | Contribution to the Software Execution Platform Integration during an Application Deployment Process[END_REF] [START_REF] Brun | Contribution on the Software Execution Platform Integration During an Application Deployment Process[END_REF]. The considered RTOS is given as a parameter of the deployment process. Transformation rules of the process are defined independently from the targeted RTOS. This independence is possible thanks to roles previously highlighted. The deployment is performed by mapping each application concept with its execution on the targeted RTOS. The mapping consists in locating the role of the executable concept corresponding to each application concept through the RTOS model. Once a correspondance is established, the structure of the located executable concept is instanciated, i.e., duplicated. Each instance is afterwards enriched by specifying its features with the help of the appropriate roles. Features specification emanates from application concepts information. All these specified instances finally constitute the model of the deployed application (i.e., the platform specific model of Figure 3).

The following step concerns either the code generation or the formal model generation. These both processes take in input the same generated deployed application model.

The code generator being not our focus in this paper, we only present the formalization of the deployed application model. Similarly to the deployment, the generation process of deployed application formal models instanciates TPN behavioral descriptions [START_REF] Lelionnais | Formal Behavioral Modeling of Real-Time Operating Systems[END_REF]. The location of each TPN is carried out from the structural instances of the deployed application model. Indeed, knowing the source executable concept of each structural instance, the corresponding TPN fragment is located with the <<behavioralPrototype>> role. Each corresponding TPN is thus duplicated giving a TPN behavioral instance (or each TPN fragment).

The generation of these TPN fragments engages their composition to constitute a global formal model of the deployed application. The elements serving as connection points must be located through the set of these TPN fragments. Similarly to the structural part, these elements are also located with roles. As instantiation rules, composition rules are based on these roles. In the interest of consistency, we have formalized the sequence of composition rules. This sequence is ordered to avoid any ambiguity in the formal model construction. The TPN fragments are therefore categorized according to RTOS concepts generalized in RTEPML:

• Concurrent resources: tasks, interruptions, alarms, etc.

• Interaction resources: semaphores, message queues, shared data, events, etc.

• Routines: application treatment including services called within the application. This treatment is only represented by the execution time.

The following Algorithm 1 informally describes the sequence of composition rules. We admit here that TPN fragments were already instanciated.

Each composition rule is labelled from a) to d) in comments through this algorithm. Firstly, a) each routine instance is composed of all its called service instances. Then, each concurrent resource must be composed with its execution routine. The execution routine is called the entry point of the concurrent resource. Each entry point is located with the <<entryPointElement>> role (see Figure 2). As a consequence, b) each concurrent resource instance is composed with its entry point. The next composition c) concerns all concurrent resource instances in order to put them in concurrency. As a final step, d) interaction resource instances are composed with the set of composed concurrent resource instances so that these latter interact with some of them. This order will be respected in Section V in which these rules will be formalized. Next, in Section IV, the composition operator of TPN based on roles is defined to formally express these rules afterwards.

IV. TPN COMPOSITION BASED ON ROLES

In order to define the composition of TPN fragments, roles are added to the TPN modeling. These roles are therefore assigned to places. The interest of such a method is to merge places [START_REF] Taïani | Composing Real-Time Objects: A Case for Petri Nets and Girard's Linear Logic[END_REF] [START_REF] Peres | On the Composition of Time Petri Nets[END_REF], which are the connection points of the deployed system that must be generated in TPN.

Algorithm 1 Composition rules

Input:

• I S = {I S R1 , I S R2 , . . . , I S R l }; // The service calls behavioral instances with ∀j ∈ [1, l], I S Rj ⊆ I S and l the number of routines to compose

• I C = {i C 1 , i C 2 , . . . , i C m }; // m concurrent re- sources behavioral instances • I I = {i I 1 , i I 2 , . . . , i I n }; // n interaction resources
behavioral instances Output:

• M // The composed deployed application behavioral model 1: for j = 1 to l do for all j such that 1 ≤ j ≤ l do 7:

if ∃i Rj such that i Rj is the entrypoint of i C k then 8: // b) Each entry point is composed 9: i EP k ← ruleComposeEntryP oint(i C k , i Rj ) 10: else 11: i EP k ← i C k 12: end if 13:
end for 14: end for 15: for all k such that 1 ≤ k ≤ m do 16: In this section, TPN with roles are firstly defined. The definition of the instantiation of TPN with roles is then given. Finally, the composition of TPN is highlighted through a synchronization formalism based on roles.

I EP ← {i EP 1 } ∪ • • • ∪ {i EP k } ∪ • • • ∪ {i EP m

A. Formal definition of TPN with roles

TPN are a timed extension of classical Petri nets [START_REF] Petri | Kommunikation mit Automaten[END_REF] in which an implicit clock and an explicit time interval are associated with each transition of the net. Informally, the clock measures the time since the transition has been (continuously) enabled, whereas the interval is interpreted as a firing condition: the transition, once enabled, may be fired only if the value (or valuation) of its clock belongs to the time interval.

In the following, N denotes the set of natural numbers, R ≥0 the set of non-negative real numbers, ∅ is the empty set and 0 is the null vector.

Definition 1 (TPN):

A TPN T is a tuple P, T, Pre, Post, m 0 , I s where:

• P is a finite, non-empty set of places;

• T is a finite, non-empty set of transitions;

• Pre : P × T → N is the backward incidence function;

• Post : P × T → N is the forward incidence function;

• m 0 is the initial marking of the net;

• I s : T → N × (N ∪ {+∞}) assigns a static time interval to each transition.

A marking of the net T is an application from P to N giving for each place of the net the number of tokens it contains. A transition t ∈ T is enabled by a marking m, which is denoted by t ∈ enabled(m), if all of its input places contain "enough" tokens; more formally, enabled(m) = { t ∈ T | ∀p ∈ P, m(p) ≥ Pre(p, t) }. A transition t ∈ T is newly enabled by the firing of transition t f from the marking m, which is denoted by t ∈↑ enabled (m, t f ), if it is enabled by the final marking m f defined by ∀p ∈

P, m f (p) = m(p) -Pre(p, t f ) + Post(p, t f ) but not by the intermediate marking m i defined by ∀p ∈ P, m i (p) = m(p) -Pre(p, t f ). More formally, ↑ enabled(m, t f ) = enabled(m f ) ((T \ enabled(m i )) ∪ {t f }).
Finally, for any interval I s , we denote by I s ↓ the smallest left-closed interval with lower bound 0 that contains I s . For each transition tr there is an associated clock x tr . We consider valuations on the set of clocks { x tr | tr ∈ T } and we will slightly abuse the notations by writing v(tr) instead of v(x tr ) to denote the valuation of the clock associated with transition tr.

The operational semantics of a TPN can be formally described as a time transition system; as it is a special case of the semantics of TPN with read and inhibitor arcs (given in Def. 3, we will omit it here for the sake of clarity.

In order to model such behaviors as conditional executions and preemption mechanisms, TPN have been extended with read arcs (represented in the following with a white square instead of a regular arrow) and inhibitor arcs (represented with a white circle). It should be noted that these arcs only impact the enabling rules of the net but not the marking obtained by firing a transition: read arcs test the presence of tokens in places without consuming them, whereas an inhibitor arc is used to stop the elapsing of time on a transition as long as there is a certain number of tokens in the place.

Definition 2 (TPN with read/inhibitor arcs):

A TPN with read and inhibitor arcs (RI TPN) is a tuple T RI = T , Read, Inh where:

• T = P, T, Pre, Post, m 0 , I s is a TPN, • Read : P × T → N is the read function; • Inh : P × T → N ∪ {+∞} is the inhibition function 1 .
Informally, a transition is enabled if there are "enough tokens" in the places linked by either input arcs or read arcs and if there are "not too many tokens" in the places linked by inhibitor arcs. More formally, the definition of the set of transitions enabled by a marking m is updated as follows: The definition of the set of transitions newly enabled from a marking m by the firing of a transition t f is similarly updated.

enabled(m) = {t ∈ T |

Definition 3 (Semantics of the RI TPN):

The operational semantics of the RI TPN with read and inhibitor arcs T RI defined above is given by the time transition system S = (Q, q 0 →) such that:

• Q = N P × R T ≥0 ; • q 0 = (m 0 , 0); • →∈ Q × (T ∪ R ≥0 ) × Q is the transition relation and is composed of: • the discrete transition transition, defined ∀t f ∈ T by (m, v) t f -→ (m ′ , v ′ ) iff: (t f ∈ enabled (m); v(t f ) ∈ I s (t f ); ∀p ∈ P , m ′ (p) = m(p) -Pre(p, t f ) + Post(p, t f ); ∀t ∈ T , v ′ (t) = 0 if t ∈↑ enabled (m, t f ) v(t) otherwise ; • the discrete transition transition, defined ∀d ∈ R ≥0 by (m, v) d -→ (m, v ′ ) iff ∀t ∈ enabled(m), ∀δ ∈]0; d], (v(t) + δ) ∈ I s ↓ (t).
Definition 4 (RI TPN with roles): A RI TPN with roles is a tuple N = T RI , R, λ where:

• T RI is a RI TPN,
• R is a finite set of roles,

• λ : P → R ∪ {⊥} is the function assigning a role to a place and ⊥ denoting that no role is assigned to a place. Hereafter, some notations and properties of this function are enumerated:

1) P λ = {p ∈ P | λ(p) = ⊥} is the set of places with role. 2) λ \P λ : P λ → R is an injective function; 3) λ -1 : R ∪ {⊥} → P ∪ {∅} such that    ∀r ∈ R, λ -1 (r) = p if λ(p) = r ∅ otherwise λ -1 (⊥) = ∅
The operational semantics of the RI TPN with roles N = T RI , R, λ is the same as that of RI TPN. Indeed, the use of roles within the definition of RI TPN does not impact its semantics.

B. Instantiation of RI TPN with roles

As seen previously, all RI TPN fragments are instantiated before being composed. In order to distinguish the fragments to compose, atomic elements such as roles, places and transitions must be identified according to the instances names, but also according to referenced instances names. Indeed, referenced instances emerge when instances are service calls. Each service call refers to a resource instance. As an example, a task activation service refers to a task. The two concepts are distinguished because this has an impact during the composition between a service call instance and its referenced resource instance. For this reason, the renaming of a role and a renaming of places and transitions are distinctly separated. This distinction is made with the following instantiation operator.

Let N = P, T, Pre, Post, m 0 , I s , Read, Inh, R, λ be the RI TPN with roles to instantiate. The following labels ins and ref respectively gives the names of the instance and the referenced instance. If the instance is a resource, there is no referenced instance with ref = ins. The global renaming function ⇁ is a bijective function from Set to Set ′ where Set ∈ {P, T, R}.

N ins = Ins(N ,
(p) = r iff λ ins (p ins ) = r ref λ ins (p) = ⊥ iff λ ins (p ins ) = ⊥

C. Specific extension of instantiated RI TPN with roles

Once RI TPN are instantiated, we have sometimes been faced with the need to extend them according to the application to deploy. For intance, in a real-time system based on a cooperative multitasking application with priorities, eligible low priority tasks are inhibited by eligible high priority tasks when allocating the processor.

We have focused on this case through this paper in order to enrich our previous work [START_REF] Lelionnais | Formal Composition Based on Roles within a Model Driven Engineering Approach[END_REF] in which all tasks had the same priorities. The cooperative multitasking case with priorities is depicted in Figure 4. The RI TPN N T 1 = Ins(N , ins, ref ) is an instance of concurrent resource such that a periodic task where ref = ins = T 1. In bold, some places with inhibitor arcs, represented with circles, are connected to the resume T 1 transition to inhibit the state change from READY T 1 to RU N N IN G T 1 . The marking of one of the places set {READY T 2 , READY T 3 , . . . , READY T x } carries out this inhibition action and ensures the cooperative scheduling of tasks. This action being a scheduling specific case, we defined a dedicated operator for adapting instantiated RI TPN of concurrent resources such that N T 1 to a cooperative scheduling context.

Let N ins = P ins , T ins , . . . , λ ins be a RI TPN with roles of a concurrent resource firstly instantiated as previously seen. N cs ins = P cs ins , T cs ins , . . . , λ cs ins represents the same instance extended according to a set of n concurrent resources identified by IN S = {ins 1 , ins 2 , . . . , ins n } with upper priorities.

Definition 6 (Extension of RI TPN with roles):

Cooperative scheduling of concurrent resources:

The EN ABLET 1 enablingT 1 LAP SET 1 ACT IV AT IONT 1 activationT 1 SU SP EN DEDT 1 terminatedStateT 1 [inc; inc] incrementT 1 [period; period] cycleT 1 [0;0 ] resumeT 1 READYT 1 activatedStateT 1 READYT 2 activatedStateT 2 READYT 3 activatedStateT 3 READYT x activatedStateT x [0; 0] activateT 1 P ROCESSORT 1 processorT 1 resumedStateT 1 RU N N IN GT 1 startT 1 ST ARTT 1 [0; 0] executeT 1 endT 1 EN DT 1 N T 1
Fig. 4: Specific extension of periodic task in RI TPN for cooperative multitasking extension of N ins in concurrence with n instances adapted to a cooperative scheduling is denoted by:

N cs ins = CoopSched(N ins , IN S)
with ∀t ∈ T ins , ∃Pre(λ -1 (activatedState ins ), t) ∈ Pre ins and ∃Post(λ -1 (resumedState ins ), t) ∈ Post ins Formally, this definition gives:

• R cs ins = R ins ∪ R IN S with R IN S = ∀i∈[1,n]
{r insi };

(p, t) =                  Inh ins (p, t) if p ∈ P cs ins \ P IN S 1 if              p ∈ P IN S t ∈ T cs ins , ∃Pre(λ -1 (activatedState ins ), t) ∈ Pre ins and ∃Post(λ -1 (resumedState ins ), t) ∈ Post ins

D. RI TPN Synchronization based on roles

In order to synchronize some RI TPN, we must clarify the definition of the composition of RI TPN, which will be based on roles assigned to places. Let N 1 , . . . , N n be n RI TPN

N i = P i , T i , Pre i , Post i , m 0i , I si , Read i , Inh i , R i , λ i with roles such that ∀k = k ′ ∈ [1, n] =⇒ T k ∩ T k ′ = ∅ and P k ∩ P k ′ = ∅.
The composition N = P, T, Pre, Post, m 0 , I s , R, λ of the previous RI TPN with roles will be denoted by N = N 1 ||N 2 || . . . ||N n . Linked to this composition, we define a function leading to the merging of places whose assigned roles will be taken into account in parameters.

The merging function ֒→ is a partial function from

(R 1 ∪ {•}) × (R 2 ∪ {•}) × • • • × (R n ∪ {•}) → P × R
where • is a special symbol used when a RI TPN is not involved in a particular merge of the global system. We then extend the definition of the assigning inverse function with λ -1 (•) = ∅

The composition of n RI TPN with m merging is denoted by

N 1 || . . . ||N n (r 1 1 , . . . , r 1 n ) ֒→ (p 1 , r 1 ) . . . (r m 1 , . . . , r m n ) ֒→ (p m , r m ) with ∀i ∈ [1, n], ∀j ∈ [1, m] , r j i ∈ R i , r j ∈ R and p j ∈ P , and ∀k ∈ [1, m], k = j ⇒ r k i = r j i
We will subsequently use the following notations:

• Let P merged i ⊆ P i be the set of places of the net N i merged by the composition. Formally

P merged i = ∀j∈[1,m] {λ -1 i (r j i )}
• Let P ֒→ ⊆ P be the set of places of the net N obtained by the merging. Formally

P ֒→ = ∀j∈[1,m] {p j }

Definition 7 (Composition of RI TPN with roles):

The composition of the n RI TPN N i with the merging ֒→ denoted by:

N = N 1 || . . . ||N n (r 1 1 , . . . , r 1 n ) ֒→ (p 1 , r 1 ) . . . (r m 1 , . . . , r m n ) ֒→ (p m , r m )
is defined by:

• R = ∀i∈[1,n] R i \ ∀j∈[1,m] {r j i } ∪ ∀j∈[1,m]
r j ;

• P = ∀i∈[1,n] P i \ P merged i ∪ P ֒→ ; • T = ∀i∈[1,n]
T i ;

• λ : P → R is defined by: • ∀p ∈ P \P ֒→ meaning that ∃i such that p ∈ P i then λ(p) = λ i (p) • ∀p j ∈ P ֒→ , meaning that p is the result of a merging, λ(p j ) = r j

• Pre :

P × T → N is defined ∀p ∈ P and ∀t ∈ T i ⊆ T by Pre(p, t) =              Pre i (p, t) if p ∈ P \ P ֒→ and p ∈ P i Pre i (p ′ , t), if    p ∈ P ֒→ and p ′ ∈ P i (. . . , r k i , . . . ) ֒→ (p, λ(p)) λ i (p ′ ) = r k i 0 otherwise. • Post : P × T → N is defined ∀p ∈ P and ∀t ∈ T i ⊆ T by Post(p, t) =              Post i (p, t) if p ∈ P \ P ֒→ and p ∈ P i Post i (p ′ , t), if    p ∈ P ֒→ and p ′ ∈ P i (. . . , r k i , . . . ) ֒→ (p, λ(p)) λ i (p ′ ) = r k i 0 otherwise. • m 0 : P → N is defined ∀p ∈ P by: m 0 (p) =    m 0i (p) if p ∈ P \ P ֒→ and p ∈ P i n i=1 m 0i λ -1 (r k i ) if p ∈ P ֒→ (r k 1 , . . . , r k n ) ֒→ (p, λ(p)) • I s : T → I is defined ∀t ∈ T by: I s (t) = I si (t) if t ∈ T i ;
• Read : P ×T → N is defined ∀p ∈ P and ∀t ∈ T i ⊆ T as Pre(p, t);

• Inh : P × T → N is defined ∀p ∈ P and ∀t ∈ T i ⊆ T as Pre(p, t)

As an example, N = N 1 ||N 2 ||N 3 (r 1 , r 2 , •) ֒→ (p, r)
is the parallel composition of the 3 TPN, i.e., N 1 , N 2 and N 3 , where the place p 1 ∈ P 1 such that λ 1 (p 1 ) = r 1 and the place p 2 ∈ P 2 such that λ 2 (p 2 ) = r 2 are merged. The name of the place obtained by this merging in N is p ∈ P and its role is λ(p) = r ∈ R.

Property 1 (Associativity):

The composition of TPN with roles is associative in the following sense: Property 2 (Commutativity): The composition of TPN with roles is commutative:

N 1 ||N 2 ||N 3 (r 1 , r 2 , r 3 ) ֒→ (p, r) = N 1 ||N 2 (r 1 ,r 2
N 1 ||N 2 (r 1 1 , r 1 2 ) ֒→ (p 1 , r 1 ) . . . (r k 1 , r k 2 ) ֒→ (p k , r k ) = N 2 ||N 1 (r 1 2 , r 1 1 ) ֒→ (p 1 , r 1 ) . . . (r k 2 , r k 1 ) ֒→ (p k , r k )

V. CONSTRUCTION AND ILLUSTRATION

The definitions presented above will help with the formal construction of behavioral models expressed as RI TPN. This construction will serve as a basis for the transformation process within the SExPIsTools framework (Figure 3). As described in Algorithm 1, the process consists of four successive composition rules, detailled in the paragraphs below and defined by equations ( 1) to (4).

A construction example in RI TPN is provided to illustrate the method. Figure 5 presents some RI TPN with roles, one per box, instantiated and ready for construction. Every operation details the fragments involved in the composition. The mergeable places are represented in double circle and those ready to be merged are connected by a hook-dotted arc with a letter corresponding to the construction step, i.e., the sequence of rules in Algorithm 1. Finally, roles are indicated above and to the right of places.

The whole model is describing a monoprocessor application P roc with two periodic tasks T 1 and T 2 sharing the same semaphore S. A cooperative multitasking is established between T 1 and T 2 with a non-preemptive context. T 2 has a higher priority than T 1. Each task points to an execution routine composed of three services called in the following order:

Get k (S); Release k (S); T erminate k (T k) with k ∈ [1, 2].
a) ruleComposeRoutine: The list of services considered in RTEPML is not exhaustive at the moment. The instructions described in RI TPN are currently activation and termination of task, acquisition and release of semaphore and waiting, notification and inhibition of event.

Let n be the number of call services described following:

{N S 1 , N S 2 , . . . , N S n } such that ∀i ∈ [1, n], N Si = Ins(N S , S i , ref S i ) with N S the
RI TPN describing a service, S i the instance name and ref S i the referenced instance name. The routine construction then implies n -1 compositions, each one having m j mergings of places with j ∈ [1, n -1]. The construction of a routine instance N R is given by (1).

Illustration 1 (see Figure 5):

By applying N R from (1), ∀k ∈ [1, 2], N T kBody is built from RI TPN {N Get k (S) , N Release k (S) , N T erminate k (T k) }.
This sequence describes in the order, an acquisition of S, a release of S and a termination of T k. b) ruleComposeEntryPoint: Each resource points to a routine described by N R previously formed. Consequently, N R is composed with

N C τ = Ins(N C , C τ , C τ )
where N C is the RI TPN describing a concurrent resource and C τ is the label indexed to identify each instance. The construction N EP of a concurrent resource instance with its executable body is given by (2) for m mergings (we admit here that specific extensions of N C τ have already been applied for the needs of the application in this equation).

Illustration 2 (see Figure 5): By applying N EP from (2), ∀φ ∈ [1, 2], N T askφ withBody is built composing N T φ with its entry point N T φBody . Prior to each composition, N T 1 has been extended since this task has the lowest priority. This extension has thus been achieved by the CoopSched(N T 1 , {T 2}) operation. c) ruleComposeConcurrentResources: At this stage, concurrent resources must be linked together with the aim of being scheduled by the same processor.

Let q C be the number of concurrent resources with their composed executable bodies such that ∀i C ∈ [1, q C ], each resource is described by N EP i C in accordance with N EP previously formed. The construction then implies q C -1 compositions, each one having m jC mergings with j C ∈ [1, q C -1]. The construction of N CR is given by (3).

Illustration 3 (see Figure 5): By applying N CR from (3), N DeployedApplication CR is firstly composed of N T 1 withBody and N T 2 withBody . d) ruleComposeInteractionResources: Note that the processor is also a shared resource. It will therefore be considered as an interaction resource. Let q I be the number of interaction resources considered such that ∀i I ∈ [1, q I ], each resource is described by N Ii I = Ins(N I , I iI , I iI ) with N I the TPN describing an interaction resource. Each interaction resource is composed with N CR previously formed. The global construction then implies q I compositions, each one having m jI mergings with j I ∈ [1, q I ]. The global composition N IR is given by (4).

Illustration 4 (see Figure 5): By applying N IR from (4), N DeployedApplication is finalized by composing N DeployedApplication CR , N S and N P roc .

VI. EXPERIMENTATION

We illustrate the use of the formal model generation process on a case study. This case study is adapted from a schedulability case [START_REF] Bucci | Timed State Space Analysis of Real-Time Preemptive Systems[END_REF] in the context of cooperative multitasking.

A. Case study description

We consider an application with three concurrent real-time activities implemented as three real-time schedulable tasks T 1, T 2 and T 3. The concurrency of these tasks emanates from a cooperative multitasking scheduler (based on a non-preemptive priority policy). Here are their characteristics:

• T 1 is periodic with period P 1 = a with a ∈ [0, +∞[ and has an execution time C1 ∈ [START_REF] Davis | GME: The Generic Modeling Environment[END_REF][START_REF] Taïani | Composing Real-Time Objects: A Case for Petri Nets and Girard's Linear Logic[END_REF].

• T 2 is sporadic with only a minimal delay of P 2 = 2a time units between two activations. The execution time of T 2 is C2 ∈ [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF]28].

• Finally, T 3 is periodic with period P 3 = 3a time units and has an execution time C3 ∈ [START_REF] Taïani | Composing Real-Time Objects: A Case for Petri Nets and Girard's Linear Logic[END_REF]28].

These three tasks are defined with the following priority order: T 1 > T 2 > T 3. Period a of T 1 is a parameter determining the limit condition of schedulability of the tasks.

B. Purpose

The formal model generation process will be applied for two different RTOS. The two chosen RTOS are those used to present RTEPML in Section III: OSEK/VDX [START_REF] Group | OSEK/VDX Operating System Specification, version 2.2.3[END_REF] and VxWorks [START_REF] Windriver | VxWORKS Programmer's Guide, version 6.9[END_REF]. Both are used in the industrial sector, have different API and behave differently. Roméo [START_REF] Lime | Roméo: A Parametric Model-Checker for Petri Nets with Stopwatches[END_REF], the modelchecking tool developed within our team is used to check the generated formal models. . . . ||N EP q C

N R = N S1 ||N S2 (end ref S 1 , start ref S 2 ) ֒→ (S S 1 →S 2 , ⊥) (r 2 S 1 ,
with ∀k ∈ [1, m] if k ≥ 3 then r k Cτ = r k R N CR = N EP 1 ||N EP 2 (processor (2)
(processor P roc , processor EP q C ) ֒→ (P EP 1 ...EP q C -1 →EP q C , processor P roc

) (r 2 EP 1 ...EP q C -1 , r 2 EP q C ) ֒→ (p 2 EP q C , r 2 EP q C ) . . . (r m q C -1 EP 1 ...EP q C -1 , r m q C -1 EP q C ) ֒→ (p m q C -1 EP q C , r m q C -1 EP q C ) (3)
with

∀k C ∈ [1, m jC ] and q C ≥ 2 if k C ≥ 2 then r kC EP 1 ...EP j C = r kC EP j C +1 N IR = N CR ||N I1
with ∀k I ∈ [1, m jI ] and q I ≥ 1, r kI P Ij I -1 = r kI Ij I

The aim is to verify the limits of the schedulability and the valid values of parameter a (i.e., the period of T 1). The application is schedulable if each activity always has at most one running instance.

The sufficient condition ensuring that the system is schedulable with a non-preemptive priority policy requires a processor load U such that:

U = n i=1 (C i /P i ) ≤ 1 (5)
with n representing the number of tasks, C i indicating the worst execution time of each task, and P i being the period (resp. minimal delay) of each periodic (resp. sporadic) task T i .

The theoretical expected values (calculated without taking into account the RTOS mechanism) for the a parameter are a ≥ 44 [START_REF] Jovanović | Integer Parameter Synthesis for Timed Automata[END_REF]. We expect that our formal verification on the two deployed application on VxWorks and OSEK/VDX leads to the same result.

C. Formal composition fragment

For the sake of clarity, Figure 6 T 3 has been chosen as an illustration instead of other tasks because it has the lowest priority. Consequently, it presents the most complex case. We can indeed note the presence of inhibition arcs since tasks are scheduled in accordance with a cooperative multitasking non-preemptive priority policy. The N T 3 instance has consequently been extended by applying CoopSched(N T 3 , {T 1, T 2}), for each targeted RTOS.

The body of T 3 is simplified and contains only one service call to suspend (in OSEK/VDX variant) or pend (in VxWorks variant).

On both Figure 6(a) and Figure 6(b), roles appear in bold to highlight connection points useful for the composition through the RI TPN. In a similar manner, the mergeable places connected by a hook-dotted arc are the ones located to compose T 3 and its body according to equation [START_REF] Miller | Model Driven Architecture (MDA) Guide, version 1.0.1[END_REF].

The same reasoning is obviously applied to T 1 and T 2 before composing them with T 3 in compliance with our formalization through equations ( 3) and (4).

D. Application verification

Once the models are composed, they have subsequently been checked using Roméo in order to determine the limit value of a so that the RTES application is schedulable. Given the structure of both nets, the systems are schedulable if, at any time, there is at most one token in each place (the nets are then said to be safe). Additionally, Roméo provides the set of values of parameter a for which the property is true. The outcome is given hereafter:

---Checking property AG[0,inf]bounded [START_REF] Lelionnais | Formal Composition Based on Roles within a Model Driven Engineering Approach[END_REF] Both results match the theoretical value mentionned earlier. We can thus observe that taking into account RTOS mechanisms does not change the theoretical result in this case. Expected constraints are therefore satisfied.

Other properties could be verified, for which taking RTOS mechanisms into account could have an impact. However, this is beyond the scope of this paper. Alternatively, the same property could also be verified starting from a different design model. For instance, we could attempt to model periodicity with a delay instead of an alarm. In such a case, we would be able to verify that the expected properties are not preserved.

However, the purpose of our present case study is simply to illustrate that we can support different platforms (OSEK/VDX and VxWorks) without changing our formalization rules.

VII. BENEFITS AND LIMITS

One of the major advantage of SExPIsTools is the multiplatform deployment process. The possibility of capitalizing a large number of RTOS models as a parameter of the process, satisfies both reusability and portability criteria. The role notion presented in this paper encourages us in this way to provide more genericity to our transformation rules. This role notion also fulfills the maintainability requirements. Composition rules have been written independently of the RTOS modeling. In addition, the formalization of these rules could have been done without dealing with other stakeholders concerns. Our Algorithm 1 has been strengthened, detecting errors (i.e., TPN fragments composition ambiguity within rules). As a result, the correctness of the generation process has been improved. Furthermore, a deployment on two RTOS with different mechanisms has been achieved to show our strategy. The same safety property of schedulability has been verified on both deployments. This illustrates both genericity and correctness of deployed application model construction in TPN.

Another important point is the behavioral modeling in TPN. This results in the possibility to apply verification activities. Moreover, the verification of time properties such as RTES time constraints is possible. However, to date, this synthesis is an ongoing sketch of proof. The purpose of such a work is to demonstrate the feasability to develop a versatile tool suite. This experimentation must deal with other aspects by considering:

• more complex RTOS mechanisms such as preemption, priority ceiling protocol or special queues of message box;

• other RTOS descriptions such as ARINC-653 [START_REF]Avionics Application Software Standard Interface, ARINC Specification[END_REF], which presents other concepts (e.g., memory partition);

• other verifications such as time constraints;

• more precisely the application, so that it is not seen as just an ordered sequence of called services.

VIII. CONCLUSION

In this paper, we have presented a first formalization of the formal model generation process of our SExPIsTools tool suite. As its name suggests, this process generates, from high-level design descriptions, a formal model of the deployed application on a specific RTOS.

The presented formalization focuses on both instantiation and composition rules of the generation process. Indeed, several formal model fragments describing parts of the RTOS and RTES behaviors need to be instantiated and composed. This results in a verifiable global model of the deployed application. The composition rules are independent of a specific RTOS thanks to the notion of role. This notion is an essential point of our strategy and represents a major benefit compared to other existing approaches.

This formalization leads to the definition of a new class of Petri Net, the Time Petri Net with roles and read/inhibitor arcs. A new operator, compared to our previous work [START_REF] Lelionnais | Formal Composition Based on Roles within a Model Driven Engineering Approach[END_REF], has been defined. It allows to model the cooperative scheduling of nonpreemptive tasks. This comes to strengthen the instantiation of RI TPN behavioral fragments according to a priority policy before composing them.

An example of a composition of an application with two RTOS (OSEK/VDX and VxWorks), taking into account the different behavior of the platform, has been given. Future prospects are scheduled in order to meet the needs identified in Section VII. We are exploring the possibility of extending the formalization with other model classes such as Scheduling TPN [START_REF] Lime | Formal Verification of Real-Time Systems with Preemptive Scheduling[END_REF], where both cooperative and preemptive scheduling are considered.

Fig. 1 :

 1 Fig. 1: Structural representation of OSEK/VDX platform

Fig. 2 :

 2 Fig. 2: Behavioral representation of OSEK/VDX platform

Fig. 3 :

 3 Fig. 3: Multi-platform deployment process within SExPIsTools

  ) Each routine behavioral instance is composed 3: i Rj ← ruleComposeRoutine(I S Rj ) 4: end for 5: for k = 1 to m do 6:

  } 17: end for 18: // c) All concurrent resources are composed 19: i CR ← ruleComposeConcurrentResources(I EP ) 20: // d) All interaction resources are composed 21: i IR ← ruleComposeInteractionResources(i CR , I I ) 22: M ← i IR

Definition 5 (

 5 Instantiation of RI TPN with roles): The instantiation of N denoted by N ins = Ins(N , ins, ref ) = Pins, Tins, Preins, Postins, m0-ins, Is-ins, Readins, Inhins, R ref , λins is defined by:

N 1 || N 2

 12 )֒→(p 12 ,r 12 ) ||N 3 (r 12 ,r 3 )֒→(p,r) = ||N 3 (r 2 ,r 3 )֒→(p 23 ,r 23 ) (r 1 ,r 23 )֒→(p,r)

  only shows the behavioral arrangement of task T 3 (N T 3 ) considering the OSEK/VDX norm (Figure 6(a)) on the left side, and the VxWorks platform (Figure 6(b)) on the right side.

Fig. 5 : 3 ACT IV AT IONT 3 activationT 3 SU SP EN DED terminatedStateT 3 [ 3 EN D semGiveT 3 SEM F U LLT 3 countT 3 SEM EM P T YT 3 discountT 3 P EN DEDT 3 suspendedStateT 3 [ 3 EN DT 3 N T 3 N T 3 3 endT 3 EN 3 P

 5333333333333333 Fig. 5: Deployed application of semaphore sharing composed in RI TPN

Fig. 6 :

 6 Fig. 6: RI TPN of periodic task implemented on two different RTOS

TABLE I : Tool suites comparison Code Formal Code & Formal Not adapted to RTOS

 I

	Metropolis [9]
	GME [10]

  ins, ref ) = N P ins = {p ins s.t. p ∈ P and p ⇁ p ins },

T ins = {t ins s.t. t ∈ T and t ∈ T, t ⇁ t ins }, R ref = {r ref s.t. r ∈ R and r ⇁ r ref }, ∀p ∈ P, ∀t ∈ T, ∀r ∈ R, s.t. p ⇁ p ins , t ⇁ t ins , and r ⇁ r ref we have: Pre ins (p ins , t ins ) = Pre(p, t), Post ins (p ins , t ins ) = Post(p, t), Read ins (p, t) = Read ins (p ins , t ins ), Inh ins (p, t) = Inh ins (p ins , t ins ), λ ins