Nouha Abid

Silvano Dal Zilio

Didier Le Botlan

Silvano Dal

Real-Time Specification Patterns and Tools

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

An issue limiting the adoption of model checking technologies by the industry is the difficulty, for non-experts, to express their requirements using the specification languages supported by the verification tools. Indeed, there is often a significant gap between the boilerplates used in requirements statements and the low-level formalisms used by model checking tools; the latter usually relying on temporal logic. This limitation has motivated the definition of dedicated assertion languages for expressing properties at a higher level (see Section 5). However, only a limited number of assertion languages support the definition of timing constraints and even fewer are associated to an automatic verification tool, such as a model checker.

In this paper, we propose a set of real-time specification patterns aimed at the verification of reactive systems with hard real-time constraints. Our main objective is to propose an alternative to timed extensions of temporal logic during model checking. Our patterns are designed to express general timing constraints commonly found in the analysis of real-time systems (such as compliance to deadlines; event duration; bounds on the worst-case traversal time; etc.). They are also designed to be simple in terms of both clarity and computational complexity. In particular, each pattern should correspond to a decidable model checking problem.

Our patterns can be viewed as a real-time extension of Dwyer's specification patterns [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF]. In his seminal work, Dwyer shows through a study of 500 specification examples that 80% of the temporal requirements can be covered by a small number of "pattern formulas". We follow a similar philosophy and define a list of patterns that takes into account timing constraints. At the syntactic level, this is mostly obtained by extending Dwyer's patterns with two kind of timing modifiers: (1) P within I, which states that the delay between two events declared in the pattern P must fit in the time interval I; and (2) P lasting D, which states that a given condition in P must hold for at least duration D. For example, we define a pattern Present A after B within ]0, 4] to express that the event A must occur within 4 units of time (u.t.) of the first occurrence of event B, if any, and not simultaneously with it. Although seemingly innocuous, the addition of these two modifiers has a great impact on the semantics of patterns and on the verification techniques that are involved.

