Keywords: Security voting structure, auctions, small firms. JEL Classification Numbers: D44; G34

This paper endogeneizes the security voting structure in an auction mechanism used to sell a small firm. The design of security voting structure allows the seller to choose between two objectives which are not mutually consistent. If the seller wants to maximize his revenue, he should retain some shares to benefit from the future dividends generated by the acquirer. At the opposite, if he wants to sell his firm to the most efficient candidate, he should sell all the shares.

1

The small firms sale, i.e. those held and managed by a single owner, is not a central theme in corporate finance. However, it is not a marginal practice. The sale can take two forms: a negotiation between the seller and the acquirer or a tender offer which gives the firm to the highest bidder. This paper deals with the latter case. The seller may have two objectives: the maximization of his expected revenue and the allocative efficiency. This latter objective is reached when the firm is sold to the most efficient candidate, i.e. the one who will maximize the firm's value in the future.

Over the two last decades, a specific auction mechanism, the open bid, emerged as a central technic of small firms sales. The open bid is equivalent to a "classic" auction: the seller, as a monopolist, faces some potential acquirers. He has the bargaining power. He decides when to sell, what to sell (shares number) and who may participate in the auction. In practice, two types of auction can be used: ascending auction or first price auction. The ascending auction seems to be the most commonly used.

This paper considers the firm's sale as a transfer of corporate control. Corporation's securities provide the holder with particular claims on the firm's income stream and particular voting rights. These securities can be designed in various ways: one share of a particular class may have a claim to vote which is larger or smaller than its claim to income. The transfer takes place when the acquirer receives more than half of votes. Selling only the votes is prohibited. A potential acquirer must pay for the dividends rights which give voting rights (yielding private benefits). Thus, we have to distinguish between two items for sale: the dividends rights and the control of the firm through the voting rights. Nevertheless, these two items are interdependent because the income stream depends on the identity of the acquirer who has taken control.

In this paper, we show how a seller can take into account the respective impact of voting rights and dividends in bidders valuation. Actually, the choice of the optimal security voting structure reflects the interdependencies between voting rights/private benefits and dividends rights/public benefits. Hence, this optimal structure determines the willingness to pay of the bidder. It changes the relative weight of private and public benefits in the total valuation of the bundle of assets. We argue that from the seller point of view, the optimal structure may sometimes differ from the traditional oneshare-one-vote structure.

The paper is organized as follows. Section 1 presents the model. Unlike [START_REF] Cornelli | Large Shareholders, Private Benefits of Control and Optimal Schemes of Privatization[END_REF] who analyze privatization schemes in the context of optimal auction design, our aim is not to characterize the optimal selling mechanism. Actually, we study a standard auction process, in which we ex-plicitly introduce security voting structure. Following [START_REF] Grossman | One Share-One Vote and the Market for Corporate Control[END_REF], we use it as a tool which allows the seller to screen the candidates. Our model is closed to the [START_REF] At | The Choice of the Voting Structure for Privatizing a Company[END_REF] approach. They study the role of security voting structure when a government wants to privatize a company and faces asymmetric bidders. We depart from these contributions considering that both private and public benefits are private information of the bidders. Section 2 derives the results. We identify the security voting structure which maximizes the expected revenue of the seller. We show that the one share-one vote structure is not always optimal from the seller's standpoint. However, it ensures that the most efficient candidate takes control, i.e. the candidate who will maximize the firm's value in the future. The literature on hostile takeovers has also discussed the role of security voting structure, notably [START_REF] Grossman | One Share-One Vote and the Market for Corporate Control[END_REF] and [START_REF] Harris | Corporate Governance: Voting Rights and Majority Rules[END_REF]. Our results mitigate the superiority of the one share-one vote structure shown by these authors. Section 3 concludes.

The model

The model considers a firm sold through an auction. It is owned by a single risk neutral shareholder. A candidate must obtain at least the fraction α ∈ (0.5, 1] of votes to take control of the firm. Seller may keep a share in the firm, i.e. give up control but not all income claims. Hence, he sells a package Ω of voting and income rights which brings the fraction α of votes. The Ω-security voting structure represents the amount of income rights attached to the voting rights majority. These income claims determine the cost of majority.

We consider two candidates which we shall to refer as r and t. They are risk neutral. This model makes the traditional distinction between security benefits (discounted sum of dividends) denoted by y r and y t under the two managements and the private benefits of control, respectively b r and b t . The private benefits of control refer to benefits the acquirer obtain for himself (See [START_REF] Schleifer | A survey of corporate governance[END_REF] for various examples of private benefits). The security benefits refer to the total market value of the corporation's securities. We assume that r is more efficient than t iff y r > y t . We have to mention that the highest bidder may not be the most efficient candidate because of private benefits. The willingness to pay of a buyer m for the package is:

w m = Ωy m + b m f or m = r, t (1)
We may notice that under one share-one vote structure Ω = α. It implies that under this security voting structure, the seller can not obtain a Ωstructure such that Ω < 0.5. In spirit of [START_REF] Grossman | One Share-One Vote and the Market for Corporate Control[END_REF], the seller may generate such a Ω-structure by creating C classes of shares with C ≥ 2. He specifies the fraction of dividends s c and the fraction of total votes v c , for c ∈ C to which class c is entitled. Let us remark that due to legal restrictions, unbundling votes, i.e. (s c = 0; v c > 0,∀c ∈ C), are ruled out. We assume that (v c , s c , ∀c ∈ C) are common knowledge.

The seller obtains direct revenue from the auction E(S) and indirect revenue from the fraction (1-Ω) of kept. This fraction yields dividends generated by the winner of the auction. Let E(y v ) represents the expected value of dividends under the winner control. The total revenue of the seller is so:

E(S) + (1 -Ω)E(y v ) (2)
We suppose that both public and private benefits are private information. Nevertheless, even in this multidimensional setting, the only relevant private characteristics of the bidders are the total willingness to pay for the package. The two potential acquirers are assumed symmetrical ex-ante. Public benefits of bidder m = t, r are i.i.d over [y, y] with a strictly positive density function f y (.). Similarly, private benefits are drawn independently from the same cumulative distribution function F B (.) on the interval B = [b, b], with density f b (.). The probability density f b (b m ) is non-negative. So, the probability density of the package value is given by the following convolution function with f Ωy (.) the density function of Ωy:

f w (w) = +∞ -∞ f b (b)f Ωy (w -b)db = 1 Ω b b f b (b)f y ( w -b Ω )db (3)
Without loss of generality, we consider that the firm, i.e. the package of securities, is sold through an ascending auction. In our settings, with risk neutral, symmetric bidders and independent private value, every traditional auction mechanism is revenue-equivalent. Therefore, the same results would apply with every auction mechanisms in which the package of securities always goes to the buyer with the highest valuation and any bidder with the lowest-feasible value expects zero surplus.

Firm's sale revenue

In ascending auction, the bidder optimal strategy is to remain active as long as the price is not greater than the willingness to pay and the opponent remains active. So, the expected revenue of the auction corresponds to the expected willingness to pay of the second bidder. The density function of the rank two order statistic is 2f w (.) [1 -F w (.)]. We obtain:

E(S) = Ωy+b Ωy+b 2wf w (w) [1 -F w (w)] dw (4)
Let us consider two pairs (y m , b m ) for m = r, t and assume that Ωy r +b r > Ωy t + b t . The revenue of the auction is S (Ω) = Ωy t + b t i.e.e the willingness to pay of the second bidder. Consider that Ω > Ω, then there are two cases.

If Ω y r + b r > Ω y t + b t then S (Ω ) = Ω y t + b t > S (Ω). If Ω y r + b r < Ω y t + b t then S (Ω ) = Ω y r +b r > S (Ω)
. Hence, whatever the characteristics (y m , b m ) of the two bidders are, we have S (Ω ) > S (Ω). The expected sale revenue E (S) is increasing with respect to Ω. So, it is maximized when Ω = 1. The seller sells all the shares.

The allocative efficiency

In this part, we shall derive the security voting structure which ensures the allocative efficiency. Let 2F w (w)f w (w) be the density function of the better valuation between the two bidders. We can so derive the expected cash flows of the winner. Since w v = Ωy v + b v , we have y v = wv-bv Ω and so:

E(y v ) = 2 Ω 3 Ωy+b Ωy+b b b (w v -b)f b (b)f y ( w v -b Ω )db wv Ωy+b b b f b (b)f y ( w -b Ω )db dw v (5)
Let w v = Ωy v + b v be the willingness to pay of the winner. Let us consider two Ω-structures Ω ∈ (0, 1] and Ω ∈ (0, 1] such that Ω > Ω . By assuming that Ω y r + b r > Ω y t + b t , the winner is (y v |Ω = Ω ) = y r . Under the Ω -structure, there are two cases.

If Ω y r + b r > Ω y t + b t then (y v |Ω = Ω ) = y r = (y v |Ω = Ω ). If Ω y r + b r < Ω y t + b t then (y v |Ω = Ω ) = y t .
From assumptions, Ω y r + b r > Ω y t + b t and Ω > Ω , we deduce that y t = (y v |Ω = Ω ) > y r = (y v |Ω = Ω ). This result holds whatever the characteristics of the two bidders are, i.e. (y m , b m ) for m = r, t.

We may conclude that E (y v ) is increasing with respect to Ω. We derive the following proposition.

