Nouha Abid
email: nabid@laas.fr

Silvano Dal

Zilio Didier

Le Botlan
email: dlebotla@laas.fr

A Verified Approach for Checking Real-Time Specification Patterns

Keywords: Model-Checking, Specification Patterns, Time Petri Nets

We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on properties expressed using real-time specification patterns, which can be viewed as a subset of timed temporal logics that includes properties commonly found during the analysis of reactive systems. Our model-checking approach is based on the use of observers in order to transform the verification of timed patterns into the verification of simpler LTL formulas. While the use of observers for model-checking is quite common, our contribution is original in several ways. First, we define a formal framework to verify that our observers are correct and non-intrusive. Second, we define different classes of observers for each pattern and use a pragmatic approach in order to select the most efficient candidate in practice. This approach is implemented in an integrated verification tool chain for the Fiacre language.

Formal Methods. Verification.

INTRODUCTION

distinctive feature of real-time systems is to be subject to severe time constraints that arise from critical interactions between the system and its environment. Since reasoning about real-time systems is difficult, it is important to be able to apply formal validation techniques early during the development process and to define formally the requirements that need to be checked.

In this work, we follow a classical approach to model checking: (1) we use a high-level language to describe a model of the system; (2) we use a logicalbased formalism to express requirements on the system; and (3) the verification consists in compiling the system's model and requirements into a low-level model for which we have the appropriate theory and the convenient tooling. We propose a new treatment for this traditional approach. In particular, for point (2), we focus on a dense real-time model and we use real-time patterns for the specification of the system instead of timed extensions of temporal logic. Our patterns can be interpreted as a real-time extension to the specification patterns of [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification ICSE[END_REF]. Time patterns can be used to express constraints on the timing as well as the order of events, such as the compliance to deadline or minimum time bounds on the delay between events. Concerning verification, point (3), we work with Time Transition Systems (see Sect. 2), an extension of Time Petri Nets with data variables and priorities.

Our first contribution is to propose a decidable verification method for checking real-time patterns on Time Transition Systems (TTS). The method is based on the use of observers and model-checking techniques in order to transform the verification of patterns into the verification of simpler LTL formula. Our observers are proved correct and non-intrusive, meaning that they compute the correct answer and have no impact on the system under observation. This is why we say our approach is verified. The formal framework we have defined is not only useful for proving the validity of formal results but also to check the soundness of optimisation in the implementation.

Our second contribution is to provide a reference implementation for these timed patterns. The complete framework defined in this paper has been integrated into a verification tool chain for Fiacre [START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification in the Topcased Environment ERTS[END_REF], a high-level modelling language that can be compiled to TTS. Fiacre can be used as input language for two verification toolboxes: TINA, the TIme Petri Net Analyzer tool set [START_REF] Berthomieu | The tool TINA-Construction of Abstract State Spaces for Petri Nets and Time Petri Nets Int[END_REF]), and CADP [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. In our tool chain (described in Fig. 1) a Fiacre specification is combined with patterns and compiled into a TTS model using the Frac compiler (the Fiacre language compiler). Then the model can be checked using the TINA toolbox. This is not a toy example. Indeed, 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 critical systems, where it is used as the target of model transformation engines from various languages, such as SDL, BPEL or AADL [START_REF] Berthomieu | Formal Verification of AADL Specifications in the Topcased Environment Int[END_REF]. Therefore, through the connection with Fiacre, we can check timed patterns on many different modelling languages.

Due to space limitations, we only give a partial descriptions of our timed patterns and give only part of our theoretical results. A complete catalogue of timed specification patterns is given in Abid et al. (2011a), while the complete formal framework is defined in a long version of this paper (Abid et al. 2011b).

For the purpose of this work, we focus on a simple deadline pattern, named leadsto , and define different classes of observers that can be used to check this pattern. We define observers for the leadsto patterns that are based on the monitoring of places or transitions. In addition to these two traditional kind of observers, we propose a class of TTS observers that monitor data modifications. The goal is to choose the most efficient observer in practice. We give some experimental results on the impact of the choice of observer on the size of the state graphs that need to be generatedthat is on the space complexity of our verification method-and on the verification time. The goal of this particular study is not to define a method for automatically generating an observer from a pattern. Instead, we define a set of possible observers that are compared in order to choose the best one in practice.

Outline

The paper is organised as follows. We start by introducing our formal framework in Sect. 2. This section is useful to define the notion of composition and non-interference for our observers. In Sect. 3 and 4, we describe a subset of our real-time specification patterns and the verification framework. We describe the implementation of our tool chain and give some experimental results on the use of the leadsto pattern in Sect. 5. We conclude with a review of the related work, an outline of our contributions and some perspectives on future work.

FORMAL FRAMEWORK

We define some formal notations that are used in the remainder of this paper. In our approach, the observers and the systems are presented as [START_REF] Merlin | A study of the recoverability of computing systems[END_REF]) with data variables and priorities. Our formal framework is based on the work of [START_REF] Peres | On the composition of time Petri nets[END_REF], where the authors define formally the composition of two TPN.

s 0 click s 1 [1; 1]
Their presentation has been extended to the full TTS model in Abid et al. (2011b).

The notion of composition is important in our work since we use TTS models for both the system and the observer and, for verification, we use TTS composition to graft the system with the observer.

This section is organised as follows: first, we introduce informally a TTS example. Then, we give a formal definition of TPN following the presentation of [START_REF] Peres | On the composition of time Petri nets[END_REF], which is then extended to TTS. The semantics of TTS is defined using sets of timed traces. Finally, we define the composition of two TTS.

Informal Presentation of the TTS Model

We introduce next a graphical syntax of TTS using a simple example that models the behaviour of a mouse button with double-clicking, as pictured in Fig. 2. The behaviour, in this case, is to emit the event double if there are more than two click events in strictly less than one unit of time (u.t.).

Ignoring at first side conditions and side effects (the pre and act expressions inside dotted rectangles), the TTS in Fig. 2 can be viewed as a TPN with one token in place s 0 as its initial marking. From this "state", a click transition may occur and move the token from s 0 to s 1 . With this marking, the internal transition τ is enabled and will fire after exactly one unit of time, since the token in s 1 is not consumed by any other transition. Meanwhile, the transition labeled click may fire one or more times without removing the token from s 1 , as indicated by the read Data is managed within the act and pre expressions that may be associated to each transition. These expressions may refer to a fixed set of variables that form the store of the TTS. Assume t is a transition with guards act t and pre t . In comparison with a TPN, a transition t in a TTS is enabled if there is both:

(1) enough tokens in the places of its pre-condition; and (2) the predicate pre t is true. With respect to the firing of t, the main difference is that we modify the store by executing the action guard act t . For example, when the token reaches the place s 2 in the TTS of Fig. 2, we use the value of the variable dbl to test whether we should signal a double click or not.

Labeled Time Petri Nets and Time Transition Systems

Labeled Time Petri Nets (or TPN) extend Time Petri Nets [START_REF] Merlin | A study of the recoverability of computing systems[END_REF]) with an action alphabet and a function labelling the transitions with those actions.

Notation : Let I + be the set of nonempty real intervals with non negative rational endpoints. For i ∈ I + , the symbol ↓i denotes the left end-point of the interval i and ↑i its right end-point, if i is bounded, or ∞ otherwise. We use N to denote the set of non negative integers.

