Mohamed Bouali
email: mohamed.bouali@hds.utc.fr

Pavol Barger
email: pavol.barger@hds.utc.fr

Walter Schon
email: walter.schon@hds.utc.fr

Backward Reachability of Colored Petri Nets for Systems Diagnosis

Keywords: Colored Petri Nets (CPN), Backward Reachability, Structural Analysis, Dependability, Embedded Systems, diagnosis

Embedded systems development creates a need of new design, verification and validation technics. Formal methods appear as a very interesting approach for embedded systems analysis, especially for dependability studies. The chosen formalism for this work is based on Colored Petri Net (CPN)for two main reasons : the expressivity and the formal nature. Also, they model easily the static and the dynamic natures of the studied systems. The main challenge of this work is to use existing models, which describe the system structure and/or behavior, to extract the dependability information in a most general case and failure diagnosis information in a particular case. The proposed approach is a CPN structural backward reachability analysis. It can be split in two parts. The first one is to perform the proposed analysis : inverse CPN. It is obtained thanks to structural transformations applied on the original CPN. The second part is the analysis implementation. This part needs some complementary concepts of which the most important is the marking enhancement. The proposed approach is studied under two complementary aspects : algorithmic and theoretic aspects. The first one proposes transformations for the CPN inversion and the analysis implementation. The second aspect (the theoretical one) aims to offer a formal proof for the approach by applying two methods which are linear algebra and linear logic.

Introduction

In the last few years, the part of embedded systems in electronic and computer-based devices is ever growing. These omnipresent systems are used in most tasks and activities like communications, transportation or industrial processes. If we look at mobil phones, for example, we can see easily that their complexity increased highly in short period. What was, in the beginning, a heavy and cumbersome device becomes a light ergonomic tablet which includes a multimedia station, office applications, a networks terminal (WiFi, Bluetooth, 3G), a game console, etc. This amount of functionalities is necessary because of the harsh competition between manufacturers. This phenomenon produces two strong constraints on the embedded systems design process : 1) to market delays must be as short as possible ; and 2) the proposed product has to contain more functionalities than its rival. The product has also to respect strong financial and dependability conditions.

To take into account the increasing requirements on embedded systems, Methods and designing tools evolve in the same way as the system evolution. These tools have to deal with hardware increasing complexity, large size embedded software and reduced design delays. In addition, the designed system has to fulfill strict dependability requirements. Even for large consumption products, the dependability requirements are very rigorous. The example of a mobil phone is very illustrative : an entertainment application must not interfere with a voice call ; the later must respect a low electromagnetic emission level with a minimal energy consumption ; the battery, which must have a long autonomy period, must not overheat ; the whole system has to respect pollution norms. All these requirements are a very synthetic overview.

In this economic context, one of the research issues is the development of technics to take into account dependability requirements in embedded system design as the classical methods in this field (failure trees, reliability block diagrams, ...) reach quickly their limits when confronted to new requirements. Discrete event systems based modelling appears as an efficient way to reach this objective in the way that models describe system contents, components hierarchy, process events scheduling and they are easily analysable.