Allocative efficiency is maximized under Ω = 1. This result is straightforward. The relative weight of cash flows in total valuation of the shares bundle is increasing with respect to Ω. This tends to minimize the probability of having a less efficient pretender with high private benefits, which defeats a more efficient one with low private benefits.

The maximization of expected total revenue

We have shown that the firm's sale efficiency (the probability of sale to the bidder with high public benefits) is obtained when the seller sells all the shares. This structure minimizes the relative weight of private benefits in the securities valuation and so maximizes efficiency of the sale. In symmetric auction, the bidder with the highest willingness to pay will obtain the firm. Nevertheless, the seller cannot obtain more than the second valuation of the bundle of share. Hence, if the winning bidder is also the most efficient acquirer, then the seller is better off retaining part of the shares. He will so obtain future high dividends. But, as the fraction of shares retained by the seller increases, the probability of selling the firm to the less efficient pretender increases because the relative weight of private benefits in the total valuation is increased. The choice of the security design maximizing the global revenue reflects this trade off.

Hence, in order to benefit from the dividends generated by the winner, the seller has to retain the fraction (1 -Ω) of shares. This fraction implies a negative impact of Ω in the total revenue of the seller. This total revenue may be written:

E (R) = E (S) + (1 -Ω) E (y v )
We cannot exhibit general results. To derive explicitly convolution function, we have to add a further assumption. Actually, the shape of the convolution function is closely related to the comparison of b, b and y, ȳ . Recall that w = Ωy + b. If y ∈ [y, y], Ωy ∈ [Ωy, Ωy], with f Ωy (s) = 1 Ω f y ( s Ω ). If we suppose that y-y < b -b, then Ω(y-y) < b -b ∀Ω ∈ (0, 1] . Technically, this hypothesis involves a constant convolution density function, whatever the choice of Ω. Let us remark that this hypothesis reflects that, even in an independent private value setting (i.e. where y r is statistically independent of y t ), public benefits cannot radically differ between the two potential acquirers. The difference between bidders efficiency has just a marginal effect on the benefits. Nevertheless, private benefits may highly differ. So, we can derive the general density function of the willingness to pay for the bundle of assets:

∀w ∈ [Ωy + b, Ωy + b], f w (w) = f 1 w (w) = 1 Ω w-Ωy b f b (b)f y ( w -b Ω )db (6) ∀w ∈ [Ωy + b, Ωy + b], f w (w) = f 2 w (w) = 1 Ω w-Ωy w-Ωy f b (b)f y ( w -b Ω )db (7) ∀w ∈ [Ωy + b, Ωy + b], f w (w) = f 3 w (w) = 1 Ω b w-Ωy f b (b)f y ( w -b Ω )db (8)
With uniform distribution function and b = 0, we have:

E(R) = 20b 3 + 30b 2 (y -y) + 5b(y -y) 2 (2 -3Ω)Ω + (y -y) 3 Ω 2 (4Ω -3) 60b 2
Maximizing the total revenue gives Ω * , the optimal security structure. We have :

∂E(R) ∂Ω = 2(y -y) 2 b(5 -15Ω) + 3(y -y)Ω(2Ω -1) 60b 2
and:

∂ 2 E(R) ∂Ω 2 = (y -y) 2 -5b + (y -y)(4Ω -1) 10b 2 ≤ 0 ∀Ω ∈ (0, 1]
so, if ∃Ω ∈ (0, 1] such that ∂E(R) ∂Ω = 0 then this is the optimal Ω-structure. We have:

Ω * = 15b + 3(y -y) -9(5b + y -y) 2 -120b(y -y) 12(y -y)
Recall that if Ω * < 0.5, then the seller cannot use only one-share-one-vote structure. He has to issue two classes of shares characterized by different security voting structure. We can exhibit cases where the optimal structure departs from traditional one. Consider the following example: Suppose y = 1050, y = 1000, b = 100, then:

Ω * = 33 - √ 849 12 0, 32186
The optimal structure Ω * which maximizes total revenue, is strictly less than 0.5. It cannot be reached with traditional one share-one vote structure.

This last counterexample allows us to have the following proposition: When the candidates are symmetrical and both private and public benefits are private informations, there exists some cases in which the seller should issue several classes of shares with one at least richer in votes. This structure differs from the efficiency-maximizing structure, which is reached under the one share-one vote structure and the vote rule α = 1. ȳ = y, i.e. no uncertainty on public benefits, yields ∂E(R) ∂Ω = 0. The global revenue of the seller is independent of the security design.

Conclusion

A small firm's seller may have two distinct objectives which are not mutually consistent. He may want to maximize the sale's revenue. But he may want to ensure himself that his firm will be well managed. This paper endogeneizes the security voting structure in an auction mechanism used to sell the firm. Thus, by designing a specific security voting structure, the seller may choose between the two objectives. If the seller wants to maximize his revenue, he should keep some shares. The security voting structure design trades off between sell all the shares and retain some shares to benefit from the future dividends generated by the winner. At the opposite, if he wants to sell his firm to the most efficient candidate, he should sell all the assets.


Martin John Barbetti

Jean-Noel Aubertot

Jay Ram Lamichhane

Ming Pei

Integrated disease management of soilborne pathogen complexes: a complicated but achievable management challenge

à 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.

Integrated disease management of soilborne pathogen complexes -a complicated but achievable management challenge

Martin J. Barbetti 1 , Jean-Noël Aubertot 2 , Jay Ram Lamichhane 2 , Ming Pei You 2 1 School of Agriculture and Environment and UWA Institute of Agriculture, University of Western Australia, WA, 6009, Australia. 2 INRAE, Université Fédérale de Toulouse, UMR AGIR, F-31326 Castanet-Tolosan Cedex, France.

Although soilborne diseases of forage and crop legumes are often considered to be caused by a single oomycete or fungal pathogen, a complex of pathogens are associated to these diseases (Lamichhane et al 2017). However, management of soilborne diseases is generally targeted to a single pathogen (You et al 2017a;2017b). Because each pathogen within a soilborne complex is differentially affected by environment, variety, cultural and chemical control practices, failures of management are frequent. The complexity of soilborne pathogens x environment interactions is highlighted by the multifaceted and contrasting interactions in relation to temperature, moisture, type of soil, nutrition and variety, even for individual pathogens (You and Barbetti 2017a,b;You et al. 2017aYou et al. ,b, 2018)). The unpredictable and everchanging proportions of different pathogens within complexes further challenges their management. Hence, identifying all soilborne pathogens operating within disease complexes remains a prerequisite to their effective management. Management challenges, including chemical control, are illustrated by a recent study showing how fungicides that are effective against single pathogens are ineffective against pathogen complexes (You et al. 2020). Consequently, there is a need to refocus away from reliance on fungicide options in managing soilborne disease complexes. Because no host resistance is available for all pathogens within a complex, You andBarbetti (2017a, 2019) highlight the need for and benefits of manipulating the ecosystem to better manage disease complexes, including crop sequence adaptation with less frequent legumes, adjusting tillage, plant density and crop variety. Although all these help improve productivity and persistence of legume systems adversely affected by soilborne pathogen complexes, a more important added value could be to integrate host tolerance within an integrated disease management framework. Current studies on forage legumes highlight huge potential benefits through such an approach to better manage soilborne disease complexes.

Keywords: forage legumes, crop legumes, soilborne pathogens, pathogen complexes, damping-off, root disease


Jean-Paul Bodeveix
email: bodeveix@irit.fr

Mamoun Filali-Amine

Shuanglong Kan
email: kanshuanglong@outlook.com

A Refinement-based compiler development for synchronous languages

Keywords: synchronous languages, refinement, code generation, semantics, verification cMeta Constraint Pb cMeta_SF

In this paper, we are concerned by the elaboration of generic development steps for the code generation for synchronous languages. Our aim is to provide a correct by construction solution. For that purpose, we adopt a refinement-based approach where proof obligations for each step guarantee properties preservation. We use the Event-B formal method. We start with a big step semantics specified by an Event-B machine. Through a sequence of refinements, expressed as Event-B refinement machines, we end up with a code generation step which implements a small step semantics preserving the properties of the big step semantics.

INTRODUCTION

Our study concerns system development. We are interested by the development of reactive systems. For such systems, for instance, avionic systems and interactive systems, synchronous languages have revealed well suited. From the beginning, synchronous languages have put forward a strong mathematical framework underlying their basic principles: synchrony and deterministic concurrency [START_REF] Benveniste | The synchronous languages 12 years later[END_REF]. Thanks to that, synchronous languages have received a significant audience, especially within the critical embedded systems community where high levels of certification are required. However, one must acknowledge that although significant efforts have been devoted to explain the software architecture for implementing frameworks for the development of such languages and https://doi.org/10.1145/3127041.3127056 even to mechanize them [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Izerrouken | Machine Checked Sequencer for Critical Embedded Code Generator[END_REF][START_REF] Schneider | Proving the Equivalence of Microstep and Macrostep Semantics[END_REF], the production of a certified compiler remains a challenge.

In this paper, we are concerned by the elaboration of generic development steps for the code generation for synchronous languages. Our aim is to provide a correct by construction solution. For that purpose, we adopt a refinement-based approach where proof obligations for each step guarantee the preservation of some classes of properties [START_REF] Derrick | Temporal-logic property preservation under Z refinement[END_REF]. We use the Event-B formal method. We start with a big step semantics specified by an Event-B machine. Through a sequence of refinements, expressed as Event-B refinement machines, we end up with a code generator and an interpreter which implements a small step semantics preserving the properties of the initial big step semantics, i.e. the sequences of reactions observed when executing the concrete machine were allowed by the big step semantics.