Definition 1 A labeled Time Petri Net (or TPN) is a 8-tuple (P, T, B, F, M 0 , I s , , L) in which:

• P is a finite set of places p i ;

• T is a finite set of transitions t i ;

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

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

• M 0 is the initial marking function M 0 : P → N;

• I s is a function called the static interval function I s : T → I + ; Function I s associates a temporal interval I s (t) ∈ I + with every transition of the system. ↓I s (t) and ↑I s (t) are called the static earliest and latest firing times of t, respectively. Assuming that a transition t became enabled at time τ , then t cannot fire before (τ + ↓I s (t)) and no later than (τ + ↑I s (t)) unless disabled by firing some other transition.

•

is a finite set of actions, or labels, not containing the silent action ε;

• L : T → ∪{ε} is a transition labelling function.
A marking is a function M : P → N that records the current (dynamic) value of the places in the net, as transitions are fired. The transition t ∈ T is enabled by M iff (M B(t)). The dynamic interval function I : T → I + is a mapping from transitions to time intervals. The dynamic interval function is used to record the current timing constraints associated to each transition, as time passes.

A transition t can fire from (M, I) if t is enabled at M and instantly fireable, that is 0 ∈ I(t). In the target state, the transitions that remained enabled while t is fired (t excluded) keep their time interval, the intervals of the others (newly enabled) transitions are set to their respective static intervals. Together with those "discrete" transitions, a time Petri Net adds the ability to model the flowing of time. A transition of amount d (i.e. taking d time units) is possible iff d is less than ↑I(t) for all enabled transitions t.

The definition of TTS is a natural extension of TPN that takes variables and priorities into account. Details are presented in Abid et al. (2011b).

Definition 2 (Timed traces) A timed trace σ is a possibly infinite sequence of events t ∈ T and duration d with d ∈ R + . Formally, σ is a partial mapping from N to Ṫ = T ∪ {d | d ∈ R + } such that σ(i) is defined whenever σ(j) is defined and i ≤ j.

The domain of σ is written dom σ. If dom σ is finite, the duration of σ, denoted ∆(σ), is the sum of the delays in σ, that is i|σ(i)∈R + σ(i).

The semantics of a TPN (resp. TTS) is the set of its timed traces. (see details in Abid et al. (2011b)).

Composition of TTS and Timed Traces

We study the composition of two TTS and consider the relation between traces of the composed system and traces of both components. This operation is particularly significant in the context of this work, since both the system and the observer are TTS and we use composition to graft the latter to the former. In particular, we are interested in conditions ensuring that the behaviour of the observer does not interfere with the behaviour of the observed system.

The "parallel composition" of labeled Petri nets is a fundamental operation that is used to model large systems by incrementally combining smaller nets. Basically, the composition of two labeled TPN N 1 and N 2 is a labeled net N def =(N 1 N 2 ) such that: the places of N is the cartesian product of the places of N 1 and N 2 , and the transitions of N is the fusion of the transitions in N 1 and N 2 that have the same label. A formal definition for the composition of two TPN is given in [START_REF] Peres | On the composition of time Petri nets[END_REF]. Composition of TTS is basically the same (Abid et al. 2011b), with the noticeable restriction that transitions which have priority over other transitions may not be synchronised across components. This is required to ensure the compositionality theorem, which we introduce below.

In the same way, we can define the composition of timed traces as an operation that builds a timed trace σ 1 σ 2 from two traces σ 1 and σ 2 . The trace σ 1 σ 2 is obtained by merging the events with the same labels. This operation is well-defined for pairs of composable traces. Let N 1 (resp. N 2 ) be a TPN, and σ 1 (resp. σ 2 ) one of its traces. We say that σ 1 and σ 2 are composable iff dom σ 1 = dom σ 2 , and for all i ∈ dom σ 1 , (1)

σ 1 (i) = d ∧ d ∈ R + ⇒ σ 2 (i) = d, and (2) σ 1 (i) = t ∧ t ∈ T ⇒ L(σ 1 (i)) = L(σ 2 (i)).
The compositionality theorem states that the behaviour of the composed system (expressed as a set of timed traces) is a subset of the behaviour of both components. In other terms, composing a system with an observer cannot generate new behaviour.

Theorem 1 (Compositionality) Let N 1 and N 2 be two TTS and N = N 1 N 2 be their composition. Then, for every timed trace σ of N , there exist two timed traces, σ 1 and σ 2 , such that: (1) σ i is a trace of N i for i ∈ 1.. 2 and(2) σ = σ 1 σ 2 . In the compositionality theorem, the trace σ 1 (resp. σ 2 ) is obtained from σ by "erasing" all transitions of N 2 (resp. N 1 ). Due to lack of space, we omit the proof here and invite the reader to consult Abid et al. (2011b).

REAL-TIME SPECIFICATION PATTERNS