To deal with the present research issues, some works (see [START_REF] Müller | Duality in high level petri-nets: a basis to do diagnoses[END_REF], [START_REF] Portinale | Petri net models for diagnostic knowledge representation and reasoning[END_REF], [START_REF] Khalfaoui | Mthode de recherche des scnarios redouts pour l'valuation de la sret de fonctionnement des systmes mcatroniques du monde automobile[END_REF]) exploited the discrete event systems, and especially Petri nets, to perform some diagnosis and dependability analyses over different embedded systems types. The interest is not only to analyse the system. It is also to do the analysis in a formal framework thanks to mathematic tools like Linear Logic. We undertake, in this work, to extend and to generalize this approach. We choose Colored Petri Nets (CPN) based modelling. CPN are extension of Ordinary Petri Nets which integrates a tokens differentiation semantics. This choice is motivated by the large expressivity of CPN models, their mathematic basics allowing formal analysis, their compliance with embedded systems modelling (like parallel processing, communication and events). The CPN model can be easily analyzed by forward analysis, that means, by determining the causes we find consequences. The use of CPN to model the embedded systems gives some interesting issues. First of all, the CPN large expressivity, and especially arc expressions, make the model analysis more complicated than the case of Ordinary Petri Nets. Also, the failure diagnosis is difficult because, in diagnosis, consequences are known (a failure state is indicated using an alarm, a red light, a profil deviation, ...) and we aim to know causes. As in embedded systems, failures are very rare events, the forward analysis can't be applied by simulation.

This work studies a dual vision to the forward analysis called backward analysis. It is more adapted to diagnosis and aims to offer a design aided tool for dependable embedded systems. The basic idea is to transform (invert) the model to drive the analysis following consequences (usually which are failures). The inversion is performed thanks to structural transformations. The analysis is then driven on inversed models using complementary mechanisms such as the marking enhancement generalized to CPN. The algorithmic aspects are strengthened by two theoretic studies: the first one for the local aspect (inversion algorithms), the second one for global aspect (backward reachability analysis).

This paper is outlined as follows: after this introduction, the section 2 summarizes the related works in the Petri Nets Inversion Field. The section 3 presents a formal definition of a Colored Petri Net and then details the algorithms to perform the CPN inversion. The two following sections deal with theoretical aspects. The section 4 treats proofs using linear algebra formalism. The section 5 treats proofs using Linear logic formalism. The presented approach is illustrated in the case study of the section 6. Finally, the paper ends with a conclusion and some propositions to future works.

Related works

This paper deals with the backward reachability analysis based on an inverse CPN. The main objective is to perform a diagnostic analysis using a Petri Nets based modelling without the reachability graph with an exclusive use of the structure of the model itself. The PN model (and its extensions) inversion is based on different technics according to the objective and the extension. For ordinary Petri Nets, works directed by H. Demmou and R. Valette ([3], [START_REF] Medjoudj | Contribution l'analyse des systmes pilots par calculateurs : Extraction de scnarios redouts et vrification de contraintes temporelles[END_REF], [START_REF] Sadou | Aide la conception des systmes embarqus sr de fonctionnement[END_REF]) propose the use of an inverse Petri Net model. These ones are obtained by inverting arc directions in the original Petri Nets. The benefit of this method are its theoretical and implemental simplicity. It is used to deriving feared scenarios (which might lead the system to critical situation). But this method suffers from limitations when applying it to Colored Petri Nets. Portinale, in [START_REF] Anglano | B-W analysis: a backward reachability analysis for diagnostic problem solving suitable to parallel implementation[END_REF], proposes the B-W Analysis. It is a backward reachability through Behavioral Petri Net (BPN) models which introduce a (reduced) semantic of tokens differentiation. Nevertheless, the proposed extension is very particular and endowed with a limited expressivity. Concerning the CPN class, Cho et al. [START_REF] Cho | Safety analysis using colored petri nets[END_REF] proposes a method inspired from [START_REF] Leveson | Safety analysis using petri nets[END_REF]. It is based on a modified version of the CPN fundamental equation. It allows to express a backward transition firing.

It allows also to consider the transition firing even if some tokens are missing. The problem of this method is the association of each such transition firing with a predicate which can speed down analysis and even make it impossible because of undecidability introduced for each transition. In a very close context to CPN, Muller and Schnieder [START_REF] Müller | Duality in high level petri-nets: a basis to do diagnoses[END_REF] propose an approach using High Level Petri Nets (HLPN). It generalizes, to HLPN, the dualization formula of [START_REF] Kowalsky | Lineare Algegra[END_REF] initially applied for Ordinary PN models. It transforms the model by changing places by transitions, transitions by places and inverting arc directions. Physical interpretation of modelled phenomena becomes very hard and the practical application of this method shows that the main benefit of the dualization is the limitation of some calculating intervals but the analysis itself is still done on the original HLPN models.

Inverse Colored Petri Net

The Backward Reachability in CPNs is a dual concept to the Forward Reachability. That is, if a marking M f is reachable from M 0 , we say that M 0 is backward reachable from M f . By backward reachability we mean that M 0 is the cause or the source of M f . Our contribution concerns firstly the generalization of the backward reachability from the PN class to the CPN class and secondly the development of adapted transformation rules. The generalization implies a definition of an inverse CPN which is obtained by applying the proposed transformations on the original CPN.

Definition of Petri Net and Colored Petri Net

A Petri Net [START_REF] Petri | Communication with automata[END_REF], called also an Ordinary Petri Net or a Place/Transition Net, is a directed bipartite graph defined by the 4-tuple (P, T, P re, P ost), where: P is a finite set of places, T is a finite set of transitions (P ∩ T = ∅), P re is the backward incidence application, P ost is the forward incidence application.

The notation of Colored Petri Net noted CPN [START_REF] Jensen | High-level Petri Nets : Theory and Application[END_REF] introduces the notion of token types, namely tokens are differentiated by colors, which may be arbitrary data values. Each place has an associated type determining the kind of data that the place may contain. A non-hierarchical CPN is defined by the 9-tuple (Σ, P, T, A, N, C, G, E, I) where :

• Σ is a finite set on non-empty types,

• P is a finite set of places,

• T is a finite set of transitions,

• A is a finite set of arcs such that:

P ∩ T = P ∩ A = T ∩ A = ∅, • N is a node function. It is defined from A into P × T ∪ T × P , • C is a color function. It is defined from P ∪ T into Σ,
• G is a guard function. It is defined from T into expressions such that:

∀t ∈ T : [T ype(G(t)) = B ∧ T ype(V ar(G(t))) ⊆ Σ],
• E is an arc expression function. It is defined from A into expressions such that:

∀a ∈ A : [T ype(E(a)) = C(p(a))MS∧T ype(V ar(E(a))) ⊆ Σ]
Where p(a) is the place of N (a),

• I is an initialization function. It is defined from P into closed expressions such that:

∀p ∈ P : [T ype(I(p)) = C(p) M S ]
For practical reasons, we write E in a split form P re and P ost (as used in [START_REF] Haddad | A reduction theory for coloured nets[END_REF]) such that P re (resp. P ost) is the backward (resp. forward) incidence application. It is defined as E where p(a) is the place of a part of N (a) defined from A to P × T (resp. T × P ).

CPN transformation for the definition of an inverse CPN

Let R = (Σ, P, T, A, N, C, G, E, I) be a CPN and let R ′ = (Σ ′ , P ′ , T ′ , A ′ , N ′ , C ′ , G ′ , E ′ , I ′ ) be the inverse CPN of R. To define R ′ , we perform some transformations on R. These transformations are directly dependent on the CPN structure. Consequently, we have to define a transformation for each structure case studied. Nevertheless, the most common transformations in representative cases are presented in this section.

The following transformations (trivial, basic, parallel, parametric) are structure changes applied to CPN and result in inverse CPN. Their usefulness is to allow performing the backward reachability analysis. Each transformation is a generic algorithm applied on transitions type having same characteristics. These characteristics are ⋆ the nature of arc expressions (constant, variable, function), ⋆ the number of functions using the same variable (none, one, two or more), ⋆ arc orientation (input, output).

The combination of these three items leads to 81 possible cases. This number decrease quickly because many associations are obsolete like input functions, output variables 1 and functions without input variables. A second criterium reduces the possible number of associations : the number of constants and number of input arcs marked by the same variable have not the effect on the transformation type to apply but their presence/absence influences. At the end, among 81 initial possible cases, only 5 are relevant : input constant and output constant (trivial transformation), input variable and exactly one output function (basic transformation), input variable and no output function or more than two output functions (parametric transformations) and finally, input variable and more than one output function using it (parallel transformation). Combinations of different transformations types are possible. An example will be given to illustrate this case called mixed transformation. 1 A variable associated to output arc is considered as an identity function

f(x) x p1 p2 t x   x f 1      x G t       x f G t 1  Inversion -a- -b-

Trivial and basic transformations

Figure 1-a-shows a trivial case of a CPN inversion. Arcs (input and output) are marked with constants a, b. In this case, it is enough to generalize the definition of the inverse PN to CPN obtaining : P re ′ (p2, t) = P ost(p2, t) P ost ′ (p1, t) = P re(p1, t) Note that, in the original CPN, M 0 = a .p1 gives M 1 = b .p2 by firing t. In the inverse CPN M 1 = b .p2 gives M 0 = a .p1 by firing t. Thus, we performed the backward reachability using the inverse CPN.

Figure 1-b-shows the case where the input arc is marked with a variable x, the output arc is marked by a function f (x) and a guard G(x) can be associated to the transition t. Generalized application of the rule shown before (inverting arcs directions) can lead to the construction of an incorrect net. In this example, the input arc would be marked with a function while the output arc would be marked with the variable of this function. That leads to the impossibility for the function evaluation. This is why we suggest marking the input arc by the variable, the output arc by the function f -1 and update the guard to express new constraint associated to the transition. This assumes the necessity to know whether the function f is reversible. If yes, it is necessary to define its inverse noted f -1 . This transformation gives :

   P re ′ (p2, t) = P re -1 (p1, t) P ost ′ (p1, t) = P ost -1 (p2, t) G ′ t (P re ′ (p2, t)) = G t (P ost -1 (p2, t))
P re -1 (p1, t) denotes the transformation of the arc P re(p1, t) which is marked with a new variable defined on f -1 domain. P ost -1 (p2, t) denotes the transformation of the arc P ost(p2, t) which is marked by f -1 (the opposite reverse of P ost(p2, t) marking function).

Parametric transformations

Some CPN structures can't be transformed to get deterministic markings in the backward reachability. The reason is that the inversion process could be assimilated to mathematic operations whose solutions may be intervals. The CPN inversion, in these cases, is parametric. That means that some additional Figure 2-a-shows a case where output arc is marked with a multivariable function. In this case, the CPN is not directly reversible. The values of variables {x, y} can not be deduced by knowing only the value of g(x, y). The partial (parametric) solution proposed consists in finding the admissible values of one variable knowing other variable values and the function result. As illustrated in Figure 2-a-, the firing t (in inverse CPN) requires tokens either in {p2,p3} or in {p1,p3}. Functions g -1

x (y) and g -1 y (x) are partial inverses of g(x, y). Figure 2-b-shows a case of a variable which is not associated with a function. We note that input arc expression is a variable and output arc (or arcs) expression is constant. This CPN inversion is similar to the case of Figure 1-a-, except the arc P ost ′ (p1, t) which is marked by a parametric expression noted AnyV alue. It means that this arc expression can take all values out of t in the set of the place p1 color.

Parallel transformations

The term 'parallel' means the existence of a shared variable. Figure 3 shows the case where the same variable is used by more than one function (two functions in this case). To inverse this CPN, we have to calculate the inverse of only one function using the shared variable (which supposes existence of, at least, one reversible function).

Let f be a reversible function. In the original CPN (shown on the left in Figure 3), the transition t firing produces two tokens (in p2 and p3). Each token value results from a function applied to the shared variable : function f to the token in p2 and function h to the token in p3. The inverse CPN must produce a token in p1 by firing t whose preconditions are p2 and p3. But it is not enough to have tokens in p2 and p3 to fire t because token values (in p2 and p3) must have coherent values towards applied functions f and h. For this reason, we define a guard associated to transition t. It checks that the value of f -1 (x) applied to h gives as the result the value of y (token initially in p3). If the guard value is True, t will be fired, then the initial marking of p1 will be found. If the guard value is False, t will not be fired. The algorithm describing the parallel transformation can be written as follows: Let R be a CPN containing a variable

p1 p2 t x p3   x h   x f 1  p1 p2 t x p3 y       x f h y 1   Inversion   x f
x (P re(p, t) = x) which is shared by n functions f 1 , f 2 , . . . , f n (P ost(qi, t) = f i (x), i = 1 . . . n) with f 1 inversible.
The inverse CPN is defined by :

• P re ′ (q1, t) = P re -1 (p, t), • P re ′ (qi, t) = Id i , i = 2 . . . n, • P ost ′ (p, t) = P ost -1 (q1, t), • G ′ t = i=2 n [P re ′ (qi, t) == f i (f -1 1 (P re ′ (q1, t)))].

Mixed/Complexe transformations

Transformations previously presented are "simple", easily recognizable and transformable. However, in real models, transitions can gather some characteristics which don't allow them to be categorized in a unique transformation type (eg. parametric and parallel transition at the same time). The transformation of such transition is a mix of elementary transformations. To perform it, all transformation types to apply must be identified and applied in a pertinent order. The procedure often begins by parallel transformation, followed by the parametric, the basic and the trivial. This sequence is a general indication. But for each case, the transformation have to use the maximum available information and answers the expressed need. In real use, the dynamic available information influences the structural transformation choice to apply (practical examples can be found in the case study).

Figure 4 shows a mixed case where some input arcs are marked with variables {x, y} and other arcs by constants {a, b}. Output arcs are marked with constants {c} and reversible functions {f, g}. This CPN inversion is a mix (generalization) of a trivial and a basic transformations. For arcs marked with a constant, it is sufficient to generalize the rule applied on PNs (changing arcs direction). For the remaining arcs, we have to

c q3     y x G t ,         y g x f G t 1 1 ,   Inversion   x f   x f 1    y g 1 

Special transformations

Among the huge possible cases of generalized CPN structures, there exists some of them which transformation is difficult. The problem is directly related to the model itself. Whe following presents some of the most frequent cases and proposes solutions (tradeoffs) to perform the backward reachability analysis.

Loop transformations

The models aimed with this study show a recurrent presence loops. Characterization of these cycles can be very difficult in CPN because of the token values evolution. In the case of Ordinary Petri Nets, [START_REF] Sadou | Reliability analysis of discrete event dynamic systems with petri nets[END_REF] reduces the number of feared paths returned by the backward reachability by detecting cycles and analyzing them only once. This method can not be generalized to CPN since two successive executions of the same structural cycle can produce tokens with very different values. An partial solution can be found in some cases by applying, for example, transitions agglomeration [START_REF] Haddad | A reduction theory for coloured nets[END_REF].

The minimal cycle is a loop between a place and a transition representing a very simple timer or sampler. To avoid a repetition of iterations, we propose the use of sequences, and especially, arithmetic and geometric sequences allowing to determine in only one operation the final value after a given number of iterations or, by duality, to calculate the number of necessary iterations to reach a value without having to simulate the loop. So, the main idea here is to consider that the concerned loops have a progression which can be compared to a sequence and according to the form of arc expression, token values generated by the loop execution can be considered as terms of sequences and can be deduced easily.

Constraint programming transformations

The model inversion often supposes the existence of, at least, one inversible function. This one gives source values for known results. In some cases, the requested function is inversible by pieces, inversible in a subset of the colors set, partially inversible or pseudo-inversible [START_REF] Diaz | Les rseaux de Petri : modles fondamentaux[END_REF]. The problem is when the inversible function does not exist. One of possible solutions is the use of constraint programming [START_REF] Fruewirth | Essentials of Constraint Programming[END_REF]. This solution express the relation between inputs and outputs in a constraint form instead of a direct (function) form. The use of constraints implies the introduction of the decidability notion. In other words, if the constraints are resolved, the solution exists. In contrast, if constraints are not resolved, no response can be made about the existence on solution.

Supplementary mechanisms

The transformation rules presented above allow the inversion of the CPN structure. That is, they allow to obtain a structure on which the backward reachability can be performed. Sometimes, this analysis becomes impossible because the lack of information consisting on a partial knowledge of the system state. So, in certain situations, the final marking (or the intermediate marking) does not allow a complete analysis. This is why, in order to analyse the inverse dynamic behavior, the following complementary principles have to be introduced.

Potentially Valid Transition

In a marked CPN, a transition is potentially valid if it has, at least, 1.) one precondition place marked by a token whose value is compatible with the transition firing (i.e. token compatible with arc expression and guard) ; and 2.) one precondition place which is not marked by a token whose value is compatible with the transition firing. Identifying this kind of transitions allows the marking enhancement.

Marking Enhancement

The marking enhancement is a mechanism allowing to complete the information about a model by adding assumptions about the modelled system state (additional tokens). It is done when constructing successor states. Sometimes, the immediate successor of a given state (which is equivalent to fire a transition) can only be constructed with help of added tokens with appropriate values in certain places. The marking enhancement interpretation consists in assuming that the system is in some given state allowing it to operate. This mechanism has to be performed if only a part of the token distribution is available.

Partiel Order of transition firings

The partial order in CPN is a relation between transitions (not necessary all transitions of the model) noted by "≺" [START_REF] Portinale | Petri net models for diagnostic knowledge representation and reasoning[END_REF]. This relation defines a precedence in transitions firing. For two transitions t1 and t2, the formula t1 ≺ t2 means that the firing of t1 occurs before the firing of t2 (all properties of this relation are detailed in [START_REF] Portinale | Petri net models for diagnostic knowledge representation and reasoning[END_REF]). The notion of partial order is very important in the backward reachability analysis in order to decide which transition has to be fired first at each step of the analysis evolution. The partial order in the backward reachability is inverted comparing to forward analysis. For example, if in the original CPN, the relation t1 ≺ t2 is true so, in the inverse CPN, the formula t2 ≺ t1 is also true.

Linear algebra

The structural analysis with backward reachability uses the inverse CPN which is obtained by performing structural transformations on the original CPN. Question asked then are : 1) are transformation algorithms previously presented correct? and 2) is the backward analysis performed thanks to inverse CPN correct?

The answer to these questions needs the study of two theoretical aspects of CPN inversion. The first one, linear algebra, concerns each transition as standalone. The definitions are inspired from [START_REF] Haddad | A reduction theory for coloured nets[END_REF], [START_REF] Goblot | Algbre Linaire[END_REF], [START_REF] Richard | Algbre et analyse pour l'automatique[END_REF] and [START_REF] Cottet-Emard | Algbre linaire et bilinaire : : cours et exercices corrigs[END_REF]. The methodology is inspired from [START_REF] Haddad | A reduction theory for coloured nets[END_REF] concerning CPN theory and precisely Well Formed Petri Nets (WPN). The second theoretical aspect (linear logic) is detailed in section 5.

Definitions and preliminaries 4.1.1. Bilinear form

A form is an application of a vector space in his number set K (the number corp is a number set defining external vectors multiplication such as integers, reals or complexes). A Bilinear form is an application defined on a couple of vectors x and y, from the Cartesian product of E ×F that have the same number corp. For a given application f , we write:

f : E × F → K (x, y) → f (x, y)
A form is said linear for its first variable if for each y 0 , the application f which, to x, associates f (x, y 0 ) is linear. In the same way, the form is linear for its second variable if for each x 0 , the application f which, to y, associates f (x 0 , y) is linear. If the two previous proprieties are satisfied, the form is bilinear.