The rest of the paper is organized as follows: in the next section, we give an overview of the Event-B language. In Section 3, we present the development of a generic compiler for synchronous languages. Finally, in Sections 4 and 5, we discuss related and future work.

EVENT-B

The Event-B method allows the development of correct by construction systems and software [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF]. To achieve this, it supports natively a formal development process based on a refinement mechanism with mathematical proofs. Figure 1 illustrates a refinement step where a machine M0 using a context C0 (the sees edge) is refined (the refines edge) by a machine M1 using an extension C1 of C0 (the extends edge). Contexts define abstract data types through sets, constants and axioms while machines define symbolic labelled transition systems. The state of a transition system is defined as the value of machine variables. Labelled transitions are defined by events specifying the new value of variables while preserving invariant properties. Proof obligations for wellformedness and invariant preservation are automatically generated by the Rodin tool [18].

They can be discharged thanks to the available automatic proof engines (CVC4, Z3, . . . ) or through human-assisted proofs.

Notations

For the most part, Event B uses standard set theory and its usual set notation. As a matter a fact, in Event-B, an array and a function are both considered as set of couples. Some notations are specific to Event B :

• pair construction: pairs are constructed using the maplet operator →. A pair is thus denoted a → b instead of (a, b).

The set of pairs a → b where a ∈ A and b ∈ B is denoted

A × B. • A subset of A × B is a relation. A relation
→ z | ∃y. y ∈ B ∧ x → y ∈ f ∧ y → z ∈ д}. • domain restriction: D r = {x → y | (x → y) ∈ r ∧x ∈ D} • overwrite: f -д = ((dom( f )\dom(д)) f ) ∪ д.
For instance, such a notation is used to denote a new array obtained by changing the element of an array A at index i: A -{i → e }. • lambda expressions: the usual expression for a lambda expression is: λx . x ∈ T | bdy, where T is a set denoting the "type" of x: here the definition domain and bdy is the body of the lambda expression.

As already said, Event-B machines specify symbolic transitions through events. An event has three optional parts: parameters (any p1 . . . pn), guards (where . . . ) specifying constraints to be satisfied by parameters and state variables, and actions (then . . . ) specifying state variables updates. Guards are defined in set-based predicate logic. Concurrent updates of distinct variables may be deterministic (x := e), non deterministic (x :∈ E or x :| P (x, x )). In x :∈ E, x takes any value belonging to the set E. In x :| P (x, x ), the new value x of x is specified by the predicate P.

Preliminary example

As a preliminary example for section 3.1, Figure 2 illustrates basic labelled transitions systems [START_REF] Arnold | Finite transition systems -semantics of communicating systems[END_REF]. The static description of transition systems is given through the context cLTS. cLTS introduces State and Label as abstract sets. Then, the set of initial states is given through the constant I, and the transition relation through the constant Trans. The description of the dynamics of a transition system is given through the machine mLTS. First, we represent the state space by the variable st ∈ State. The dynamics is specified through two events: the INITIALISATION event which chooses non-deterministically a state among elements of the set I and the next event which also chooses non-deterministically a label and a transition having such a label.

Figure 3 illustrates an Event-B refinement of the preceding machine mLTS. Intuitively, we model the introduction of an internal event that will take control for some time after which the next event becomes enabled again. For such a purpose, the machine mLTS_r refines mLTS and introduces a new variable cpt : a counter that will be initialized non deterministically. When the counter reaches the zero value, next is enabled. The refined machine refines the events INITIALIZATION and next and introduces the new event silent which is similar to τ events of CCS [START_REF] Milner | Communication and Concurrency[END_REF]. We notice that in the new (refining) next event, the enabled guard is strengthened by the conjunct cpt = 0. Moreover, this new next event provides a witness of the parameter of the old (refined) next event: the parameter lr is said to be the witness of the parameter l. When the new next event has been executed, cpt is again assigned a positive value. In Event-B, the proof obligations enforce a weak refinement semantics [START_REF] Milner | Communication and Concurrency[END_REF]. The purpose of the variant clause is to enforce that introduced events will not take control forever. Usually, the variant belongs to a well ordered domain and is decreased by newly introduced (internal) events declared to be convergent.

A GENERIC COMPILER DEVELOPMENT FOR SYNCHRONOUS LANGUAGES

In this section, we elaborate a generic refinement-based approach for the compilation of synchronous languages. Starting from the so-called labelled synchronous transition systems, we propose a sequence of refinement steps, illustrated by Figure 4, leading to code generation. Thanks to the refinement-based approach, the generated code is known to preserve by construction the initial semantics provided all the proof obligations have been discharged.

Labelled synchronous transition systems

In the synchronous context, executions are seen as sequences of reactions [START_REF] Potop-Butucaru | Concurrency in Synchronous Systems[END_REF]. A reaction r assigns values to the subset of variables said to be present: undefinedness of r on a variable v means absence of v in r . We suppose a fixed domain D for the values and define a reaction over the set of variables V as a partial function from V to the domain D, i.e., Reaction(V ) = V →D. We remark that the usual definition of a reaction is a total function to D ∪ {⊥} where ⊥ machine mLTS_r refines mLTS sees cLTS variables st cpt invariants @cpt_ty cpt ∈ N variant cpt events event INITIALISATION then @I st :∈ I @cpt_i cpt := 0 end event next refines next any lr // parameter is renamed where @lr lr ∈ Label @enabled cpt = 0 ∧ st → lr ∈ dom(Trans) with @l l = lr // link with abstract paramater; l witness relation