Our second contribution is an integrated model checking tool chain that can be used to check timed requirements. We provide a compiler for Fiacre [START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification in the Topcased Environment[END_REF], a formal modelling language for real-time systems, that we extended to support the declaration of real-time patterns. In our tool chain, Fiacre is used to express the model of the system while verification activities ultimately relies on Tina [START_REF] Berthomieu | The tool tina -construction of abstract state spaces for Petri nets and time Petri nets[END_REF], the TIme Petri Net Analyzer. This tool chain provides a reference implementation for our patterns when the systems can be modeled using an extension of Time Petri Nets with data variables and priorities that we call a TTS (see Sect. 2.1). This is not a toy example; Fiacre is the intermediate language used for model verification in Topcased [START_REF] Farail | The TOPCASED project: a Toolkit in Open source for Critical Aeronautic SystEms Design[END_REF], an Eclipse-based toolkit for system engineering, where it is used as the target of model transformation engines for various high-level modelling languages, such as SDL or AADL [START_REF] Berthomieu | Formal verification of AADL specifications in the Topcased environment[END_REF]. In each of these transformations, we have been able to use our specification patterns as an intermediate format between high-level requirements (expressed on the high-level models) and the low-level input languages supported by the model checkers in Tina.

The rest of the paper is organized as follows. In the next section, we define technical notations necessary to define the semantics of patterns. Section 3 gives our catalog of real-time patterns. For each pattern, we give a simple definition in natural language as well as an unambiguous, formal definition based on two different approaches. Before concluding, we review the results of experiments that have been performed using our verification tool chain in Sect. 4.

Technical Background

Since patterns are used to express timing and behavioral constraints on the execution of a system, we base the semantics of patterns on the notion of timed traces, which are sequences mixing events and time delays, (see Def. 1 below). We use a dense time model, meaning that we consider rational time delays and work both with strict and non-strict time bounds.

The semantics of a pattern will be expressed as the set of all timed traces where the pattern holds. We use two different approaches to define set of traces:

(1) Time Transition Systems (TTS), whose semantics relies on timed traces; and (2) a timed extensions of Linear Temporal Logic, called MTL. In our verification tool chain, both Fiacre and specification patterns are compiled into TTS.

Time Transition Systems and Timed Traces

Time Transition Systems (TTS) are a generalization of Time Petri Nets [START_REF] Merlin | A study of the recoverability of computing systems[END_REF] with priorities and data variables. We describe the semantics of TTS using a simple example. Figure 1 gives a model for a simple airlock system consisting of two doors (D 1 and D 2 ) and two buttons. At any time, at most one door can be open. This constraint is modeled by the fact that at most one of the places D1isOpen and D2isOpen may have a token. Additionally, an open door is automatically closed after exactly 4 units of time (u.t.), followed by a ventilation procedure that lasts 6 u.t. This behavior is modeled by adding timing constraints on the transitions Open1, Open2 and Ventil. Moreover, requests to open the door D 2 have higher priority than requests to open D 1 . This is modeled using a priority (dashed arrow) from the transition Open2 to Open1. A shutdown command can be triggered if no request is pending.

Idle Shutdown pre: ¬(req 1 ∨ req 2 )
Ventil. To understand the model, the reader may, at first, ignore side conditions and side effects (the pre and act expressions inside dotted rectangles). In this case, a TTS is a standard Time Petri Net, where circles are places and rectangles are transitions. A transition is enabled if there are enough tokens in its input places. A time interval, such as I = [d 1 ; d 2 [, indicates that the corresponding transition must be fired if it has been enabled for d units of time with d ∈ I. As a consequence, a transition associated to the time interval [0; 0] must fire as soon as it is enabled. Our model includes two boolean variables, req1 and req2, indicating whether a request to open door D 1 (resp. D 2 ) is pending. Those variables are read by pre-conditions on transitions Openi, Buttoni, and Shutdown and are modified by post-actions on transitions Buttoni and Closei. For instance, the pre-condition ¬req 2 on Button 2 is used to disable the transition when the door is already open. This implies that pressing the button while the door is open has no further effect.

We introduce some basic notations used in the remainder of the paper. (A complete, formal description of the TTS semantics can be found in [START_REF] Abid | Verification of Real-Time Specification Patterns on Time Transitions Systems[END_REF].) Like with Petri Nets, the state of a TTS depends on its marking, m, that is the number of tokens in each place. We write M the set of markings. Since we manipulate values, the state of a TTS also depends on its store, that is a mapping from variable names to their respective values. We use the symbol s for a store and write S for the set of stores. Finally, we use the symbol t for a transition and T for the set of transitions of a TTS. The behavior of a TTS is defined by the set of all its (timed) traces. In this particular case, a trace will contain information about fired transitions (e.g. Open1), markings, the value of variables, and the passing of time. Formally, we define an event ω as a triple (t, m, s) recording the marking and store immediately after the transition t has been fired. We denote Ω the set T ×M×S of events. The set of non-negative rational numbers is written

Q + .

Definition 1 (Timed trace). A timed trace σ is a possibly infinite sequence of events ω ∈ Ω and durations d(δ) with

δ ∈ Q + . Formally, σ is a partial mapping from N to Ω * = Ω ∪ {d(δ) | δ ∈ Q + } such that σ(i) is defined whenever σ(j) is defined and i ≤ j.
Given a finite trace σ and a-possibly infinite-trace σ ′ , we denote σσ ′ the concatenation of σ and σ ′ . This operation is associative. The semantics of patterns will be defined as a set of timed traces. Given a real-time pattern P , we say that a TTS T satisfies the requirement P if all the traces of T hold for P .

Metric Temporal Logic and Formulas over Traces

Metric Temporal Logic (MTL) [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF] is an extension of LTL where temporal modalities can be constrained by a time interval. For instance, the MTL formula A U [1,3[ B states that in every execution of the system (in every trace), the event B must occur at a time t 0 ∈ [1, 3[ and that A holds everywhere in the interval [0, t 0 [. In the following, we will also use a weak version of the "until modality", denoted A W B, that does not require B to eventually occur. We refer the reader to [START_REF] Ouaknine | On the decidability and complexity of metric temporal logic over finite words[END_REF] for a presentation of the logic and a discussion on the decidability of various fragments.

An advantage of using MTL is that it provides a sound and unambiguous framework for defining the meaning of patterns. Nonetheless, this partially defeats one of the original goal of patterns, that is to circumvent the use of temporal logic in the first place. For this reason, we propose an alternative way for defining the semantics of patterns that relies on first-order formulas over traces. For instance, when referring to a timed trace σ and an event A, we can define the "scope" σ after A-that determines the part of σ located after the first occurrence of A-as the trace σ 2 such that ∃σ 1 .σ = σ 1 Aσ 2 ∧ A / ∈ σ 1 . We believe that this second approach may ease the work of engineers that are not trained with formal verification techniques. Our experience shows that being able to confront different definitions for the same pattern, using contrasting approaches, is useful for teaching patterns.

Model checking, Observers and TTS

We have designed our patterns so that checking whether a system satisfies a requirement is a decidable problem. We assume here that we work on discrete models (with a continuous time semantics), such as timed automata or time Petri Nets, and not on hybrid models. Since the model checking problem for MTL is undecidable [START_REF] Ouaknine | On the decidability and complexity of metric temporal logic over finite words[END_REF], it is not enough to simply translate each pattern into a MTL formula to check whether a TTS satisfies a pattern. This situation can be somehow alleviated. For instance, the problem is decidable if we disallow simultaneous events in the system and if we disallow punctual timing constraints, of the form [d, d]. Still, while we may rely on timed temporal logics as a way to define the semantics of patterns, it is problematic to have to limit ourselves to a decidable fragment of a particular logic-which may be too restrictive-or to rely on multiple real-time model checking algorithms-that all have a very high complexity in practice.

To solve this problem, we propose to rely on observers in order to reduce the verification of timed patterns to the verification of LTL formulas. We provide for each pattern, P , a pair (T P , φ P ) of a TTS model and a LTL formula such that, for any TTS model T , we have that T satisfies P if and only if T ⊗ T P (the composition of the two models T and T P ) satisfies φ P . The idea is not to provide a generic way of obtaining the observer from a formal definition of the pattern. Rather, we seek, for each pattern, to come up with the best possible observer in practice. To this end, using our tool chain, we have compared the complexity of different implementations on a fixed set of representative examples and for a specific set of properties and kept the best candidates.

A Catalog of Real-Time Patterns

We describe our patterns using a hierarchical classification borrowed from Dwyer [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] but adding the notion of "timing modifiers". Patterns are built from five categories, listed below, or from the composition of several patterns (see Sect. 3.4):

-Existence Patterns (Present): for conditions that must eventually occur; -Absence Patterns (Absent): for conditions that should not occur; -Universality Patterns : for conditions that must occur throughout the whole execution; -Response Patterns (Response): for (trigger) conditions that must always be followed by a given (response) condition;

-Precedence Patterns : for (signal) conditions that must always be preceded by a given (trigger) condition.

In each class, generic patterns may be specialized using one of five scope modifiers that limit the range of the execution trace over which the pattern must hold:

-Global : the default scope modifier, that does not limit the range of the pattern. The pattern must hold over the whole timed trace; -Before R : limit the pattern to the beginning of a time trace, up to the first occurrence of R; -After Q : limit the pattern to the events following the first R; -Between Q and R : limit the pattern to the events occurring between an event Q and the following occurrence of an event R; -After Q Until R : similar to the previous scope modifier, except that we do not require that R must necessarily occur after a Q.

Finally, timed patterns are obtained using one of two possible kind of timing modifiers that limit the possible dates of events referred in the pattern:

-Within I : to constraint the delay between two given events to belong to the time interval I; -Lasting D : to constraint the length of time during which a given condition holds (without interruption) to be greater than D.

When defining patterns, the symbols A, B, . . . stand for predicates on events ω ∈ Ω such as Open 2 ∨ req 2 . In the definition of observers, a predicate A is interpreted as the set of transitions of the system that match A. Due to the somewhat large number of possible alternatives, we restrict this catalog to the most important presence, absence and response patterns. Patterns that are not described here can be found in a long version of this paper [START_REF] Abid | A Real-Time Specification Patterns Language[END_REF].

For each pattern, we give its denotational interpretation based on First-Order formulas over Timed Traces (denoted FOTT in the following) and a logical definition based on MTL. We provide also the observer and the LTL formula that should be combined with the system in order to check the validity of the pattern. We define some conventions on observers. In the following, Error, Start, . . . are transitions that belong to the observer, whereas E 1 (resp. E 2 ) represents all transitions of the system that match predicate A (resp. B). We also use the symbol I as a shorthand for the time interval

Existence patterns

An existence pattern is used to express that, in every trace of the system, some events must occur. The associated ltl formula is ¬(foundB ∧ bad). Explanation:

Variable f oundB is set to true after each occurrence of E 2 . Conversely, we set the variables bad to true and f oundB to false at each occurrence of E 1 . Therefore f oundB is true on every "time interval" between an E 2 and an E 1 . We use transition Reset to set bad to false if this interval is longer than D. As a consequence, the pattern holds if we cannot find an occurrence of E 2 (f oundB is true) while bad is true.

Response patterns

Response patterns are used to express "cause-effect" relationship, such as the fact that an occurrence of a first kind of events must be followed by an occurrence of a second kind of events.

A leadsto first B within I The associated ltl formula is ( ¬Error) ∧ ( ¬(B ∧ bad)). Explanation:

Every occurrence of A must be followed by an occurrence of B within time interval I (considering only the first occurrence of B after A).

After each occurrence of E 1 , variables f oundA and bad are set to true and the transition Start is enabled. Variable bad is used to control the beginning of the time interval. After each occurrence of E 2 variable f oundA is set to false. Hence Error is fired if there is an occurrence of E 1 not followed by an occurrence of E 2 after d 2 u.t. We use priorities to avoid errors when E 2 occurs precisely at time d 1 or d 2 .

A leadsto first B within I before R Before the first occurrence of R, each occurrence of A is followed by a B-and these two events occur before R-in the time interval I. The pattern holds if R never occur. The associated ltl formula is ♦R ⇒ ( ¬Error ∧ ¬(B ∧ bad)). Explanation:

Same explanation than for the previous case, but we only take into account transitions E 1 and E 2 occurring before E 3 .

A leadsto first B within I after R

Same than with the pattern "A leadsto first B within I" but only considering occurrences of A after the first R.

Example:

Button2 leadsto first Open2 within [0, 10] after Shutdown mtl def.:

(R ⇒ ( (A ⇒ (¬B) UI B))) fott def.: ∀σ1, σ2 . (σ = σ1Rσ2Aσ3 ∧ R / ∈ σ1) ⇒ ∃σ4, σ5 . σ3 = σ4Bσ5 ∧ ∆(σ4) ∈ I ∧ B / ∈ σ4
Observer: It is similar to the observer of the pattern A leadsto first B within I before R . We should just replace ¬foundR in transition E1 and E2 by foundR.

The associated ltl formula is ♦R ⇒ ( ¬Error ∧ ¬(B ∧ bad)). Explanation:

Same explanation than in the previous case, but we only take into account transitions E 1 and E 2 occurring after an E 3 .

Composite Patterns

Patterns can be easily combined together using the usual boolean connectives. For example, the pattern "P 1 and P 2 " holds for all the traces where P 1 and P 2 both hold. To check a composed pattern, we use a combination of the respective observers, as well as a combination of the respective LTL formulas. For instance, if (T 1 , φ 1 ) and (T 2 , φ 2 ) are the observers and LTL formulas corresponding to the patterns P 1 and P 2 , then the composite pattern P 1 and P 2 is checked using the LTL formula φ 1 ∧ φ 2 . Similarly, if we check the LTL formula φ 1 ⇒ φ 2 (implication) then we obtain a composite pattern P 1 ⊸ P 2 that is satisfied by systems T such that, for all traces of T , the pattern P 2 holds whenever P 1 holds.

Use Cases and Experimental Results

In this section, we report on three experiments that have been performed using an extension of a Fiacre compiler that automatically compose a system with the necessary observers. In case the system does not meet its specification, we obtain a counter-example that can be converted into a timed sequence of events exhibiting a problematic scenario. This sequence can be played back using play and nd, two Time Petri Nets animators provided with Tina.

Avionic Protocol and AADL. Our first example is a network avionic protocol (NPL) which includes several functions allowing the pilot and ground stations to receive and send information relative to the plane: weather, speed, . . . AADL has been used to model the dynamic architecture for this demonstrator [START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF]. The AADL model includes several threads that exchange information through shared memory data and amounts to about 8 diagrams and 800 lines of code (using AADL textual syntax). The AADL code specifies both the hardware and software architecture of the system and defines the real time properties of threads, like for instance their dispatch protocol (periodic or sporadic) or their periods.

We used the AADL2Fiacre plug-in of Topcased to check properties on the NPL specification. The Fiacre model obtained after transformation takes into account the complete behavior described in the AADL model but also the whole language execution model, meaning that our interpretation takes fully into account the scheduling semantics as specified in the AADL standard. The abstract state space for the TTS generated from Fiacre has about 120 000 states and 180 000 transitions and can be generated in less than 12s on a typical development computer (Intel dual-core processor at 2GHz with 2Gb of RAM). On examples of this size, our model checker is able to prove formal properties in a few seconds. We checked a set of 22 requirements that were given together with the description of the system, all expressed using a natural language description and, in one case, a scenario based on a UML sequence diagram. Of these 22 requirements, 18 where instances of "untimed patterns", such as checking the absence of deadlock or that threads are resettable. The four remaining requirements where "response patterns" of the kind A leadsto first B within [0, d]. Using patterns, we were able to check the 22 patterns in less than 5min.

Service Oriented Applications. We consider models obtained from the composition of services expressed using a timed extension of BPEL, the Business Process Execution Language. Our example models a scenario from the health-care domain related to patient handling during a medical examination. The scenario involves three entities, each one managed by a service: a Clinic Service (CS); a Medical Analysis Service (MAS); and a Pharmacy Service (PS). When a patient arrives in clinic, a doctor should check with the MCS whether its social security number is valid. If so, the doctor may order some medical analyses from the MAS and, after analyzing the results, he can order drugs through the PS. Timing constraints can be added to this scenario by associating a duration to each activity of the workflow and a delay to each service invocation.

We use our patterns to express different requirements on this system. An example involving the absence pattern is that we cannot have two medical analyses for a patient in less than 10 days (240 hours): absent MAS.medicalAnalysis after MAS.medicalAnalysis for interval ]0, 240]. A more complicated example of requirement is to impose that if a doctor does not cancel a drug order within 6 hours, then it should not cancel drugs for another 48 hours. This requirement can be expressed using the composition of two absence patterns (see Sect. 3.4):

(absent MCS.drugsChanging after MCS.drugsAsking for interval [0; 6]) ⊸ (absent MCS.drugsChanging after MCS.drugsAsking for interval [0; 54]).

Finally, using the notation S.init and S.end to refer to a start (resp. end) event in the service S, we can express that drugs must be delivered within 48 hours of the medical examination start: MCS.init leadsto PS.sendDrugsOrder within

[0; 48].
The complete scenario is given in [START_REF] Guermouche | Formal Requirement Verification for Timed Choreographies[END_REF], where we describe a transformation tool chain from Timed BPEL processes to Fiacre. For a more complex version of the health care scenario, with seven different services and more concurrent activities, the state graph for the TTS generated from Fiacre is quite small, with only 886 states and 2476 transitions. The generation of the Fiacre specification and its corresponding state space takes less than a second. For examples of this size, the verification time for checking a requirement is negligible (half a second).

Transportation Systems. Our final example is an automated railcar system, taken from [START_REF] Dong | Timed automata patterns[END_REF], that was directly modeled using Fiacre. The system is composed of four terminals connected by rail tracks in a cyclic network. Several railcars, operated from a central control center, are available to transport passengers between terminals. When a car approaches its destination, it sends a request to signal its arrival to the terminal. This system has several real-time constraints: the terminal must be ready to accommodate an incoming car in 5s; a car arriving in a terminal leaves its door open for exactly 10s; passengers entering a car have 5s to choose their destination; etc. There are three key requirements:

(P1) when a passenger arrives in a terminal, a car must be ready to transport him within 15s. This property can be expressed with a response pattern, where Passenger/sndReq is the state where the passenger requests a car and Car/ack-Term is the state where it is served: Passenger/sendReq leadsto Car/ackTerm within [0, 15] (P2) When the car starts moving, the door must be closed: present CarDoor/closeDoor after CarHandler/moving within [0, 10] (P3) When a passenger select a destination (in the car), a signal should stay illuminated until the car is arrived: absent Terminal/buttonOff before Control/ackTerm for duration [START_REF] Dong | Timed automata patterns[END_REF] We can prove that these three patterns are valid on our Fiacre model. Concerning the performances, we are able to generate the complete state space of the railcar system in 310ms, using 400kB of memory. This gives an upper-bound to the complexity of checking simple (untimed) reachability properties on the system, like for instance the absence of deadlocks. The three patterns can all be checked in under 1.5s. For instance, we observed that checking property (P1) is not more complex than exploring the complete system: the property is checked in 450ms, using 780kB of memory. Also, this is roughly the same complexity than checking the corresponding untimed requirement in LTL that is:

(Passenger/sendReq ⇒ ♦Control/ackTerm).

Conclusion.

In other benchmarks, we have often found that the complexity of checking timed patterns is in the same order of magnitude than checking their untimed temporal logic equivalent. An exception to this observation is when the temporal values used in the patterns are far different from those found in the system; for example if checking a periodic system, with a period in the order of the milliseconds, against a requirement using an interval in the order of the minutes. More results on the complexity of our approach can be found in [START_REF] Abid | Verification of Real-Time Specification Patterns on Time Transitions Systems[END_REF]. These experimentation, while still modest in size, gives a good appraisal of the use of formal verification techniques for real industrial software. These experimental results are very encouraging. In particular, we can realistically envisage that system engineers could evaluate different design choices in a very short time cycle and test the safety of their solutions at each iteration.

Related Work and Contributions

We base our approach on the original catalog of specification patterns defined by Dwyer [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF]. This work essentially study the expressiveness of their approach and define patterns using different logical framework (LTL, CTL, Quantified Regular Expressions, etc.). As a consequence, they do not need to consider the problem of checking requirements as they can readily rely on existing model checkers. Their patterns language is still supported, with several tools, an online repository of examples [START_REF] Dwyer | Online Repository of Specification Patterns[END_REF] and the definition of the Bandera Specification Language [START_REF] Corbett | A language framework for expressing checkable properties of dynamic software[END_REF] that provides a structured-English language front-end. A recent study by Bianculli et al. [START_REF] Bianculli | Specification Patterns from Research to Industry: a Case Study in Service-based Applications[END_REF] show the relevance of this pattern-based approach in an industrial context. Some works consider the extension of patterns with hard real-time constraints. Konrad et al. [START_REF] Konrad | Real-time specification patterns[END_REF] extend the patterns language with time constraints and give a mapping from timed pattern to TCTL and MTL. Nonetheless, they do not consider the complexity of the verification problem (the implementability of their approach). Another related work is [START_REF] Gruhn | Patterns for timed property specifications[END_REF], where the authors define observers based on Timed Automata for each pattern. However, they consider a less expressive set of patterns (without the lasting modifier) and they have not integrated their language inside a tool chain or proved the correctness of their observers. By contrast, we have defined a formal framework that has been used to prove the correctness of some of our observers [START_REF] Abid | Verification of Real-Time Specification Patterns on Time Transitions Systems[END_REF]. Work is currently under way to mechanize these proofs using the Coq interactive theorem prover.

Our patterns can be viewed as a subset of the Contracts Specification Language (CSL), defined in the context of the SPEEDS project [START_REF] Gafni | Contract Specification Language (CSL)[END_REF], which is intended as a pragmatic proposal for specifying contract assertions on HRC models. While the semantics for HRC is based on hybrid automata, the only automatic verification tools available for CSL use a discrete time model. Therefore, our verification tool chain provides a partial implementation for CSL (the part concerned by timing constraints) for a dense time model. This is an important result since more conception errors can be captured using a dense rather than a discrete time model.

Compared to these related works, we make several contributions. We extend the specification patterns language of et al. with two modifiers for real-time constraints. We also address the problem of checking the validity of a pattern on a real-time system using model-based techniques: our verification approach is based on a set of observers, that are described in Sect. 3. Using this approach, we reduce the problem of checking real-time properties to the problem of checking simpler LTL properties on the composition of the system with an observer. Another contribution is the definition of a formal framework to prove that observers are correct and non-intrusive, meaning that they do not affect the system under observation. This framework is useful for proving the soundness of optimization. Due to space limitations, we concentrate on the definition of the patterns and their semantics in this paper, while most of the theoretical results are presented in a companion research report [START_REF] Abid | Verification of Real-Time Specification Patterns on Time Transitions Systems[END_REF]. Finally, concerning tooling, we offer an EMF-based meta-model for our specification patterns that allow its integration within a model-driven engineering development: our work is integrated in a complete verification tool chain for the Fiacre modelling language and can therefore be used in conjunction with Topcased [START_REF] Farail | The TOPCASED project: a Toolkit in Open source for Critical Aeronautic SystEms Design[END_REF], an Eclipse based toolkit for system engineering.

Conclusion and Perspectives

We define a set of high-level specification patterns for expressing requirements on systems with hard real-time constraints. Our approach eliminates the need to rely on model checking algorithms for timed extensions of temporal logics that-when decidable-are very complex and time-consuming. While we have concentrated our attention on model checking-and although we only provide an implementation for TTS models-we believe our notation is interesting in its own right and can be reused in different contexts.

There are several directions for future works. We plan to define a compositional patterns inspired by the "denotational interpretation" used in the definition of patterns. The idea is to define a lower-level pattern language, with more composition operators, that is amenable to an automatic translation into observers (and therefore can dispose with the need to manually prove the correctness of our interpretation). In parallel, we plan to define a new modelling language for observers-adapted from the TTS framework-together with specific optimization techniques and easier soundness proofs. This language, which has nearly reached completion, would be used as a new target for implementing patterns verification.

¬req 2 Fig. 1 .

 21 Fig. 1. A TTS model of an airlock system

  [d 1 , d 2 ]. The observers for the pattern obtained with other time intervals-such as ]d 1 , d 2 ], ]d 1 , +∞[, or in the case d 1 = d 2 -are essentially the same, except for some priorities between transitions that may change. By convention, the boolean variables used in the definition of an observers are initially set to false.

absent

  Open1 before Close1 for duration 3mtl def.: ♦B ⇒ (A ⇒ ( [0,D] ¬B)) U B fott def.: ∀σ1, σ2, σ3, ω . (σ = σ1ωσ2Bσ3 ∧ B / ∈ σ1ωσ2 ∧ ∆(σ2) D) ⇒ ¬A(ω)

  Open2 within [0, 10] mtl def.: (A ⇒ (¬B) UI B) fott def.: ∀σ1, σ2 . (σ = σ1Aσ2) ⇒ ∃σ3, σ4 . σ2 = σ3Bσ4 ∧ ∆(σ3) ∈ I ∧ B /

  Open2 within [0, 10] before Shutdownmtl def.: ♦R ⇒ ( (A ∧ ¬R ⇒ (¬B ∧ ¬R) UI B ∧ ¬R) U R fott def.: ∀σ1, σ2, σ3 . (σ = σ1Aσ2Rσ3 ∧ R / ∈ σ1Aσ2 ⇒ ∃σ4, σ5 . σ2 = σ4Bσ5 ∧ ∆(σ4) ∈ I ∧ B / ∈σ4Observer: E1 act: if ¬ foundR then foundA := true bad := true Start act: bad := false [d1, d1] Error pre: foundA ]d2, ∞[ E2 act: if ¬ foundR then foundA := false E3 act: foundR=true

⋆ This work was partially supported by the JU Artemisia project CESAR and the FNRAE project Quarteft

The associated ltl formula is []¬Error. Explanation:

In this observer, transition Error is conditioned by the value of the shared boolean variables foundA and foundB.

Observer: The associated ltl formula is ¬Error. Explanation:

Variable foundA is set to true when transition P oll is fired, that is when A becomes true for the first time. Transition OK is used to set win to true if A is true for duration D without interruption (otherwise its timing constraint is resetted). Otherwise, if variable win is still false after D u.t., then transition Error is fired. We use a priority between Error and OK to disambiguate the behavior D u.t. after Poll is fired.

Absence patterns

Absence patterns are used to express that some condition should never occur.


S Msolli
email: smsolli@enit.fr

O Dalverny

J Alexis
email: cjoel.alexis@enit.fr

M Karama

Effects of the unified viscoplastic formulation and temperature terms on the thermomechanical behavior of soldering materials

Keywords: Viscoplasticity, thermomechanical, solders, hysteresis loops, jump tests, hardening, FEM, thermal cycling

Solder materials are critical packaging compounds and due to usually weakest melting temperature among packaging constitutive materials, thus, they are frequently subjected to a multitude of physical phenomena: creep, fatigue and combined hardening effects. The complexity and interaction of such factors must be considered in suitable way in the mechanical behavior modeling using the appropriate material behavior laws. The choice of the mechanical model depends on several factors such as the complexity of constitutive equations to be integrated, the availability and suitability of implementation in the FE codes, the number of parameters to be identified, the capability of the model to represent the most common physical features of the material… Following these observations and in order to deal with these critical remarks, comparisons between the most common unified viscoplastic models should be done in the local and finite element levels for the decision upon the most efficient model. That is the aim of this paper with application to a tin based solder token as the test material.

Thermoviscoplastic modeling of solders

Two ways of reasoning are in general followed by researchers in the modeling efforts. In one side, available models with few material parameters are preferred because they are in generally predefined and available in the FE codes, which is leading to less identification and computation efforts but the price is a weak correlation with some material experimental data. This is acceptable in some cases based on the resemblance, the complexity of the long-term behavior of some commonly used solders, the low level of applied loadings and also the most important objective which is the lifetime prediction of the solder. We can include Anand [1] and the separated viscoplastic models [2] among these categories. On the other point of view, and inspite of the complexity of their constitutive equations, some kind of unified viscoplastic such as McDowell [3], Basaran et al. [4] Wei et al. [5] Chaboche [6] are "painfully" implemented in the FE codes by suitable integration algorithms. They also present a huge number of parameters but can describe the majority of the material physical mechanisms such creep, relaxation, Bauschinger effects, cyclic hardening, ratcheting,…These models are also suitable for complex and combined loadings such as thermal, in-phase and out-of-phase thermomechanical fatigue [7], nonproportional loadings,…they may offer the possibility of fatigue model coupling or damage model incorporation in the constitutive equations themselves leading to a realistic follow-up of the degradation of the material [8]. Based on these facts, the aim of this work is limited to the comparison of some of these models. So we present firstly a brief description of the chosen models i.e. Anand, McDowell and Chaboche unified viscoplastic models. Next, we describe the experimental tests and identification model. Then, comparisons of the numerical results issued from shear and relaxation tests are made and finally a comparison is done using finite element simulation for assembled structure.

Description of the studied laws

The unified viscoplastic models are usually formulated using two kinds of equations: flow law which represents the inelastic strain rate variation and a set of evolution equations for describing the variation of the state variables. The flow law reflects the inelastic deformation of metals with respect to the stress and temperature levels. Then, its formulation is mainly related to the high temperature creep mechanisms such dislocation climb and dislocation glide, creep dislocation, etc [START_REF] Stouffer | Inelastic Deformation Of Metals: Models, Mechanical properties and metallurgy[END_REF]. The state variables could be kinematic hardening, isotropic hardening and damage of the material. In the evolution equation and in order to represent accurately the hardening/softening effects, hardening, dynamic and thermal static recovery terms are employed. Hardening represents purely the resistance to plastic deformation and it is proportional to the inelastic strain rate. Dynamic recovery terms are used for the thermally activated mechanisms which acts especially at high temperature and serves in certain manner to take into account the dislocation annihilation during deformation. Static thermal recovery terms dominate when time-dependent effects such creep and relaxation are strongly present. So, it reduces shear stresses due to dislocation interactions (hardening) and isotropically dispersed material defects. Anand viscoplastic model. The model presents only one scalar state variable denoted by s for isotropic hardening effects [START_REF] Anand | [END_REF] or « deformation resistance ». The scalar form of the model is expressed as follows:

1/ exp sinh m in G Q A B R T s              (1)
Where A and B are material parameters, Q is the activation energy, m is the strain rate sensitivity, R G is the gas constant, and T is the absolute temperature, respectively. A simple form of the evolution equation of s is defined as

0 1 . 1 ; 1 * * a in s s s h sign a s s                   (2) With * ˆexp n in G Q ss A R T          (3)
Where s* represents a saturation value of s. ŝ is a material parameter. The parameter h 0 is hardening/softening coefficient and n is a rate sensitivity parameter for the saturation value of s. Finally, there was nine temperature-independent parameters to be identified which are Q, A, n, m, a, h0, ŝ , B and s 0 the initial value of the deformation resistance. Chaboche's viscoplastic model. Contrarily to Anand's model, the Chaboche's viscoplastic model expressed here in its uniaxial form [11], includes combined hardening effects, moreover, it's includes a power term in the flow written below

  n in X R k sign X Z         (4)
With <x> = max(x,0), k is the initial yield stress and the constants Z and n are material parameters. Kinematic hardening is described by the internal state variable X whose equation is expressed as

    . r X C a sign X X p d X      (5)
C, a, d and r are material parameters and p is the cumulated inelastic strain. Isotropic hardening effects are taken into account by scalar state variable R which evolves according to

  R b Q R p  (6)
Knowing that R(0) = k, b and Q are material parameters. So, in the whole model, there were nine temperature-dependent parameters to be identified in each test temperature which are Z, n, k, C, a, d, r, b and Q.

McDowell's viscoplastic model. The model contains combined features as compared to Anand and Chaboche's constitutive equations. It includes activation energy term, a Zener-Hollowman parameter for creep activation mechanisms and finally combined kinematic/isotropic hardening equations as for Chaboche's model [12,13]. In this case, flow law is expressed in the uniaxial form as follows

  1 exp n n in X R k X R k A B sign X Z Z                        ( (7)
With A, n, Z and B are material parameters.

The Arrhenius Term used in the flow law is given by exp for 2

2 exp ln 1 for 2 2 m m m m T Q T kT T T Q T kT T                                  (8)
T m is the melting temperature, Q the activation energy, and k the Boltzmann's constant. In the other hand, X is token as the sum of X 1 and X 2 in such a way that

    1 1 1 1 1 . m X C a sign X p X p C a X       (9)
And

    2 * 2 2 2 m X H sign X p C X      (10)
Coupling between R and b is considered using the variable so

      ' 3 1 2 m R Q p QC            (11)     ' m a Q p QC          (12)
with R(0) = k and a(0) = a 0 . The McDowell's model presents sixteen parameters to be determined. Only C, H*, a0, k, ' and Q are temperature-independent parameters. It's obvious that the formulation of the constitutive equations differs from a model to another: Anand proposes an Arrhenius term to improve for thermal effects description in such a way that the model parameters are temperature-independent.

But he only used one evolution equation which contains only a hardening term (proportional to the inelastic strain). For the time-dependent effects, he uses a sin hyperbolic term in conjunction with the Arrhenius Term. Chaboche introduces a power term similar to Norton creep law without introducing explicitly temperature dependent terms. Following these facts, all the model parameters are temperature dependent and must be identified in each temperature range. Moreover, he uses more than one state variable to take into account the influence of both kinematic and isotropic hardening effects. Each equation includes simultaneously hardening, dynamic recovery and static thermal recovery terms. Contrarily to Anand and Chaboche's model, McDowell considers that the dislocation motion mechanisms can be described by an exponential Zener Hollowman parameter. He also used the Arrhenius Term for the thermal effects such as for the Anand's model and adopts a Frederick-Armstrong kinematic hardening evolution equation such as that used in the chaboche's model. In this case, some model constants are fixed as temperature-independent parameters.

Models comparison in strain controlled cyclic responses

Models are evaluated and compared using various material behavior cases, in fact, the material exhibits isotropic hardening, kinematic hardening or both. In Jumps tests. The aim of these tests is to evaluate the capability of the models to represent transient stages and to take into account the loading history [START_REF] Krausz | Unified constitutive laws of plastic deformation[END_REF]. This is important because during service, solder is continuously subjected to a variable rate of deformation due to thermal fatigue conditions. In order to examine this fact, numerical jumps tests are performed respectively at 10 -5 , 10 -4 , 10 -3 and 10 -2 /s.

Effect of thermomechanical and thermal fatigue loading

There are two approaches which are used to represent temperature variation effects. One empirical approach is consisting on the introduction of temperature effect on the material parameters as for Chaboche's viscoplastic model. Thus, it's necessary to identify the set of material parameters of the model in each temperature range using isothermal data for different temperature levels. Then, it's obvious to interpolate parameters conveniently in intermediate temperatures. On the other hand, temperature effects can be used explicitly such in the Arrhenius term which means that the parameters may not be strictly temperature-dependent. According to these facts, the Anand, Chaboche and McDowell models are compared in the case of a thermomechanical and thermal fatigue loading. The parameters used for the comparison are those identified by isothermal data and shown in Table 1 and2 McDowell and Chaboche model where kinematic hardening contributes to the progressive dynamic recovery of the material and thus smooth profiles were obtained. Effect of thermal fatigue loading. For the thermal fatigue effects, the comparison is made in the finite element level by simulating a thermal cycling of a 2D typical assembly of electronic components. The assembly is constituted by a soldered silicon Chip brazed to a DBC substrate by a 62Sn36Pb2Ag solder alloy. The power assembly is presented in figure 6. The consequences may be observed when lifetime prediction is proceeded using based inelastic deformation energy or plastic deformation fatigue models which must be verified.

Discussions

Following the calculated numerical responses, Anand model in its presented fully isotropic formulation is unable to describe exactly SnPbAg solder results obtained by McDowell model especially in the case of thermal fatigue loading. On the other hand, Chaboche and McDowell models show good agreements even when varying the imposed strain rate and temperature. Timedependent effects are also well fitted. According to the thermomechanical and thermal fatigue data, the two models show some similarities which are due to the way of taking into account temperature and temperature effects and multiple sets of identified parameters at close temperatures. Introducing a temperature rate term in the kinematic hardening equations and an Arrhenius term in the flow law in the McDowell model has incidence in the thermal fatigue tests. In fact, when temperature rates are not important, the acting creep terms in the flow laws varies differently. So, in the modeling steps and especially at fast and low thermal fatigue cycles, care must be taken for the choice of the constitutive model.

Summary

Three unified viscoplastic models are integrated and implemented in the finite element code Abaqus. The responses of these models are compared for various loading cases including isothermal mechanical tests, thermomechanical fatigue and thermal fatigue tests. Generally, no remarkable differences are present and responses profile keep resemblance excepting the case of thermal fatigue. Thus and at long term behavior, models are expected to exhibit divergence especially when they'll be used for the lifetime prediction of the solder in spite of the dependence on the coupled fatigue or damage model. These facts have to be verified with a comparative study of extensive lifetime numerical data.

Fig. 2 :

 2 Fig. 2: cyclic strain controlled tests at various temperatures (a) 293 K (b) 373 K (c) 423 K. Strain controlled tests are performed at 10 -2 , 10 -3 and 10 -4 /s for various temperatures 293, 323, 373 and 423 K. Results shown in figure 2, indicates that Chaboche (continuous lines) and McDowell (markers) models are able to reproduce the cyclic response of the material under various strain rates and temperatures. It's also obvious that 62Sn36Pb2Ag solder don't exhibit cyclic hardening which reduces the two models to the kinematic hardening formulation. Due to its fully isotropic Character, Anand model (broken lines) can't reproduce correctly the solder behavior with its actual formulation in comparison with McDowell numerical simulations. Moreover, effects of strain rate variation are well represented by both Chaboche and McDowell models.Jumps tests. The aim of these tests is to evaluate the capability of the models to represent transient stages and to take into account the loading history[START_REF] Krausz | Unified constitutive laws of plastic deformation[END_REF]. This is important because during service, solder is continuously subjected to a variable rate of deformation due to thermal fatigue conditions. In order to examine this fact, numerical jumps tests are performed respectively at 10 -5 , 10 -4 , 10 -3 and 10 -2 /s.

Fig. 3 :

 3 Fig. 3: Jumps tests at various temperatures.Following figure3, the Chaboche and McDowell models correlate well, either in high temperature level and very small strain rate as it was shown in the first tensile portion of the curves which indicates a pertinent identification procedure for material parameters too. However, in the same figure, Anand model shows in this jump test, some weakness in describing high strain rate behavior at low temperatures and vice-versa. Stress relaxation tests. In order to evaluate the ability of the models to reproduce purely timedependent effects, stress relaxation tests are realized using an initial tensile step which is performed at 10 -2 /s at different temperatures followed by a 20 s hold time at 0.05 deformation range.

Figure 4 :

 4 Figure 4: Stress relaxation tests at various temperatures. Results shown in figure 4 indicate that relaxation numerical results are in good agreements for both Chaboche and McDowell laws. At high temperatures, solder reaches quickly the stress saturation level which is numerically well described. Anand model appears to be more convenient for saturation at high temperature even with regards to jump tests.

  .

Table 2 :Fig. 5 :

 25 Fig. 5: (a) in-phase (b) out-of-phase TMF test. This observation means mainly that linear interpolation of the Chaboche parameters in one hand and explicit-empirical formulation of McDowell model induce quite similar results. For the Anand model, the evolution of stress is only driven by the variation of saturation level contrarily to

Fig. 6 :

 6 Fig. 6: Power electronic assembly. The assembly is subjected to thermal heating-cooling cycles in air. Thermal fatigue conditions are applied to observe temperature and temperature rate influences on the studied assembly. Temperature histories are shown on figure 7. Results are compared at the more solicited regions in the solder in term of shear stress evolution.

Fig. 7 :

 7 Fig. 7: Temperature histories with fast and slow transient regimes.Results in figure8indicate that shear stress history prediction differs for all the models and this observation is also valuable for all the imposed thermal cycles. Anand model responses show more accumulation of plastic deformation. This is due to the independent-temperature nature of the parameters so hardening behavior don't vary so much from high to low or low to high temperature. Moreover, Chaboche and McDowell models give similar results when cycle 2 is imposed. However, diminishing temperature rate in cycle 1, leads to divergent results. In fact, creep mechanisms (terms) are more influent in this case of loading and that's why the differences between Arrhenius term in McDowell model and Norton power law formulation in Chaboche model is more apparent.

Table 1 :

 1 Anand and McDowell's models are included in this kind of formulation. It includes also temperature rate effects for fast transient thermal regimes by introducing explicitly a rate term in the hardening equations. Identified Anand's model parameters for 62Sn36Pb2Ag.

	S 0 39.5	Q/R 9692.1	A 122.2	m 10.98 0.21	n 120554 30.55 0.0483 2.344 a h 0


G Gandanegara

X Roboam

B Sareni

G Dauphin-Tanguy

Bond Graph Based Stability Analysis of a Railway Traction System

Keywords: Bond graph, system design, heterogeneous devices, modelling, stability

This paper emphasises the interest of the Bond Graph approach for analysis and system design of heterogeneous and multi-field devices. In particular, the local stability analysis of non linear systems can be directly derived from the linearised Causal Bond

Graph. This method is applied to a typical electrical engineering system : a railway traction device involving electromechanical couplings. Validity, usefulness and originality of this approach are displayed.

I. INTRODUCTION

Electrical engineering systems are more and more complex and heterogeneous, being constituted by elements of different natures and different physical fields. In order to face these issues, a unified formalism is particularly useful : the Bond Graph (BG) [START_REF] Paynter | Analysis and Design of engineering systems[END_REF][START_REF] Karnopp | System Dynamics : Modelling and Simulation of Mechatronic Systems[END_REF][START_REF] Dauphin-Tanguy | Les Bond Graphs[END_REF] has been conceived in this way to represent power transfers by establishing energetic analogies between each field. The causality, essential property for power systems, is graphically represented in the BGs. Several interesting properties can be directly derived from the Causal Bond Graph in terms of system analysis and design:

Homogeneous modelling of a heterogeneous system makes easier coupling analysis by means of causal properties; Several analysis methods are directly applicable on BGs, such as structural or modal analysis [START_REF] Dauphin-Tanguy | Les Bond Graphs[END_REF][START_REF] Sueur | Bond-graph approach for structural analysis of MIMO linear systems[END_REF][START_REF] Dauphin-Tanguy | Bond graph aided design of controlled systems[END_REF], stability analysis, model simplification methods [START_REF] Sueur | Bond Graph Approach to Multi-time Scale Systems Analysis[END_REF][START_REF] Louca | A Physical-based Model reduction Metric with an Application to Vehicle Dynamics[END_REF][START_REF] Louca | Energy-based Model Reduction of Linear Systems[END_REF][START_REF] Gandanegara | Bond Graph Multi-time Scale Analysis of a Railway Traction System[END_REF][START_REF] Gandanegara | Modeling and Multi-time Scale Analysis of Railway Traction Systems Using Bond Graphs[END_REF][START_REF] Gandanegara | One Model for One Frequency Range : Comparison of Bond Graph Based Simplification Methods[END_REF][START_REF] Gandanegara | Methodologie de conception systémique en genie Electrique à l'aide de l'outil Bond Graph : Application à une chaîne de traction ferroviaire[END_REF]; An inverse modelling of the system can be obtained by means of bi-causality concept [START_REF] Gawthrop | Bicausal Bond Graph[END_REF] allowing to synthesize constraints relative to system requirements at each level of the BG. In this paper, a railway traction system is considered as case study. A bond graph model of this typical non linear system in electrical engineering allows to analyse the stability. For this purpose, the system is linearised thanks to the linearised BG [START_REF] Karnopp | Power and Energy in Linearised Physical Systems[END_REF]. This paper is divided in four sections:

-Firstly, a short review of the BG formalism is described.

-Several analysis techniques, directly applicable on BGs are presented in section III, in particular for the stability analysis. -The modelling of the railway traction device is presented in the fourth section : an original BG of AC induction motors is described especially when the system must be linearised around an operating point in order to achieve the stability analysis. -The fifth section shows the stability analysis of the obtained models.

II. BOND GRAPH BASIC PRINCIPLES

The BG formalism [START_REF] Paynter | Analysis and Design of engineering systems[END_REF][START_REF] Karnopp | System Dynamics : Modelling and Simulation of Mechatronic Systems[END_REF][START_REF] Dauphin-Tanguy | Les Bond Graphs[END_REF], introduced by H. Paynter in 1961 and formalised by Karnopp and Rosenberg in 1975, is now regularly used in many companies, particularly in automobile industry (PSA, Renault, Ford, Toyota, General Motors, …). This graphical method illustrates the energetic transfers in the system. The orientation of a half arrow indicates the power flow as expressed in Fig. 1. The primary characteristic of the BG is relative to its unified aspect through analogies summarised in Table 1. It obviously shows that this method can be applied to all physical domains by using generalised variables for : power : effort e (voltage in electricity) and flow f (current in electricity), energy : moment p (integral of effort) and displacement q (integral of flow). B Each bond brings simultaneously both information of effort and flow, where the product gives the transmitted power. Elements can be connected with 0-junctions (common effort), 1-junctions (common flow), transformers TF (relations effort-effort and flow-flow) and gyrators GY (relations effort-flow). These junctions are considered as power conservative. Active elements for effort and flow sources are added with three types of passive elements, each one representing storage or dissipative interactions between generalised variables as displayed by Paynter's tetrahedron in Fig. 2.

One of the most important bond graph properties for system analysis and design is the causality. It is graphically described by the "causal stroke" :

Properties of causal BGs are particularly rich in information :

As power transfers are concerned, they indicate if basic physical rules have been fulfilled when several elements are coupled. Indeed, respecting the integral causality ensures that the association is physically (and energetically) convenient and then "numerically consistent"; By following the causal loops and causal paths in the BGs, one can analyse couplings between elements in spite of domain changes; Many properties, useful for system analysis, can be extracted (see section III).

Simplified example :

Better than detailing the Bond Graph theory, which has been developed in several references [START_REF] Paynter | Analysis and Design of engineering systems[END_REF][START_REF] Karnopp | System Dynamics : Modelling and Simulation of Mechatronic Systems[END_REF][START_REF] Dauphin-Tanguy | Les Bond Graphs[END_REF], we illustrate this approach with the simple example of a DC traction system (see Fig. 4). The DC-DC converter is supposed to be perfect and power conservative. It can then be modelled as a modulated transformer ( MTF). If an instantaneous model is considered the modulation of the transformer is relative to the firing order state of the chopper (C H ). In average values, the gain is relative to the duty cycle following (eq. 1) :

m H Cf m I I V V α α = = (eq. 1)
where I H and V Cf denote the output current and voltage of the LCR filter, V m and I m represent the input current and voltage of the DC motor. The electromechanical coupling represented by (eq. 2) can be modelled by a gyrator (GY) crossing electrical effort (i.e. the emf E m ) with the mechanical flow (the rotation speed Ω m ) and the mechanical effort (i.e. the em torque T em ) with the flow (i.e. the current I m ) on the electrical side.

E I m C H ,α Ω m Ω 1 Ω 2 R f L f C f Filter DC motor V Cf F r Ν = Ω 1 /Ω 2 J c V m D T DC-DC converter I H E I m C H ,α Ω m Ω 1 Ω 2 R f L f C f Filter DC motor V Cf F r Ν = Ω 1 /Ω 2 J c V m D T DC-DC converter I H
m em m m I K T K E = Ω = (eq. 2)
The motor is coupled with a mechanical load through a reducer. The associated causal BG with integral (physical) causality is represented by Fig. 5. For example, the causal analysis of the input filter shows that the inductance L f imposes a common current (junction 1) in the E, R f , L f branch, while the capacitor (C f ) imposes its effort (voltage) to other elements placed in parallel (junction 0).

II. BOND GRAPH BASED SYSTEM ANALYSIS METHODS

Several analysis can be directly applied on BGs :

Firstly, structural analysis as model order, observability and commandability, can be deduced from BGs [START_REF] Dauphin-Tanguy | Les Bond Graphs[END_REF]. Secondly, mathematical models such as transfer function and state equations can be directly derived from causal BGs [START_REF] Karnopp | System Dynamics : Modelling and Simulation of Mechatronic Systems[END_REF]. The model modes can then be determined. By analysing these modes associated with the parameters values, stability analysis or coupling analysis can be characterised.

Thirdly, several model simplification methods can be applied directly on BGs. One can speak about the Singular Perturbations Method (SPM) [START_REF] Sueur | Bond Graph Approach to Multi-time Scale Systems Analysis[END_REF][9-10], which is based on the element dynamics, and the Model Order Reduction Algorithm (MORA) based on the energetic transfers [7-8][10-12]. Finally, by using the concept of bicausality [START_REF] Gawthrop | Bicausal Bond Graph[END_REF], the inverse BG model can be determined to synthesize the constraints with respect to requirements.

In our research, we have mainly considered the issue of model simplification [START_REF] Gandanegara | Bond Graph Multi-time Scale Analysis of a Railway Traction System[END_REF][START_REF] Gandanegara | Modeling and Multi-time Scale Analysis of Railway Traction Systems Using Bond Graphs[END_REF][START_REF] Gandanegara | One Model for One Frequency Range : Comparison of Bond Graph Based Simplification Methods[END_REF] even if this paper is only focused on the stability analysis.

II.1. Bond Graph based Method for Local Stability Analysis

Analysing the system stability is of prime importance and the stability domain must be characterised to avoid risks of system damage. Being generally non linear, the system cannot be analysed on the whole range of parameters space. Thus, a linearised model around operating point has to be derived. In fact, all the variables of a non linear model can be written as :

X = X + ∆X U = U + ∆U (eq. 3)
where X and U represent respectively the values of state and input vectors at the operating point, while X ∆ and U ∆ are respectively their small variations.

Classically, the small signal model can be derived from the state equations. But this linearisation can also be directly applied on the BG by determining the linearised BG as presented in [START_REF] Gandanegara | Methodologie de conception systémique en genie Electrique à l'aide de l'outil Bond Graph : Application à une chaîne de traction ferroviaire[END_REF] [START_REF] Karnopp | Power and Energy in Linearised Physical Systems[END_REF]. Several types of non linearities can exist :

-Non linear characteristics of passive (R, C, I) or active (Se, Sf) elements : for example, if an R dissipative element involves a non linear : -Non linear variation of an element modulus or of modulated gain for a GY (gyrator) or TF (transformer) junction :

Example of a non linear I element (integral causality) :

Non linear Linearised ( )

β Ψ I : e 1 f 1 ∆e 1 0 MSf : ∆f 1 ( ) β Ψ I : ( ) β β β β ∆ ∂ Ψ ∂ Ψ - . . . 2 1 p ( ) 1 1 1 . : p f β - Ψ = ( ) ( ) β β β β β ∆ ∂ Ψ ∂ Ψ - ∆ Ψ = ∆ - - . . . . : 2 1 1 1 1 p p f
Example of a modulated transformer : Non linear Linearised

MTF

.. ( )

β Ψ = m e 1 f 1 e 2 f 2 TF .. ( ) β Ψ = m ∆e 2 ∆f 2 1 0
MSf:

β β β ∆ ∂ Ψ ∂ . . 1 f MSe: β β β ∆ ∂ Ψ ∂ - . . 2 e ∆e 1 ∆f 1 ( ) ( ) 1 2 2 1
. :

. :

f f e e β β Ψ = Ψ = ( ) ( ) β β β β β β β β ∆ ∂ Ψ ∂ + ∆ Ψ = ∆ ∆ ∂ Ψ ∂ + ∆ Ψ = ∆ . . . : . . . : 1 1 2 2 2 1 f f f e e e
It can be observed that the linearised elements strongly depend on the causality assignment. Finally, the small signal model only includes small variations on control variables and on system inputs.

II.2. Example

To illustrate this method, we take the example of the DC traction system previously presented in Section 0. The following linearised BG is derived from the causal BG of Fig. 5. The small signal state equations can be deduced from this BG. The stability analysis of the open loop system can then be performed directly by analysing the root locus obtained from the linearised state equation.

In fact, several modulated inputs (MSf α , MSe α ) are relative to the control variations of the DC-DC chopper (∆α : duty cycle small variations) :

α α α α α α ∆ - = ∆ - = ∆ = ∆ = . . . . 9 7 5 6 m f L p f MSf C q e MSe (eq. 4)
The PI current controller can also be linearised to achieve the stability analysis of the closed loop system. From the controller equation :

( ) ( ) (
)

m ref I m ref P I I K I I K E - + - = & & & 1 α (eq. 5)
The small signal variation of the duty cycle can be derived :

        ∆ + ∆ - ∆ - = ∆ 13 5 5 1 p J K C q q C ET m f f CL α α α & (eq. 6)
by assuming that the current reference is kept constant (

0 = ∆ = ref ref I I &
) and that the controller parameters K P and K I are adjusted to compensate the motor electric pole :

CL m I CL m P T R K T L K = = (eq. 7)
where CL T represent the desired time constant in closed loop.

Finally, (eq. 8) gives the small signal state equation corresponding with the closed loop system : where p 3 , p 9 , p 13 , p 18 and q 5 represent the generalised energy variables respectively associated with the L f , L m , J m , J l and C f elements.

          ∆ - ∆ ∆                     - +                 ∆ ∆ ∆ ∆ ∆                               - - + - - - - - =                 ∆ ∆ ∆ ∆ ∆ ch m f m f c r m r c r m r m m f m m m f f f C E L p C q q p p p p L L J F N J F N J F N J F F L K C J K L R C L R
By using the numerical values, the root locus can be obtained, by considering a given operating point obtained with I ref = 100 A and the motor angular speed Ω m = 250 Rd/s. For example, the influence of the filter inductance L f on the pole locus is presented on Fig. 8. With the zoom, we see that for L f > 9 mH, there are poles in the positive real plan. It indicates that the poles are unstable. As we can see in Fig. 9 this analysis is validated by temporal simulations which also validate the proposed approach.

Let notice that this analysis process can be rather complex to handle, especially as the controlled system becomes complex itself. However, some software tools like ARCHER [START_REF] Azmani | ARCHER: a program for computer aided modelling and analysis[END_REF] provide the state equations from the BG. Furthermore, symbolic calculation tools like Maple, Mathematica or Matlab are useful to derive the linearised state equations of the control unit. In this case study, the root locus has been obtained from Matlab.

III. MODELLING OF THE RAILWAY TRACTION SYSTEM

A BB36000 railway traction system, produced by Alstom, France, is considered [12][16]. In fact, this case study is typical of the stability issues due to the existence of an input filter whose the natural frequency interacts both with the vector control bandwidth and with the resonant frequency of the mechanical transmission line. Simplifying the approach, only a single motor and transmission line is considered as presented on the synoptic of Fig. 19.

III.1. Power feeding

An ideal DC voltage source is considered and represented by an effort source Se : U cont . This source feds an LCR filter to reduce the harmonic currents produced by the traction system and to filter perturbations caused by the power network (see Fig. 12). A three-phase alternating current is provided by a classical PWM voltage source inverter. In this model, each inverter leg is modelled by a modulated transformer whose gain is given by a control signal η i (see Fig. 13). The PWM inverter can be modelled in average value (MTF modulated by the duty cycles) or in instantaneous value (MTF modulated by the conducting state of each leg).

U cont

Se:

U cont V Cf R f L f C f U cont V Cf R f L f C f U cont V Cf R f L f C f V Cf 0 1 U cont C :Cf I : L f R :Rf (a) (b)
0 MTF MTF MTF V 3 V 2 V1 1/η 1 1/η2 1/η 3 V Cf

III.2. Control unit

A classical Direct Field Oriented Control of the motor is used to independently regulate the rotor flux and the electromagnetic torque. Choosing PI controllers to obtain zero-error at steady state, this control unit is of order 2. The structure of the applied control is shown in Fig. 14. All variables are represented in a Park's reference frame (d,q) oriented along the rotor field.

m L 1         + s K K s K I P I 1 ref Φ sdref I ε sdref V d E ˆsd V + + + - ref m r L p L Φ         + s K K s K I P I 1 sqref I ε sqref V q E ˆsq V + + + - ref T ( )s R L R s r s sr σ + 1 1 d E sd I + - ( )s R L R s r s sr σ + 1 1 q E sq I + - ( )s R L L r r m + 1 r Φ r r m L L p Φ

III.3. Induction motor

Squirrel cage induction motors drive the locomotive. Several BG models can be developed [START_REF] Gandanegara | Bond Graph Multi-time Scale Analysis of a Railway Traction System[END_REF] [START_REF] Gandanegara | Methodologie de conception systémique en genie Electrique à l'aide de l'outil Bond Graph : Application à une chaîne de traction ferroviaire[END_REF], following the considered equivalent circuit or following the chosen reference frame. Different reference frames are illustrated in Fig. 15, where indexes Φ and V are respectively used for the reference frame associated with the rotor flux and the stator voltage vector.

α β Φ r d Φ q Φ d V q V V s ρ δ ϕ

Model A : Induction motor modelled in (α,β) fixed reference frame

To model the induction machine in a fixed reference frame, we have firstly chosen to totalise the leakage inductances on the stator side, (L s , L r , L m ) being respectively the stator, rotor and magnetising cyclic inductances and σ the leakage coefficient :

V s E r ' R s σL s R r ' L m 2 L r Φ r ' Φ s I s I r ' V s E r ' R s σL s R r ' L m 2 L r Φ r ' Φ s I s I r ' r r m r r s m R L L R L L L 2 ' 2 1         = - = σ

Model B : Induction motor model in (d V ,q V ) reference frame linked to the stator voltage

The model previously presented was established in a fixed reference frame which involves alternating waves for electromagnetic variables. As the stability analysis issue is concerned, we have seen (cf. section III) that a small signal model must be set around a given operating point. Thus, when alternating variables are considered, as for an induction motor modelled in the (α,β) fixed reference frame, the small signal linear model cannot be obtained because no operating point can be set, except of zero.

Therefore, an induction motor model established in a rotational reference frame must be considered. Classically, this can be made thanks to the Park's transformation. However, linearising the model including this latter transformation leads to linearise non linear cosine and sine terms which makes the approach more complex. In order to solve this issue, an original model of the induction motor has been set by considering an orientation of the rotating reference frame (d V ,q V ) along the stator voltage vector : V s = V sdV , V sqV = 0. This model depends on 2 inputs : the amplitude of stator voltage V sdV and its pulsation ω s . The first one can be determined from the inverter and its control. The last one can be calculated if we know the stator voltage phase ϕ s . Note that the derivation of the stator pulsation (ω s ) limits the utilisation of this model. Indeed, an instantaneous model of the inverter does not allow derivation of the phase angle which changes brutally. Thus, only an inverter modelled in average value can be associated with this particular model of the machine.

The interest of this modelling is that the inverter can be represented by only one modulated transformer (see Fig. 17) whose the gain η d is calculated as shown in Table 2. The input current of this converter is then the consequence of the power balance :

sdV d c I I . η = .
The associated bond graph of the induction machine modelled in this reference frame is displayed in Fig. 18.

Stator voltage PWM inverter model

Modelling in (α,β) reference frame Modelling in (d,q) reference frame associated with the stator voltage vector

Cf Cf Cf V V V V V V 3 1 3 1 3 2 3 1 3 1 3 2 3 1 3 1 3 2 2 1 3 1 3 2 1 1 3 2 1 1       - - =       - - =       - - = α α α α α α α α α ( ) ( ) Cf s Cf s V V V V V V V V V . 2 1 . 2 1 2 1 2 1 . 3 2 2 1 2 1 . 3 2 3 2 3 2 3 2 1 3 2 1 α α α α α β α - = - =       - - =       - - = ( ) ( ) ( ) Cf d Cf s s sd V V V V V . . . 3 1 2 3 2

III.4. Mechanical transmission line

The mechanical transmission line is constituted of 2 couplings. The motor inertia, followed by a first coupling on the primary shaft supplies a mobile reducer which is fixed on the locomotive body through a track link. At the reducer output, another coupling element, namely Jacquemin, is present before the wheel inertia. A complete description of the mechanical transmission line can be found in more details in [START_REF] Gandanegara | Modeling and Multi-time Scale Analysis of Railway Traction Systems Using Bond Graphs[END_REF] [START_REF] Lochot | High speed railway traction system modelling for simulating electromechanical interactions[END_REF]. A reduced BG model can be obtained for the low frequencies [START_REF] Gandanegara | Bond Graph Multi-time Scale Analysis of a Railway Traction System[END_REF][START_REF] Gandanegara | Modeling and Multi-time Scale Analysis of Railway Traction Systems Using Bond Graphs[END_REF]. The synoptic of this line is presented in Fig. 19. The associated BG model is displayed in Fig. 20. In our modelling, we do not consider the wheel-rail contact which is modelled without sliding. With this hypothesis, the model is of 11 th order.

III.5. Validations by simulations

We validate our models by simulations. In particular, the two models of the induction machine are compared :

Model A is the one with an induction motor modelled in the (α,β) fixed reference frame with leakage totalised on the stator side, Model B, is the one modelled in the rotating reference frame linked to the voltage (d V ,q V ).

For all models, 2 different cases are examined : a normal operating mode (system starting), a degraded operating mode obtained by short-circuiting one leg of the inverter.

Every model is simulated with the PWM inverter modelled in average value because the second model (B) is not valid for instantaneous operations. Fig. 21 and Fig. 22 show that all models have similar responses in a normal and a degraded operating mode which validates the original approach proposed for Model B.

IV. STABILITY ANALYSIS OF THE RAILWAY TRACTION MODELS

IV.1. BG based stability analysis procedure

We apply the stability analysis procedure previously presented in Section II. We have explained in Section III.3 that the models of the induction motor in the (α,β) reference frame can not be linearised. Therefore, we consider the induction motor modelled in the (d V ,q V ) reference frame linked to the voltage vector for the stability analysis of the railway traction system. To simplify the analysis, the mechanical part is here represented only by an inertia J m (equivalent to the I 6 ), a friction f and a load torque T l .

st step : Small signal BG derivation

As for the example of the DC traction system (see section II) the linearised BG of the railway traction system can be directly derived from the causal BG (see Fig. 23).

Se : ' 8

Control inputs

The inputs of this linearised (small signal) BG are relative to the control unit (i.e. ∆η d , ∆ω s ).

nd step : Stability analysis of the open loop system

The stability of the open loop system can be analysed from that small signal BG by deducing the state equations. This can be made by means of the ARCHER software. When a simplified mechanical system is considered only including an inertia, a viscous friction and a load torque, the open loop system is of order 7. The state vector is then composed of :

[ ] T rqV rdV sqV sdV Cf Lf I I V I ∆Ω ∆Φ ∆Φ ∆ ∆ ∆ ∆ = ∆X (eq. 9)
Finally, the analysis of the root locus allows to determine the stability domain.

rd step : Stability analysis of the closed loop system

However, for such systems, the control bandwidth strongly influences the stability. Thus, closed loop operation must be considered by including the control unit in the analysis as presented in the example of the DC traction system (see section III). For that purpose, the control outputs (∆η d , ∆ω s ) have to be calculated from the control equations.

-Calculation of

d η ∆ : 2 . Cf Cf sdV Cf sdV Cf sdV d V V V V V V V ∆ - ∆ =         ∆ = ∆η (eq. 10)
The motor input voltage is defined as :

2 2 Φ Φ + = sqref sdref sdV V V V (eq. 11)
The linearisation of this voltage then leads to :

( ) Φ Φ Φ Φ ∆ + ∆ = ∆ sqref sqref sdref sdref sdV sdV V V V V V V . . 1 (eq. 12)
Thus, the small signal state equations can be established as (eq. 13). The inputs of this latter model are (∆U cont , ∆V sdref Φ , ∆V sqrefΦ , ∆ω s ). The control inputs (∆V sdrefΦ , ∆V sqrefΦ , ∆ω s ) can also be developed. In our case study, the field oriented control strategy involves control variables operating in another (d Φ ,q Φ ) reference frame linked to the rotor field. A classical strategy of rotor flux oriented control presented on Fig. 14 is considered. However, in order to simplify the complex development leading to the linearised control, we have neglected the electromotive forces (E d and E q ) which decouple the current controllers (see Fig. 14). Then, the control state equations can be expressed as (eq. 14), where T ref and Φ ref represent the reference values of the electromagnetic torque and the rotor flux, and the Φ r term is defined as By using autopiloting equation, the pulsation ω ρ can be formulated as : The angle δ * can be calculated from (eq. 17).

2 2 rqV rdV r Φ + Φ = Φ . ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )
        ∆ - ∆Ω - ∆Φ - ∆ Φ - ∆Φ + ∆ Φ = ∆Ω Ω - ∆Φ - ∆Ω - ∆ Φ - ∆Φ - ∆ = ∆Φ Ω - ∆Φ + ∆Ω - ∆ Φ + ∆Φ - ∆ = ∆Φ               Ω ∆Φ - ∆Ω Φ - ∆ - ∆ - ∆Φ + ∆ - = ∆               Ω ∆Φ + ∆Ω Φ + ∆ + ∆ + ∆Φ + ∆ - ∆ + ∆ = ∆                 ∆ + ∆ - ∆ + ∆ - ∆ = ∆ ∆ + ∆ - ∆ - = ∆ Φ Φ Φ Φ Φ Φ Φ Φ
I L I L R L L I R L I dt d L L p L L p I L I L R L L I R V V V V V L I dt d V V V V V V I V V I V I V V I C V dt d U V I R L I
( ) ( ) ( )         + Φ Φ -         - Φ =         - Φ +         - Φ = -         - Φ =         - Φ +         - Φ = Φ Φ Φ Φ Φ Φ Φ Φ Φ Φ sq r
        = Φ Φ sdref sqref V V arctan * δ (eq. 17)
Its derivation, the * δ ω term, can be defined as :

( ) ( ) 2 2 * Φ Φ Φ Φ Φ Φ + - = sqref sdref sdref sqref sqref sdref V V V dt d V V dt d V δ ω (eq. 18)
By using (eq. 15), (eq. 16) and (eq. 18), we obtain the angular velocity ω s . The variation of this pulsation can then be deduced.

The complex linearisation of these expressions is detailed in [START_REF] Gandanegara | Methodologie de conception systémique en genie Electrique à l'aide de l'outil Bond Graph : Application à une chaîne de traction ferroviaire[END_REF]. It allows to enhance the order of the state equation (9 th order) as :

[ ] T sqref sdref rqV rdV sqV sdV Cf Lf V V I I V I Φ Φ ∆ ∆ ∆Ω ∆Φ ∆Φ ∆ ∆ ∆ ∆ = ∆X (eq. 19)
This small signal model depends on the physical system parameters but also on the control requirement through the controller parameters (K P and K I ).

By means of the Matlab © software, the stability domain can be characterised by analyzing the root locus of the closed loop system linearised around an operating point defined by the reference parameters (T ref , Φ ref ) and of the load (T l ).

In the following simulations, the rated operating point is defined by : T ref = 5 kNm, Φ ref =6 Wb et T l = 4998 Nm, which sets the motor angular speed at 20 rad/s.

IV.2. Analysis results of the railway traction system stability

Influence of the filter capacitor value C f

We have firstly investigated the stability of the operating point as a function of the filter capacitor value C f which varies here between 1 and 100 mF. Fig. 24 presents the poles locus. The arrows show the poles propagation direction when the C f value increases. For this particular operating point (T ref = 5 kNm, Ω = 20 Rd/s, Power = 100 kW), it can be seen that the model is unstable for C f < 1.3 mF.

Influence of the control bandwidth

We examine the influence of this parameter value by setting the closed loop time constant from T CL = 1 ms to T C L = 100 ms. In this range, and for the rated filter capacitor of 17mF, we do not find unstable zones. However, reducing this latter parameters or varying the rotation speed could lead to unstability.

Influence of the mechanical angular speed Ω

The investigated range of this latter parameter is between 0 and 100 Rd/s. For a rated value of the filter capacitor (C f = 17 mF), the model is always stable. However, when we use a reduced value of filter capacitor (C f = 3 mF), there is an unstable doma in when Ω > 51 Rd/s.

IV.3. Validation of the analysis procedure

In this section, we verify the stability analysis procedure by simulating the non linear BG model of the traction system. A reduced value of the filter capacitor (C f = 3 mF) is set. Four different states are simulated (see Fig. 27) We present in Fig. 27 the simulation results for the motor mechanical angular speed Ω = 60 Rd/s. These figures show the instability where oscillation variables are amplified. For the mechanical speed of Ω = 55 Rd/s, it can be seen from the zoom on the capacitor voltage that an unstable behaviour is obtained. The system is stable for Ω = 50 Rd/s. Note that equivalent results have been obtained thanks to the previous stability analysis procedure based on the BG approach, which proves its validity.

For mF 17 = f C , we have verified by simulations that the system is always stable as indicated in the analysis procedure.

V. CONCLUSIONS

In this paper, a homogeneous BG model of a railway traction system has been presented allowing to emphasise the electromechanical couplings. We have mainly focused our attention on a stability analysis procedure that can be directly deduced from the BG model. For that purpose, the BG has to be linearised around an operating point. We have also proposed an original model of the induction motor, represented in the (d V ,q V ) rotating reference frame related to the stator voltage vector. This model allows to avoid the non linear Park's transformation which makes easier to linearise the BG and to obtain a small signal model. The influence of system parameters on the stability has then be investigated and validated by simulations on the non linear model.

This work is a contribution showing how the Bond Graph formalism is useful for modelling and analysing electrical engineering multi-field systems. Indeed, obtaining a homogeneous modelling greatly facilitates the system approach by emphasising couplings in spite of physical fields crossing. More particularly, we have shown in this contribution, how this methodology is convenient for the local stability analysis. Of course, the same kind of analysis could be done from the state model through its linearisation around the same operating point. The Bond Graph formalism can then be seen as a powerful alternative allowing a systematic and structured approach from which the linearised model of an energetic system can be systematically deduced. As the stability analysis of a closed loop controlled system is concerned, a signal part (control part) is associated with the causal Bond Graph (energetic part). The linearisation of the signal part can only be done by means of state equations derivation of the control strategy, which greatly contributes to the complexity of the analysis as it was emphasised on the typical example of a railway traction system.

More generally, this contribution on system stability is a complement of other studies dedicated to model reduction and other issues particularly useful for system design.

Fig. 1 .

 1 Fig. 1. Bond graph power transfer.

Fig. 2 .

 2 Fig. 2. Paynter's tetrahedron.

Fig. 3 .

 3 Fig. 3. Causality assignments.

Fig. 4 .

 4 Fig. 4. DC motor traction system.

Fig. 5 .

 5 Fig. 5. Bond graph of the DC motor traction system.

Fig. 6 .

 6 Fig.6. Linearisation of an R element.

Fig. 7 .

 7 Fig. 7. Linearised BG of the DC traction system..

Fig. 8 .

 8 Fig. 8. Poles analysis : influence of the filter inductance value L f .

Fig. 9 .

 9 Fig. 9. Influence of the filter inductance value L f on the motor current I m and on the motor angular speed Ω m : (a) unstable case (L f = 10 mH) and (b) stable case (L f = 9 mH)

Fig. 10 .

 10 Fig. 10. The BB36000 simplified bloc diagram.

Fig. 11 .

 11 Fig. 11. Bond graph of alimentation source.

Fig. 12 .

 12 Fig. 12. Input filter : (a) electrical circuit and (b) associated bond graph.

Fig. 13 .

 13 Fig. 13. BG model of the voltage source inverter.

Fig. 14 .

 14 Fig. 14. Direct Field Oriented Control.

Fig. 15 .

 15 Fig. 15. Relations between reference frames.

Fig. 16 .

 16 Fig. 16. induction motor model with totalised leakages inductances : (a) equivalent circuit brought to the stator side and (b) associated bond graph.

1 Fig. 17 .Fig. 18 .

 11718 Fig.17. Simple BG of the inverter for the induction motor modelled on the (d V ,q V ) reference frame.

Fig. 19 .CemFig. 20 .

 1920 Fig. 19. Synoptic of the mechanical transmission line.

Fig

  Fig. 21. A starting transient mode.

Fig. 22 .

 22 Fig. 22. A short-circuit of one inverter leg.

  Fig. 23. Linearised BG of the railway traction system On this BG, the elements MSe and MSf are associated with :

:

  The pulsation ω s is the angular velocity of the angle ϕ s , where *

Fig. 24 .

 24 Fig. 24. Influence of the filter capacitor value C f .

  Fig. 25. Influence of the controller time constant value T CL .

Fig. 26 .

 26 Fig. 26. Influence of the motor mechanical angular speed Ω.

Fig. 27 .

 27 Fig. 27. Influence of the motor mechanical angular speed Ω : unstable operating points.

Fig. 28 .

 28 Fig. 28. Tests for : (a) Ω (static) = 55 Rd/s and (b) Ω (static) = 50 Rd/s.

Table 2 .

 2 Stator voltage on the inverter output.

:

  State 1 : the angular speed is null (a null load torque is applied). State 2 : the angular speed increases with an important gradient (first transient state) because we use only one tenth of the train mass to accelerate the simulation. State 3 : it is the second transient state where we use the whole train inertia. State 4 : the desired load is applied to set the operating point at steady state of the speed.

& & & &

THE AUTHORS

Grace Gandanegara received her Ph.D. degree in Control Systems from the Institut National Polytechnique of Toulouse, France, in 2003. She is currently post doctoral researcher at the Laboratory of Electrotechnics and Industrial Electronics (LEEI) of Toulouse. Her research interests include the analysis and system design in electrical engineering with bond graph methods.

Xavier ROBOAM received the PHD Degree in Electrical Engineering from the Institut National Polytechnique of Toulouse, FRANCE in 1991. He has been in the Laboratory of Electrotechnics and Industrial Electronics (LEEI) of Toulouse since 1992 as a full-time researcher. Since 1998, he is head of the team ''SYSTEM'' whose the objective is to process the design problem at a "system level". He develops methodologies specifically oriented towards multi-fields systems design for applications such as electrical embedded systems or renewable energy systems. Bruno Sareni is assistant professor in Electrical Engineering and Control Systems Department at the Institut National Polytechnique of Toulouse, France. He is also researcher at the Laboratory of Electrotechnics and Industrial Electronics (LEEI) of Toulouse. He received his Ph.D. degree in 1999 from the Ecole Centrale de Lyon. His research activities are related to the analysis of complex heterogeneous power devices in electrical engineering with bond graph methods and the optimization of these systems using artificial evolution algorithms. Genevieve Dauphin-Tanguy (senior member IEEE), graduated from University of Lille, France (BSc Physics, BSc Mathematics, MSc Mechanics) and from the french Grande Ecole