Similitudes

Let consider E to be a space provided with the bilinear form φ : E × E → K. Let f : E → E be a linear application. We define the symmetric bilinear form φ f by

φ f : E × E → K (x, y) → φ(f x, f y)
We say that f is a similitude of φ multiplier µ (noted also µ(f )) if the following propriety is verified:

∀x ∈ E, ∀y ∈ E, φ(f x, f y) = φ f (x, y) = µφ(x, y)
The result produced by this definition is that the orthogonal applications are similitudes (whose multiplier is 1).

Equivalence between linear and bilinear forms

A color function can be defined either from Bag(C(t)) 2 to Bag(C(p)) or from C(t)×C(p) to N. The two forms are useful to define CPN transformations (developed later in this work). It is why the same symbol is used in the two forms. The formula that gives the relation between the two forms is expressed as follows:

f (c) = c ′ ∈C(p) f (c ′ , c).c ′
Where f (c) denotes the mapping of c to an item of Bag(C(p)) by f as a linear application and where f (c ′ , c) denotes the mapping of (c ′ , c) to an integer value. We note that no confusion can appear since the first definition implies one argument while the second definition implies two arguments.

Multi sets properties

• The Identity function of Bag(C) (noted Id) is defined as Id(c) = c. This function can also be defined as

Id(c ′ , c) = (If (c = c ′ )1 else 0) • A function f from Bag(C) to Bag(C) is orthonormal if and only if there exists a substitution σ of C such that f (c) = σ(c). The equivalent definition is: f (c ′ , c) = (If (σ(c) = c ′ )1 else 0).
We can also write this condition as a similitude form [START_REF] Evangelista | Syntactical colored petri nets reductions, Automated Technology for Verification and Analysis (ATVA 05)[END_REF]:

∀c ∈ C, ∃c ′ ∈ C ′ , f (c, c ′ ) = 1 and ∀c ′ ∈ C ′ , ∃c ∈ C, f (c, c ′ ) = 1 • The projection from Bag(C × C ′ ) to Bag(C) (noted P roj) is defined by P roj( c, d ) = c. The equivalent definition is: P roj(c ′ , c, d ) = (If (c = c ′ )1 else 0). • A function f from Bag(C) to Bag(C ′ ) is quasi-injective if and only if ∀c ′ ∈ C ′ , ∀c 1 ∈ C, ∀c 2 ∈ C : f (c ′ , c 1 ) = 0 ∧ f (c ′ , c 2 ) = 0 ⇒ c 1 = c 2 • A function f from Bag(C) to Bag(C ′ ) is unitary if and only if ∀c ′ ∈ C ′ , ∀c ∈ C : f (c ′ , c) = 0 ∨ f (c ′ , c) = 1

Composition

Let f be a function from Bag(C) to Bag(C ′ ) and g a function from Bag(C ′ ) to Bag(C ′′ ). The composition of f and g is a function g • f from Bag(C) to Bag(C ′′ ) defined by :

g • f (c) = g(f (c)) = c ′′ ∈C ′′ c ′ ∈C ′ g(c ′′ , c ′ ).f (c ′ , c) .c ′′

Orthonormalization of a transition

Let R be a CPN where R = (Σ, P, T, A, N, C, G, E, I), t be a transition of R and f an orthonormal function of C(t). The CPN R r = (Σ r , P r , T r , A r , N r , C r , G r , E r , I r ) obtained by forthonormalization of t is defined by: By its definition, the function P re(p, h) is orthonormal, i.e. there exists a substitution σ of C such that f (c) = σ(c). Using this substitution, we define the inverse substitution σ -1 . This definition is possible thanks to a part of the orthonormality condition which is ∀c

• P r = P , T r = T • ∀t ∈ T r , ∀p ∈ P r , C r (t) = C(t) AND C r (p) = C(p) • ∀t ′ ∈ T r -{t},
′ ∈ C ′ , ∃c ∈ C, f (c, c ′ ) = 1.
This inverse substitution is associated to a new color function noted P re -1 defined from Bag(C(p)) to Bag(C(h)). Expressions of P re -1 (p, h) and P ost(p, h) can be expressed as follows:

       P re -1 (p, h)(c) = c ′ ∈C(h) P re -1 (p, h)(c ′ , c).c ′ for c ∈ C(p) (1) P ost(p ′ , h)(c ′ ) = c ′′ ∈C(p ′ ) P ost(p ′ , h)(c ′′ , c ′ ).c ′′ for c ′ ∈ C(h) (2)
Replacing c ′ expressed in (1) by (2) gives :

c ′ ∈C(h) P re -1 (p, h)(c ′ , c). c ′′ ∈C(p ′ ) P ost(p ′ , h)(c ′′ , c ′ ).c ′′ = c ′′ ∈C(p ′ ) c ′′ .P ost(p ′ , h)(c ′′ , c ′ ). c ′ ∈C(h) P re -1 (p, h)(c ′ , c) = c ′′ ∈C(p ′ ) c ′′ . c ′ ∈C(h) P ost(p ′ , h)(c ′′ , c ′ ).P re -1 (p, h)(c ′ , c) = P ost(p ′ , h) • P re -1 (p, h)(c ′′ , c)
Note that the relation between C and C ′′ is expressed as P ost(p ′ , h) • P re -1 (p, h) which is defined from C to C ′′ . This result can be obtained by orthonormalization of the transition h with the orthonormal function P re -1 (p, h). This operation composes P re(p, h) with P re -1 (p, h) and also P ost(p ′ , h) with P re -1 (p, h). Note that P re(p, h) • P re -1 (p, h) equals to identity (Id), which explains the result.

Since the two CPNs are equivalent, we define a relation (noted ⋄) such that f ⋄ g = g • f -1 . This operator allows to express that f is a precondition and g is a postcondition and is useful for handling easily the symbolic operations applied to incidence matrices of the CPN.

Dual CPN Notation

In this study, we exploit two different notations of CPN : generalized PN and Well-Formed PN. The first one is very useful to model real systems. It is implemented in softwares like the CPN Tools 3 ([20]). It marks input arcs (of a given transition) by variables and output arcs by functions. This notation is equivalent to the alternative one ( [START_REF] Haddad | A reduction theory for coloured nets[END_REF]) which is useful to perform formal proofs. In the second notation, a transition takes its color values in a set defined by a cartesian product

C = C 1 × • • • × C n
where each C i corresponds to original colors domain of an arc expression. So P re i = P roj i (C) noted P roj i (or constant). P roj i projects transition color values to its i th precondition place. Variables of output function take their values in C. Figure 6 illustrates a concrete example.

C = C(t) = C 1 × C 2 × C 3 × C 4 .
The function f 1 takes its values in C 1 such that C 1 = P roj 1 (C) (that can be noted P roj 1 ). In the same manner, f 2 takes its values in C 2 which is a projection of C on its second item.

CPN transformations proofs

The inversion applied to ordinary PN can be generalized to CPN in two steps: 1) inversion of arcs direction and 2) CPN functions transformation. The application of only the first step, i.e. generalize the inversion method as announced for ordinary PN, may lead to the construction of a CPN whose precondition expressions are neither orthonormal, nor unitary, nor quasiinjective. This is why it is necessary to check and to transform (second step).

Arcs inversion

This proof is illustrated in the trivial case where input arc is marked by identity function (Id) and the output arc by a function f . In this case, it is necessary to know whether f is orthonormal. If yes, it is necessary to define its inverse f -1 . Applying the two steps mentioned above leads to associate the input arc with the identity function Id and the output arc with f -1 .

The proof is a generalization of the demonstration applied in Ordinary PN. The forward relation between places (one step) is given by P re.P ost T and the backward relation (one step) is given by the transpose of this last matrix which is P ost.P re T . Let's check these relations in the Trivial transformation case.

We have :

P re = Id 0 , P ost = 0 f , P re.P ost T = 0 Id ⋄ f 0 0
So, the forward relation between the places is verified by the expression Id ⋄ f = f • Id -1 = f . In addition, we have backward relation P ost.P re T = 0 0 f ⋄ Id 0 which verifies a relation from cartesian product of places color sets through the term f ⋄ Id. As f ⋄ Id = Id • f -1 , the algorithm provides the inverse CPN.

Mixed transformations

Figure 6 shows a mixed case noted with the two different notations : generalized PN and Well-Formed PN. The proof of this case merges those of trivial and basic transformations.

Proof:

Figure 7 illustrates the two steps allowing to inverse the CPN. The first one is the inversion of arcs direction. It remains to prove the transformation to the interpreted form of the CPN.

Let's note by C colors domain of the transition such as

C = C 1 × C 2 × • • • × C n . We define f i : C i → C ′ ,
and a projection P roj i : C → C i . The composition of the two functions is defined by

f i (P roj i ) : C → C ′ .
Let's note by Ci The colors domain defined by

Ci = C 1 × . . . C i-1 × C ′ × C i+1 × • • • × C n .
We define fi : Ci → C ′ with fi (x) = (proj 1 (x), . . . , P roj i-1 (x), f i (P roj i (x)), P roj i+1 (x), . . . , P roj n (x)). We define also a projection P roj i : Ci → C. The composition of the two functions is defined by

P roj i ( fi ) : C → C ′ .
Note that f (P roj i ) and P roj i ( fi ) gives the same result. P roj i ( fi )(x) = P roj i (proj 1 (x), . . . , P roj i-1 (x), f i (P roj i (x)), P roj i+1 (x) . . . , P roj n (x)) = f (P roj i )(x) Finally, we define the function f -1 i such as f -1 i (x) = (proj 1 (x), . . . , P roj i-1 (x), f -1 i (P roj i (x)), P roj i+1 (x) . . . , P roj n (x)) The transformation is done thanks to orthonormalization sequence using f -1 i . For each function f -1 i , three different cases are identified as illustrated in Figure 8. Part a. Figure 8.a shows a part of the transition composed by an input arc marked with the function f i • P roj i and an output arc marked by P roj i . The composition with the function f -1 i gives the following results: In input arc side we have

t p i Proj q i i Proj f  t p j Proj q   i j j j Proj f   t a p q c … … … … -a- -b- -c-
f i • P roj i • f -1 i = f i • f -1 i • P roj 1 = P roj i In output arc side, we have P roj 1 • f -1 i = f i • P roj i
We conclude that this composition produces a part of transition which can be evaluated (functions indexed by i).

Part b. Figure 8.b shows a part of the transition composed by an input arc marked with the function f j •P roj j (such as j = i) and an output arc marked with the function P roj j . The composition with the function f -1 i gives the following results. At input arc side, we have f j •P roj j • f -1 i = f j •P roj j . At output arc side, we have P roj j • f -1 i = P roj j . So, this composition does not affect other functions that those indexed by i. Part c. Figure 8.c shows the remaining part of the transition, means, arcs marked with constants. Knowing that composition does not affect constants, this still true for the composition with f -1 i . To complete the transition transformation, it is enough to repeat precedent steps for all functions marking input arcs.

Parallel transformations

As in previous inversions, the proof of the parallel transformation is composed of two steps. The first one is the inversion of arc directions. So, it remains to prove the transformation on the interpreted form of the inverse CPN. This proof can be performed in the case of two parallel functions, and then, generalized for any number of parallel functions.