We have defined in Abid et al. (2011a) a set of specification patterns that can express constraints on the delays between the occurrences of two events or on the duration of a given condition. In our context, the event of a model can be: a transition that is fired; the system entering or leaving a state; a change in the value of variables; . . . The advantage of proposing predefined patterns is to provide a simple formalism to non-experts for expressing properties that can be directly checked with our verification tool chain. Our patterns can be viewed as a real-time extension of [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification ICSE[END_REF] specification patterns. 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 the condition defined by 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 unit of time 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. We describe our patterns using a hierarchical classification borrowed from [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification ICSE[END_REF], with patterns arranged in categories such as universality, absence, response, etc. In the following, we give some examples of absence and response patterns based on the TTS example of Fig. 2. Each of these patterns can be checked using our tool chain. A complete catalogue of patterns, with their formal definition, is given in Abid et al. (2011a). In this section, we focus on the "response pattern with delay", to give an example of how patterns can be formally defined and to explain our different classes of observers.

Absence Pattern with Delay

This category of patterns is used to specify delays within which activities must not occur. A typical pattern in this category is:

absent E 2 after E 1 for interval [d 1 ; d 2 ] , (absent)
which asserts that a transition (labeled with) E 2 cannot occur between d 1 and d 2 units of time after the first occurrence of a transition E 1 . An example of use for this pattern would be the requirement that we cannot have two double clicks in less than 2 units of time (u.t.), that is: absent double after double for interval [0; 2]. (This property is not true for our example in Fig. 2.) A more contrived example is to require that if there are no single clicks in the first 10 u.t. of an execution then there should be no double clicks at all. This requirement can be expressed using the composition of two absence patterns using the implication operator and the reserved transition init (that identifies the start of the system): absent single after init for interval [0; 10] ⇒ absent double after init for interval [0; ∞[ .

Response Pattern with Delay

This category of patterns is used to express that some (triggering) event must always be followed by a given (response) event within a fixed delay of time. The typical example of response pattern states that every occurrence of a transition labeled with E 1 must be followed by an occurrence of a transition labeled with E 2 within a time interval I. (We consider the first occurrence of E 2 after E 1 .)

E 1 leadsto E 2 within I . (leadsto)
For example, using a disjunction between transition labels, we can bound the time between a click and a mouse event with the pattern: click leadsto (single ∨ double) within [0, 1].

Other Examples of Patterns

To give a feel of the expressiveness of our patterns, we briefly describe some other examples. For each pattern, we give just a textual definition. In each example, E 1 , E 2 and E 3 refer to events in the system and d 1 (resp. d 2 ) stand for the left end-point (resp. right end-point) of the time interval I.

Present Before the first occurrence of E 3 , each occurrence of E 1 is followed by an occurrence of E 2 which occurs both before E 3 , and in the time interval I after E 1 .

The pattern holds if E 3 never occurs.

E 1 leadsto first E 2 within I after E 3 Same than with the pattern "E 1 leadsto first E 2 within I" but only considering occurrences of E 1 after the first E 3 .

Interpretation of Patterns

We can use different formalisms to define the semantics of patterns. In this work, we focus on a denotational interpretation, based on first-order formulas over timed traces (with equality and trace composition). We illustrate our approach using the pattern E 1 leadsto E 2 within I.

For the "denotational" definition, we say that the pattern E 1 leadsto E 2 within I is true for a TTS N if and only if, for every timed-trace σ of N , we have:

∀σ 1 , σ 2 . (σ = σ 1 E 1 σ 2 ) ⇒ ∃σ 3 , σ 4 . σ 2 = σ 3 E 2 σ 4 ∧∆(σ 3 ) ∈ I ∧ E 2 / ∈ σ 3
where ∆(σ 3 ) is the sum of all the duration in σ 3 . The denotational approach is very convenient for a "tool developer" (for instance to prove the soundness of an observer implementing a pattern) since it is selfcontained.

For another example, the denotational definition for the pattern absent E 2 after E 1 for interval I is given by the following condition on the traces σ of a system:

∀σ 1 , σ 2 , σ 3 .(σ = σ 1 E 1 σ 2 E 2 σ 3 ) ∧(E 1 / ∈ σ 1 ) ⇒ (∆(σ 2 ) / ∈ I)
On our complete catalogue of patterns (Abid et al. 2011a), we provide an alternative (equivalent) semantics for patterns based on MTL, a timed extension of linear temporal logic (see e.g. Maler et al. 2006 for a definition of the logic). For instance, for the leadsto pattern, the equivalent MTL formula is E 1 ⇒ ((¬E 2 ) U I E 2 ) , which reads like a LTL formula enriched by a time constraint on the until modality U.

PATTERNS VERIFICATION

We define different types of observers at the TTS level that can be used for the verification of patterns.

It is important to note that we do not give an automatic method to generate observers. Rather, we define a set of observers for each patterns and, after selecting the "most efficient one", we prove that it is correct (see the discussion in Sect. 5). We make use of the whole expressiveness of the TTS model to build observers: synchronous or asynchronous rendez-vous (through places and transitions); shared memory (through data variables); and priorities. We believe that an automatic method for generating the observer, while doable, will be detrimental for the performance of our approach. Moreover, when compared to a "temporal logic" approach, we are in a more favorable situation because we only have to deal with a finite number of patterns.

Observers for the Leadsto Pattern

We focus on the example of the leadsto pattern. We assume that some events of the system are labeled with E 1 and some others with E 2 . We give three examples of observers for the pattern: E 1 leadsto E 2 within [0, max [. The first observer monitors transitions and uses a single place; the second observer monitors places; the third observer monitors shared, boolean variables injected into the system (by means of composition). We define our TTS observers using a classical graphical notation for Petri Nets, where arcs with a black circle denote read arcs, while arcs with a white circle are inhibitor arcs. (These extra categories of arcs can be defined in TTS and are supported in our tool chain.) The use of a data observer is quite new in the context of TTS systems. The results of our experiments seem to show that, in practice, this is the best choice to implement an observer.

Transition Observer

The observer O t , see Fig. 3, uses a place, obs, to record the time since the last transition E 1 occurred.

E 1 error [max , max ] E 2 obs E 1 E 2 Figure 3: Transition Observer: Ot
The place obs in O t is emptied if a transition labeled E 2 is fired, otherwise the transition error is fired after max unit of time. The priority arc (dashed arrow) between error and E 2 is used to observe the transition error even in the case where a transition E 2 occurs exactly max u.t. after the place obs was filled.

By definition of the TTS composition operator, the composition of the observer O t with the system N duplicates each transitions in N that is labeled E 1 : one copy can fire if obs is empty-as a result of the inhibitor arc-while the other can fire only if the place is full. As a consequence, in the TTS N O t , the transition error can fire if and only if the place obs stays full-there has been an instance of E 1 but not of E 2 -for a duration of max . Then, to prove that N satisfies the leadsto pattern, it is enough to check that the system N O t cannot fire the transition error. This can be done by checking the LTL formula (¬error) on the system N O t .

The observer O t given in Fig. 3 is deterministic and will "react" to the first occurrence of E 2 that miss a deadline. It is also possible to define a non-deterministic observer, such that some occurrences of E 1 or E 2 may be disregarded. This approach is safe since model-checking performs an exhaustive exploration of the states of the system; it considers all possible scenarios. This non-deterministic behaviour is quite close to the treatment obtained when compiling an (untimed) LTL formula "equivalent" to the leadsto pattern, namely (E 1 ⇒ ♦E 2 ), into a B üchi automaton [START_REF] Gastin | Fast LTL to B üchi Automata Translation[END_REF]. We have implemented the deterministic and non-deterministic observers and compared them taking in account their impact on the size of the state graphs that need to be generated and on the verification time. Experiments have shown that the deterministic observer is more efficient, which underlines the benefit of singling out the best possible observer and looking for specific optimisation.

Data Observer

We define the data observer O d in Fig. 4. The data observer has a transition error conditioned by the value of a boolean variable, flag, that "takes the role" of the place obs in O t (every boolean variable is considered to be initially set to false). Indeed, flag is true between an occurrence of E 1 and the following transition E 2 . Therefore, like in the previous case, to check if a system N satisfies the pattern, it is enough to check the reachability of the event error. Notice that the whole state of the data observer is encoded in its store, since the underlying net has no place.

Place Observer

We define the place observer O p in Fig. 5. In this section, to simplify the presentation, we assume that the events E 1 and E 2 are associated to the system entering some given states S 1 and S 2 . (But we can easily adapt this net to observe events associated to transitions in the system.) We also rely on a composition operator that composes TTS through their places instead of their transitions [START_REF] Peres | On the composition of time Petri nets[END_REF] and that is available in our tool chain. In O p , we use a transition labeled τ 1 whenever a token is placed in S 1 and a transition τ 2 for observing that the system is in state S 2 (we assume that the labels τ 1 and τ 2 are fresh-private to the observerand should not be composed with the observed systems). The remaining component of O p is just like the transition observer. We consider both a place and a transition observer since, depending on the kind of events that are monitored, one variant may be more efficient than the other.

S 1 [0, 0] τ 1 obs error [max, max] [0, 0] τ 2 S 2

Proving Innocuousness and Soundness of Observers

The goal of this section is to show how to prove that an observer for a pattern is correct. We demonstrate our approach on the particular examples of observers for the pattern E 1 leadsto E 2 within [0, max[, given in the previous section.

We say that an observer O for this pattern is sound if it can "detect" the traces of a system N that do not hold for the pattern. More formally, if there is a trace σ of N such that:

σ = σ 1 E 1 σ 2 E 2 σ 3 with ∆(σ 2 ) ≥ max and E 2 /
∈ σ 2 , then there should be a trace σ in N O such that error ∈ σ . (The condition on the trace σ directly follows from the denotational definition of the pattern, see Sect. 3.4) On the opposite, the observer is correct if it can detect that a system satisfies a pattern: if for all trace σ of N O we have error / ∈ σ then for all trace σ of N the pattern holds.

From our compositionality theorem, see Sect. 2.3, we have that every trace σ of N O can be defined as the composition σ σ o of a trace σ of the system N with a trace σ o of the observer O. Therefore, to prove that an observer is correct, it is enough to prove that the pattern does not hold for a trace σ o in O iff error ∈ s o . Indeed, if there is a trace σ in N that does not hold for the pattern, then we obtain a trace σ σ o in N O that does not hold either.

We can use our formal framework to prove the soundness of an observer (work is currently under way to mechanise these proofs using the Coq interactive theorem prover). Correctness proofs are more complicated, since they require to reason on the traces of a system composed with the observer to figure out the behaviour of the system alone. Therefore, instead of proving that an observer is correct, we prove a stronger assumption, that is that observers should be innocuous. A net is said to be innocuous if it cannot interfere with a system placed in parallel. More formally, the TTS O is innocuous if for all TTS N and for all trace σ in N there exists a trace σ o in O such that σ σ o is a trace in N O. Innocuousness means that the observer cannot restrict the behaviour of another system. This is particularly useful in our case since, with innocuous observer, any trace σ of the observed system N is preserved in the composed system N O: the observer does not obstruct the behaviour of the system (see Lemma 1 below).

Instead of proving that observers are non-intrusive in a case by case basis, we can give a set of sufficient conditions for an observer O to be innocuous. These conditions are met by the three observers given in Fig. 345.

Given a TTS N , we say that a transition t of the observer is synchronised when there exists a labeled transition t of N such that L(t) = L(t ) (and the label L(t) is not ). We write T sync the set of synchronised transitions of the observer and L sync the labels of the synchronised transitions. The transitions in T sync are the transitions used by the observer to probe the system. In the examples defined in the previous section, the only synchronised transitions are the ones labeled E 1 and E 2 in the data (O d ) and transition (O t ) observers. We define T imm as the set of transitions of the observer whose static time interval is [0, 0]. By construction, no transiton in T sync can also be part of T imm .

Lemma 1 Assume O satisfies the following three conditions:

• all synchronised transitions have a trivial static time interval and no priority (that is, for every t in T sync , I t s = [0; +∞[ and t has no priority over another transition in O);

• from any state of the observer, and for every label l ∈ L sync , there is at least one transition t in O with label l that can fire immediately;

• from any state of the observer, there is no infinite sequence of transitions in T imm .

then, for all timed trace σ in N there exists a timed trace

σ σ o in N O such that σ o is a trace of O.
The proof of Lemma 1 can be found in Abid et al. (2011b). A few comments on these conditions. The first condition is necessary for defining the composition of two TTS (see Sect. 2.3). The second condition ensures that the observer cannot delay the firing of a synchronised transition "for a non-zero time". Assume s is a state of the observer O and σ a finite trace of O starting from state s. We define O(s, σ) to be the (necessarily unique) state reached by the observer after trace σ has been executed. From the second condition, in every reachable state s of O, and for every label l in L(T sync ), there exists a (possibly empty) finite trace σ not containing transitions in T sync such that the duration of σ is 0 and there exists t ∈ T sync with L(t) = l, which is fireable in state O(s, σ). Note also that the observer cannot involve other synchronised transitions while reaching a state where l is firable, since this would abusively constrain the behaviour of the main system N , not to mention deadlock issues. This condition is true for the observer O t in Fig. 3 since, at any time, exactly one of the two transitions labeled E 1 (resp. E 2 ) can fire.

EXPERIMENTAL RESULTS

Our verification framework has been integrated into a prototype extension of frac, the Fiacre compiler for the TINA toolbox. This extension supports the addition of real time patterns and automatically compose a system with the necessary observers. (Software and examples are available at http://homepages.laas.fr/ ~nabid.) 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 two programs provided in the TINA tool set, nd and play. The first program is a graphical animator for Time Petri Net, while the latter is an interactive (textbased) animator for the full TTS model.

We define the empirical complexity of an observer as its impact on the augmentation of the state space size of the observed system. For a system S, we define size(S) as the size (in bytes) of the State Class Graph (SCG) [START_REF] Berthomieu | The tool TINA-Construction of Abstract State Spaces for Petri Nets and Time Petri Nets Int[END_REF]) of S generated by our verification tools. In TINA, we use SCG as an abstraction of the state space of a TTS. State class graphs exhibit good properties: an SCG preserves the set of discrete traces-and therefore preserves the validation of LTL properties-and the SCG of S is finite if the Petri Net associated with S is bounded and if the set of values generated from S is finite. We cannot use the "plain" labeled transition system associated to S to define the size of S; indeed, this transition graph maybe infinite since we work with a dense time model and we have to take into account the passing of time.

The size of S is a good indicator of the memory footprint and the computation time needed for model-checking the system S: the time and space complexity of the model-checking problem is proportional to size(S). Building on this definition, we say that the complexity of an observer O applied to the system S, denoted C O (S), is the quotient between the size of (S O) and the size of S.

We resort to an empirical measure for the complexity since we cannot give an analytical definition of C O outside of the simplest cases. However, we can give some simple bounds on the function C O . First of all, since our observers should be non-intrusive, we can show that the SCG of S is a sub graph of the SCG of S O, and therefore C O (S) ≥ 1. Also, in the case of the leadsto pattern, the transitions and places-based observers add exactly one place to the net associated to S. In this case, we can show that the complexity of these two observers is always less than 2; we can at most double the size of the system. We can prove a similar upper bound for the leadsto observer based on data. While the three observers have the same (theoretical) worstcase complexity, our experiments have shown that one approach was superior to the others. We are not aware of previous work on using experimental criteria to select the best observer for a real-time property. In the context of "untimed properties", this approach may be compared to the problem of optimising the generation of B üchi Automata from LTL formulas, see e.g. [START_REF] Gastin | Fast LTL to B üchi Automata Translation[END_REF].

We have used our prototype compiler to experiment with different implementations for the observers. The goal is to find the most efficient observer "in practice", that is the observer with the lowest complexity. To this end, we have compared the complexity of different implementations on a fixed set of representative examples and for a specific set of properties (we consider both valid and invalid properties). The results for the leadsto pattern are displayed in Fig. 6. For the experiments used in this paper, we use three examples of systems selected because they exhibit very different features (size of the state space, amount of concurrency and symmetry in the system, . . . ):

• TRAIN is a model of a train gate controller.

The example models a system responsible for controlling the barriers protecting a railroad crossing gate. When a train approaches, the barrier must be lowered and then raised after the train's departure. The valid property, for the TRAIN example, states that the delay between raising and lowering a barrier does not exceed 100 unit of time. For the invalid property, we use the same requirement, but shortening the delay to 75.

• APOTA is an industrial use case that models the dynamic architecture for a network protocol in charge of data communications between an air plane and ground stations [START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF]. This example has been obtained using an translation from AADL to Fiacre. In this case, timing constraints arise from timeouts between requests and periods of the tasks involved in the protocol implementation.

The property, in this case, is related to the worst-case execution time for the main application task.

• CAR is a system modelling an automated rail car system taken from [START_REF] Dong | Timed automata patterns[END_REF]. The system is composed of four terminals connected by rail tracks in a cyclic network. Several rail cars, operated from a central control center, are available to transport passengers between terminals. When a car approaches its destination, it sends a request to the terminal to signal its arrival. Passengers in the terminal can then book a travel in the car. The valid property, for the CAR example, states that a passenger arriving in a terminal, must have a car ready to transport him within 15 unit of time. For the invalid property, we use the same requirement, but shortening the delay to 2 unit of time.

In Fig. 6, we compare the growth in the state space size-that is the value of C o (S)-for the place and data observers defined in Sect. 4.1 and our three running examples. We do not consider the transition observer in these results since the events used in the requirements are all related to a system entering a state (and therefore our benchmark favor the place observer over the transition observer). We use one chart to display the result for patterns that are invalid and another for valid patterns.

In Fig. 7 (page 10), we give results on the total verification time for the APOTA example. The value displayed in the table refer to the time spent generating the complete state space of the system and verifying the property. The row SYSTEM gives the time needed for exploring the complete state space of the system (without adding any observer) while "VALID" and "INVALID" refer to the state space of the system synchronised with data observer and state observer in the case of valid and invalid property respectively.

In our experiments, we have consistently observed that the observer based on data is the best choice; it is the observer giving the minimal execution time in almost all the cases and that seldom gives the worst result. We can explain the efficiency of the data observer by the fact that it adds less transitions than the state observer; which means that it adds less intermediary states to the state space of (N O).

Example

RELATED WORK

Two broad approaches coexist for the definition and verification of real-time properties: (1) real-time extensions of temporal logic [START_REF] Henzinger | It's About Time: Real-Time Logics Reviewed[END_REF]; and (2) observer-based approaches, such as the Context Description Languages (CDL) of Dhaussy et al. [START_REF] Raji | Automating Context Description for Software Formal Verification[END_REF] or approaches based on timed automata (Maler et al. 2006;[START_REF] Aceto | Model Checking via Reachability Testing for Timed Automata[END_REF][START_REF] Aceto | The power of reachability testing for timed automata[END_REF].

Obviously, the logic-based approach provides most of the theoretically well-founded body of works, such as complexity results for different fragments of real-time temporal logics [START_REF] Henzinger | It's About Time: Real-Time Logics Reviewed[END_REF]):

Temporal logic with clock constraints (TPTL); Metric Temporal Logic-with or without interval constrained operators-; Event Clock Logic; etc. The algebraic nature of logic-based approaches make them expressive and enable an accurate formal semantics. However, it may be impossible to express all the necessary requirements inside the same logic fragment if we ask for an efficient model-checking algorithm (with polynomial time complexity). For example, Uppaal [START_REF] Behrmann | A Tutorial on Uppaal[END_REF]) chose a restricted fragment of TCTL with clock variables, while Kronos provide a more expressive framework, but at the cost of a much higher complexity. As a consequence, selecting this approach requires to develop model-checkers for each interesting fragment of these logics-and a way to choose the right tool for every requirement-which may be impractical.

Pattern-based approaches propose a user-friendly syntax that facilitates their adoption by non-experts. However, in the real-time case, most of these approaches lack in theory or use inappropriate definitions. One of our goal is to reverse this situation. In the seminal work of [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification ICSE[END_REF], patterns are defined by translation to formal frameworks, such as LTL and CTL. There is no need to provide a verification approach, in this case, since efficient model-checkers are available for these logics. This work on patterns has been extended to the real-time case. For example, [START_REF] Konrad | Real-time specification patterns[END_REF] extends the patterns language with time constraints and give a mapping from timed pattern to TCTL and MTL, but they do not study the decidability of the verification method (the implementability of their approach). Another related work is (Gruhn et al. 2006), where the authors define observers based on Timed Automata for each pattern. However, they do not provide a formal framework for proving the correctness or the innocuousness of their observers and they have not integrated their approach inside a model-checking tool chain.

Concerning observer-based approaches, [START_REF] Aceto | The power of reachability testing for timed automata[END_REF][START_REF] Aceto | Model Checking via Reachability Testing for Timed Automata[END_REF] use test automata to check properties of reactive systems. The goal is to identify properties on timed automata for which model checking can be reduced to reachability checking. In this framework, verification is limited to safety and bounded liveness properties. In the context of Time Petri Net, a similar approach has been experimented by [START_REF] Toussaint | Time Constraints Verification Methods Based on Time Petri Nets[END_REF], but they propose a less general model for observers and consider only two verification techniques over four kinds of time constraints. [START_REF] Bayse | A passive testing approach based on invariants: application to the WAP[END_REF] propose a method to verify the correctness of their approach formally. However, they do not prove formally all their invariants (patterns in our case).

CONTRIBUTIONS AND PERSPECTIVES

In contrast to these related works, we make the following contributions. We reduce the problem of checking real-time properties to the problem of checking LTL properties on the composition of the system with an observer. We define also a real-time patterns language based on the work of [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification ICSE[END_REF] and inspired from real-case studies. To choose the best way to verify a pattern, we defined, for each pattern, a set of non-intrusive observers.

We are based on a formal framework to verify the correctness of an observer, whether it can interfere with the behaviour of the system under observation.

Our approach has been integrated into 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]. We give several experimental results based on the use of this tool chain in Sect. 5. The fact that we implemented our approach has influenced our definition of the observers. Indeed, another contribution of our work is the use of a pragmatic approach for comparing the effectiveness of different observers for the same property. Our experimental results seem to show that data observers look promising.

We are following several directions for future work. A first goal is to define a new low-level language for observers-adapted from the TTS model-equipped with more powerful optimisation techniques and with easier soundness proofs. On the theoretical side, we are currently looking into the use of mechanised theorem proving techniques to support the validation of observers. On the experimental side, we need to define an improved method to select the best observer. For instance, we would like to provide a tool for the "syntax-directed selection" of observers that would choose (and even adapt) the right observers based on a structural analysis of the target system.

Figure 2 :

 2 Figure 2: The double-click example in TTS

Figure 1 :

 1 Figure 1: The global verification tool chain

Figure 4 :

 4 Figure 4: Data Observer: O d

Figure 5 :

 5 Figure 5: Place Observer: Op

Figure 6 :

 6 Figure 6: Compared complexity of the data and place observers (in percentage of system size growth)-average time for invalid properties (right) and valid properties (left).

Figure 7 :

 7 Figure 7: Total verification time for APOTA (in seconds)

  E 1 after E 2 within I Predicate E 1 must hold between d 1 and d 2 u.t after the first occurrence of E 2 . The pattern is also satisfied if E 2 never holds. Present first E 1 before E 2 within I The first occurrence of E 1 should be between d 1 and d 2 u.t. before the first occurrence of E 2 . The pattern also holds if E 2 never occurs. Starting from the first occurrence when the predicate E 1 holds, it remains true for at least duration D. This pattern makes sense only if E 1 is a predicate on states (that is, on the marking or store); since transitions are instantaneous, they have no duration. Absent E 1 before E 2 for duration D No E 1 can occur less than D u.t. before the first occurrence of E 2 . The pattern holds if there are no occurrence of E 2 .

	Present E 1 lasting D

E 1 leadsto first E 2 within I before E 3


Souad Bezzaoucha

Benoît Marx

Didier Maquin

José Ragot

State and Parameter Estimation for Nonlinear Systems: a Takagi-Sugeno Approach

Keywords: Time-varying nonlinear systems, Takagi-Sugeno models, sector nonlinearity approach, convex polytopic transformation, state and parameter observer, linear matrix inequality

The main contribution of this paper is to propose a systematic approach to observer design for nonlinear Takagi-Sugeno (T-S) time-varying systems. The proposed procedure is based on the sector nonlinearity approach using the convex polytopic transformation. The exact writing of the time-varying nonlinear system as a T-S model allows to provide a state and parameter estimation.

I. INTRODUCTION

The observer design for nonlinear systems can be viewed as the heart of system control and model-based diagnosis [START_REF] Chen | Robust Model Based Fault Diagnosis for Dynamic Systems[END_REF], [START_REF] Basseville | On-board component fault detection and isolation using the statistical local approach[END_REF]. Unfortunately, the introduction of time-varying parameters in the system models, needed to accurately represent the system behaviour, leads to more challenging problems in estimation.

In the present work, a focus is made on the time-varying parameter systems, where the parameter variations are inaccessible (non measurable) and may be used as model faults (acting as disturbances or/and uncertainties). In this case, a conventional observer cannot be used directly, and so called adaptive observers developed for joint state and unknown parameter estimation have to be implemented. Numerous approaches were proposed in order to deal with observer design for nonlinear systems [START_REF] Zhang | Implicit adaptive observers for a class of nonlinear systems[END_REF], [START_REF] Rajamani | Adaptive observer for active automotive suspensions: theory and experiment[END_REF], [START_REF] Besanc ¸on | Remarks on nonlinear adaptive observer design[END_REF], [START_REF] Cho | A systematic approach to adaptive synthesis for nonlinear systems[END_REF]. An efficient way consists in rewriting the original nonlinear system in a simplier form, like the T-S one. Originaly introduced by [START_REF] Takagi | Fuzzy identification of systems and its applications to modeling and control[END_REF], the T-S representation allows to describe the exact nonlinear behaviour of a system, under the condition that its nonlinearities are bounded. This is reasonable as variables of physical systems are real and always bounded. See for example [START_REF] Akhenak | Design of sliding mode unknown input observer for uncertain Takagi-Sugeno model[END_REF], [START_REF] Marx | Design of observers for Takagi-Sugeno descriptor systems with unknown inputs and application to fault diagnosis[END_REF] and the references therein. The T-S formalism is based on a time-varying interpolation between linear submodels. The global model is a convex combination of the r submodels [START_REF] Tanaka | Fuzzy Control Systems Design and Analysis: A Linear Matrix Inequality Approach[END_REF]:

       ẋ(t) = r ∑ i=1 µ i (ξ (t))(A i x(t) + B i u(t)) y(t) = r ∑ i=1 µ i (ξ (t))(C i x(t) + D i u(t)) (1)
where x(t) ∈ R n x is the system state variable, u(t) ∈ R n u is the control input and y(t) ∈ R m is the system output. ξ (t) ∈ R q is the decision variable vector assumed to be either measurable (as the system output), known (as the system input) or unmeasurable (as the system state). The weighting functions µ i (ξ (t)) of the r submodels satisfy the convex sum property

   r ∑ i=1 µ i (ξ (t)) = 1 0 ≤ µ i (ξ (t)) ≤ 1, i = 1, . . . , r (2)
This representation is very interesting in the sense that it simplifies the mathematical manipulation compared to the original nonlinear models. It allows to extend the use of some tools developed in the linear framework to the nonlinear systems, for the stability study, the control design and observer synthesis.

A systematic procedure to transform a nonlinear system by rewriting it into a T-S form, without any loss of information is known as the sector nonlinearity transformation (SNT) [START_REF] Tanaka | Fuzzy Control Systems Design and Analysis: A Linear Matrix Inequality Approach[END_REF], [START_REF] Nagy | Systematic multimodeling methodology applied to an activated sludge reactor model[END_REF]. This transformation advantage is to be analytical and systematic. Based on the nonlinear equations of the original model, a quasi-Linear Parameter Varying (quasi-LPV) is written. The local models of this form are state and control input affine, however, this representation is not unique. Depending on the objectives, many quasi-LPV forms may be obtained [START_REF] Nagy | Systematic multimodeling methodology applied to an activated sludge reactor model[END_REF].

II. PROBLEM STATEMENT: T-S MODELLING OF NONLINEAR TIME-VARYING PARAMETER

A first contribution of this work is to model nonlinear time-varying systems using the T-S representation. For that, each time-varying parameter is rewritten under a particular form.

Let us consider the nonlinear time-varying T-S system represented by equation ( 3) with n parameters θ j (t)

   ẋ(t) = r ∑ i=1 µ i (x(t))(A i (t)x(t) + B i (t)u(t)) y(t) = Cx(t) (3) with          A i (t) = A i + n ∑ j=1 θ j (t)A i j B i (t) = B i + n ∑ j=1 θ j (t)B i j (4)
Remark 1: In (4), it is supposed that the matrices A i (t) and B i (t) depend on the same parameters. However, if a parameter θ j (t) does not affect A i (t) (resp. B i (t)), then the corresponding matrix Āi j (resp. Bi j ) is null. A i , A i j , B i , B i j are known matrices with suitable dimensions. θ j (t) are time-varying parameters. They are nonmeasurable but bounded θ j (t) ∈ [θ 2 j , θ 1 j ]. Each parameter θ j (t) is ex- pressed as:

θ j (t) = µ 1 j (θ j (t))θ 1 j + µ 2 j (θ j (t))θ 2 j (5) with          µ 1 j (θ j (t)) = θ j (t) -θ 2 j θ 1 j -θ 2 j µ 2 j (θ j (t)) = θ 1 j -θ j (t) θ 1 j -θ 2 j (6) µ 1 j (θ j (t)) + µ 2 j (θ j (t)) = 1, ∀t
Replacing ( 5) in (4), it becomes:

A i (t) = A i + n ∑ j=1 2 ∑ k=1 µ k j (θ j (t))θ k j A i j B i (t) = B i + n ∑ j=1 2 ∑ k=1 µ k j (θ j (t))θ k j B i j (7)
In order to have the same weighting functions for all the time-varying matrices A i (t) and B i (t), exploiting the convex sum property of the weighting functions µ 1 j (t) and µ 2 j (t) of each parameter θ j (t), (7) is written as:

                                                         A i (t) = A i + n ∑ j=1 ( µ 1 j (θ j (t))θ 1 j + µ 2 j (θ j (t))θ 2 j )A i j ×    n ∏ k=1 k = j 2 ∑ m=1 µ m k (θ k (t))    = A i + 2 n ∑ j=1 µ j (t)A i j B i (t) = B i + n ∑ j=1 ( µ 1 j (θ j (t))θ 1 j + µ 2 j (θ j (t))θ 2 j )B i j ×    n ∏ k=1 k = j 2 ∑ m=1 µ m k (θ k (t))    = B i + 2 n ∑ j=1 µ j (t)B i j (8) with                  µ j (θ (t)) = n ∏ k=1 µ σ k j k (θ k (t)) A i j = n ∑ k=1 θ σ k j k A ik B i j = n ∑ k=1 θ σ k j k B ik (9)
The indices σ k j equal to 1 or 2, indicate which partition of the k th parameter ( µ k 1 or µ k 2 ) is involved in the j th submodel.

The relation between the submodel number j and the σ k j indices are given by the following equation

j = 2 n-1 σ 1 j + 2 n-2 σ 2 j + . . . + 2 0 σ n j -(2 1 + 2 2 + . . . + 2 n-1 ) (10
) Equation ( 8) presents the advantage to have the same global convex weighting functions for A i (t) and B i (t) (see [START_REF] Bezzaoucha | Linear feedback control input under actuator saturation : A Takagi-Sugeno approach[END_REF] for calculation details). In the following, θ (t) is the vector of components θ j (t), j = 1, . . . , n. Finally, using equations ( 8) and ( 4), (3) becomes:

     ẋ(t) = r ∑ i=1 2 n ∑ j=1 µ i (x(t)) µ j (θ (t))(A i j x(t) + B i j u(t)) y(t) = Cx(t) (11) A i j = A i + A i j B i j = B i + B i j ( 12
)

III. STATE AND TIME-VARYING PARAMETER OBSERVER

Based on the obtained T-S model, a simultaneous state and parameter observer may be designed and implemented. An L 2 attenuation approach will be proposed to minimize the effect of the time-varying parameters on the state and parameter error estimation.

The state and parameter observer is taken as the following

                       ẋ(t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) (A i j x(t) + B i j u(t) + L i j ( ŷ(t) -y(t))) θ (t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) (K i j (y(t) -ŷ(t)) -α i j θ (t)) ŷ(t) = C x(t) (13
) where L i j ∈ R n x ×m , K i j ∈ R n×m and α i j ∈ R n×n are the gains to be determined such that the estimated state and parameter converge to the system state and parameter. Let us define the state estimation error e x (t) as

e x (t) = x(t) -x(t) (14)
Its dynamics cannot be easily computed directly from [START_REF] Zhang | Implicit adaptive observers for a class of nonlinear systems[END_REF] since in equation ( 11) the weighting functions of the state depends on the unmeasurable variables (θ (t) and x(t)).

Because of that, based on the convex sum property of the weighting functions, the state equation ( 11) is rewritten as follow

ẋ(t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t))(A i j x(t) + B i j u(t))+ µ i (x(t)) µ j (θ (t)) -µ i ( x(t)) µ j ( θ (t)) (A i j x(t) + B i j u(t)) (15)
This form allows a better comparison of x(t) with x(t), since µ i ( x(t)) µ j ( θ (t)) not only appears in [START_REF] Tanaka | Fuzzy Control Systems Design and Analysis: A Linear Matrix Inequality Approach[END_REF], but also in (15).

Let us define:

∆A(t) = r ∑ i=1 2 n ∑ j=1 µ i (x(t)) µ j (θ (t)) -µ i ( x(t)) µ j ( θ (t)) A i j = A Σ A (t)E A (16
) and

∆B(t) = r ∑ i=1 2 n ∑ j=1 µ i (x(t)) µ j (θ (t)) -µ i ( x(t)) µ j ( θ (t)) B i j = BΣ B (t)E B (17) with A = A 11 . . . A r2 n , Σ A (t) = diag(δ 11 (t), . . . , δ r2 n (t)), B = B 11 . . . B r2 n , Σ B (t) = diag(δ 11 (t), . . . , δ r2 n (t)), E A = I n x . . . I n x T , E B = I n u . . . I n u T δ i j (t) = µ i (x(t)) µ j (θ (t)) -µ i ( x(t)) µ j ( θ (t))
(18) where diag(A 1 , . . . , A n ) refers to a block diagonal matrix with the square matrices A 1 , . . . , A n on its diagonal. Thanks to property (2), we also have

-1 ≤ δ i j (t) ≤ 1 (19)
which implies from definition (18)

Σ T A (t)Σ A (t) ≤ I, Σ T B (t)Σ B (t) ≤ I (20)
Using ( 16) and (17), the system (15) is then written as an uncertain system given by: 21), ( 13) and ( 14), the dynamics of the state estimation error is given by ėx

ẋ(t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) ((A i j + ∆A(t))x(t) + (B i j + ∆B(t))u(t)) (21) From equations (
(t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) ((A i j -L i j C)e x (t) + ∆A(t)x(t) + ∆B(t)u(t)) (22)
Let us now define the parameter estimation error e θ (t) as

e θ (t) = θ (t) -θ (t) (23)
From equation ( 13), the dynamics of this error is given by

ėθ (t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) θ (t) -K i j Ce x (t) + α i j θ (t) -α i j e θ (t) (24
) Due to the coupling between the errors e θ (t) and e x (t), it is convenient to consider the augmented vectors e a (t) and ω(t)

e a (t) = e x (t) e θ (t) , ω(t) =     x(t) θ (t) θ (t) u(t)     (25)
From ( 22), ( 24) and (25), it follows

ėa (t) = r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) (Φ i j e a (t) + Ψ i j (t)ω(t)) (26) with Φ i j = A i j -L i j C 0 -K i j C -α i j Ψ i j (t) = ∆A(t) 0 0 ∆B(t) 0 α i j I 0 (27)
Considering (26), our objective is to design joint state and parameter observer with a minimal L 2 gain of the transfer from ω(t) to e a (t). The computation of the observer gains is detailed in the next theorem. Theorem 1: exists a joint robust state and parameter observer [START_REF] Tanaka | Fuzzy Control Systems Design and Analysis: A Linear Matrix Inequality Approach[END_REF] for a nonlinear time-varying parameter system (3) with an L 2 gain from ω(t) to e a (t) bounded by β (β > 0) if there exists matrices P 0 = P T 0 > 0,

P 1 = P T 1 > 0, Γ 0 2 , Γ 1 2 , Γ 2 2 , Γ 3
2 > 0, α i j , F i j , R i j and scalars β , λ 1 and λ 2 > 0 solution of the optimization problem (28) under LMI constraints (29) and ( 30) min

P 0 ,P 1 ,R i j ,F i j ,α i j ,λ 1 ,λ 2 ,Γ k 2 β ( 28
) for i = 1, . . . , r and j = 1, 2 n Γ k 2 < β I for k = 0, 1, 2, 3 (29)             Q 11 i j -C T F T i j 0 0 0 0 P 0 A P 0 B * -α i j -α T i j + I n 0 α i j P 1 0 0 0 * * -Γ 0 2 + λ 1 E T A E A 0 0 0 0 0 * * * -Γ 1 2 0 0 0 0 * * * * -Γ 2 2 0 0 0 * * * * * -Γ 3 2 + λ 2 E T B E B 0 0 * * * * * * -λ 1 I 0 * * * * * * 0 -λ 2 I             < 0 (30)
with

Q 11 i j = P 0 A i j + A T i j P 0 -R i j C -C T R T i j + I n x (31)
The observer gains are given by   

L i j = P -1 0 R i j K i j = P -1 1 F i j α i j = P -1 1 α i j (32)
For the proof of theorem 1, the following lemma is used: Lemma 1: Consider two matrices X and Y with appropriate dimensions, a time-varying matrice ∆(t) and a positive scalar ε. The following property is verified

X T ∆ T (t)Y +Y T ∆(t)X ≤ εX T X + ε -1 Y T Y (33) for ∆ T (t)∆(t) ≤ I.
Proof: Let us consider the following quadratic Lyapunov function

V (e a (t)) = e T a (t)Pe a (t), P = P T > 0 (34)
Its time derivative is given by

V (t) = ∑ r i=1 ∑ 2 n j=1 µ i ( x(t)) µ j ( θ (t)) e T a (t)(Φ T i j P + PΦ i j )e a (t) +e T a (t)PΨ i j (t)ω(t) + ω T (t)Ψ T i j (t)Pe a (t) (35)
It is known that a (t) asymptotically converges toward zero when ω = 0 and that the L 2 gain from ω to e a is bounded by β if the following inequality holds

V (t) + e T a (t)e a (t) -ω T (t)Γ 2 ω(t) < 0 (36) with Γ 2 = diag(Γ k 2 ), Γ k 2 < β I, for k = 0, 1, 2, 3 (37)
An adequate choice of Γ 2 allows to attenuate the transfer from some components of ω(t) to e a (t). From ( 35), (36) becomes:

r ∑ i=1 2 n ∑ j=1 µ i ( x(t))µ j ( θ (t)) e a (t
From ( 23), ( 27), ( 37) and ( 39), (38

) holds if r ∑ i=1 2 n ∑ j=1 µ i ( x(t)) µ j ( θ (t)) Q i j + Q(t) + Q T (t) < 0 (40)
with:

Q i j =         Q 11 i j -C T K T i j P 1 0 0 0 0 * -P 1 α i j -α T i j P 1 + I n 0 P 1 α i j P 1 0 * * -Γ 0 2 0 0 0 * * * -Γ 1 2 0 0 * * * * -Γ 2 2 0 * * * * * -Γ 3 2         (41)
Q 11 i j = P 0 A i j + A T i j P 0 -P 0 L i j C -C T L T i j P 0 + I n x ( 42
)
Based on ( 16) and ( 17), the time-varying term of (40) can be expressed as:

Q(t) =         P 0 A 0 0 0 0 0         Σ A (t) 0 0 E A 0 0 0 +         P 0 B 0 0 0 0 0         Σ B (t) 0 0 0 0 0 E B ( 43
)
Using lemma 1 and property (19), there exists positive scalars λ 1 and λ 2 , such that

Q(t) + Q T (t) <         Q 1 0 0 0 0 0 0 0 0 0 0 0 0 0 λ 1 E T A E A 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 λ 2 E T B E B         (44)
with:

Q 1 = λ -1 1 P 0 A A T P 0 + λ -1 2 P 0 BB T P 0 ( 45
)
for i = 1, . . . , r and j = 1, . . . , 2 n . From inequality (44), since µ i ( x(t)) and µ j ( θ (t)) satisfy the convex sum property, with the variable changes (32), the LMI (30) implies (40) and (36). As a consequence, the L 2 -gain of the transfer from ω(t) to e a (t) is bounded by β , which achieves the proof.

IV. NUMERICAL EXAMPLE

In this section, the proposed approach is applied to a biological wastewater treatment plant. A reduced form of an activated sludge reactor model is considered with only the carbon pollution and two state variables. Starting from the nonlinear equations of the system, a T-S representation is given. Modelling errors (function of a time-varying parameter) are considered. The objective is to synthesize an observer in order to simultaneously estimate the states and the varying parameter. The process consists in mixing used waters with a rich mixture of bacteria in order to degrade the organic matter [START_REF] Nagy Kiss | State estimation of two time-scale multiple models. Application to wastewater treatment plant[END_REF]. Under specific assumptions, some simplifications can be made and the nonlinear system can be represented with the following equations [START_REF] Ichalal | Estimation d'état des systèmes non linéaires incertains sous forme multimodèle de type Takagi-Sugeno[END_REF]:

ẋ1 (t) = a(t)x 1 (t)x 2 (t) x 2 (t)+b -x 1 (t)u(t) ẋ2 (t) = -ca(t)x 1 (t)x 2 (t) x 2 (t)+b + (d -x 2 (t))u(t) (46)
with x 1 (t) and x 2 (t), the biomass and substrat concentration respectively. The input u(t) represents the dwell-time in the treatment plant. The output is the biomass concentration (y(t) = x 1 (t)).

It is assumed that there is a error on the parameter a such that:

a(t) = a + ∆a(t) (47)
It can also be written as: x 1 (t)

a(t) = a + θ (t)a, θ (t) ∈ [θ , θ ] (48)
x 2 (t)

x 1 (t) estimate

x 2 (t) estimate In the present paper, a new systematic procedure is presented to deal with the state and parameter estimation for nonlinear time-varying systems. It consists in transforming the original system into a Takagi-Sugeno model, based on the sector nonlinearity approach and the convex polytopic transformation. This transformation has the major interest to exactly represent the system without any loss of informations. Then a state and parameter observer can be designed by minimizing the L 2 gain from the augmented input to the estimation errors. The chosen application example is an activated sludge reactor with modeling uncertainties represented by an unknown time-varying parameter. From the nonlinear equations of the system, a T-S model is derived. The proposed observer is synthetized and the obtained results illustrate its performance.

Fig. 1 .

 1 Fig. 1. System states with and without θ (t)

Fig. 3 .Fig. 4 .

 34 Fig. 3. System states and their estimates

The authors are with Université de Lorraine, CRAN, UMR 7039, 2 avenue de la Forêt de Haye, Vandoeuvre-lès-Nancy Cedex, 54516, France. CNRS, CRAN, UMR 7039, France. firstname.name@univ-lorraine.fr

with a = 0.5, a = 0.4 and θ = -0.230, θ = 0.213. Parameters b, c, d have been identified and set to b = 0.07, c = 0.7 et d = 2.5. From the system nonlinearities, let us consider the following premise variables:

As in the previous sections, using the so-called sector nonlinearity approach, the bounded parameter θ (t) is described by equations ( 5) and [START_REF] Cho | A systematic approach to adaptive synthesis for nonlinear systems[END_REF]. Considering [START_REF] Chen | Robust Model Based Fault Diagnosis for Dynamic Systems[END_REF], the premise variables (49) become:

for i = 1, 2 and a 1 = θ a and a 2 = θ a.

Then, the following quasi-LPV form is obtained:

(51) For the considered simulation, the maximum and minimum values of the premisse variables have been computed:

.3894] and z 22 (t) ∈ [0.0033, 3.0587]. That knowledge allows to deduce a T-S form. Indeed, using the convex polytopic transformation, two partitions for each premise variables are constructed as follows:

with

where the scalars z 1 , z 1 , z 2i and z 2i are defined as

The submodels are defined by the pairs (A i j , B i j ) with i = 1, . . . , 4 and j = 1, 2. Due to the choice of premise variables, all the B i j matrices are equal to B T = 0 d . The matrices A i j are given by:

The T-S model is obtained by an interpolation of the eight previous submodels:

The weighting functions μ j (θ (t)) are calculated from equations [START_REF] Cho | A systematic approach to adaptive synthesis for nonlinear systems[END_REF] and µ i j (z(t)) as the following:

where σ l i represents the l th partition. For example, we have:

Then, from the nonlinear system (46), an equivalent T-S model is obtained and given by (55). As mentioned at the begining of this section, the objective is to synthesize a robust state and parameter observer applying the proposed approach. To illustrate the time-varying parameter effect on the system, figure 1 depicts the states in the nominal case (with a(t) = a) and in the time-varying case (a(t) = a + θ (t)a).

The system input, the state variables and their estimates, the time-varying parameter and its estimate are depicted in the figures 2, 3 and 4 respectively. The initial conditions are x 0 = 0.1 1.5 for the system state and xa (0) = 0.09 2.3 0 for the joint state and parameter estimate.

From the depicted figures, one can conclude on the robustness of the synthetized state observer, since the two states are perfectly estimated as well as the time-varying parameter θ (t).