• then @ns st :| ( st → lr → st ') ∈ Trans @restart cpt :∈ N end convergent event silent
where @g cpt > 0 then @cpt_d cpt := cpt -1 end end We introduce now labelled synchronous transition systems which generate synchronous executions.

Definition 3.1 (LSTS).

A Labelled Synchronous Transition System is a quadruple V, S, I, → where V is a set of variables, S a set of states, I ∈ S is an initial state and →⊆ S × Reaction(V ) × S is the set of transitions labelled by reactions.

Signal and its LSTS semantics.

In order to illustrate the definition of an LSTS, we present the syntax of a kernel of the Signal language [START_REF] Gamatié | Designing Embedded Systems with the SIGNAL Programming Language -Synchronous[END_REF] and its semantics defined as an LSTS [START_REF] Potop-Butucaru | Concurrency in Synchronous Systems[END_REF]. A Signal program over a set of variables V is a set of equations of the following form which define each variable at most once:

•

x 1 = x 2 when x 3 undersampling • x 1 = x 2 default x 3 deterministic merge • x 1 = f (x 2 , x 3 ) instantaneous function • x 1 = x 2 $ init v delay
With respect to the Signal language, we essentially do not consider local variables. This aspect is not relevant for our presentation. The semantics of Signal can be defined as an LSTS where a state is a mapping from memorized (or persistent) variables to values. A variable is memorized if it is introduced by a delay equation. In order to define the denotational semantics of Signal, we introduce the function R m where m is a memory state. It takes as parameter a Signal equation and returns the set of allowed reactions. We also suppose the existence of a constant ∈ D representing true.

• R m [x 1 = x 2 when x 3 ] = {r ∈ V →D | ∀v • x 1 → v ∈ r ⇔ (x 2 → v ∈ r ∧ x 3 → ∈ r ) } • R m [x 1 = x 2 default x 3 ] = {r ∈ V →D | ∀v • x 1 → v ∈ r ⇔ (x 2 → v ∈ r ∨ x 2 dom(r ) ∧ x 3 → v ∈ r ) } • R m [x 1 = f (x 2 , x 3 )] = {r ∈ V →D | ∀v 1 , v 2 , v 3 • x 1 ∈ dom(r ) ⇔ x 2 ∈ dom(r ) ⇔ x 3 ∈ dom(r ) ∧(x 1 → v 1 ∈ r ∧ x 2 → v 2 ∈ r ∧ x 3 → v 3 ∈ r ⇒ v 1 = f (v 2 , v 3 ) } • R m [x 1 = x 2 $ init v] = {r ∈ V →D | x 1 ∈ dom(r ) ⇒ r (x 1 ) = m(x 1 ) ∧ x 1 ∈ dom(r ) ⇔ x 2 ∈ dom(r ) }
We are now ready to introduce the semantics of a Signal program P over variables of V as an LSTS. We define the set M ⊆ V of memory variables as those introduced by $ init equations. Then, the LSTS associated to P is the quadruple

V, M → D, {v → c | v = w$ init c ∈ P }, {m r → m | r ∈ p ∈P R m [p] ∧ m = m -{v → r (w ) | w ∈ dom(r ) ∧ v = w$ init c ∈ P } .
In the following, we will use an abstraction of the set of reactions p ∈P R m [p] as a parameterized constraint problem. The parameters are here the variables which are not defined through a Signal program equation.

3.1.2

The refined LSTS. We intend to produce LSTS from synchronous languages as Lustre or Signal. The corresponding LSTS are specialized as follows:

• The reaction is computed from the synchronous program and the current state. For instance, in the Signal setting, the program can be read as a set of constraints of which solutions are the set of allowed reactions. • The state contains the value of variables defined by a delay construct. The state space is thus a mapping from a (memory) subset M of the set of variables V to the domain D. • The state is updated by storing for each memory variable x its next value defined to be the value of some variable N (x ) when x is present. Otherwise, the memorized value remains unchanged, thus allowing persistence of information over cycles. Thus, we introduce what we call a refined LSTS (rLSTS) by the following definition:

Definition 3.2 (rLSTS). A rLSTS is a quintuple V, M ⊆ V, I ∈ M → D, N ∈ M → V, C ∈ (M → D) → P(V →D) where: • V is a set of variables,
• M is the subset of memory variables,

• I is the initialization of these variables,

• N associates to each memory variable the variable, the value of which is stored, • C returns the set of allowed reactions from a given memory state.

The LSTS corresponding to the rLSTS is defined as follows by the quadruple

V = V, S = M → D, I = I, m r -→ m ≡ r ∈ C(m) ∧ m = m -N ;
px = 0 px = 1 px = 3 r = _ x = 1 px = 0 nx = 1 r = 3 x = 3 px = 1 nx = 2 r = _ x = 4 px = 3 nx = 4
process INCR = (?integer r; !integer x;) (| (| | px := x$ init 0 | nx := px + 1 | x := r default nx |)/px,nx |)
If we keep local variables visible, the associated rLSTS is defined as follows:

V = {r , x, px, nx }, M = {px }, I = {px → 0}, N = {px → x }, C(m) = R m [px = x$ init 0] ∩ R m [nx = px + 1] ∩ R m [x = r default nx]
Figure 5 is a partial run of this example. A run is an alternating sequence of states (ovals) and transitions labelled by reactions (vectors). In the first reaction, r is absent and x is one more than the memorized value. The second transition is labelled by a reaction where r is present. Thus x takes the value of r. In the third transition, r is chosen to be absent and x is incremented. The reaction could also be empty (all variables being absent). However, this will be forbidden in the remaining of the paper to avoid Zeno behaviors.

Event-B representation.

First of all, we define the context cMeta (Fig. 6) containing the various fields of the rLSTS we will consider. With respect to definition (3.2), we have added one parameter of type P(V ) to the function C denoting the constraint problem of which reactions should be solutions. It contains the set of variables that are constrained and is now the full set V. This parameter will be modified to specify the incremental computation of the reaction in the next refinement.

Second, we define the semantics of the given rLSTS through an Event-B machine which specifies the Labelled transition system associated to the rLSTS through the state variable m initialized using I. The state evolves through the bigStep event parameterized by a This bigStep event is intended to be split into small steps that compute reactions incrementally. machine mBigStep sees cMeta variables m // memory invariants @m_ty m ∈ M → D events event INITIALISATION then @m_init m := I end event bigStep any r where @r_ty r ∈ V → D // r is a reaction @g r ∈ C(m)(V) // r is a solution of the constraint system @ne r ∅ // to avoid Zeno behaviors then @m m := m -(N ;r) // memory update end end

context cMeta sets V D constants M I N C axioms @fVat finite ( V) @I_ty I ∈ M → D @N _ty N ∈ M → V @C_ty C ∈ (M → D) → (P(V) → P(V → D)) end

Solved form (context cMeta_SF) and small step semantics (machine mSmallStep)

This refinement aims at splitting the big step which specifies what are valid reactions. The small steps should compute one variable at a time. To make it possible, the constraint system should be put in solved form.

Solved form.

We define the constraint problem as a set of equations supposed to be in triangular form: a left hand side variable is said to depend on right hand side variables and this dependency relation should be acyclic. In fact, two informations must be computed: the presence of a variable, and if present, its value. The value of a present variable is either defined by a formula, or read from input (indeterminate), or read from memory. Thus, we first introduce the constant isPresent together with the dependency relation pdep. The function isPresent takes as parameters a variable and a partially computed reaction and returns a set of booleans which indicate if the variable is allowed to be present or absent, or both. isPresent returns either {TRUE}, either {FALSE}, or {TRUE,FALSE} to encode indeterminacy, as it is the case for master clocks of Signal programs [START_REF] Gamatié | Designing Embedded Systems with the SIGNAL Programming Language -Synchronous[END_REF]. Concerning pdep, it maps each variable to the set of variables on which its presence depends. Moreover, a variable which does not depend on other variables can be chosen to be present or absent. Now, we introduce the eqns function for value computation, together with the dependency relation dep. Contrary to presence, values are specified in a functional way. Indeterminacy of values is inferred from the absence of equations for some variables. The function eqns takes as parameters the considered variable and returns its value for the currently computed reaction. This function is partial at several orders: it is defined for a subset of non memory variables. Accepted reactions (which are partial functions) should at most give a value to variables on which the first argument depends. These reactions are those that allow the presence of the variable. constants eqns dep axioms @eqns_ty eqns ∈ V → ((V → D) → D) @mem_eqns M ∩ dom(eqns) = ∅ @dep_ty dep ∈ V -→ P(V) @dep_def ∀v• v ∈ dom(eqns) ⇒ dom(eqns(v)) ⊆ (dep(v) → D)

constants isPresent pdep axioms @isPresent_ty isPresent ∈ V × (V → D) -→ P1(B) @pdep_ty pdep ∈ V -→ P(V) @check_empty ∀ v • pdep(v) = ∅ ⇒ isPresent (v →∅) = B

Figure 8: cMeta_SF (part II)

Figure 9 introduces the link between Presence and the existence of a value for a variable: a partial solution ps allows the presence of a variable v if and only if the partial solution ps is in the domain of eqns(v).

axioms @isp_dom ∀v,ps• v∈dom(eqns) ∧ ps ∈ dep(v) → D ⇒ (TRUE ∈ isPresent(v →pdep(v) ps) ⇔ ps ∈ dom(eqns(v)))

Figure 9: cMeta_SF (part III)

We suppose that for any variable v, pdep(v) is a subset of dep(v): the value of v (depending on variables of dep(v) can be computed once we know its presence (depending on variables of pdep(v). Then, we add properties stating that dep is transitively closed and irreflexive, thus a strict partial order. Now, we define the constraint problem C m,S for a memory state m and a subset S ⊆ V of seen variables. A solution r is a partial function on S, undefinedness meaning absence. It is constrained by three properties (Fig. 11): • The presence or the absence of a variable v within a reaction r should be allowed by the set returned by the function isPresent where r is restricted to variables on which v depends.

@pdep_dep ∀v• pdep(v) ⊆ dep(v) @pdep_trans ∀v1, v2• v1 ∈ pdep(v2) ⇒ pdep(v1) ⊆ pdep(v2) @dep_trans ∀v1, v2• v1 ∈ dep(v2) ⇒ dep(v1) ⊆ dep(v2) @dep_irrefl ∀v• v dep(v)
• The restriction of r to memory variables is given by the memory state.

• The value of a present variable v associated to an equation is given by this equation taking as parameter v and a restriction of r to variables it depends on.

axioms @C_def C = (λm• m ∈ M -→ D | λS• S ⊆ V | { r | r ∈ S → D ∧ ( ∀v• v∈S ⇒ bool(v ∈ dom(r)) ∈ isPresent (v → pdep(v) r )) ∧ (( M ∩ S) r ⊆ m) ∧ ∀v• v ∈ dom(r) ∩ dom(eqns) ⇒ r (v) = eqns(v )( dep(v) r ) })
Figure 11: The constraint problem 3.2.2 Memory access. We introduce dedicated variables, from the set NextMem, used as markers for memory updates. The injective function write associates to each memory variable v, its memory write event. This event should be fired after all reads of v and after the computation of the next value of v given by the variable N (v). The presence of the write event depends on the presence of the next value. It is actually present if the next value is present.

constants NextMem write axioms @write write ∈ M NextMem @wdep ∀v•v∈M ⇒ {w | v ∈ dep(w)} ∪ {v, N (v)} ⊆ dep(write(v )) @wpdep ∀v•v∈M ⇒ pdep(write(v)) = {N (v)} ∪ pdep(N (v)) @wpres ∀ps,v• ps∈V →D ∧ v∈M ⇒ isPresent ( write (v) →pdep(write(v )) ps) = {bool( N (v)∈dom(ps))}
3.2.3 Small step semantics. Given a constraint system in triangular form, it is possible to compute reaction variables one by one through so-called small steps. In the same way, the memory can be updated incrementally once the current value of a variable becomes useless in the current cycle: it will not be read anymore. For this purpose, we introduce a refinement machine with three new variables: the partially updated memory pm, the partial solution ps and the set of processed variables done. machine mSmallStep refines mBigStep sees cMeta_SF variables pm // partially updated memory ps // partial solution done // processed signals invariants @pm pm ∈ M -→ D @ps_ty ps ∈ V → D @done_ty done ⊆ V

These variables satisfy the following invariant properties:

• The restrictions of pm and m to unprocessed memorized variables are identical functions. • ps is a partial solution restricted to variables of done.

• If a variable is present, variables of which depends its value (given by dep) have been processed. • If a variable has been processed, variables on which depends its presence (given by pdep) have also been processed. • The partial solution is not empty as soon as one variable has been processed, i.e. the first processed variable should be marked as present. • The memory is partially updated by the next value of memory variables of which the write event has been processed. Initially, the partial solution and the set of processed variables are empty. Memory gets the rLSTS initial value.

invariants @pmu ∀v•v∈M\done ⇒ pm(v) = m(v) //

event INITIALISATION

then @init_ps ps := ∅ @init_done done := ∅ @init_pm pm := I end Small steps determine the presence and compute the value of individual variables. These steps must be transparent from the point of view of the abstract machine: they do not modify previously introduced variables and should apply a finite number of times. This is why they are declared convergent, which means that they must decrease the variant. Several convergent events are defined. They respectively process absent variables, present variables defined by an equation, memory accesses or undetermined variables (considered as inputs or parameters). Due to space restrictions, two cases are presented: equational variables and absent variables. Other events are related to memory read and write variables, parameters (non memory and non equational variables).

The following listing manages variables defined by an equation. The event selects such a variable v which has not been processed before. Variables on which it depends should have been processed and v is allowed to be present. Then, its binding to the value given by the equation is inserted into the partial solution and v is added to done. It follows that the variant decreases. variant V \ done events convergent event smallStep_P // processing of a present variable any v where @v v ∈ dom(eqns) \ done @d dep(v) ⊆ done // thus pdep(v) ⊆ done @p TRUE ∈ isPresent(v →pdep(v) ps) // v is allowed to be present then @ps ps(v) := eqns(v )( dep(v) ps) @done done := done ∪ {v} end end

The following listing manages absent variables. Contrary to present ones, they are processed by blocks. This will allow optimisations in the generated code. So, we consider a non empty set of variables V such as variables on which they depend are either already processed or in V . Absence should be allowed for all these variables. Note that this permission is checked by supposing variables of V are absent as unprocessed variables are seen as absent. Lastly, the partial solution should not be empty to ensure that the computed reaction will not be the empty one. convergent event smallStep_mA // processing of absent variables any V where @v V ⊆ V \ done @vnv V ∅ // ensures that the variant decreases

@d ∀v• v ∈ V ⇒ pdep(v) ⊆ done ∪ V // variables of V are allowed to be absent @abs ∀v• v ∈ V ⇒ FALSE ∈ isPresent (v →pdep(v) ps) @ps ps ∅ then @done done := done ∪ V end
When all the variables have been processed by the small steps, we can refine the big step of the abstract machine and prepare the next round by resetting the variable done. event bigStep refines bigStep where @g done = V with @r r = ps // r witness relation then @ps ps := ∅ @d done := ∅ end 3.2.4 Example. Given the Signal example previously introduced in Paragraph 3.1.3, we add the write event marker px w for the memory variable px. Figure 12 shows how the declared constants introduced in the solved form can be instantiated. The graph represents the functions pdep and dep. All the antecedents with plain arrows of a node x form its dependency for pdep. dep is obtained by adding the dashed arrows.

Concerning the isPresent function, written isP in the figure, it allows presence and absence for r. If r is actually present, px must be present; otherwise px presence does not care. Then the authorization of presence of variables nx, x and px w is determined by the actual presence of px and x.

Concerning eqns, it associates a value to nx and x by accessing to the value of variables they depend on.

Introduction of clocks (machine mSmallStep_CC)

We now associate clocks to variables. The role of a clock is to manage presence. Thus, a variable will be present if and only if its clock is present. For this purpose, the set Clock is declared as a subset of variables supposed to be neither memory variables nor defined by an equation: they are not valued. Each variable has a clock (defined by the function cP). The clock of a clock is itself.

context cMeta_CC extends cMeta_SF constants Clock cP axioms @Clock_ty Clock ⊆ V \ (M ∪ NextMem ∪ dom(eqns)) @isP_ty cP ∈ V → Clock @isP_clk ∀s• s ∈ Clock ⇒ cP(s ) = s @Clk_def ∀s•cP(s)=s ⇒ s ∈Clock @isP_dep ∀s• s∈V\Clock ⇒ cP(s) ∈ pdep(s) @clk_dep ∀v• v∈Clock ∧ dep(v) = ∅ ⇒ v ∈ IO @chk_clk ∀v,ps• ps∈V →D ⇒ isPresent (v →pdep(v) ps) = isPresent (cP(v) →pdep(cP(v)) ps) @pdep_clk ∀v• v∈Clock ⇒ pdep(v) = dep(v) end
A new refinement can now be defined. It differs from the previous machine by the fact that presence of clocks are tested through the isPresent function while presence of valued variables comes to the presence of their clocks. One invariant is added. It states that for a processed variable, its presence and the presence of its clock are equivalent. The following listing illustrates the transformation of the two events. For equational variables: cP(v) presence is now checked. For absence, constraints on V are strengthen to ensure clocks are also selected and that they are absent. The big step is unchanged.

machine mSmallStep_CC refines mSmallStep sees cMeta_CC variables pm ps done invariants @pres ∀v• v ∈ done ⇒ (cP(v) ∈ dom(ps) ⇔ v ∈ dom(ps)) events event smallStep_P refines smallStep_P any v where @v v ∈ dom(eqns) \ done @d dep(v) ⊆ done @p cP(v) ∈ dom(ps) then @ps ps(v) := eqns(v )( dep(v) ps) @done done := done ∪ {v} end event smallStep_mA extends smallStep_mA where @clk_done cP[V] ⊆ done ∪ V @clk_abs cP[V] ∩ dom(ps) = ∅ end event bigStep extends bigStep end // unchanged end 3.3.1 Example. Given our working example, we introduce the clocks r , px, x, nx, px w , thus defining the cP function by cP (v) = v. We have chosen to take the same clock for x and nx. This is allowed by the axioms since their respective presence are defined in the same way. The dependencies between the variables are now given by the following graph:

∈ Clock ∧ v ∈ sub(w) ⇒ w ∈ pdep(v) @sub_present ∀v1,v2• v1∈Clock ∧ v2 ∈ sub(v1) ⇒ ( ∀m,D,ps• m∈M→D ∧ pdep(v1) ⊆ D ∧ pdep(v2) ⊆ D ∪ {v1} ∪ sub(v1) ∪ cP -1 [{v1} ∪ sub(v1 )] ∧ v1 D ∧ sub(v1) ∩ D = ∅ ∧ ps ∈ C(m)(D) ∧ FALSE ∈ isPresent (v1 → pdep(v1) ps) ⇒ FALSE ∈ isPresent (v2 → pdep(v2) ps )) end
The refined machine declares one new invariant stating that if a clock has not been processed, the clocks it subsumes have not been dealt with either. The only modified event is the one managing absence: clocks declared to be absent are clocks subsumed by a clock v or variables of which clock is subsumed by v. Thus only one absence test is performed to discard V . machine mSmallStep_SUB refines mSmallStep_CC sees cMeta_SUB variables pm ps done invariants @sub_done ∀c• c∈Clock\done ⇒ sub(c) ∩ done = ∅ events event smallStep_mA refines smallStep_mA any v V where These new arrows define a subgraph of the dependency graph and should satisfy the axiom sub_present. For instance, let us consider the bended arrow between px and x. Given a partial solution ps defined at least on pdep(px ) and not on px we must check the implication between each presence property. This property is satisfied since the right side of the implication is True because px dom(ps).

@v v ∈ Clock \ done @d pdep(v) ⊆ done @abs FALSE ∈ isPresent(v →pdep(v) ps) @ps ps ∅ @V V ⊆ {v} ∪ sub(v) ∪ cP -1 [{v} ∪ sub(v )] @Vv v ∈ V @Vd V ∩ done = ∅ @Vp ∀w• w ∈ V ⇒ pdep(w) ⊆ done ∪ V then @done done := done ∪ V end end 3.
for a compiler to be correct? It should preserve the semantics of the source code, i.e., preserve some observable behaviors, which is ultimately expressed as proving a forward simulation for safe programs property. In this paper, a safe program is a program that can be put in solved form. Forward simulation is a consequence of refinement. Observable behaviors are sequences of reactions. Thus, Event-B brings us a methodology to incrementally build a similar proof (for a much less complex language).

Constructive semantics

A so called constructive semantics has been proposed for various synchronous languages [START_REF] Talpin | Constructive Polychronous Systems[END_REF]. This semantics aims at specifying how to compute output variables from inputs for each reaction. As in our case, small steps are proposed to solve constraints upon presence and values of the variables of the program. Specific rules are provided for various synchronous languages. The main difficulty of this approach, which is linked to the considered languages, is to find a trigger, i.e. a signal of which presence can be enforced in order to determine the presence and value of all other signals without failing to find a global solution when solving incrementally the constraint system. The authors define several classes of processes (reactive, deterministic, isochronous, ...) ensuring convergence properties. In this paper, we do not address these aspects and suppose that constraints have been put in solved form, which guarantees the ability to incrementally build a solution and has the same consequences as isochrony [START_REF] Talpin | Constructive Polychronous Systems[END_REF], i.e., the ability to non deterministically select a non empty subset of triggers to present. Then, we mainly focus on refinement-based methodology to extract an optimizing compiler and the interpretor of the compiled code from the small step semantics which is itself shown to conform with the big step semantics. Furthermore, our framework is independent from a specific synchronous language.

CONCLUSION

In this paper, we have presented the development of a generic compiler for synchronous languages. Our main contribution was to structure such a development as successive refinement steps. Through these steps, we have introduced progressively the main ingredients of such a compilation process: presence of variables, clock calculus, optimization and code generation. Properties preservation was ensured thanks to the semantics of refinement supported by the Event-B formal method. With respect to the expression of the properties, set theory has revealed well suited to express: as well atomicity in high level specifications thanks to the composition of relations, as well the progressive approach thanks to partial functions. The proof obligations have been generated by the Rodin platform. All the proofs have been done. These proofs were made easier by the automatic SMT provers. We envision to carry on this work with respect to two directions: first we would like to instantiate this generic compiler by well known synchronous languages as [START_REF] Benveniste | The synchronous languages 12 years later[END_REF][START_REF] Schneider | A Verified Compiler for Synchronous Programs with Local Declarations[END_REF]. Second, also, we would like to adapt code generation for targeting concurrent architectures [START_REF] Aguado | Denotational fixed-point semantics for constructive scheduling of synchronous concurrency[END_REF].

Figure 1 :

 1 Figure 1: Event-B development step

Figure 2 :

 2 Figure 2: Event-B LTS semantics

Figure 3 :

 3 Figure 3: Event-B refinement

Figure 4 :

 4 Figure 4: Refinement steps

Figure 5 :

 5 Figure 5: Signal LSTS partial run

Figure 6 :

 6 Figure 6: The Event-B context cMeta

Figure 7 :

 7 Figure 7: cMeta_SF (part I)

Figure 10 :

 10 Figure 10: cMeta_SF (part IV)

Figure 12 :

 12 Figure 12: Solved Form level (example)

w px w 3 . 4

 34 Clock hierarchy (machine mSmallStep_SUB)

4 . 1

 41 Example. Considering our example, we add the subsumtion relation as bended arrows to the dependency graph restricted to clocks. r px x = nx px w

  r where C associates to a memory state a set of reactions.

				cMeta_SUB	cMeta_SEQ
			Introduction	Introduction	Sequential
			of clocks	of the clock hierarchy	code
	mBigStep LSTS semantics	mSmallStep	mSmallStep_CC Use of clocks presence	mSmallStep_SUB Optimization	mSmallStep_SEQ Sequential code VM simulation

  The goal of this refinement is to introduce the clock inclusion relation: if a clock is absent, sub-clocks are also absent and it is not useful to check them at runtime. For this purpose, we introduce the relation sub represented by a function associating to a clock the set of clocks it subsumes (or contains). This relation should be compatible with the pdep relation: a clock depends on clocks containing it. Subsumption declarations should be consistent with presence semantics as given by the isPresent function. Clock → P(Clock) // gives the set of subsumed clocks @sub_dep ∀v,w• w

	context cMeta_SUB extends cMeta_CC
	constants sub
	axioms
	@sub_ty sub ∈

Sequential code generation (machine mSmallStep_Seq)

This refinement step is the key point of the verified compiler generation. It consists in separating actions that can be performed at compile time (statically) from actions performed at run time, the link between them being the generated code. The principle is the following:

• At the abstract level, an event is fired if its parameters satisfy static properties (linked to the dependency relations) and dynamic properties (linked to presence / value) of variables in the partial reaction already built. • To each such event is associated a convergent event that will select its parameter depending only on static properties and store it in the sequence of instructions built by the compilation phase. These events constitute the code of the compiler. • The abstract event itself is refined by an event which simulates the created instruction by testing and updating the dynamic state. • The correction of this separation relies on the fact that static properties should be sufficient to select event parameters. It is ensured if we suppose that, given parameters satisfying the static properties, there exists an event of which dynamic properties are also satisfied. These principles are applied to small step events. Such an event may be fired on a variable if previous variables (for dep or pdep partial orders) have been processed and if some conditions depending on the partial reaction (presence of the clock for example) are satisfied. Building the reaction is left for the dynamic phase. However, variable selection, i.e., topological sort, can be performed at compile time. As a result, we get a sequence of statements specifying the event to fire and the variable to be selected. Statements

The invariant specifies the link between old and new dynamic variables (done and pc) and between generated instructions and expected properties of the variable selected by the old small step events:

• processed variables (the set done) are arguments of previous statements in the code sequence,

We now consider the event smallStep_P of paragraph 3.3. The management of other events is similar. According to the splitting method, we introduce a convergent event acting as the compilation step. It non-deterministically selects an equational variable provided that the variables it depends on have already been processed. Then it adds a new instruction, here a conditional assignment and updates the iff pointers to allow the new instruction to be skipped if the required conditions are satisfied.

The interpretation of generated events. The second event recognizes the generated instruction and performs the dynamic part of the refined event: the presence of the argument of the instruction is checked and the reaction is updated. Note that presence check could be removed: within the bloc of code skipped by the iff pointer, the presence condition is known to be satisfied. Due to lack of space, this optimization is not detailed here. event smallStep_P refines smallStep_P where @pc pc < N // end of generated code ¬reached @arg stmt(pc) = Assign // current statement is an Assign @p cP(arg(pc)) ∈ dom(ps) // the clock of the assigned variable is present with @v v = arg(pc) // the processed variable is the argument of the statement then @ps ps(arg(pc )) := eqns(arg(pc ))( dep(arg(pc )) ps) @npc pc := pc + 1 end Absence being managed through the update of the iff pointers during the generation of all small step statement related to presence, only remains the dynamic part which consists in skipping a block of instructions in case a presence test fails. The new event declares the values of the parameters of the refined event.

event smallStep_mA refines smallStep_mA when @pcN pc < N // end of generated code ¬reached @pc stmt(pc) = GetPresence @pcnz pc > 0 // it is ¬the first statement @abs FALSE ∈ isPresent(arg(pc) →pdep(arg(pc )) ps) // absence allowed with @v v = arg(pc) // the processed variable @V V = arg[pc. .iff(pc)-1] // the set of variables to be skipped then @npc pc := iff (pc) // jump to next block end At last, the big step event is modified to take into account the new state variables: the compilation should have been performed before, the small steps should have been executed. It has to be noted that, except for this last event, compilation and execution of generated instructions can be interleaved during the computation of the first reaction of the run. This property is partially lost if presence test optimization is considered: if execution jumps to the end of the code as a consequence of a presence test failure, the compiler could insert an optimized statement (without presence check) at this point. event bigStep refines bigStep where @g ran(arg) = V // compilation ended @pc pc = N // end of small steps then @ps ps := ∅ @d pc := 0 end 3.5.3 Example. The following table is an example of sequence of statements that could be obtained by executing the convergent events according to their ordering constraints. The table contains the sequence of statements (stmt) together with their arguments (arg). The arrows represent the iff jumps when the source condition is false. We remark that our specification of the compilation phase is actually non deterministic, other sequences of code could be generated.

Development overview

All the preceding development has been performed under the Rodin framework for Event-B. For all the development (contexts and machines), the tool generated 17 proof obligations for contexts and 239 proof obligations for machines. Most of the proof obligations could be discharged automatically thanks to the SMT solvers (CVC3-4, Z3,veriT). Some proof obligations needed manual quantification instantiation and case analysis. We remark that unlike usual assistant theorem provers [START_REF] Huet | The Coq Proof Assistant : A Tutorial : Version 6.1[END_REF][START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-order Logic[END_REF][START_REF] Owre | PVS: A Prototype Verification System[END_REF], elementary proof obligations are generated automatically, e.g., the preservation of each conjunct of the invariant by each action of each event. However, concerning Rodin, strategy languages are still missing.

RELATED WORK

In this section we review some related works. In the following, we position our work with respect to them.

Clock calculus

Here, we have adopted an axiomatic approach: in the context cMeta_SUB, we have specified a subsumption relation compatible with data dependency. The work of [START_REF] Tochéou Pascalin Amagbegnon | Arborescent canonical form of boolean expressions[END_REF] can be seen as a concretization of this specification. As a future work, we intend to validate some of these constructions by taking into account the language to which they apply.

Translation validation

Translation validation has been pioneered by A. Pnueli et al. [START_REF] Pnueli | Translation Validation: From SIGNAL to C[END_REF]. Recently, [START_REF] Van Chan Ngo | Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler[END_REF] have pushed forward this approach for the Signal language. The basic idea is that each individual translation is followed by a validation phase which verifies that the produced code implements the source code. Unlike this approach, here we are interested in the compilation approach: which verifies the compiler once for all. It follows that any produced code is guaranteed to be correct.

Compcert

The CompCert project [START_REF] Leroy | A Formally Verified Compiler Back-end[END_REF] aims at the development of a formally verified C compiler. This work is far more complex than our one and could be used as a back end of a synchronous language to C compiler. However, one point is interesting to be discussed and is put forward in the CompCert project. It is related to what means


Atef Khedher
email: khedheratef@yahoo.fr

Kamel Benothman
email: kamal.benothman@enim.rnu.tn

Didier Maquin
email: didier.maquin@ensem.inpl-nancy.fr

Mohamed Benrejeb
email: mohamed.benrejeb@enit.rnu.tn

STATE AND SENSOR FAULTS ESTIMATION VIA A PROPORTIONAL INTEGRAL OBSERVER

Keywords: state estimation, Takagi-Sugeno, sensor fault, unknown input, multiple model

This paper deals with the problem of fault detection and identification in noisy systems. A proportionnal integral observer with unknown inputs is used to reconstruct state and sensors faults. A mathematical transformation is made to conceive an augmented system, in which the initial sensor fault appear as an unknown input. The noise effect on the state and fault estimation errors is also minimized. The obtained results are then extended to nonlinear systems described by nonlinear Takagi-Sugeno models.

INTRODUCTION

State estimation is an important field of research with numerous applications in control and diagnosis. Generally the whole system state is not always measurable and the recourse to its estimation is a necessity. An observer is generally a dynamical system allowing the state reconstruction from the system model and the measurements of its inputs and ouputs [?]. For linear models, state estimation methods are very efficient [?]. However for many real systems, the linearity hypothesis cannot be assumed. In that case, the synthesis of a nonlinear observer allows the reconstruction of the system state. For example, let us cite sliding mode observers [?], the Thau-Luenberger observers [?] and observer for nonlinear systems described by Takagi-Sugeno models [?]. Approaches using Takagi-Sugeno model (sometimes named multiple model) are the object of many works in different contexts including the taking into account of unknown inputs or parameter uncertainties [?, ?]. Various studies dealing with the presence of unknown inputs acting on the system were published [?, ?, ?]. Some of them tried to reconstruct the system state in spite of the unknown input existence. This reconstruction is assured via the elimination of unknown inputs [?, ?]. Other works choose to estimate, simultaneously, the unknown inputs and system state [?, ?]. Among the techniques that do not require the elimination of the unknown inputs, Wang [?] proposes an observerable to entirely reconstruct the state of a linear system in the presence of unknown inputs and in [?], to estimate the state, a model inversion method is used. Using the Walcott and Zak structure observer [?] Edwards et al. [?, ?] have also designed a convergent observer using the Lyapunov approach. Observers with unknown inputs are used to estimate actuators faults wich can be assumed to unknown inputs, this estimation can be made by the use of a proportionnel integarl observer [?]. In often cases, process can be subjected to disturbances which have as origin the noises due to its environment, uncertainty of measurements, fault of sensors and/or actuators. These disturbances have harmful effects on the normal behavior of the process and their estimation can be used to conceive a control strategy able to minimize their effects. In the case of sensor faults, Edwards [?] propose for linear systems to use a new state wich is a filtrate version of the output, to conceive an augmeted system in wich th sensor fault appear as un unknown input. This formulation was used by [?]. In this paper, a prportionnel integral observer will be conceived to estimate the state and sensor faults. The extension of this method to nonlinear systems described by nonlinear Takagi-Sugeno models will be proposed afterthat.

LINEAR SYSTEM CASE

The objective of this part is to estimate a sensor fault affecting a linear system via an unknown input proportional integral state observer.

Problem formulation

Consider the linear model affected by a sensor fault and a measurement noise described by :

ẋ(t) = Ax(t) + Bu(t) (1) y(t) = Cx(t) + Ef (t) + Dw(t) (2)
where x(t) ∈ R n represents the system state, y(t) ∈ R m is the measured output, u(t) ∈ R r is the system input, f (t) represents the fault and w(t) is the measurement noise.

A, B and C are known constant matrices with appropriate dimensions. E and D are respectively the fault and the noise distribution matrices which are assumed to be known. Consider also the state z(t) ∈ R p [?] that is a filtered version of the output y(t). It is given by :

ż(t) = -Āz(t) + ĀCx(t) + ĀEf (t) (3)
where -Ā ∈ R p * p is a stable matrix. One introduce the augmented state X = x T z T T , this state is given by the equation (??).

Ẋ(t) = A a X(t) + B a u(t) + E a f (t) (4) Y (t) = C a X(t) + D a w(t) (5)
with :

A a = A 0 ĀC -Ā, , C a = C 0 0 I (6) B a = B 0 , E a = 0 ĀE and D a = D D (7)
The structure of the chosen observer is as follows :

Ẋ(t) = A a X(t) + B a u(t) + E a f (t) + K(Y (t) -Ŷ (t)) (8)
ḟ (t) = L(Y (t) -Ŷ (t)) (9) Ŷ (t) = C a X(t) (10)
where X(t) is the estimated state, f (t) represents the estimated fault, Ŷ (t) is the estimated output, K is the proportional observer gain and L is the integral gain to be computed. It is supposed that the fault affecting the system is bounded. Let us define the state estimation error x(t) and the fault estimation error f (t) :

x(t) = X(t) -X(t) and f (t) = f (t) -f (t) (11)
The dynamics of the state estimation error is given by the computation of ẋ(t) which can be written :

ẋ(t) = Ẋ(t) -Ẋ(t) = (A a -K a C)x(t) + E a f (t) -KD a w(t) (12)
The dynamics of the fault estimation error is :

ḟ (t) = ḟ (t) -ḟ (t) = ḟ (t) -LC a X(t) -LD a w(t) (13)
The following matrices are introduced :

ϕ = x f and ε = w ḟ (14)
From the equations (??) and (??), one can obtain :

φ = A 0 ϕ + B 0 ε (15)
with :

A 0 = A a -KC a E a -LC a 0 , B 0 = -KD a 0 -LD a I (16)
The matrix I is the identity matrix with appropriate dimensions. In order to analyse the convergence of the generalized estimation error ϕ(t), let us consider the following quadratic Lyapunov candidate function V (t) :

V (t) = ϕ T P ϕ (17)
where P denotes a positive definite matrix.

The problem of robust state and fault estimation is to find the gains K and L of the observer to ensure an asymptotic convergence of ϕ(t) toward zero if ε(t) = 0 and to ensure a bounded error in the case where ε(t) = 0, i.e. :

lim t→∞ ϕ(t) = 0 for ε(t) = 0 ϕ(t) Qϕ ≤ µ ε(t) Qε for ε(t) = 0 and e(0) = 0 (18)
where µ > 0 is the attenuation level. To satisfy the constraints (??), it is sufficient to find a Lyapunov function V (t) such that :

V (t) + ϕ T Q ϕ ϕ -µ 2 ε T Q ε ε < 0 (19)
where Q ϕ and Q ε are two positive definite matrices. In order to simplify the notations, the time index (t) will be omitted henceforth.

The inequality (??) can also be written as :

ψ T Ωψ < 0 (20)
with :

ψ = ϕ ε , Ω = A T 0 P + P A 0 + Q ϕ P B 0 B T 0 P -µ 2 Q ε (21)
The quadratic form in (??) is negative if :

Ω < 0 (22)
The matrix A 0 can be expressed as :

A 0 = Ã -K C (23)
with :

à = A a E a 0 0 , K = K L , C = C a 0 (24)
The matrix B 0 can be written as :

B 0 = -K D + Ĩ (25)
with :

Ĩ = 0 0 0 I and D = D a 0 (26)
Using ?? and ??, the matrix Ω can be written as :

Ω = P Ã + ÃT P -P K C -CT KT P + Q ϕ ... ĨT P -DT KT P ... ... -P K D + P Ĩ ... -µ 2 Q ε (27)
The presence of the terms P K and -µ 2 make the inequality ?? non linear and the LMI's methods of resolution can not be used. To make linear this inequality, let us define the following changes of variables G = P K and m = µ 2 . The matrix Ω can be written as :

Ω = P Ã + ÃT P -G C -CT G T + Q ϕ ... ĨT P -DT G T ... ... -G D + P Ĩ ...
-mQ ε (28) The resolution of the inequality ?? that is now linear with regard the different unknowns leads to find the matrix P and G and the scalar m. The gain matrix K is determined via the resolution of K = P -1 G and the attenuation level is given by µ = √ m.

Example

Lets us consider the linear system described by the following matrices :

A =     -0.3 -3 -0.5 0.1 -0.7 -5 2 4 2
-0.5 -5 -0.9 -0.7 -2 1 -0.9

    , B =     1 2 5 1 4 -3 1 2     , C =     1 0 0 0 0 1 0 0 0 0 1 0 0 0 0 1     , D =     0.5 0.5 0.2 0.2 0.1 0.1 0 0.1     , E = B
The system input u(t) is defined as follows :

u(t) = u 1 (t) u 2 (t)
T where u 1 (t) is a telegraph type signal varying between zero and one and u 2 (t) is defined by u 2 (t) = 0.3 + 0.1 sin(πt). The fault f (t) is made up of two components :

f (t) = f 1 (t) f 2 (t)
T with :

f 1 = 0, t ≤ 0.6sec sin(0.5πt), t > 0.6sec , f 2 = 0, t ≤ 1sec 0.
           
The simulation results are shown in the figure ??. This method allows to estimate well the sensor faults even in the case of time-varying faults.

EXTENSION TO MULTIPLE MODEL REPRESENTATION

The objective of this part is to extend the previous proposed method to nonlinear systems represented by a multiple model.

Problem formulation

Consider the following nonlinear Takagi-Sugeno system affected by a sensor fault :

ẋ(t) = M i=1 µ i (ξ(t))(A i x(t) + B i u(t)) (29a) y(t) = Cx(t) + Ef (t) + Dw(t) (29b)
where x(t) ∈ R n represents the system state, y(t) ∈ R m is the measured output, u(t) ∈ R r is the system input, f (t) represents the fault and w(t) is the measurement noise. A i , B i and C are known constant matrices with appropriate dimensions. E and D are respectively the fault and noise distribution matrices which are assumed to be known. The scalar M represents the number of local models. The weighting functions µ i are nonlinear and depend on the decision variable ξ(t) which must be measurable. The weighting functions satisfy the sum convex property expressed in the following equations :

0 ≤ µ i (ξ(t)) ≤ 1, M i=1 µ i (ξ(t)) = 1 (30)
Let us consider the state z ∈ R p given by :

ż(t) = M i=1 µ i (ξ(t))(-Āi z(t) + Āi Cx(t) + Āi Ef (t))
(31) where -Āi , i ∈ 1, .., M are stables matrices. One introduce the augmented state X = x T z T T , this state is given by the equation (??) :

Ẋ(t) = M i=1 µ i ξ(t))(A ai X(t) + B ai u(t) + E ai f (t)) (32a) Y (t) = C a X(t) + D a w(t) (32b)
with :

A ai = A i 0 Āi C -Āi , B ai = B i 0 , E ai = 0 Āi E (33)
The matrices C a and D a are given by the equation (??). The structure of the proportional integral observer is chosen as follows :

Ẋ(t) = M i=1 µ i (ξ(t))(A ai X(t) + B ai u(t) + E ai f (t) + K i (Y (t) -Ŷ (t))) (34) f (t) = M i=1 µ i (ξ(t))(L i (Y (t) -Ŷ (t))) (35) Ŷ (t) = C a X(t) (36)
where X(t) is the estimated system state, f (t) represents the estimated fault, Ŷ (t) is the estimated output, K i are the local model proportional observer gains and L i are the local model integral gains to be computed. It is assumed that the fault affecting the system is bounded. Using the expressions of x(t) and f (t) given by the equation (??), the dynamics of the state reconstruction error is given by the computation of ẋ(t) which is written :

ẋ(t) = ẋ(t) -ẋ(t) = M i=1 µ i (ξ(t))(A ai -K i C a x(t) + E ai f (t) + K i D a w(t)) (37)
as the fault estimation error can be written :

ḟ (t) = ḟ (t) -ḟ (t) = ḟ (t) - M i=1 µ i (ξ(t))(L i C a x(t) -L i D a w(t)) (38)
Using the definitions of ϕ and ε given in (??) and omitting to denote the dependance with regard to the time t, the equations (??) and (??) can be written :

φ = A m ϕ + B m ε (39)
with :

A m = M i=1 µ i ξ Ãi and B m = M i=1 µ i ξ Bi (40)
where :

Ãi = A ai -K i C a E ai -L i C a 0 , Bi = -K i D a 0 -L i D a I (41)
The matrix I is the identity matrix with appropriate dimensions. By considering the Lyapunov function V given in (??), and following the same reasoning as for linear systems, convergence of state and fault estimation errors as well as attenuation level are guaranteed if :

ψ T Ωψ < 0 (42)
with :

ψ = ϕ ε , Ω = A T m P + P A m + Q ϕ P B m B T m P -µ 2 Q ε (43)
The inequality (??) holds if Ω < 0. The matrix A m can be written as :

A m = Ãm -Km Ca (44)
with :

Ãm = M i=1 µ i (u(t)) Ãmi , Km = M i=1 µ i (u(t)) Kmi (45)
and

Ca = C a 0 (46)
where

Kmi = K i L i and Ãmi = A ai E ai 0 0 (47)
In the same way, the matrix B m can be formulated as :

B m = -Km Da + Ĩ (48)
with :

Ĩ = 0 0 0 I et D = D a 0 (49)
With the following changes of variables G m = P Km and m = µ 2 , the matrix Ω can be put in the following form :

Ω = P Ãm + ÃT m P -G m Ca -CT a G T m + Q ϕ ... ĨT P -DT a G T m ... ... -G m Da + P Ĩ ... -mQ ε (50)
As Ω = M i=1 µ i (ξ(t))Ω i , the negativity of Ω is assured if, for i = 1...M :

Ω i < 0 (51)
with :

Ω i = P Ãmi + ÃT mi P -G i Ca -CT a G T i + Q ϕ ... ĨT P -DT a G T i ... ... -G i Da + P Ĩ ...
-mQ ε (52) and G i = P Kmi . Solving LMI's (??) leads to the determination of the matrices P and G i and the scalar m. The gain matrices are then deduced : Kmi = P -1 G i .

Example

Consider the nonlinear system described by a Takagi-Sugeno model with two local models, four states and four outputs which structure is given by the following equations :

ẋ(t) = 2 i=1 µ i (u)(A i x(t) + B i u(t)) (53a) y(t) = Cx(t) + Ef (t) + Dw(t) (53b)
The system matrices are defined as below :

A 1 =     -0.3 -3 -0.5 0.1 -0.7 -5 2 4 2
-0.5 -5 -0.9 -0.7 -2 1 -0.9

    , B 1 =     1 2 5 1 4 -3 1 2     A 2 =     -0.2 -3 -0.6 0.3 -0.6 -4 1 -0.6 3 -0.9 -7 -0.2 -0.5 -1 -2 -0.8     , B 2 =     4 6 0 0 -4 2 7 6     C =     1 0 0 0 0 1 0 0 0 0 1 0 0 0 0 1     , D =     0.5 0.5 0.2 0.2 0.1 0.1 0 0.1     , E 1 = B 1 E 2 = B 2 Considering u(t) = u 1 (t) u 2 (t) T , the signal u 1 (t)
is a telegraph type signal whose amplitude is belongs to the interval [0, 0.5]. The signal u 2 (t) is defined by u 2 (t) = 0.3 + 0.1 sin(πt).

The two fault signals

f (t) = f 1 (t) f 2 (t)
T are defined as :

f 1 = 0, t ≤ 0.6sec sin(0.5πt), t > 0.6sec ,f 2 = 0, t ≤ 1sec 0.4, t > 1sec Choosing Q ϕ = Q ǫ = I, the µ, K 1 , K 2 ,
            K 2 =             -
           
The simulation results are shown in the figures ?? and ??.

As for the previous linear case, the proposed method provides good estimates of the system state (one present the states error of estimation of system (??) and sensor faults.

CONCLUSION

This paper has presented an estimation method of sensor faults which can be, by a mathematical transformation, considered as unknown inputs to an augmented system. This reconstruction is made for linear and nonlinear system represented by a Takagi-Sugeno model. The proposed method uses a proportionnal integral observer which is able to estimate simultaneously the state of the system and the unknown inputs. Small size examples have illustrated the efficiency of the proposed approach.

Figure 1 .

 1 Figure 1. Sensor faults and their estimates .

Figure 2 .

 2 Figure 2. State reconstruction error.

Figure 3 .

 3 Figure 3. Faults and their estimate.

  4, t > 1secTo define the state z, one choose Ā = 25 * I, where I is the identity matrix. The µ, K and L computation gives : µ = 0.3317,

		and
		K =	            ... 49.140 -6.962 14.658 -8.925 -54.319 39.277 4.858 ... -2.688 -7.409 14.877 2.259 ... -2.567 -12.062 16.080 2.343 ... -1.704 10.346 -5.056 14.141 ... -0.751 -41.280 37.530 6.423 ... 5.449 15.115 1.393 ... -16.984 -3.115 -7.090 33.576 3.298 ... -9.858 1.925 -2.030 30.579 ... 3.805 1.019 ... 11.930 -3.436 3.833 0.763 ... 11.558 -3.353 3.778 ... -1.357 0.191 -1.603 -0.741 5.102 ... 38.041 -7.502 10.874 2.896 ... 22.549 -4.191 6.355 ... 3.621 4.755 3.737 -1.686 ... 7.681 6.721 -5.810 -6.283
	L =	-99.566 -31.179 -25.850 -18.090 ... -71.636 -38.768 -4.346 -34.992 ... ... -31.055 323.373 94.166 18.293 ... 86.279 44.744 -83.663 37.041

  L 1 and L 2 computation gives : µ = 1.2247, L 1 = -283.182 -121.148 74.310 -62.490 ... -345.040 -151.396 85.418 -61.771 ... ... 153.758 410.074 -5.716 63.338 ... 431.054 -96.606 -19.597 61.520

	L 2 =	-115.420 -105.768 35.048 -50.308 ... -141.015 -123.698 40.092 -49.400 ... ... 75.051 190.906 -3.992 50.902 ... 202.223 -41.755 -15.471 49.379
	K 1 =	            ... 15.166 59.843 -482.376 16.116 -166.067 12.729 -106.775 16.208 156.945 37.647 -470.569 8.187 -166.308 13.973 -78.243 -34.769 69.786 3.291 ... 3.843 0.496 ... 1.939 0.185 ... -13.356 -4.889 0.677 547.587 215.763 131.025 -350.338 69.215 ... 97.355 ... 41.211 ... 23.323 ... 530.406 95.417 ... 210.176 37.676 ... 104.622 22.092 ... -227.2868 58.444 ... 6.620 -2.133 2.505 -0.482 1.409 -0.301 4.829 1.561 ... 38.368 -2.347 5.611 ... 0.897 31.048 2.941 1.2672
		... -10.948 8.999 ... 33.251 29.593 -0.997 26.308 12.093 -1.030

  16.369 -33.252 66.898 41.566 ... -2.997 ... 4.031 12.337 2.670 -0.683 ... -2.535 5.046 -0.200 -1.937 ... 24.354 17.096 0.599 6.319

	29.702 18.084 ... 18.480 10.259 ... -32.873 84.740 -35.444 35.046 ... -11.586 -0.592 -4.653 -5.738 -23.446 -32.323 67.143 39.703 ... 26.598 15.452 ... -13.176 -3.498 0.306 25.970 10.024 ... -4.670 -49.221 46.993 -16.385 33.501 ... ... 13.788 4.941 6.121 -5.722 ... 4.862 1.629 2.405 -2.268 ... 2.675 0.908 1.364 -1.309 ... 3.369 1.273 2.063 -1.122 ... 21.968 1.427 5.201