The transformation, as illustrated in Figure 9 can be done by an orthonormalization of the transition. The choice of the orthonormal function is arbitrary (f or g in Figure 9). This gives two possible inverse CPNs which are equivalent. The scheme Figure 9 left is obtained by a composition with g -1 and Figure 9 right is obtained by a composition with f -1 . The two inverse CPNs are equivalent so that the functions f -1 and g -1 are applicable to a subset of the transition color domain c ∈ Bag(C(t)) where f -1 (c) = g -1 (c). For this color subset, f • g -1 = Id and g • f -1 = Id. By substitutions in arc expressions, illustrated in Figure 9 (left and right), identical results are obtained. The inverse CPN obtained is endowed with a restrictive condition about the color domains. This condition is called guard and it is expressed with the notation related to the transition.

p1 p2 t Id f p3 h 1  f p1 p2 t Id p3 1  f h  p1 p2 t 1  g f  1  g p3 Id -a- -b- -c-

Linear logic

The second theoretical aspect studied in this work aims to prove the correctness of results obtained by the backward reachability analysis using the whole (or a part) of the inverse CPN. The proofs are based on the Linear Logic (LL) formalism. Previous studies, like [START_REF] Khalfaoui | Mthode de recherche des scnarios redouts pour l'valuation de la sret de fonctionnement des systmes mcatroniques du monde automobile[END_REF] and [START_REF] Valette | Rseaux de petri pour la dtection et le diagnostic[END_REF], used LL to prove reachability methods in ordinary PN but not in higher models. The challenge of this paper is to adapt and to use the LL formalism for CPN proofs.

Introduction to Linear Logic

Linear Logic was introduced by Girard [START_REF] Girard | Linear logic[END_REF]. Its expressive power is demonstrated by some very natural encodings of computational models such as Petri Nets, counter machines, Turing machines and others [START_REF] Lincoln | Linear logic[END_REF]. The Linear Logic differs from a classic logic by introducing the notion of a ressource. A classic logic deals with static propositions where each proposition is either true or false. Because of the static nature of propositions in a classic logic, there may be duplicated [P ⇒ (P ∧ P )] and/or discarded [(P ∧Q) ⇒ P ]. Both of these propositions are valid in classical logic for any P and Q. In Linear Logic, these propositions are not valid because no information is available about how the second P is produced (in the first proposition) or where Q is consumed (in the second proposition). The rules of Linear Logic imply that linear propositions stand for dynamic properties or finite resources.

For example, let us consider the propositions E, C and T conceived as resources: 1)E: one Euro, 2)C: cup of Coffee, 3)T: cup of Tea. Consider the following axiomatization of a vending machine: 1)E ⇒ C, 2)E ⇒ T . Then in classical logic, the proposition E ⇒ (C ∧ T ) can be deduced. Which may be read as "With one Euro, I may buy both a cup of coffee and a cup of tea". Although this deduction is valid in classical logic, it is a nonsense in the intended interpretation of propositions as resources: two cups of hot drinks cannot be bought with one Euro from the described vending machine.

In this work, we only use a fragment of the Linear Logic related to Petri Nets which is the MILL fragment (Multiplicative Intuitionistic Linear Logic). This fragment contains a multiplicative connector TIMES (⊗) and a linear implication connector (⊸). The TIMES connector traduces the accumulation of resources. The proposition A⊗A means that two resources A are available. The Linear implication (⊸) expresses the causality between production and consumption of resources. The proposition A ⊸ B means that when the proposition A is consumed, the proposition B is produced. The meta-connector "," (comma) is cumulative [START_REF] Girard | Linear logic[END_REF].

Sequent calculus

The sequent calculus notation, due to Gentzen [START_REF] Gentzen | The Collected Works of Gerhard Gentzen[END_REF], is composed of two sequences of formulas separated by a turnstile symbol (⊢). The formula Γ, Γ ′ ⊢ ∆, ∆ ′ means that the conjonction of Γ and Γ ′ allows to deduce the disjonction ∆ or ∆ ′ . A sequent calculus proof rule consists of a set of hypothesis sequents, written above a horizontal line, and a single conclusion sequent, written below the line, as follow:

Hypothesis 1 Hypothesis 2 Rule attribute Conclusion
The goal is to construct a proof tree. Starting from the sequent, and applying step by step some adapted rule, the proof consists on eliminating the connectors. These rules are shown in Figure 10 where : A is an atom ; F , G and H are formulas ; Γ and ∆ are blocs of formulas separated by commas. The attribute indicates whether the rule is applied at left (L), at right (R) or to the whole sequent (empty attribute). The interest of Linear Logic is that it provides, for example, a natural and simple coding of Petri Net reachability [START_REF] Lincoln | Linear logic[END_REF]. Based on the sequent calculus, Linear Logic helps to get a necessary and sufficient condition of reachability from one marking to another, thanks to the equivalence between the reachability in a Petri Net and the provability of the corresponding sequent [START_REF] Girault | Formalisation en logique linaire du fonctionnement des rseaux de petri[END_REF].

id A ⊢ A Γ ⊢ F ∆, F ⊢ H Cut Γ, ∆ ⊢ H Γ, F, G, ∆ ⊢ H Exchange Γ, G, F, ∆ ⊢ H Γ ⊢ F ∆, G ⊢ H ⊸ L Γ, ∆, F ⊸ G ⊢ H Γ, ∆, F ⊢ G ⊸ R Γ, ∆ ⊢ F ⊸ G Γ, F, G ⊢ H ⊗ L Γ, F ⊗ G ⊢ H Γ ⊢ F ∆ ⊢ G ⊗ R Γ, ∆ ⊢ F ⊗ G
Moreover Linear Logic gives the partial firing order of the different transitions in order to reach the final marking M f from an initial marking M 0 [START_REF] Demmou | Critical scenarios derivation methodology for mechatronic systems[END_REF].

Linear logic and Petri Nets

To translate a Petri Net to Linear Logic, a logical formula is associated for each marking and each transition. The left hand of the initial sequent must hold the list of all the transitions that can be fired to obtain a marking M f from an initial marking M 0 . The building of the proof generates a proof tree beginning by a sequent and finishing by the identity axiom. For a given Petri Net, the translation is performed as follows:

• An atomic proposition P is associated with each place p of the Petri Net,

• A single sequent using the multiplicative conjunction TIMES (⊗), is associated with each marking, precondition and post-condition of transition,

• For each transition t of the net, an implicative formula is defined as follows:

t :

i∈P re(pi,t)

P i ⊸ o∈P ost(po,t) P o
To show the reachability between two markings M 0 and M f , the proof of the sequent M 0 , t 1 , . . . , t n ⊢ M f is performed as follows: first, the initial marking M 0 is replaced by separate atoms by applying the ⊗ L rule as many times as necessary. Then, by applying ⊸ L , the causality relation of atoms (from M 0 to M f ) can be extracted. Each time the ⊸ L rule is applied, the ⊗ L rule is applied if necessary to separate atoms connected with ⊗. The proof continues essentially at the right side of the tree because after each application of the ⊸ L rule, the left member is proven by using, if necessary, the ⊗ R rule. The sequent proof ends when all implicative formulae (expressing transitions) are eliminated.

Linear Logic and Colored Petri Nets

The application of Linear Logic to CPN reachability analysis requiers a translation between the two models (from CPN to Linear Logic). This translation has to respect the CPN characteristics, particularly token types and arc expressions which do not exist in ordinary PN. To express the token differentiation and their value evolution in CPNs, the predicative Linear Logic is very limited ; this is why, in this work, the first order Linear Logic was preferred. This section presents the chosen First Order Multiplicative Intuitionistic Linear Logic (noted MILL1) and then presents the translation algorithm.

First Order Multiplicative Intuitionistic Linear Logic

MILL1 language is defined as follows:

Alphabet:. The alphabet consists of disjoint sets: a set of variable symbols (e.g. x, y), a set of function symbols (e.g. f , g, h), a set of relation symbols (e.g. R, S, T ), the binary connectives (⊗, ⊸) and quantifier ∀. Each language L is equipped with a map from L to the set of natural integers ar : L → N. This map ar stands for symbol arity.

Terms. Given a language L, the first-order terms over L are defined by the syntactic category below:

τ ::= x | f (τ 1 , . . . , τ n )
where x ranges over variables and f belongs to the function symbols of L such that ar(f ) = n.

Formulas. First-order formulas of MILL are defined by the inductive syntactic category below:

ϕ, φ ::= R (τ 1 , . . . , τ n ) | ϕ ⊗ φ | ϕ ⊸ φ | ∀x • ϕ
where R belongs to relation symbols of L such that ar(R) = n and where the variable x occurrences in the formula ϕ are bound in formula ∀x • ϕ by the universal quantifier. Variables that are not bound by a quantifier are called free.

Sequents. If Γ is a multiset of formulas separated by "," and ϕ is a formula then Γ ⊢ ϕ is a sequent. By taking Γ as a multiset, we will implicitly assume that the sequent comma "," is associative and commutative. Γ is called the antecedent of the sequent and ϕ the succedent. Proofs in MILL1 are given in terms of proof trees that are inference rule composition over judgments. Judgments are pairs of a set of formulas Γ and a formula ϕ that are written Γ ⊢ ϕ. This means that the formula ϕ is a logical consequence of the conjunction of those of Γ. Inference rules (n-ary) are relations between n + 1 judgments that are noted as follows:

Γ 1 ⊢ ϕ 1 • • • Γ n ⊢ ϕ n Γ ⊢ ϕ
which means that it is sufficient to establish the below-rule judgment Γ ⊢ ϕ if the above-rule ones hold; in other words, to establish the below-rule judgment it is necessary to prove the above-rule judgments Γ i ⊢ ϕ i (1 i n). Inference rules of MILL are given in Figure 11.

id ϕ ⊢ ϕ Γ, ϕ ⊢ φ ⊸ r Γ ⊢ ϕ ⊸ φ Γ ⊢ ϕ φ, ∆ ⊢ ψ ⊸ l Γ, ϕ ⊸ φ, ∆ ⊢ ψ Γ ⊢ ϕ ∆ ⊢ φ ⊗ r Γ, ∆ ⊢ ϕ ⊗ φ Γ, ϕ, φ ⊢ ψ ⊗ l Γ, ϕ ⊗ φ ⊢ ψ Γ ⊢ ϕ ∀ r ( * ) Γ ⊢ ∀x • ϕ Γ, ϕ ⊢ ψ ∀ l Γ, ∀x • ϕ ⊢ ψ
The constraint ( * ) requires that the variable x isn't free in formulas of Γ.

Translation of a Colored Petri Net to MILL1

A logical formula is associated to each marking and each transition. The left hand of the initial sequent must contain the list of all the transitions that can be fired to obtain the marking M f from an initial marking M 0 . The building of the proof generates a proof tree beginning by a sequent and finishing by the identity axiom. For a given CPN, the translation is performed as follows:

• A unary atomic predicate R is associated with each place p of the CPN,

• A single sequent using the multiplicative conjunction TIMES (⊗), is associated with each marking, each precondition and each post-condition of transition,

• To each transition t of the net, an implicative formula is defined as follows:

t : ∀x1 . . . ∀xi   i∈P re(pi,t) Ri(xi) ⊸ o∈P ost(po,t)
Ro(fo(Xo))   where: x i are variables marking the input arcs of t ; f o are functions associated to the output arcs of t ; X o are vectors composed of different associations of x i .

The following example translates the CPN illustrated in Figure 12 to its equivalent in MILL1.

• places p i are translated by unary atomic predicates x → R i (x) where (1 i 5);

• the transition t 1 is translated by the formula:

ϕ 1 = ∀x • R 1 (x) ⊸ R 2 f (x) ⊗ R 4 g(x)
• transition t 2 is translated by the formula:

ϕ 2 = ∀y • ∀z • R 2 (y) ⊗ R 5 (z) ⊸ R 3 h(y, z)
• the initial state is translated by the formula:

φ 0 = R 1 (i) ⊗ R 5 (j)
• the final state is translated by the formula:

φ = R 3 (a) ⊗ R 4 (b)
The remaining of the example treats a case of reachability between two markings M 0 and M f where: M 0 = i .p1 + j .p5 and M f = a .p3+ b .p4. The reachability between M 0 and M f is obtained by the means of the judgment φ 0 , ϕ 1 , ϕ 2 ⊢ φ following proof in MILL1 (see proof tree in Figure 13): first, the initial state formula φ 0 is treated by ⊗ l , then the transition σ 1 is treated by ∀ l and ⊸ l . The result of the first transition is treated by ⊗ l . The second transition σ 2 is treated twice by ∀ l and ⊸ l . The results of the second transition is treated by ⊗ r . In a parallel direction, we treat the final state formula φ by ⊗ r as well. We finally apply id rules and unify the remaining equations by the substitution ς:

ς(a) = h f (i), j ς(b) = g(i)

Case study

This section shows a practical use of the backward reachability (through an inverse CPN) presented in previous paragraphs. The application example is inspired from the railway transport. It consists in the tram braking system. The aim is to show, through a case study, how to exploit efficiently the backward reachability analysis. The organization of this section begins with the specification of the studied system (in this paper, we focus only on the braking system). It is followed by the detailed modelling using CPN. The model includes complement information about the functions calculating braking values and the impact of each braking type on the vehicle speed. Then, finally, the CPN inversion and the backward reachability analysis are presented.

Specification

The driver has a control console (Figure 14.a) endowed with traction/braking handle which gives effort orders (acceleration, neutral, braking).

The acceleration or braking orders are transmitted to the different Traction Braking Electronics (TBE) which manage the different train bogies (set of two axles). The common braking mode, named service braking, is obtained by pulling the handle beyond the neutral position but without pulling it thoroughly. The extreme position of the handle causes an emergency braking (see below). In the case of the service braking, the TBE realize the effort (variable according to the handle position) with an electrodynamic brake. This braking mode uses also, when necessary, the disc brake. To avoid frequent falls in the train, the braking effort is modulated by the passengers load (measured by a weighing device). The device named anti-slip (anti wheels locking, equivalent to ABS system in automotive world) is also active in this mode.

The emergency braking is obtained by pulling the handle thoroughly. It is maintained till the train stops. In this mode, maximum deceleration performance is needed. So, TBE order the maximum effort to the electrodynamic brake and the disc brake, the modulation with the passengers weight and the antislipping stay active. The sanding (injection of sand under the wheels) is ordered for the whole train. In addition to this, electromagnetic skates (long electromagnet) are applied on the rail.

i = x id R 1 (i) ⊢ R 1 (x) f (x) = y id R 2 f (x) ⊢ R 2 (y) j = z id R 5 (j) ⊢ R 5 (z) ⊗ r R 5 (j), R 2 f (x) ⊢ R 2 (y) ⊗ R 5 (z) h(y, z) = a id R 3 h(y, z) ⊢ R 3 (a) g(x) = b id R 4 g(x) ⊢ R 4 (b) ⊗ r R 4 g(x) , R 3 h(y, z) ⊢ φ ⊸ l R 5 (j), R 2 f (x) , R 4 g(x) , R 2 (y) ⊗ R 5 (z) ⊸ R 3 h(y, z) ⊢ φ ∀ l × 2 R 5 (j), R 2 f (x) , R 4 g(x) , ϕ 2 ⊢ φ ⊗ l R 5 (j), R 2 f (x) ⊗ R 4 g(x) , ϕ 2 ⊢ φ ⊸ l R 1 (i), R 5 (j), R 1 (x) ⊸ R 2 f (x) ⊗ R 4 g(x) , ϕ 2 ⊢ φ ∀ l R 1 (i), R 5 (j), ϕ 1 , ϕ 2 ⊢ φ ⊗ l φ 0 , ϕ 1 , ϕ 2 ⊢ φ

Colored Petri Net Modelling

The CPN, shown in Figure 15 models the different braking types cited in the specification: service braking and emergency braking. Each braking type is represented by a transition which links causes (pre conditions) and requested devices (post conditions). The specification does not provide numerical values or functions about orders to apply. Their choice has only limited effects on the analysis. So these choices are made by authors to demonstrate the progress and the contribution of the backward reachability analysis.

The transition Service models the service breaking which is engaged by the position of the handle (represented by the place handle) beyond the neutral position but not in the maximal one. This condition is represented by the guard associated to this transition. It allows the transition firing if the variable m ∈]0..1[ like that 0 is the neutral position and 1 is the maximal one. The effort order value is proportional to the handle position. It is modulated also by the weighting and the antislipping (represented by the places having same names). The values of the variables w and a (for weighting and anti-slipping respectively) belong to the interval [0..1]. The output braking order is sent to the electrodynamic brake. It is calculated by the function f 1 (h, w, a) = 5h + 2w + a. When the cumulated value of w and a is higher then a threshold (1, 5 in this case), an order is sent to the disc brake calculated by the function f 2 (h, w, a) = 7h + 2w + a.

The transition Emergency models the emergency braking caused by pulling the handle to its maximal position. This

x       x f f y h 1 1 2 1 .. 0     y   w h x f a , ,

Colored Petri Net Model transformation

The transition Service is, at the same time, parallel and parametric. It is parallel because same input variables are used is two output functions. The parametric property comes from the output variables which are multi-variable functions. Several transformations are possible, each one depends on the input variable to calculate, but all of them have to respect the two properties (parallel and parametric). One of possible transformations is illustrated in Figure 16. The values of h and w are assumed in their domaines. So the calculation is done over the variable a using the partial inverse function f -1 1a (x) = x -5m -2p. When calculating, the values that do not belong to the color set of the Anti -Slipping place (so variable a) are deleted. An additional guard is associated to the transition according to the application of the parallel transformation. This guard is written y = f 2 (f -1 1 (x)) and

f -1 1 (x) = (h, w, a) = ( x-2w-a 5 , x-5h-a 2 , x -5h -2w) f 2 (f -1 1 (x)) = If (((3x -15h -4w -a)/2) < 1.5) T hen 0 Else (17x -50h -24w -12a)/5
The transition Emergency, for the same reasons as the transition Service, is parallel and parametric. In addition, it is mixed because it has constant arc expressions that produce anonymous token e. One of the possible transformations of this transition is illustrated in Figure 17. In the original CPN, the transition firing is conditioned by the value h = 1. So, in the transformed model, the expression of the arc (Emergency, Handle) is associated to the constant value 1. The Antislipping values are calculated using the function f -1 3a (x, w) = x -2w -5. The added guard express adequation between values of x and y like that f 4 (f -1 3 (x)) = 2x -2wa -3.

Handle Weighting

Anti-slipping

Emergency

Electro Dynamic Brake

x     x f f y 1 3 4   y   w x f a ,

. The Service Braking

The first analysis concerns the service braking. The process consists in studying a braking which requires, at the same time, the electrodynamic brake and the disc brake with a known value on the first one (5 in this example). The aim is to find possible command values applied to the disc brake and the control values corresponding (weighting w and anti-slipping a). We consider in this case that the handle position is known and constant: h = 0.5

The backward reachability analysis uses the inverse CPN and takes into account, in the partial state, the value 5 of the electrodynamic brake and the value 0.5 of the handle. The (backward) firing of the transition Service is done thanks to the marking enhancement as the disc brake order, which is necessary on the transition firing, is unknown. It is added as a complementary assumption meaning that the disc brake device was activated. Calculations use the guard associated to the transition and the constraint 2w + a = 2.5 is obtained and easily verified in each component of the triplet f -1 1 (x), which is itself a component of the guard. The results are illustrated in Figure 18. The backward analysis algorithm, which searches the input values, is written as follows:

for p ∈ [0..1] do a ← 2.5 -2p if 0 ≤ a ≤ 1 then Return f 2 (f -1 1 (x)) /*x = 5, m = 0.5*/ end if end for
The conclusion of this case analysis is that the final markingM f = 5 .ElectroDynamicBrake is reachable, by firing the transition Service, by the initial marking M 0 = 0.5 .Handle + ŵ .W eighting + â .AntiSlipping such that â = 2.5 -2 ŵ and 0 ≤ â ≤ 1. The final marking really reachable is the enhanced marking M f e = 5 .ElectroDynamicBreake + ŷ .DiscBrake. The values of ŷ, ŵ and â are the possible combination of y, w and a (respectively) corresponding to the line segment shown in Figure 18.

To find same results in forward reachability analysis, the search algorithm has to choose among all possible y val- Figure 18: Service braking analysis ues those which are really possible using the constraint f 1 (h, w, a) = 5 ∧ h = 0.5. But no constraint joins the variables w and a. The forward reachability analysis algorithm can be written as follow:

for a ∈ [0..1] do for p ∈ [0..1] do if f 1 (m, p, a) = 5 then Return f 2 (m, p, a) end if end for end for
The difference between the two algorithms (backward reachability and forward reachability) is their algorithmic complexity. Knowing that the the complexity of f 2 and f 2 (f -1 ) are strictly identical, the difference between the two is that the second presented algorithm (forward reachability) includes two nested loops whereas the first includes only one loop. This is due to the inverse CPN which exploits the parallelism relation (parallel transformation) thus introducing an a priori knowledge reducing the calculation complexity.

The Disc Brake

The second analysis concerns the diagnosis of a particular state of the disc brake. The known state is the command value of the disc brake. In this case study, it is chosen as 9. The purpose is to find initial states (M 0 ) that could produce the final partial state (M f = 9 .DiscBrake) knowing only this last state. The analysis is done by backward reachability using the inverse CPN marked with marking corresponding to M f .

The transition Emergency

The inverse firing of the transition Emergency requires a marking enhancement for Sanding, Skate and ElectroDynamiBrake. In the first two places, the tokens to add are anonymous (no calculus to do). However, token values in ElectroDynamiBrake (the variable x) have to satisfy the guard. To simplify the process, we rewrite the guard to get x values knowing y. This guard can be written as Applying an analogue approach as the one used in the previous case study, the possible order values of the electrodynamic brake and the control values corresponding (weighting and anti-slipping) are calculated. The results are illustrated in Figure 19. The conclusion is that the marking M f = 9 .DiscBrake is backward reachable from M 0 = 1 .Handle + ŵ .W eighting + â .AntiSlipping. This reachability is conditioned by the marking enhancement. The final marking really reachable is the enhanced marking M f e = x .F reinElectroDynamique + 9 .DiscBrake + e .Sanding + e .Skate. The values of x, ŵ and â are possible combinations of variables x, w and a (respectively) corresponding to the line segment of Figure 19.

The transition Service

As for the transition Emergency, the backward firing of the transition Service requires a marking enhancement. The place to enhance is ElectroDynamicBrake. Token values in this place (variable x) have to satisfy the guard. Since the value of y is known, the guard is rewritten to calculate easily x values. The new guard is written x = f 1 (f -1 2 (y)). In this case, the condition y = 0 in the function f 2 is valid. So in the original CPN, the condition p + a > 1.5 is valid and the token value in DiscBrake (9 in this example) is obtained by applying the formula 7m + 2p + 1. The new guard is given by (0 < m < 1)∧(3y-21m-4p-a > 3)∧(x = (19y-98h-24w-12a)/7) under the constraint a = y -7h -2w.

By using the inverse CPN modified and completed, the possible order values applied to the electrodynamic brake and the control values corresponding (weighting and anti-slipping) are calculated. The results can't be shown in a unique graphic (too many variables). This is why they are drown in the two schemas of marking M f = 9 .DiscBrake is backward reachable by M 0 = ĥ .Handle + ŵ .W eighting + â .AntiSlipping. This reachability is conditioned by the marking enhancement. The final marking really reachable is the enhanced marking M f e = x .ElectroDynamicBrake + 9 .DiscBrake. The values of x, ĥ, ŵ and â are possible combinations of variables x, h, w and a (respectively) corresponding to the illustrated values in Figure 20.

Summary of the Disc Brake case study

The backward reachability analysis of the final marking considered in this case study (M f = 9 .DiscBrake) shows that it is reachable by two different paths (Figure 21). Each path represents a specific scenario and needs complementary information about the system final state. This is why the final marking was enhanced to assume coherent system states.

Conclusion

The diagnostic and dependability issues in embedded systems are very large and not easy to deal with. This work focuses on a particular aspect which is model based verification and analysis. The main objective is to propose a formal method for: 1) looking for sources of a known failure (diagnosis) ; 2) performing analysis to verify/validate a system relatively to a given specification and, in case of need, to propose a correction of the system to satisfy the specification. Such a study needs an appropriate model that can represent the structure and the dynamic behavior of the system and that has also a formal basis. The chosen model is a Colored Petri Net (CPN) and in this work we propose a structural analysis by backward reachability using inverse models. The CPN inversion is a research issue because of the model structure. Some solutions can be found in literature ([2], [START_REF] Cho | Safety analysis using colored petri nets[END_REF], [START_REF] Khalfaoui | Mthode de recherche des scnarios redouts pour l'valuation de la sret de fonctionnement des systmes mcatroniques du monde automobile[END_REF], [START_REF] Müller | Duality in high level petri-nets: a basis to do diagnoses[END_REF]). We proposed a generalization of the method of [START_REF] Khalfaoui | Mthode de recherche des scnarios redouts pour l'valuation de la sret de fonctionnement des systmes mcatroniques du monde automobile[END_REF] based on inverse CPN. The basic idea is to define some elementary transformations, each one is appropriate to a specific transition structure type. These transformations can be combined to express a very large amount of possible cases. The definition of the inverse CPN is the first part of the contribution. The second part aims the backward analysis. To achieve this, complementary mechanisms were defined to drive the analysis and to deal with a lack of information.

The inverse CPN and the complementary mechanisms are first presented in an intuitive way. To consolidate the formal aspect of the proposed approach, two theoretical studies were presented. The first formalism (linear algebra) proves the pertinence of presented transformation algorithms in a local way by focusing in a single transition. The second formalism (linear logic) aims to prove the correctness of the performed backward analysis using the inverse CPN. This is done by adapting the LL fragment that has to be used in a CPN context and which is MILL1 (First Order Multiplicative Intuitionistic Linear Logic). When the translation MILL1/CPN is made, the reachability is proven thanks to sequent calculus.

To test the proposed method, a practical case inspired from railway domain was studied. It treats a specification of a tramway braking system. The system was modelled using CPN and then the inverse CPN was generated. The backward analysis answers efficiently a sequence of diagnostic and V&V questions and the approach proves its usefulness.

Figure 1 :

 1 Figure 1: Trivial and basic transformations for CPN inversion

Figure 2 :

 2 Figure 2: Parametric transformations for CPN inversion

Figure 3 :

 3 Figure 3: Parallel transformation for CPN inversion

Figure 4 :

 4 Figure 4: Mixed transformations for CPN inversion

Figure 5 :

 5 Figure 5: Color correspondance in CPN

Figure 6 :

 6 Figure 6: Equivalence between generalized PN and Well-Formed PN

2 ProjFigure 7 :

 27 Figure 7: Mixed transformations viewed in generalized PN and Well-Formed PN

Figure 8 :

 8 Figure 8: Mixed transformations proof for CPN inversion

Figure 9 :

 9 Figure 9: Proof of parallel transformations for CPN inversion

Figure 10 :

 10 Figure 10: Sequent calculus rules of the MILL fragment

Figure 11 :Figure 12 :

 1112 Figure 11: First-Order Multiplicative Intuitionistic Linear Logic

Figure 13 :Figure 14 :

 1314 Figure 13: example of proof tree calculating reachability conditions in CPN

Figure 16 :

 16 Figure 16: Transformation of the transition Service

Figure 17 :

 17 Figure 17: Transformation of the transition Emergency

Figure 19 :

 19 Figure 19: Emergency Braking in case of Disc Brake case study

Figure 20 .Figure 20 :

 2020 Figure 20: Service Braking in case of Disc Brake case study

Figure 21 :

 21 Figure 21: Backward reachability tree of Disc Brake case study

  ∀p ∈ P r , P ost r (p, t ′ ) = P ost(p, t ′ ) AND P re r (p, t ′ ) = P re(p, t

	C		C'		C"
	p	Pre(p, h)	h	Post(p', h)	p'

′ ) • ∀p ∈ P, P re r (p, t) = P re(p, t) • f AND P ost r (p, t) = P ost(p, t) • f • ∀p ∈ P r , M r (p) = M (p)

We note Bag(U ) the multi set defined over U (U is a finite set). A Bag (or multi set) is a non ordered set where the repetition is permitted. An element of Bag(U ) is noted u∈U au.u. Using Bag notion allow treatment of color sets case which are characterized by the repetition of their values.

http://wiki.daimi.au.dk/cpntools


S Alves
email: salves@laas.fr

F Morancho
email: morancho@laas.fr

J-M Reynès

J Margheritta
email: joel.margheritta@freescale.com

I Deram

K Isoird
email: kisoird@laas.fr

Experimental validation of the "FLoating Island" concept: A 95 Volts Vertical breakdown voltage FLIDiode

Keywords: Floating Island, FLIMOS, Superjunction, Breakdown Voltage, Specific On-Resistance

In this paper, the "FLoating Island" concept has been implemented on silicon: a FLIDiode has been built for the first time. Experimental results confirm the predictive 2D simulations: this new diode exhibits an important breakdown voltage (about 95 Volts) with a N -epitaxial layer doping concentration (1.1 x 10 16 cm -3 ) usually dedicated to 50 Volts devices. These measurements validate the "FLoating Island" concept and the efficiency of the original edge cell that will be used in the FLIMOS technology: it can be expected that the specific onresistance of the FLIMOSFET will be drastically reduced compared to the conventional VDMOSFET.

INTRODUCTION

The power MOSFET is a very important device in many power electronics applications for its well-known intrinsic advantages: high input impedance, short switching time and thermal stability. The increase in electronic contents in today's automobiles requires a higher voltage, and 42 V batteries will be the most satisfactory standard. The incentive of this work is to address the rising need of this class of MOSFETs in Automotive applications. Thus, 85V power MOSFET will be the emerging device of choice for these applications. In power electronics circuits, the power MOSFET is mainly used as a switch, in which the specific on-resistance R ON , sp and the breakdown voltage BV dss are the two most important parameters to be considered. Actually, to reduce the conduction losses in a MOSFET, its specific on-resistance must be reduced. The Vertical Double diffused MOSFET structure -VDMOSFET -(Fig. 1) is widely used as a power MOSFET. This structure is based upon the double diffusion of the P-body and N + source regions using the edge of the polysilicon as a masking boundary. The voltage handling capability of this structure is given by the breakdown voltage of the "P-body/N-epilayer" junction, that is strongly dependent on the thickness and the doping of the lower doped region (i.e. the N -epilayer region in the case of N-channel VDMOS transistors) [START_REF] Cézac | A New Generation of Power Unipolar Devices: the Concept of the FLoating Islands MOS Transistor (FLIMOST)[END_REF].

Today, advances in process technology have improved transistor's packing density and consequently transistor's specific on-resistance. However improvements in specific on-resistance have been limited by material and breakdown voltage, which required a relative thick and lowly doped epitaxial layer. Recently, several MOSFET configurations have been proposed to reduce specific on-resistance while keeping a high breakdown voltage: P Floating Islands devices [START_REF] Chen | A Novel High-Voltage Sustaining Structure with Buried Oppositely Doped regions[END_REF], [START_REF] Saitoh | Ultra Low On-Resistance SBD with P-Buried Floating Layer[END_REF], [START_REF] Fujihira | Theory of Semiconductor Superjunction Devices[END_REF] and Superjunction devices [START_REF] Alves | Vertical Nchannel FLIMOSFETs for Future 12 V / 42 V Dual Batteries Automotive Applications[END_REF].

P FLoating Islands unipolar devices -FLIMOSFET [START_REF] Chen | A Novel High-Voltage Sustaining Structure with Buried Oppositely Doped regions[END_REF], Opposite Doped Buried Regions (ODBR) MOSFET [START_REF] Saitoh | Ultra Low On-Resistance SBD with P-Buried Floating Layer[END_REF] and P-buried layer Schottky Barrier Diode [START_REF] Fujihira | Theory of Semiconductor Superjunction Devices[END_REF] -have recently caught the attention of many researchers because they are good challengers of Superjunction devices under 600 Volts [START_REF] Chen | A Novel High-Voltage Sustaining Structure with Buried Oppositely Doped regions[END_REF]; furthermore, the technology needed to manufacture such as devices is less complex than the Superjunction devices technology [START_REF] Fujihira | Theory of Semiconductor Superjunction Devices[END_REF].

In this paper, new Vertical N-channel FLIMOSFETs dedicated to automotive applications (12 V / 42 V dual batteries, i.e. below 100 V breakdown voltage devices) are proposed; these FLIMOSFETs comprise only one P floating island between drain and source: it will be shown that, even in low voltage applications, they exhibit a better "specific on-resistance / voltage handling capability" trade-off than the conventional Vertical DMOSFETs. Then, the "Floating Island" concept will be experimentally validated by the realization of a Floating Island Diode (FLIDiode).

FLOATING ISLANDS MOS PRINCIPLE

Principle.

Schematic cross-sections of the conventional Vertical DMOSFET (VDMOSFET) and the newly developed Vertical FLIMOSFET are shown in Fig. 1 and2. The essential difference is the introduction of a P buried layer (called FLoating Island) in the N -epitaxial layer; this P buried layer is located under the PHV/N -plane junction in order to divide, under reverse bias conditions, the maximal electric field in two parts (Fig. 3), allowing the improvement of the breakdown voltage for the same N -epitaxial layer doping concentration.

In other words, to reach the same blocking voltage as with a conventional VDMOSFET, the N -epitaxial layer doping concentration of the FLIMOSFET can be strongly increased.

Device parameters.

For instance, when the voltage handling capability of the two devices is about 85 V, the N - epitaxial layer doping concentration required is equal to 5.5 x 10 15 cm -3 for the conventional VDMOSFET and to 1.1 x 10 16 cm -3 for the FLIMOSFET.

RESULTS AND DISCUSSION

In order to validate the "Floating Island" concept, it has been decided to study and to realize a FLIDiode. This study concerns the reverse behavior of the FLIDiode compared to a conventional PN -N + Diode. The main device parameters of the two Diodes are given in Table 1. Compared to the conventional Diode, the main difference is the introduction of a P buried layer in the N -epitaxial layer.

Concerning the OFF-state, it should be noted that 2D simulations confirm what we expected (Fig. 4): the maximal electric field is divided in two parts located around the two junctions (i.e. the P-body/N-epilayer and the Pburied layer/ N-epilayer junctions); Figure 4 shows the doping concentration (Fig. 4a), electric field distribution (Fig. 4b) and potential distribution Fig. 2: Vertical FLIMOSFET with one FLoating P buried layer between drain and source. In our study, the simulated FLIDiode breakdown voltage of the central cell is about 95 V (Fig. 4c); the breakdown voltage of the edge cell is also 95 V. At breakdown, this structure is in non punch through configuration. The breakdown occurs in the P + N -junction and the electric field is math linear by parts. The electric field is divided by the P + floating islands. We can also observe that the potential is parabolic by parts, and is sustain by the N -layers. In fact, it can be observed that there is no voltage drop in the P + floating islands.

In the edge cell, two lateral P Floating Islands are introduced in the N -epitaxial layer and the positions of the two lateral P FLoating Islands have been optimized: the optimal position is obtained when the maximums of the electric field in the three FLoating Islands and at the PHV cylindrical junction are equal. Figure 6 presents the doping concentration for the edge cell of the Vertical FLIDiode. Figure 7 shows 2D simulation of the electric field distribution at breakdown for the edge cell of the Vertical FLIDiode. The lateral FLoating Island depth is very important: the more the lateral FLoating Islands are deep, the more the potential lines are pushed away in the volume. Then the breakdown occurs at the PHV plane junction. FLIDiodes have been implemented on silicon: Figure 8 shows the variation of the voltage handling capability versus the second epitaxial layer thickness: a wide operating area higher than 85 Volts is obtained. This work validates the FLoating Island concept and the efficiency of the edge cell: this new Diode exhibits an important breakdown voltage (about 95 Volts) with a N -epitaxial layer doping concentration (1.1 x 10 16 cm -3 ) usually dedicated to 50 V devices.

Electric field peaks

Figure 9 shows the BV dss measurements of the conventional Diode (50 Volts) and the Vertical FLIDiode (97 Volts), for the same N -epitaxial layer doping concentration (1.1 x 10 16 cm -3 ). The V f measurements presented Figure 10, shows that the P FLoating Island is fully "transparent", compared to the conventional Diode (50 Volts) and the Vertical FLIDiode (97 Volts). The P FLoating Island has no impact on the V f .

1.E-12

1.E-11

1.E-10

1.E-09

1.E-08

1.E-07

1.E-06

1.E-05

1.E-04

1.E-03

1.E-02 The next step of this work is to implement this concept on Vertical MOSFET: with this high epitaxial layer doping concentration, it can be expected that the specific on-resistance of this new MOSFET will be drastically reduced compared to its equivalent conventional VDMOSFET [START_REF] Alves | Vertical Nchannel FLIMOSFETs for Future 12 V / 42 V Dual Batteries Automotive Applications[END_REF], [START_REF] Alves | New Generation of Vertical MOSFETs for Future 12 Volts / 42 Volts Dual Batteries in Automotive Applications[END_REF]. This Vertical MOSFET will use the same edge cell as the Vertical FLIDiode. The technology process is now in progress for the FLIMOSFET using more particularly multi-epitaxy layers (see the SUPREM doping profile, Fig. 11). This Vertical MOSFET will use the same edge cell as that of the Vertical FLIDiode. FLIMOSFETs become interesting when increasing the breakdown voltage. For instance, for the same breakdown voltage (about 85 Volts), compared to the conventional VDMOSFET, it has been shown that the specific on-resistance of FLIMOSFET is strongly reduced (33 %) when using P floating squares [START_REF] Alves | New Generation of Vertical MOSFETs for Future 12 Volts / 42 Volts Dual Batteries in Automotive Applications[END_REF].

CONCLUSION

In this paper, the "FLoating Island" concept has been implemented on silicon, and a FLIDiode has been built for the first time. These experimental results confirm the predictive 2D simulations: this new diode exhibits an important breakdown voltage (about 97 Volts) with a N -epitaxial layer doping concentration (1.1 x 10 16 cm -3 ) usually dedicated to 50 Volts devices. These measurements validate the "FLoating Island" concept and the efficiency of the original edge cell that will be used in the FLIMOS technology: it can be expected that the specific on-resistance of the FLIMOSFET will be drastically reduced compared to the conventional VDMOSFET.

Fig. 1 :

 1 Fig. 1: Conventional Vertical DMOSFET.

Fig. 3 :Fig. 4 :

 34 Fig. 3: Electric field distribution in the conventional VDMOSFET and in the FLIMOSFET.

Fig. 5 :

 5 Fig. 5: Edge cell of the Vertical FLIDiode.

Fig. 6 :

 6 Fig. 6: Doping concentration for the edge cell of the Vertical FLIDiode.

Fig. 7 :

 7 Fig. 7: Electric field distribution at breakdown for the edge cell of the Vertical FLIDiode.

Fig. 8 :

 8 Fig. 8: BV dss measurements vs 2nd epitaxial layer thickness.

Fig. 9 :

 9 Fig. 9: BV dss measurements of the conventional Diode and the Vertical FLIDiode.

Fig. 10 :

 10 Fig. 10: V f measurements of the conventional Diode and the Vertical FLIDiode.

Fig. 11 :

 11 Fig. 11: SUPREM profile of the new developed FLIDiode. '0 µm' corresponds to the substrate / 1 st epitaxial layer interface. '-5.15 µm' distance corresponds to the surface of the device.

Table 1 :

 1 Main device parameters of the conventional 91 Volts Diode and the Vertical 95 Volts FLIDiode.

		Conventional	Vertical	Vertical
		VDiode	FLIDiode	FLIDiode
			central cell	edge cell
	N -epitaxial layer
	thickness (µm)	4.75	4.05	4.05
	N -Epitaxial layer resistivity (Ω.cm)	1.05	0.50	0.50
	Floating P
	maximum doping	--	10 17	10 17
	concentration (cm -3 )
	Lateral Floating P
	maximum doping	--	--	10 19
	concentration (cm -3 )


L Théolier
email: ltheolie@laas.fr

K Isoird

H Tranduc

F Morancho

J Roig

Y Weber

E N Stefanov

J-M Reynès

Switching Performance of 65 Volts Vertical N-Channel FLYMOSFETs

Keywords: capacitance modeling, gate charge, VDMOSFET, FLYMOSFET, power MOSFET

In this paper, the switching performance of 65 Volts vertical N-channel FLYMOSFETs is investigated for the first time and compared to a conventional VDMOSFET. It is shown that measurements of the different capacitances and the gate charge of the two divices are comparable. A 2D simulation study of two equivalent structures (i.e. FLYMOSFET and VDMOSFET exhibiting the same breakdown voltage) confirms that floating islands did not cause parasitic or new phenomenon, in the case of weakly doped islands.

INTRODUCTION

In the power electronics field, semiconductor devices are switches operating between the off-state and the onstate. So the breakdown voltage and the on-resistance are two important caracteristics of these devices. The P-Floating Islands MOS devices -FLIMOS [START_REF] Cézac | A New Generation of Power Unipolar Devices: the Concept of the FLoating Islands MOS Transistor (FLIMOST)[END_REF], FLYMOS™ [START_REF] Alves | Technological realization of low on-resistance FLYMOS™ transistors dedicated to automotive applications[END_REF], Opposite Doped Burried Regions (ODBR) MOS [START_REF] Chen | A Novel High-Voltage Sustaining Structure with Buried Oppositely Doped regions[END_REF] and FITMOS [START_REF] Takaya | Floating Island and Thick bottom oxide trench gate MOSFET (FITMOS) -A 60V ultra low On-resistance novel MOSFET with superior internal body diode[END_REF] for example -have recently caught the attention of many researchers because they can offer lower specific on-resistance values than conventional MOSFETs in medium voltage applications (around 600 Volts). It was also shown [START_REF] Cézac | A New Generation of Power Unipolar Devices: the Concept of the FLoating Islands MOS Transistor (FLIMOST)[END_REF] that they are good chalengers of Superjunction devices [START_REF] Fujihira | Theory of Semiconductor Superjunction Devices[END_REF] under 600 Volts; furthermore, the "Floating Islands" concept is not based on the charge compensation principle unlike the Superjunction devices technology [START_REF] Alves | Technological realization of low on-resistance FLYMOS™ transistors dedicated to automotive applications[END_REF]. Although a superior FLYMOSFET static performance in comparaison with power MOSFET was experimentally demonstrated in [START_REF] Alves | Technological realization of low on-resistance FLYMOS™ transistors dedicated to automotive applications[END_REF], no study about its dynamic performance has been done to date. This work investigates the FLYMOSFET's dynamic behaviour: in this way, simulations analysis are combined with experimental results to compare the novel device performance with the conventional power VDMOSFET's one.

FLOATING ISLANDS PRINCIPLE

Schematic cross-sections of the conventional VDMOSFET and the Vertical FLYMOSFET are shown respectively in Fig. 1-a and 2-a. The main difference is the introduction of a P-buried layer (called Floating Island) in the N -epitaxial layer. In contrast to the conventional VDMOSFET, for which the breakdown voltage is supported at one location (Fig 1-b), the Pburied layer allows the division of the maximal electric field in two parts (Fig. 2-b). When the breakdown voltage is the same, the N -epitaxial layer doping concentration of the FLYMOSFET (N D2 ) can be increased compared to the VDMOSFET case (N D1 ), resulting in a reduction of the on-resistance. Nevertheless, the drawback of this increase in doping concentration is the impact that can be expected on the capacitance of the drain depletion layer beneath the gate oxide (C gddep ) and on the drain-source capacitance (C ds ) that is the capacitance of two PN junctions in series in the FLYMOSFET's case (Fig. 2-a

DEVICE STRUCTURE

The studied device is a 65V FLYMOSFET fabricated by Alves et al [START_REF] Alves | Technological realization of low on-resistance FLYMOS™ transistors dedicated to automotive applications[END_REF]. In previous works, 1D process simulation and crystalline revelation have allowed to reveal some qualitative representations of P-floating islands in order to understand their evolution [START_REF] Alves | Experimental validation of the "Floating Island" concept: a 95 Volts Vertical breakdown voltage FLIDiode[END_REF]. But neither process simulation nor 1D physical characterization gave a clear and accurate representation of the islands. Thus, the purpose of creating a physical characterization tool by using Scanning Capacitance Microscopy (Fig. 3) is to determine precisely the shape and the dimensions of the Floating Island to quantify its impact on FLYMOSFET electrical characteristics.

Thanks to SCM, it is possible to quantify directly the 2D island forms and the Floating Island resulting picture exhibits a ball-like shape.

On the contrary to the first theorical representation [START_REF] Cézac | A New Generation of Power Unipolar Devices: the Concept of the FLoating Islands MOS Transistor (FLIMOST)[END_REF], in witch the islands are thin and long, the SCM results show that islands capacitances are more cylindrical than plane.

CAPACITANCE EXPRESSIONS

The switching performance of the FLYMOSFET and the conventional VDMOSFET is strongly related to MOSFET capacitances, which are needed to charge and to discharge during switching. FLYMOSFET's capacitances exhibit the same expressions than those of a VDMOSFET; nevertheless, the Floating Islands play a in drain-source capacitance. All these capacitances depend on geometric and technological parameters of the structure.

Gate-Drain Capacitance (C gd ) Modeling

The FLYMOSFET's gate-drain capacitance is comparable to the gate-drain capacitance of a VDMOSFET. This capacitance is constituted by two capacitances in series: an oxide capacitance (C gdmax ) and a depletion capacitance (C gddep ).

• in the accumulation regime, i.e. when V dg < 0, C gd is equal to the oxide capacitance C gdmax .

• in the depletion (or weak inversion) regime, when V ds > V gs , C gd obeys the following relation:

1 C gd = 1 C gd max + 1 C gddep (1)
where

C gd max = " 0 #" ox e ox # S 1 (2)
and

C gddep = S 1 " q " N D "# 0 "# si 2 " $ S ( 3
)
S 1 represents the inter-cellular total area beneath the gate (Nregion) and "s the voltage that is substained by the space charge zone.

The main difference between a conventional VDMOSFET and its equivalent FLYMOSFET (i.e. same breakdown voltage and same gate oxide thickness) comes therefore from the doping concentration N D of the N -region (epitaxial layer) that influences C gddep (depletion capacitance).

Drain-Source Capacitance (C ds ) Modeling

The drain-source capacitance of a VDMOSFET is due to the PN -junction which is formed by the P body region and the N -epitaxial layer. This junction is constituted by a plane junction (C ds1Plan ) and a cylindrical junction in parallel (C ds1cyl ). We can then consider that the analytic model of C ds is:

C ds = C ds1Plan + C ds1cyl .
The analytical expressions of the C ds1cyl capacitance is recalled [START_REF] Tardivo | Le transistor D.MOS Vertical en amplification haute-fréquence de puissance[END_REF]: (5) where α is the voltage part sustained by the main junction "P-body/N -" (α = 1 for the VDMOSFET) and z is the total "perimeter" of the channel with:

ds1cyl = " #$ 0 #$ si # z # V ac % #V ds & ' ( ) * + 0.426 if " #V ds > V ac (4) C ds1cyl = " #$ 0 #$ si # z # V ac % #V ds & ' ( ) * + 0.306 if " #V ds < V ac
V ac = q " N D " r j 2 4 "# 0 " # si (6)
The analytical expression of the cylindrical junction capacitance of the FLYMOSFET is identical to the VDMOSFET's one. The only difference could come from the doping concentration of the epitaxial layer.

Therefore, for a same breakdown voltage, the increase in the doping concentration of the epitaxial layer and α will increase the value of the C ds1cyl capacitance of the FLYMOSFET.

The analytical expressions of the C ds1Plan capacitance is recalled:

C ds1Plan = S 2 " q " N D "# 0 "# si 2 "$ " V ds (7)
S 2 being the total plane surface beneath the P diffusion of channel.

The plane junction capacitance of the VDMOSFET also depend on the N -doping concentration epitaxial layer.

Concerning the FLYMOSFET, it appears two drift regions in series, due to the P-floating islands located under the plane junction. The expression of the plane capacitance beneath the island is:

C ds2Plan = S 3 " q " N D "# 0 "# si 2 " (1 $ %) " V ds ( 8
)
where S 3 is the surface of the plane junction on top and beneath the island.

Here, the expression of the cylindrical junction is:

g ds2cyl = 2 " # "$ 0 "$ si " z " V ac (1% &) "V ds ' ( ) * + , 0.426 (9) if (1 " #) $ V ds > V ac C ds2cyl = 2." #$ 0 #$ si # z # V ac (1% &) #V ds ' ( ) * + , 0.306 (10)
if (1 " #) $ V ds < V ac A higher doping concentration N D for the FLYMOSFET must imply a more important value of C ds1Pdiff compared to the VDMOSFET's one. In compensation, the capacitance C ds2 in series with C ds1diff would allow a reduction of the resulting capacitance C ds of the FLYMOSFET in relation to the VDMOSFET.

However, the analytic expressions presented in this paragraph allow to give the switching performance tendencies of the FLYMOSFET. This is not enough to quantify the evolution of the C gd and C ds capacitances precisely. In the continuation, the quantitative evolutions of these two capacitances will be presented.

RESULTS AND DISCUSSION

The measurements presented in this article have been done on a conventional 45V VDMOSFET and a 65V FLYMOSFET, using the same doping concentration of the N -epitaxial layer (around 10 16 cm -3 ) but having different active area geometries and different gate oxide thicknesses. The impedancemeter was a HP4284, used at 100 kHz. This frequency allows to free to the model of representation of the complex impedance seen by the impedancemeter.

The temporal and dynamic physical 2D simulations were performed with the ISE TCAD (Integrated Systems Engineering) software. The comparison between simulation and measurements is important in order to validate the models of dynamic behavior and to verify the software performance for these type of structures.

Gate-Drain Capacitance

Figure 4 presents the gate-drain capacitance measurements for the two structures and the 2D simulation of the FLYMOSFET's gate-drain capacitance. C gdmax capacitance expression depends essentially on the oxide thickness at reverse bias drain-gate configuaration. We have chosen to not represent them on Figure 4. Besides, the weak difference between the curves of the VDMOSFET and the FLYMOSFET seems to be due to the difference of doping concentration of the N -epitaxial layer. Indeed, a difference in the doping concentration of the drift zone influences on the depletion of the structure -expression (3) -. So, the comparison of the curves shows that the insertion of a floating island modifies lightly the gate-drain capacitance.

2D simulations of the FLYMOSFET are in good agreement with measurements: we can validate our simulations with these models and the mesh used in our simulations.

Fig. 4. Gate-drain capacitance variations vs applied voltage.

Drain-Source Capacitance

Figure 5 presents the drain-source capacitance measurements for the two structures and drain-source capacitance simulation of the FLYMOSFET. The drainsource capacitance of the FLYMOSFET seems to be proportional to 1 V ds , as the VDMOSFET and as analytically predicted. The C ds capacitance improvement is confirmed. Nevertheless, because of some differences in the design of the two structures (different gate oxide thicknesses for instance), it is difficult to do an accurate comparative study between the VDMOSFET and the FLYMOSFET.

Differences between simulated and experimental results is mainly due to the approximations of the simulation. Indeed, the structure was simulated in 2D in cylindrical coordinates, which results in a difference of volume between the cubic shape base-cell and the simulated cylinder. The "missing surface" is a part of the "Pbody/N -epitaxy": it is a non-negligible part of the drainsource (Fig. 5), whereas it did not influence the gate-drain capacitance (Fig. 4). Saito et al [START_REF] Saito | A novel low on-resistance Schottky-barrier diode with p-buried floating layer structure[END_REF] showed a two phases decrease in the capacitance for a Floating Islands Schottky diode. A rupture occurs when the depletion zone under the Pbody reaches the island. Because of the small size and the weak doping level of our P-floating islands, the same phenomenon is not observed in our measurements.

Gate Charge

The principle of the gate charge is to inject a constant current on the gate to charge it to a reference voltage. The charge to provide to the device input to turn it on is proportional to the time. Drain current is limited by a resistance and the source current is ordered by a pulse generator cutting the energy as soon as the voltage of reference is obtained, thus avoiding an internal warm-up of the device (Fig. 6). Differences in gate charge measurements (Q g ) between the two structures are due to the difference of the gate oxide thicknesses. While comparing the two measurements more finely, one can notice that the "Miller plateau" is less flat in the FLYMOSFET's case. Nevertheless, it is not proved to date that this phenomenon is due to the insertion of the floating island in the drift zone. According to FLYMOSFET's gate charge simulation, the main difference between measurements and simulation is the "Miller plateau": simulation displays a nearly flat "plateau" whereas measurements present a slope that is not negligible.

Predictive Simulations

The good match between simulations and measurements validates the used models and the good behavior of our simulations performed with ISE in dynamics and temporal.

To complete our analysis, it is good to compare this 65V FLYMOSFET with its equivalent in technology VDMOSFET (same breakdown voltage, same active area and same gate oxide thickness). Knowing that simulations match with the measurements, this comparative study may be made by mean of 2D cylindrical simulations. Table 1 gives the main parameters of the simulated structures. Concerning the gate charge simulation (Figure 9), a light deterioration of the FLYMOSFET is observed compared to the VDMOSFET. This is due to the length of the "Miller plateau", that is longer in the FLYMOSFETs case. The difference in the Q g charge is assigned in totality to this length. The V ds slope depends on the speed of the depletion zone reduction in the drift zone. This difference could come from the insertion of the island or from the difference in the N -layer doping concentration.

CONCLUSION

In this work, the switching performance of a 65V FLYMOSFET has been investigated for the first time and its performance has been compared to the conventional VDMOSFET's one. Measurements allow to note that the different capacitance behaviours were almost the same. The good match between measurements and simulations, performed with a 2D structure described in cylindrical coordinates, has allowed the validation of our simulations. Finally, the simulated 65V FLYMOSFET and its equivalent VDMOSFET have been stydied permiting a more accurate comparison of the two structures.

The FLYMOSFET is therefore an excellent power switch since he displays low losses in the on-state in compared to a conventional VDMOSFET [START_REF] Alves | Technological realization of low on-resistance FLYMOS™ transistors dedicated to automotive applications[END_REF] and nearly the same switching behavior. Besides, the dynamic models of ISE software have been validated, in order to go on doing predictive simulations of this type of structures.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Conventional VDMOSFET: a) schematic croos-section, b) theorical electric field distribution at breakdown.

Fig. 3 .

 3 Fig. 3. SCM image of the 65V FLYMOSFET.

Fig. 5 .

 5 Fig. 5. Drain-source capacitance variations vs applied voltage.

Fig. 6 .

 6 Fig. 6. Schematic of the measurement of the gate charge with R = 2Ω and I g = 2mA.

Figure 7

 7 Figure 7 presents gate charge measurements of the two structures (VDMOSFET and FLYMOSFET) and gate charge simulation of the FLYMOSFET. The three fundamental phases of the gate charge are observed: 1) the charge of the input capacitance C iss (C gdmin + C gs ) before the threshold voltage is reached, 2) the "plateau" due to the Miller effect, 3) the charge of the new value of C iss (C gdmax +C gs ).

Fig. 7 .

 7 Fig. 7. Gate charge waveforms: Q g =192 nC (FLYMOSFET) and 246 nC (VDMOSFET).

Figure 8

 8 Figure8shows the gate-drain capacitance variations versus the draind-gate bias. No significant difference in the C gdmax is observed because the gate oxide thickness is identical. The C gdmin values are also close depletion capacitances (C gddep ) are relatively weak at high drain-gate voltages and, therefore, comparable -expression (3) -. The only difference concerns the difference of depletion that depends on the doping concentration of the N -zone: in this "intermediate part", the C gd capacitance of the FLYMOSFET is lightly higher than the VDMOSFET's one. Simulation confirms therefore that the FLYMOSFET technology lightly damages the input capacitance.

Fig. 8 .

 8 Fig. 8. Simulated gate-drain capacitance variations vs applied voltage for equivalent VDMOSFET and FLYMOSFET.

Fig. 9 .

 9 Fig. 9. Simulated gate charge waveforms for equivalent VDMOSFET and FLYMOSFET. Q g = 184 nC (VDMOSFET) et 189 nC (FLYMOSFET).

Table 1 :

 1 Main device parameters of simulated conventional VDMOSFET and FLYMOSFET.