Olivier Bouissou
email: olivier.bouissou@cea.fr

Matthieu Martel
email: matthieu.martel@univ-perp.fr

A Hybrid Denotational Semantics for Hybrid Systems

In this article, we present a model and a denotational semantics for hybrid systems. Our model is designed to be used for the verification of large, existing embedded applications. The discrete part is modeled by a program written in an extension of an imperative language and the continuous part is modeled by differential equations. We give a denotational semantics to the continuous system inspired by what is usually done for the semantics of computer programs and then we show how it merges into the semantics of the whole system. The semantics of the continuous system is computed as the fix-point of a modified Picard operator which increases the information content at each step.

Introduction

The importance and usefulness of static analysis techniques [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] for software validation is no longer to be outlined. Their application to highly critical programs has become a major challenge for many industries. Such programs are usually automatically generated, imperative programs which are embedded into a heterogeneous system. They mostly behave as follows: they capture information from the physical environment via sensors, treat this information using numerical computations and consequently modify the environment via actuators. The analysis of such programs requires either to over-approximate the physical environment, which often leads to an imprecise analysis, or to analyze the whole hybrid system made of the continuous environment and the discrete program [START_REF] Cousot | Integrating physical systems in the static analysis of embedded control software[END_REF][START_REF] Goubault | Some future challenges in the validation of control systems[END_REF]. We use this approach.

The analysis of hybrid systems requires as a starting point a formal description of their behavior. Thus, we need to give a coherent interpretation of both the discrete and the continuous subsystems. The formalization of a continuous system using the same notions as for a computer program is already a challenge of its own. The continuous variables move along a continuous function of the real time while the discrete system is defined, in a denotational semantics approach, as a function between discrete environments [START_REF] Winskel | The formal semantics of programming languages: an introduction[END_REF]. In this article, we propose a formalism for modeling hybrid systems together with a description of their behavior as a hybrid denotational semantics: the evolution of the hybrid system is a function between hybrid environments (i.e. containing a discrete and a continuous part) and this function is computed as the least fix-point of a sequence of approximations.

Our model for hybrid systems is designed for an implementation level and ensures a clear separation of the discrete and the continuous subsystems. They are actually modeled in two different formalisms (see Section 3.1 and 3.2) which allows of the analysis of one program within various environments for example. Despite this heterogeneity, we give a unique description of the behavior of the hybrid system. To build the hybrid semantics of the whole system, we first give a coherent description of both parts. As a first step, we suppose that the discrete part is completely determined and we give a semantics κ for the continuous part (Section 4). It is computed as the fix-point of an operator Γ which acts on partially defined functions and we show that this fix-point is actually the limit of Tarski's iterates [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF]. Then, we suppose that the continuous part is perfectly known and we define a denotational semantics ∆ for the discrete part only (Section 5). For this, we add to the standard semantics of imperative languages denotations for some hybrid actions that represent sensors and actuators. Finally, we define the semantics Ω H of the hybrid systems as a combination of both discrete and continuous semantics (Section 6).

Running Example

We will illustrate this article with a simplified version of the well-known two tanks problem [START_REF] Kowalewski | A case study in tool-aided analysis of discretely controlled continuous systems: the two tanks problem[END_REF]. The system consists of one water tank (see Figure 1.1) which is filled by a constant flow i and which has two evacuation tubes: one at the bottom and one at height h. The evacuation tube at the bottom has a valve v which can be open or closed. The continuous system is the height x of the water in the tank, whose evolution is governed by the ordinary differential equation of Figure 1(b) and the discrete part is a controller whose goal is to maintain x between safe bounds by closing/opening the valve. A model of this system using hybrid automata requires 4 states: one for each possible equation for x. The switches between these 4 states have two natures: either they are directed by the discrete system (the valve is turned off/on), or by the continuous system (x becomes bigger/lower than h).

Related Work

The modeling of hybrid systems with hybrid automata was initiated by Henzinger [START_REF] Henzinger | The theory of hybrid automata[END_REF] as an extension of timed automata [START_REF] Alur | A theory of timed automata[END_REF]. They are finite state automata to which we add at each location a flow equation describing the continuous dynamics at this point. Their operational semantics was introduced in the early papers and their analysis using model checking techniques has been well studied, either for linear [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF] or non-linear [START_REF] Henzinger | Algorithmic analysis of nonlinear hybrid systems[END_REF] cases. A denotational semantics for these models was recently proposed by Edalat [START_REF] Edalat | Denotational Semantics of Hybrid Automata[END_REF] and proved to be equivalent with the operational semantics. Since the first results, many models for hybrid systems and verification methods were proposed. These include hybrid process algebra like HyPa [START_REF] Cuijpers | Hybrid process algebra[END_REF] or Hybrid Chi [START_REF] Van Beek | Syntax and consistent equation semantics of hybrid chi[END_REF]. Meanwhile, Hybrid-CC [START_REF] Gupta | Computing with continuous change[END_REF] introduced hybrid components to the concurrent constraints theory. All these models are generally used as high level abstract formalisms to reason about the principles of hybrid systems. However, when the verification of industrial size, critical systems is at stake, they are not fully sufficient. First, for safety reasons, the analysis of the embedded source code is always necessary. Secondly, for industrial size problems, it is necessary to have a clear distinction between discrete and continuous states to allow the modeling process of the both parts to be executed by different engineers. Most of the models we cited are not well-suited for these requirements, although some advances have been made for the separation issue [START_REF] Alur | Modular specification of hybrid systems in charon[END_REF].

On the other hand, hybrid systems may be seen as switched, dynamical systems, i.e. continuous systems whose dynamics changes in some regions [START_REF] Liberzon | Switching in Systems and Control[END_REF]. In this formalism, the discrete part is very limited and the question of the stability of the system [START_REF] Branicky | Multiple lyapunov functions and other analysis tools for switched and hybrid systems[END_REF] is of great importance, while the verification is often done via successive simulations [START_REF] Girard | Verification using simulation[END_REF]. The behavior of such systems is however not always formally defined, although some advances in that direction have recently been made [START_REF] Zheng | Operational Semantics of Hybrid Systems[END_REF].

The main difficulty in the formalization of hybrid systems is to give a coherent interpretation of the continuous and the discrete parts. Edalat et al. proposed a formalization of differential calculus and of the solution of differential equations in the theory of Scott domains, both for the mono-variate [START_REF] Edalat | Domain theory and differential calculus[END_REF] and multi-variate [START_REF] Edalat | A computational model for multi-variable differential calculus[END_REF] cases. Their theory was one of the main starting points for this work and we use some of their results here.

Notations

In the rest of the article, we will write R for the set of real numbers, R + for the set of non-negative real numbers and N denotes the natural integers. For two elements a ≤ b of a domain, we write [a, b] the interval containing all elements a ≤ x ≤ b. The set of all intervals over R (resp. R + ) will be denoted I(R) (resp. I(R + )). For i ∈ I(R), we write i -is lower bound and i + its upper bound. We define its width w(i) = i +i -and its midpoint mid(i) = i + +i - 2 . We will denote F the set of floatting point numbers and for a given real number x ∈ R, we will write ↑ ∼ (x) the closest floatting point number. This casting operation from real to floating point numbers will be necessary for the semantics of sensors that transform a real variable (the physical value) into a floating point one (the discrete measurement).

(a) Scheme. ẋ = 8 > > < > > : i -k1 √ x -k2 √ x -h if x ≥ h and v open i -k2 √ x -h if x ≥ h and v closed i -k1 √ x if x ≤ h and v open i otherwise (b) Continuous System.

Basics of Differential Equations Theory

In this Section, we present the basic notions of differential equations theory that are necessary for the understanding of this paper. They are not much explained, we invite the curious reader to refer to any differential equations book (for example [START_REF] Ince | Ordinary Differential Equations[END_REF]) for more details.

Definition 1 (Ordinary Differential Equation). Let y be a vector-valued function of the positive real variable t, y : R + → R d . Let y (i) be its i th derivative in t. Then, an ordinary differential equation (ODE) of order n and dimension d is a relation of the form F y, y (1) , . . . , y (n-1) , t = y (n) . The properties of the function F define the properties of the solution of the ODE. When the function F does not depend on t, the ODE is said to be autonomous.

ODEs of dimension 1 are particularly important and we are used to writing them ẏ = F (y, t), where ẏ = y (1) .

Proposition 1. Every differential equation of dimension d and order n is equivalent to an ODE of order 1 and dimension d + n.

Proof. We introduce an auxiliary variable y i for the ith derivative of y, such that ẏi = y i+1 . Then, the ODE is equivalent to the ODE of order one ż = g(z) where z = (y, y 1 , . . . , y n , t) T and g(z) = (y 1 , . . . , y n-1 , F (t, y, y 1 , . . . , y n-1 ), t) T .

Thus, from now on, we will only consider ordinary differential equations of order 1. For the simplicity of the presentation, we will limit this paper to ODEs of dimension 1. All the results we present can be easily extended to ODEs of arbitrary dimension (and thus differential equations of any order). An initial value problem (IVP) is an ODE ẏ = F (y, t) together with an initial condition y(t 0 ) = y 0 . We write it:

ẏ = F (y, t), y(t 0 ) = y 0 (1)
Depending on the function F and the initial condition, the behavior of the implicitly defined function y varies a lot: it may exist on a small open interval around t 0 , on the whole real line or not exist at all. Let us recall some results which give conditions for the existence and uniqueness of solutions to Equation (1). 1) is (at least locally) guaranteed.

Theorem 1 (Existence and uniqueness theorem). If the function F is locally Lipschitz in y on a neighborhood of (y 0 , t 0 ), then the IVP has a unique maximal solution around t 0 . If F is globally Lipschitz on R, then the IVP has a unique solution on R.

Theorem 1 is very important as Lipschitz functions are common. The most interesting part of the theorem is without doubt its proof, as it proves the existence and uniqueness of the solution using a fix-point argument (in the sense of Banach's fix-point theory). The solution is constructed as the fix-point of the Picard operator [START_REF] Ince | Ordinary Differential Equations[END_REF] defined for an interval I ∈ I(R), a continuous function F and an initial condition y 0 ∈ R by:

P I F, y 0 : C 0 I → C 0 I f → λx.y 0 + x I -F (f (s), s)ds (2)
where

C 0 I
∀t ∈ (a, b), f (t) = y 0 + t a F (f (s), s)ds. (3)
Theorem 2 (Convergence of the Picard iterates). If F is globally Lipschitz on R, the Picard iterates defined by: Proposition 2 gives a characterization of solutions of the IVP as solutions of a fix-point equation in the sense of Banach's fix-point theory. Theorem 2 shows that this fix-point can be computed as the limit of the iterates of a contracting operator. Let us note that the convergence of the iterates is very quick: if we start two iterations with two functions f 0 and f0 , then we have for all n ∈ N and t ∈ [a, b]:

f 0 ∈ C 0 ([a, b]), f n+1 = P [a,b] F, y 0 (f n ) converge uniformly
|f n (t) -fn (t)| ≤ K.
k n (tt 0 ) n n! where K is a constant and k is the Lipschitz-constant of F .

Our Model for Hybrid Systems

In this Section, we present our model for hybrid systems. This model is designed for large, embedded, safety critical applications and is designed for being used at an implementation level, i.e. we want to analyze the programs that will actually be embedded. These programs continuously interact with their environment via sensors and actuators, the activity of which has thus to be carefully modeled. Our objectives for this new model are the following:

1. The discrete part remains close to existing embedded software. 2. The action of sensors and actuators is clearly identified. 3. Continuous and discrete systems are modeled separately.

The last requirement is necessary for two reasons. First, if we want to analyze the behavior of a controller in different physical environments without having to rewrite the entire system, the distinction between the plant (i.e. the discrete part) and the environment must be clear. Secondly, for existing industrial applications, the discrete part (i.e. the program) is already written, so we want a description of the hybrid systems that can use this program "as it is". An obvious solution would consist of building a cartesian product between the continuous states and the states of the program. For combinatorial reasons, our approach consists of first describing a model for continuous subsystems (Section 3.1) and then a model for discrete subsystems (Section 3.2).

Model for the Continuous Subsystem

The continuous part contains variables evolving continuously with time such as the water height in the tank or the temperature of the air. Their evolution is usually described by an ordinary differential equation; for example, the temperature x of a room with a heater is given by an ODE like ẋ = 5 -0.1x. Let κ be the continuous model, its expressiveness depends on the set of functions F that we allow inside Equation [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]. We need to capture two phenomena: a change in the dynamics due to the environment itself and a change due to the discrete program. The first arises for example when the water passes above the tube (see Equation ( 4)) while the second appears when the valve is closed.

To capture the changes induced by the discrete system via actuators, we allow the function F to have boolean parameters. Thus, we will have

F = F (y, t, k),
where k is a vector of boolean values. We write F k (y, t) = F (y, t, k) for every possible value of k. To capture the changes induced by the environment itself, we let each F k be a continuous, piecewise Lipschitz function, as on Figure 3.1. Thus, F k behaves differently in different regions of the space, which is precisely the kind of changes we wanted to model. We recall that a function g is piecewise Lipschitz if there exist finitely many real numbers x 0 < x 1 < • • • < x n such that the restriction of g to [x i , x i+1 ] is Lipschitz. The theory of differential equations remain unchanged with such functions, except that the solutions are now continuous but only piecewise differentiable functions. Especially, the Picard iterates still converge uniformly on every interval. The continuous model κ is a triple κ = (F, F k k∈k , y 0 ) where F k k∈k is the set of possible modes. We write F k for F k k∈k . F is the function defining the IVP and is such that there exists t 0 < t 1 < • • • < t n < . . . such that the restriction of F to [t i , t i+1 ] is equal to one of the F k . The model representing the evolution of the liquid height in the one-tank system is (F, {F 0 , F 1 }, y 0 ) where (F 0 , F 1 ) are given by Equation (4).

F k (x) =  i -k * k1 √ x -k2 √ x -h if x ≥ h i -k * k1 √ x otherwise (4)
Let us make a parallel between this model and a computer program as the representation of a dynamical system. A source code is a model for a discrete dynamical system: the compiled binary program. Every instruction explains how the state of the system varies from instant t (the current instruction) to instant t + 1 (the next one). For a continuous function, the ODE plays that role: it links the state of the system at time t+dt with the state of the system at time t via its derivatives. So, it is natural to consider an ODE as a program for continuously varying systems.

stmt := v = exp| if(bool) then stmt elsestmt | while(bool) stmt | stmt;stmt | hyb stmt exp := c | exp+exp | exp-exp | exp*exp ... bool := v<exp | v>exp | bool∨bool | ... hyb stmt := sens.y?x | act.k!c | wait c
Table 1. Statements for the discrete system.

Model for the Discrete Subsystem

We want the discrete model ∆ to remain close to existing embedded software in order to be used for large critical applications. We thus start with a set of standard statements which are common to any imperative language (stmt in Table 1). We have assignements, if statements, while loops, arithmetic and boolean expressions. This core language can be extended to more complex statements without perturbing the semantics of the hybrid system as they represent purely discrete actions.

In addition to standard statements, we have three hybrid actions:

-sens to model the sensors. The action of sens.y?x is to bind the variable x to the value of the continuous variable y at the time the action is executed, -act to model the actuators. The action of act.k!c is to change the continuous dynamics by choosing the function F c among all the possible dynamics {F k }, -wait to model the passing of time. We suppose that all discrete and hybrid actions are instantaneous and we model the fact that they were not by explicitly adding these wait statements. The effect of wait c is to move time forward by c seconds.

This formalism is very close to existing imperative languages and, in most cases, the generated programs already contain, as comments, the hybrid statements. For example, the loops of embedded industrial programs are usually precisely cadenced and we often see in the codes comments indicating their frequency such as "this loop runs at 8kHz". Thus, adding a wait command at the end of the loop to model its cadence is easy. Clearly, every program that uses data sampling must know the sampling rate to ensure the meaning of the data given by the sensor. It is thus reasonable to assume that we know the cadence of the incoming data. Using this syntax, we can write a controller for the one tank system that measures the height x of the water with a sensor and open the valve if x is too high (see Listing 1). We suppose that the closing operation takes two seconds, so the controller must predict (using for example linear interpolation) the height of the water two seconds later (this is the role of the function anticipate) and starts the closing if this predicted value is too high.

This model for hybrid systems conforms to our three requirements:

1. Modeling the discrete system requires few additions to existing programs. 2. Sensors and actuators are clearly modeled.

3. Continuous and discrete systems are modeled using two different formalisms.

Moreover, we designed it so that it prohibits impossible phenomena like contuous state jumps or Zeno effects. Actually, time is driven by the discrete subsystem through the wait statements, thus there must exist a minimum time between two mode switchings (because the program is finite), which prohibits Zeno phenomena.

Let us now give a formal, denotational semantics for this model of hybrid systems. The semantics is defined separately for the continuous (Section 4) and the discrete (Section 5) systems and both are then joined to define the semantics for the complete, hybrid system. We define the semantics of the continuous system with the assumption that the discrete system is fully known and viceversa for the discrete part. This allows of several simplifications when specifying both parts, those simplifications are then removed by the semantics of the whole system.

Continuous Semantics

In this section, we give a formal, denotational semantics of the continuous model. Let us recall that the continuous part of an hybrid system is represented as κ = F, F k , y 0 ) where F k is a family of piecewise Lipschitz continuous functions and y 0 ∈ R is the initial condition (we suppose t 0 = 0). Each F k is supposed to be globally α-Lipschitz on R, so that there exists a unique maximal solution on R (as defined in Section 2) to each ODE ẏ = F k (y, t). Our goal is to have a coherent formalism for describing both the continuous and the discrete part of the hybrid system. We first give the intuition for this semantics (Section 4.1) and then we describe in detail the lattice structure that we manipulate (Section 4.2) and the computation of the semantics as a fix-point (Section 4.3).

Intuitive Idea of the Semantics

In an analogy with standard denotational semantics, we want to express the semantics of κ as a function mapping an initial environment to a final value. If we know the behavior of the discrete part of the system, we know the times at which the parameters k ∈ k switch. Thus, we know completely the function F and the semantics of κ maps an initial value to the semantics of the IVP ẏ = F (y, t), y(0) = y 0 (5)

Basically, the semantics of the IVP is its maximal solution, i.e. a piecewise differentiable, continuous function y : R + → R which satisfies [START_REF] Bouissou | GRKLib: a guaranteed runge-kutta library[END_REF]. Thus, the semantics of κ is a function κ mapping an initial environment (i.e. the initially available information y) to the solution of the IVP. This is very close to the denotational semantics of a program which is a function mapping the environment before the execution of the program with the environment at the end. This is very comparable to the semantics of a computer program. Actually, the most concrete semantics of a computer program is a (potentially infinite) sequence (l i , v i ) where l i ∈ L is a set of unique labels and v i is the value of the variables of the program at the label l i . A label represent a single point in the execution of the program and are linked to the usual notion of control points: they represent the control points once all the loops have been unrolled and the different instructions differentiated. It is thus a function from the discrete set of labels L to the domain V of the variable values. The main aspects of this formalism are:

1. clear separation of all the control points. 2. there is a countable number of labels. 3. the value of the variable at some label l i only depends on the value of the variables at the previous labels.

The computation of the sequence (l i , v i ) generally requires the computation of the least fix point of some monotone operator on a complete lattice [START_REF] Winskel | The formal semantics of programming languages: an introduction[END_REF]. This fix-point computation corresponds to upgrading the already computed values, i.e. updating the available information. Generally, the operator takes the already computed sequence `(l0, v0), • • • , (ln, vn) ´and extends it to the right, i.e. returns

`(l0, v0), • • • , (ln+1, vn+1)
´.

The semantics of a continuous model κ, i.e. the solution of the corresponding IVP, is a function from an infinite set of labels (R + ) to the domain R. It thus respects points 1 and 3 of the trace semantics of a computer program. Clearly, point 2 is no longer valid as we jumped from a discrete to a continuous world.

The computation of κ (y) requires the computation of a fix-point, in the sense of Banach's fix-point theory, as shown by Theorem 2. We translate this fix-point computation into Tarski's fix-point theory and compute κ (y) as the fix-point of an operator Γ . Then, we prove this is the supremum of the iterates Γ n (⊥). Γ is defined on elements with partial information and it updates them by increasing their information content. Our notion of partial information is the following: a function has only partial information if it is defined on a finite interval [0, X] for some X ∈ R + and its value at each point is bounded, i.e. is an interval. Thus, the maximal elements are the real-valued functions defined on R + and our semantics will construct one of these (the solution of (5)) as the limit of an approximations sequence, each approximation being a partially defined, interval-valued function.

The Lattice of Interval-Valued Functions

We now define the set of partially defined, interval-valued functions, i.e. continuous functions with only partial information. We also define an order and shows that this order provides a lattice structure.

Definition 4 (Partial, interval-valued functions). Let X be a non negative real number. IF X is the set of interval-valued functions defined on [0, X]:

IF X = {f : [0, X] → I(R)}
For such a function, we define its upper f + and lower f -functions as the two real-valued functions such that ∀x ∈ [0, X], f

(x) = [f -(x), f + (x)].
When f -(respectively f + ) is right-continuous (respectively left-continuous), f is (Scott) continuous and write IF 0 X the set of all continuous, partial, intervalvalued functions. We recall that a function f is right-continuous if, for all x, we have lim t→x,t>x f (t) = f (x), i.e. if t tends toward x from above, f (t) tends toward f (x); the left-continuity is the opposite. We provide the set IF 0 X with a complete partial order structure with the pointwise reverse order:

f ⊑ X g ⇔ ∀x ∈ [0, X], g(x) ⊆ f (x) (6)
This order means that at every point in [0, X], g is more informative than f . Clearly, (IF 0 X , ⊑ X ) is a CPO (actually, it is a continuous Scott domain [START_REF] Edalat | Domain theory and differential calculus[END_REF]). The left-(resp. right) continuity of f + (resp. f -) is a necessary condition for f to be Scott-continuous [START_REF] Edalat | Domain theory and differential calculus[END_REF] and for IF 0 X to be a CPO; consider for example the piecewise linear functions

f n ∈ IF 0 1 defined by f n (x) = [0, 1] if x ∈ [0, 1 2 ], f n (x) = [0, 1 -n 2 (x -1 2 )] if x ∈ [ 1 2 , 1 2 + 1 n ] and f n (x) = [0, 1 2 ] otherwise. Clearly, the supremum f = n f n is not continuous in 1 2 , while each f n is. The right- continuity condition imposes that f + (x) = 1 for x ∈ [0, 1 2 [ and f + (x) = 1 2 for x ∈ [ 1 2 , 1]. IF 0 ∞ is the natural extension of IF 0
X to the case of interval-valued functions on R + . We now build the set of interval functions defined over arbitrary intervals of R.

Definition 5 (Arbitrary long, interval-valued functions). The set of all continuous, interval-valued functions defined over any interval [0, X] is

D 0 = X∈R+ IF 0 X ∪ IF 0 ∞ .
For f ∈ D 0 , we note X f the upper bound of its domain :

X f = sup(dom(f )). The value X f is the maximum time until which f is defined; if f is defined on R + , then X f = ∞.
Note that for all X ≥ 0, the set of continuous, real-valued functions

C 0 ([0, X]) is embedded into D 0 by the function γ : f → λx.[f (x), f (x)]
. Thus, we will identify a map f ∈ C 0 ([0, X]) with the map λx.[f (x), f (x)] and write f ∈ D 0 . We extend the order ⊑ X to D 0 by requiring that g is greater than f if it is more precise on a longer interval than f :

f ⊑ g ⇔ X f ≤ Xg and f ⊑X f g | [0,X f ] and ∀x ∈ [X f , Xg], g(x) ∈ f (X f ) ( 7
)
where g | [0,X f ] denotes the restriction of g to [0, X f ]. This order may be seen as a flexible prefix order: g is greater than f if it extends it, in a coherent way. Figure 4.1 gives an example of comparable functions (left, the dark one being bigger than the light one) and an example of incomparable functions (right). The third hypothesis in Equation ( 7) states that g remains bounded by the last value of f on [X f , X g ]. It is necessary for D 0 to be a CPO: in any increasing chain f n , the functions f + n and f - n are bounded, thus (f - n ) is a bounded increasing sequence (with respect to the pointwise order for real-valued functions), so it has a limit f -. Equivalently, (f + n ) has a limit f + , which proves the existence of

n f n = [f -, f + ].
We extend (D 0 , ⊑) with a bottom ⊥ and a top ⊤ element such that ∀f ∈ D 0 , ⊥ ⊑ f ⊑ ⊤. We also define the join and meet operators ⊔ and ⊓ as follows. Let f, g ∈ D 0 , with X f ≤ X g . Then, f ⊔ g ∈ IF 0

Xg and f ⊓ g ∈ IF 0 X f are defined by: Proof. Each underlying set IF 0 X is a continuous Scott domain (see [START_REF] Edalat | Domain theory and differential calculus[END_REF] for a complete proof of that). Our extended order was specially designed so that it preserves this structure (see discussion of Equation ( 7)). Thus, D 0 is a directed CPO. We need to prove that ⊔ and ⊓ do define a join and a meet operator to prove that D 0 is a lattice. We prove that ⊔ is a join. Let f, g ∈ D 0 with X f ≤ X g , and let h = f ⊔ g. Let us suppose that h = ⊤. We have:

f ⊔ g(x) =  f (x) ∩ g(x) if x ∈ [0, X f ] f (X) ∩ g(x) otherwise f ⊓ g(x) = f (x) ∪ g(x) (

This definition of

f ⊔ g that ∀x ∈ [0, X f ], f (x) ∩ g(x) = ∅. If this is not true, f ⊔ g = ⊤.
X h = max(X f , X g ), so X h ≥ X f . Let now x ∈ [0, X h ], then if x ∈ [0, X f ], h(x) = f (x) ∩ g(x), so h(x) ⊆ f (x), and if x ∈ [X f , X h ], h(x) = f (X f ) ∩ g(x), so h(x) ⊆ f (X f ). So, we have f ⊑ h. Equivalently, g ⊑ h. Let now h ′ be such that f ⊑ h ′ and g ⊑ h ′ , with h ′ = ⊤. We have X h ′ ≥ X f and X h ′ ≥ X g , so X h ′ ≥ X h . Let now x ∈ [0, X h ′ ]: if x ∈ [0, X f ], then h ′ (x) ∈ f (x) and h ′ (x) ∈ g(x) so h ′ (x) ∈ h(x); if x ∈ [X f , X g ], h ′ (x) ∈ f (X f ) and h ′ (x) ∈ g(x) so h ′ (x) ∈ h(x); if x ∈ [X g , X h ′ ], h ′ (x) ∈ f (X f ) and h ′ (x) ∈ g(X g ), so h ′ (x) ∈ f (X f ) ∩ g(X g ) = h(X h )
. So, we have h ⊑ h ′ , so ⊔ is a join. Equivalently, we can prove that ⊓ is a meet, so D 0 is a lattice.

⊓ ⊔

Let us remark that D 0 is a lattice and a CPO, so every increasing chain does have a supremum. It is however not a complete lattice as there exist infinite sequences without supremum. For example, let us consider the sequence of functions

ϕ n ∈ IF 0 1-1 n defined by ϕ n (x) = [-1 1-x , 1 1-x ].
Clearly, this sequence does not have a supremum in D 0 except ⊤, while there are infinitely many f ∈ D 0 greater than f n for all n (for example, the constant function with value 0). This lattice is a set of approximate functions, in the sense that a function f ∈ D 0 only has partial information. We will extend and update these functions in order to get to the solution of Equation ( 5). We thus need to define some basic operations on D 0 that adapt the classical operations on real-valued functions. The arithmetic operators +, -, * , / are defined as an extension of the interval arithmetic. For ⊙ ∈ {+, -, * , /} and f, g

∈ IF 0 X , we define f ⊙ g ∈ IF 0 X as ∀x ∈ [0, X], f ⊙ g(x) = {y ⊙ z | y ∈ f (x)
f ∈ IF 0 X is the function F • X f ∈ IF 0 X defined by: ∀x ∈ [0, X], (F • X f )(x) = {F (y) : y ∈ f (x)} . F • X f is well defined because F is continuous and f (x) is an interval, so F •f (x)
is an interval for all x. We naturally extend the notion of function composition to D 0 and define the operator • as:

∀F : R → R and f ∈ D 0 , F • f = F • X f f Definition 7 (Primitive). The primitive of a function f ∈ IF 0 X is I X (f ) ∈ IF 0 X defined by: ∀x ∈ [0, X], I X (f )(x) = x 0 f -(s)ds, x 0 f + (s)ds
Again, the primitive operator is extended to D 0 straightforwardly: for f ∈ D 0 , we set

I(f ) = I X f (f ) Definition 8 (Width).
The width of a function f ∈ D 0 is computed as the maximum width of all intervals f (x):

w(f ) = max x∈[0,X f ] w(f (x))
Proposition 4. The operator • is monotone and continuous. The width w is a monotone, continuous function from

(D 0 , ⊑) to ([0, ∞[, ) where x y ⇔ y ≤ x.
The proof of this proposition is straightforward: we use the monotonicity of functions with respect to set inclusion for • and we note that for two intervals i 1 , i 2 , i 1 ⊆ i 2 ⇒ w(i 2 ) ≤ w(i 1 ), thus the monotonicity of w. The primitive operator is not monotone, as it does not preserve the third condition for the order ⊑ (Equation ( 7)). However, the second condition is preserved thanks to the monotonicity of the primitive for real-valued functions.

A measurement for D 0 Among all the functions of D 0 , one is of special interest for us: y ∞ , the maximal solution of (5).We will compute it by successive approximations and thus we need a way to measure the quality of our approximation. Following Keye Martin's measure theory [START_REF] Martin | A Foundation for Computation[END_REF][START_REF] Martin | The measurement process in domain theory[END_REF], a measurement is a continuous function µ from a CPO D into the set of positive real numbers with reverse ordering: [0, ∞[ * . The measurement of an element f reveals the distance of f to the maximal elements of D, which should have measure 0. The measurement must also be coherent with the informational order on D: the more informative f , the smaller its measure. Moreover, it must be the case that if we measure that the sequence of approximation f n converges towards 0 (lim n→∞ µ(f n ) = 0), then the sequence f n does converge towards a maximal element ( n f n = f, µ(f ) = 0). For a formal definition of a measurement, we the reader to read [START_REF] Martin | A Foundation for Computation[END_REF], Chapter 2.

In our case, the maximal elements of D 0 are the real-valued functions defined on R + . These functions have a null width and an infinitely long domain of definition. Thus, a measurement must takes both aspects into account.

Definition 9 (The measurement µ). Let f ∈ D 0 . Then, its measurement is:

µ(f ) = w(f ) + 1 X f
Clearly, µ(f ) is null if and only if f is maximal, so in particular µ(y ∞ ) = 0.

Proposition 5. µ is a measurement, i.e.:

(i) it is a Scott continuous map from (D 0 , ⊑) into [0, ∞[ * .
(ii) for all f ∈ D 0 such that µ(f ) = 0 and all sequences f n ≪ f , we have

lim n→∞ µ(f n ) = 0 ⇒ ⊔ n f n = f
We recall that the far away relation f ≪ g means that for every increasing chain ϕ n with a supremum greater than g, the elements ϕ n must become greater than f at some N ∈ N.

Proof. Point (i) is a straightforward consequence of Proposition 4. The proof of point (ii) relies on two observations runs as follows. Let f ∈ D 0 be such that µ(f ) = 0 and let f n be a sequence such that ∀ ∈ N, f n ≪ f and lim n→∞ µ(f n ) = 0. As f n ≪ f , it is true that f n ⊑ f ; moreover, it holds that lim n (X fn ) = ∞ and lim n w(f n ) = 0. Let now x ∈ R + ; there exists N ∈ N such that X fN ≥ x, and ∀n ≥ N , we have f (x) ∈ f n (x). In addition, lim n w(f n (x)) = 0, so the sequence of intervals f n (x) converges toward the singleton f (x), and always contain f (x). So, lim n f - n (x) = lim n f + n (x) = f (x) and consequently n f n = f . ⊓ ⊔

Let us recall the results of this Section. We have built a lattice D 0 and defined three operators on it: I, • and w. Furthermore, we have a measurement µ on D 0 which characterizes the maximal elements of D 0 , i.e. the real-valued functions defined on R + . This measurement will be used as follows: the semantics κ of the continuous model is defined as the fix-point of an operator Γ F,y0 on D 0 (see Section 4.3) and this operator is such that the iterates f n = Γ n F,y0 (⊥) verify f n ≪ y ∞ and lim n µ(f n ) = 0. By the definition of the measurement, we conclude that f n = y ∞ . This intuition is formalized in the next section.

The Semantics

The denotational semantics κ of a continuous model κ is a function mapping an initial state y ∈ D 0 to the solution of Equation [START_REF] Bouissou | GRKLib: a guaranteed runge-kutta library[END_REF]. κ (y) is computed as the least fix-point of the operator Γ F,y0 : D 0 → D 0 . This operator acts as follows: given some partial information (i.e. a function f ∈ IF 0 X ), it first updates the available information by bringing each f (x) closer to y ∞ (x) and then it extends the function to the right by assigning a value to f (x) for x ∈ [X, X + 1]. The first step uses an iteration of the Picard operator (Equation ( 2)) while the second step the function in such a way that if f encloses the solution at X, then the extension encloses y ∞ on [X, X + 1]. This is possible because F is α-Lipschitz, so y ∞ cannot grow faster than e αx . We recall that the Picard operator is defined as

P [0,X f ] `F, y0 ´(f ) = λx.y0 + Z x 0 F (f (s))ds = y0 + I(F • f ).
Let us now give the formal definition of κ .

Definition 10 (Updating operator ). Let f ∈ D 0 , we suppose X f < ∞. Let F be a continuous, globally α-Lipschitz function and An example of the effect of Γ F,y0 on a partial function is shown on Figure 4.3. The black line represents y ∞ ; the left part of the figure shows the updating mechanism, while the right part is the extension. The operator Γ F,y0 is not monotone on D 0 , but we know that it has a fix-point: y ∞ . We will show in the following that this fix-point can be computed as the supremum of the Γ F,y0 iterates, i.e. y ∞ = n Γ n F,y0 (⊥).

y 0 ∈ R. Then, Γ F,y0 (f ) ∈ IF 0 X f +1 is defined by: ΓF,y 0 (f )(x) = 8 > < > : P [0,X f ] `F, y0 ´(f )(x) if x ≤ X f J + F (J) * [-e α , e α ] * (x -X), with J = P [0,X f ] `F, y0 ´(f )(X) otherwise If f ∈ IF 0 ∞ , Γ F,y0 (f ) = P [0,∞[ F, y 0 (f ). Γ F,y0 (
Proposition 6. Let f ∈ IF 0 X . Γ F,y0 verifies the invariant: ∀x ∈ [0, X], y∞(x) ∈ f (x) ⇒ ∀x ∈ [0, X + 1], y∞(x) ∈ ΓF,y 0 (f )(x) Proof. Let f ∈ D 0 be such that ∀x ∈ [0, X f ], y ∞ (x) ∈ f (x). Let f ′ = γ F,y0 (f ) and x ∈ [0, X f + 1]. If x ∈ [0, X f ], we have f ′ (x) = P [0,X f ] (F, y 0 )(f )(x). Clearly, P [0,X f ] (F, y 0 ) is monotone, so P [0,X f ] (F, y 0 )(y ∞ )(x) ⊆ P [0,X f ] (F, y 0 )(f )(x) and y ∞ is a fixpoint of the Picard operator, so y inf ty (x) ∈ f ′ (x). Now, if x ∈ [X f , X f ′ ], we know that as F is k-Lipschitz, it holds that y∞(t) -y∞(t0) ≤ e k.|t-t 0 | .F (y∞(t0)).(t -t0)
for all t, t . If we apply this to t 0 = X f and t = X f ′ , we have y

∞ (t 0 ) ∈ P [0,X f ] (F, y 0 )(f )(X f ) and we thus get that f ∞ (x) ∈ f ′ (x). ⊓ ⊔
The iterates f n+1 = Γ F,y0 (f n ), starting from f 0 = ⊥, form a sequence of approximation of y ∞ : they enclose it and their width converge toward 0.

(f ) = n Γ n F,y0 (f )
. We now give the main result of this Section. Theorem 3. The solution y ∞ of (5) is a fix-point of Γ F,y0 and

κ (⊥) = F ix(Γ F,y0 ) = n Γ n F,y0 (⊥) = y ∞ .
Proof. By induction on n, we show that ∀n,

f n ∈ IF 0 [0,n] and ∀x ∈ [0, n], y ∞ (x) ∈ f n (x).
Based on that we prove that f n ≪ y ∞ . Next, we must prove that lim n→∞ µ(f n ) = 0. Clearly, lim 1 X fn = 0, so we must prove that lim w(f n ) = 0. Let x ∈ R + , we prove that lim w(f n (x)) = 0 using the property of the Picard iterates (Theorem 2). Thus, for all x ∈ R + , w(f n (x)) tends toward 0, so lim n w(f n ) = 0.

Discrete Semantics

We now give a denotational semantics of the discrete subsystem ∆. We recall that ∆ is an imperative program to which some hybrid actions (sens, act and wait) were In this section, we suppose that the semantics of the continuous system is already computed, i.e. we know exactly the solutions of each IVP ẏ = F k (y), y(t 0 ) = y 0 for each possible dynamics F k and each initial condition (t 0 , y 0 ). These solutions are ẏ = F k (y), y(t 0 ) = y 0 (⊥), i.e. the semantics of the corresponding continuous system. The semantics of the discrete program ∆ is given as a denotational semantics, i.e. a function ∆ : Σ → Σ between environments. The environments bind every variable with its value, but also carry information about time. Actually, it is important to know the absolute time at which an instruction is executed, as the denotation of sens or act action strongly depend on it. We first present the environments that we consider (Section 5.1), then the effect of discrete statements on them (Section 5.2) and finally the effect of hybrid actions (Section 5.3).

The Environments

Let V ar be the set of all variables of the program and V al be the set of values that these variables may take. For example, V al may be the set of floatingpoint numbers. We suppose that there exist two extra variables time, y ∈ V ar that represent respectively the continuous time and the continuous environment. An environment σ binds every variable with a value, as well as it binds time with a positive real number and y with a continuous function. The set of all environments is:

Σ = V ar → V al * {time} → R + * y : R + → R .
For σ ∈ Σ, we denote σ.x the value of the variable x ∈ V ar ∪ {time, y}. Thus, the instantaneous value of the physical environment within σ is σ.y(σ.time). We also note σ[x → the environment σ where the value of the variable x has been changed to v.

Denotations of Discrete Statements

The effect of the purely discrete statements on the environments is the same as for any imperative language. We quickly present the semantics of expressions, booleans and statements. The semantics of an expression e ∈ exp is a function mapping an environment to a value: e : Σ → V al. We write the functions Σ → V al as sets of pair (σ, n) with σ ∈ Σ and n ∈ V al. Some of the denotations of expressions are given in Table 2. The semantics of a boolean b ∈ bool is a function mapping an environment to a boolean value: b : Σ → {true, f alse}. The denotations for the comparison and for the ∨ operator are shown in Table 2. Finally, the semantics of a statement s ∈ stmt is a function mapping an environment to another: s : Σ → Σ. Table 2 also presents the denotations for the statements (assignments, if, while and ; sequence).

n = {(σ, n) | ∈ Σ} x = {(σ, n) | σ ∈ Σ and n = σ.x} e1 + e2 = {(σ, n1 + n2) | (σ, n1) ∈ e1 and (σ, n2) ∈ σ} v < e = {(σ, true) : v σ < e σ} ∪ {(σ, f alse) : v σ ≥ e σ} b0 ∨ b1 = {(σ, t0 ∨ t1) | (σ, t0) ∈ b0 and (σ, t1) ∈ b2 } i1; i2 = i2 • i1 v = e = ˘(σ, σ ′ ) | σ ′ = σ [v → n] and (σ, n) ∈ e ¯ if b then i1 else i2 = ˘(σ, σ ′ ) | (σ, true) ∈ b and (σ, σ ′ ) ∈ i1 ∪ ˘(σ, σ ′ ) | (σ, f alse) ∈ b and (σ, σ ′ ) ∈ i2 ¯ while(b) inst = F ix(Γ ) with Γ (ϕ) = ˘(σ, σ ′ ) | b σ = true and (σ, σ ′ ) ϕ • inst ¯∪ {(σ, σ) | b σ = f alse} Table 2.
Denotations for discrete statements.

Denotations of Hybrid Statements

The semantics of an hybrid statement hyb stmt is a function that modifies an environment: hyb stmt : Σ → Σ. The modification is as follows:

-sens.y?x changes the value of x to floating point number closest to the value of the continuous variable y at the time the action is executed, -wait c modifies the value of the variable time and adds c to it, -act.k!c changes y so that, from the time t 0 the action is executed, it follows the solution of the ODE ẏ = F c (y). Thus, the new environment maps a time t to either the value of the previous environment (if t ≤ t 0 ) or to the solution of ẏ = F c (y), y(t 0 ) = σ.y(t 0 ) if t ≥ t 0 .

Table 3 presents the denotations for hybrid instructions with the same conventions as for pure discrete ones.

Hybrid Semantics

Let us now give the semantics of the complete hybrid system. The hybrid model is a pair Ω = ∆, κ) consisting of a model ∆ for the discrete system and a model κ for the continuous environment. These define two dynamical systems (∆ and κ) that run in parallel and, from time to time, communicate. The communication between them is of two kinds:

-data are passed from κ to ∆ via the sensors. This communication requires that both dynamical systems reached the same time before the data is exchanged. The sens actions must thus be blocking.

sens.y?x ˘(σ, σ ′ )|σ ′ = σ[x →↑ ∼ `σ.y(σ.time) ´]¯ wait c = ˘(σ, σ ′ ) | σ ′ = σ[time → σ.time + c] ¯ act.k!c =  (σ, σ ′ )|σ ′ = σ » y → λx.  σ.y(x) if x ≤ σ.time yc(x) else -ff
where yc = ẏ = Fc(y), y(σ.time) = σ.y(σ.time) (⊥) Table 3. Denotations for hybrid statements.

-orders are passed from ∆ to κ via the actuators. Indeed, the discrete system only indicates to the continuous system what its semantics will be, i.e. it chooses one of the possible functions F k . This communication needs not to be blocking as it does not affect the value of the continuous variables but only their future behavior.

The hybrid denotations for sens and act respect these observations. The semantics Ω H of Ω is a function between hybrid environments that are made of a discrete and a continuous environment. The discrete environment is altered by the discrete subsystem while the continuous one is computed only when necessary, i.e. when a sens is executed. We first define the hybrid environments, then the hybrid denotations for the discrete and hybrid statements and we finally define the semantics of the hybrid system using them.

Hybrid Environments

A hybrid environment consists of a pair made of a discrete and a continuous environment. The discrete environment σ δ binds every discrete variable v ∈ V ar to a value and the time time to a positive real value. It also contains the function F that defines the semantics of the continuous variables. This function F is piecewisely defined by the discrete program through the act statements and thus storing F is equivalent to storing the sequence of all executed act actions. The discrete environment thus completely describes the discrete program: it has both the value of the variables and the execution time, as well as the sequence of modifications brought to the continuous system. We write Σ ∆ the set of all discrete environments:

Σ∆ = ˘`V ar → V al ´ * `{time} → R+ ´ * `F : R+ × R → R ´¯.
The continuous environment σ κ contains an approximation of the physical variables y ∈ D 0 and the set of functions F k defining the continuous dynamics. These are the set of possible continuous modes that are available for the discrete program to chose. We write Σ κ the set of all continuous environments:

Σκ = ˘`y ∈ D 0 ´ * `Fk | F k : R+ × R → R ´¯.
We write Σ H the of all hybrid environments:

Σ H = 8
Σ H contains all the pairs σ δ , σ κ that are compatible, i.e. such that the function σ δ .F is made of fragments of functions from {σ κ .F k }. We write Π δ : (σ δ , σ κ ) → σ δ and Π κ : (σ δ , σ κ ) → σ κ the two projections of an hybrid environment into a discrete (resp. continuous) one. As before, we write σ δ .X the the value of a variable X ∈ V ar ∪ {time, F } in the discrete environment and σ κ .Y the value of a variable Y ∈ {y} ∪ {F k } in the continuous one.

Hybrid Denotations

The denotation of the purely discrete parts of the language are left unchanged. The denotation of numerical (resp. boolean) expressions are functions from Σ H to numerical (resp. boolean) values. These values are the ones computed by the discrete environment only (see Equation ( 9)).

exp

H (σ κ , σ δ ) = exp (σ κ ) bool H (σ κ , σ δ ) = bool (σ κ ) (9)
The denotation of a statement stmt is a function from Σ H to Σ H . Its definition is exactly the same as in the discrete case, except that the environments σ must be changed to pairs (σ δ , σ κ ) in Table 2. The denotation of a wait remains as in the discrete semantics: the time is actually controlled by the discrete subsystem that imposes the sampling rate and thus the flow of time.

The denotation of an action sens.y?x is a function from Σ H to Σ H that modifies a pair (σ δ , σ κ ) as follows: it first updates σ κ to ensure that σ κ .y has a value at time σ δ .time and then it binds x with this value in σ δ . The first step is done by applying ⌊σ δ .time + 1⌋ times the operator Γ F,y0 (see Section 4.3) to σ κ .y with F = σ δ .F and y 0 = σ κ .y(0). The first equation of Table 4 formally defines this intuition.

The denotation of an action act.k!c is a function from Σ H to Σ H that modifies a pair (σ δ , σ κ ) as follows: σ κ is left unchanged and in σ δ , the function F is modified so that it takes the value of σ κ .F c for times greater than σ δ .time. The definition of act.k!c H is given in the second equation of Table 4.

Hybrid Semantics

The semantics of the hybrid model Ω = ∆, κ) is a function between hybrid environments: Ω H : Σ H → Σ H . Ω H alters a pair σ δ , σ κ as follows. It first applies ∆ H and thus computes σ ′ δ , σ ′ κ = ∆ H σ δ , σ κ . Then, two cases occur:

sens.y?x (σ δ , σκ) = (σ ′ δ , σ ′ κ ) with ( σ ′ κ = σκ[y → Γ n σ δ .F,y (0)
`y´] -σ ′ κ = σ κ . This means that the discrete program has no effect on the environment, i.e. either there are no sens statements in it, or they have no effect on σ κ . This is the case only if σ κ .y is a fix-point of Γ F,y0 , i.e. σ δ .y = κ (σ δ .y). In this case, we have computed both the continuous semantics and the discrete one, so we set

σ ′ δ = σ δ [x →↑ ∼ `mid `σ′ κ .y(σ δ .time) ´´] where n = ⌊σ δ .time + 1⌋ act.k!c H (σ δ , σκ) = (σ ′ δ , σκ) with σ ′ δ = σ δ " F → λt,
Ω H σ δ , σ κ = σ ′ δ , σ ′ κ . -σ ′ κ = σ κ .
The program has modified the environment and thus brought σ δ .y closer to κ (σ δ .y). σ ′ δ (resp. σ ′ κ ) is only an approximation of the result of the discrete (resp. continuous) system and we must iterate the process to obtain a better approximation. We thus propagate σ ′ κ into the discrete subsystem, i.e. we apply ∆ H to σ δ , σ ′ κ and repeat the operation.

The semantics Ω H is computed as a fix-point of a function that applies ∆ consecutively until the semantics of the continuous environment has been computed. The formal definition of Ω H is given in Table 5. Let us note that Ω H is actually the only fix-point of the function Γ H just like κ was the only fix-point of Γ F,y0 in Section 4. Ω H is compatible with the discrete semantics ∆ presented in the previous section and with the continuous semantics κ presented in Section 4. The continuous environment is finally computed as the fix-point of the operator Γ F,y0 as in Section 4.3. In comparison with ∆ , the hybrid semantics reveal the hidden fix-point computations. Actually, the denotation for act in the discrete semantics (see Table 3) requires that we compute the solution of an IVP, i.e. the fix-point of an operator Γ F,y0 . These internal fix-point computations are made explicit in Table 5. Let us note that we could have chosen to place this fix-point computation inside the denotation of the sens action (i.e. y → F ix(Γ σ δ .F,y(0) ) instead of y → Γ n σ δ .F,y(0) y in Table 4). This would have been more coherent with the discrete semantics, but requires an infinite computation between the execution of two statements, which is not compatible with the standard notion of denotational semantics.

Let us note that this semantics is also compatible with the standard denotational semantics of imperative languages: if ∆ does not have any hybrid actions, then Ω H is precisely the semantics of the discrete program as defined in [START_REF] Winskel | The formal semantics of programming languages: an introduction[END_REF] for example. 5. The semantics of the hybrid system.

Ω H = F ix(Γ ) where Γ H (ϕ)(σ δ , σκ) = (σ ′ δ , σ ′ κ ) with ( σ ′ δ = Π δ ` ∆ H (σ δ , σ ′ κ ) σ′ κ = Πκ `ϕ(σ δ , σ t κ ) ´where σ t κ = Πκ ` ∆ H (σκ, σ δ ) Table

Example

To illustrate our semantics and show that it really computes the behavior of the hybrid system, let us consider a simplified version of the one-tank controller. We only consider two iterations of the while loop and don't take into account the anticipation mechanism. For the example to be significant, we suppose that the while loop had a period of one second. The program representing this simplified version is given in Figure 6.1. The continuous system is still given by Equation ( 4), with i = 2, k 1 = k 2 = 1, h = 3, h max = 2.9, and the initial value for the height of water x is x 0 = 2. We suppose that the valve is initially closed.

Let us now compute the semantics of this system. of this computation. The table is to read as follows: the left column shows the program, then each column corresponds to one iteration in the fix-point computation. For example, the second column correspond to the first computation of ∆ H on the initial environment. The first row presents the environment (σ δ , σ κ ) before the computation, the last row the environment after, i.e. ∆ H (σ δ , σ κ ). Each intermediate row represents the changes in the hybrid environment due to the corresponding statement. We notice that the continuous environment has changed during this first iteration, so we compute ∆ H another time but with an updated initial environment (second column). We get better values for the sens actions, and a new continuous environment at the end. We repeat the iteration once more (third column), which gives us a more accurate result. Let us remark that during this third iteration, the second act statement was executed, which corresponds to the real behavior of the program. So, we see that the consecutive iterations compute an ever more accurate behavior, and eventually, the real semantics (i.e. as it would have been computed in Sections 4 and 5) is reached.

Conclusion

In this article, we presented a new approach to hybrid systems that can be used for the modeling and analysis of large critical embedded programs. Our model for hybrid systems is based on a clear separation of the discrete and the continuous systems. They are described in two different formalisms: ordinary differential equations with boolean parameters for the continuous system, an imperative language with hybrid statements for the discrete part. The emphasis has been placed on making this model as unintrusive as possible for existing software, so we believe that we can effectively use it for industrial size problems. We gave a denotational semantics of this model that unifies in a coherent formalism the semantics of the continuous and the discrete parts. The main difficulty was to express the solution of an IVP as the semantics of a continuous program, i.e. the underlying ODE. In [START_REF] Edalat | Domain theory and differential calculus[END_REF], Edalat and Lieutier proposed a data type for differential calculus, we extended their results to consider the maximal solutions of IVP on R + and in an analogy with imperative languages we presented the semantics of the continuous model as a function mapping the initial condition to the maximal solution. The semantics of the subsystem is an extension of the standard denotational semantics of imperative languages, we added information on time and the continuous environment to give a denotation to the actions of sensors and actuators. The semantics of the hybrid system is a composition of these two semantics and remains coherent with them. This model for hybrid systems and especially its denotational semantics is a first step toward the validation of embedded software with their environment. The analysis of such systems using, for example, abstract interpretation techniques [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] requires two stages. First, the continuous system must be abstracted in a non-naive way. Our semantics for the continuous system already does that, as it constantly computes a partial interval-valued function that encloses the realvalued solution. This abstraction is however not computable and cannot be used for a static analyzer. The theory of guaranteed integration of ODE [START_REF] Nedialkov | Validated solutions of initial value problems for ordinary differential equations[END_REF] brings us the adequate tools for the safe abstraction of the continuous system. Validated ODE solvers [START_REF] Bouissou | GRKLib: a guaranteed runge-kutta library[END_REF][START_REF] Nedialkov | The design and implementation of an objectoriented validated ODE solver[END_REF] compute interval bounds that are proved to contain the solution. They can thus be used to construct piecewise constant interval-valued functions that enclose the solution at all time. For the analysis of the discrete part, the use of an implementation level model allows us to use existing methods (for example, the verification of the absence of run-time errors [START_REF] Cousot | The ASTRE É analyzer[END_REF] or of the numerical precision of floating point computations [START_REF] Goubault | Asserting the precision of floating-point computations: A simple abstract interpreter[END_REF]). These methods must however be completed so that they consider time. Actually, the main difficulty in the analysis of the discrete system is to carefully analyze the time at which every statement is executed (this is necessary for the sensor actions to be precise enough), but taking time into account makes it hard to find a suitable widening. This modification of standard static analysis techniques to our framework will be our main concern for future work.

Another interesting application of our approach for hybrid systems is to modify standard strictness [START_REF] Mycroft | The theory and practice of transforming call-by-need into call-byvalue[END_REF][START_REF] Mycroft | Abstract interpretation Optimizing Transformations for Applicative Programs[END_REF] or termination analysis [START_REF] Cousot | Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming[END_REF][START_REF] Berdine | Variance analyses from invariance analyses[END_REF] so that they fit to our model. This could be used to solve, in an approximate way, the reachability problem of a discrete state in a hybrid system. It is well-known that this problem is undecidable [START_REF] Henzinger | The theory of hybrid automata[END_REF] and several methods have been proposed for its simplification [START_REF] Henzinger | Algorithmic analysis of nonlinear hybrid systems[END_REF]. We believe that our approach may be efficiently used for its approximate solution as it benefits from all the static analysis based methods for programming languages.

Fig. 1 . 1 .

 11 Fig. 1.1. One Tank Example.

  on [a, b], for all intervals [a, b] of R. So, whatever the choice of the first function f 0 , if we iteratively compute f n+1 = P [a,b] F, y 0 (f n ), the sequence converges toward the solution of (1) on [a, b].

Fig. 3 . 1 .

 31 Fig. 3.1. Admissible function for an ODE.

  a) Comparable functions. (b) Incomparable functions.

Fig. 4 . 1 .

 41 Fig. 4.1. Order on partially defined functions.

Figure 4 .Fig. 4 . 2 .

 442 Fig. 4.2. Join on D 0

  and z ∈ g(x)} next define the composition, primitive and width of functions in D 0 . Definition 6 (Function composition). The composition of a continuous, real-valued function F : R → R and a partial, interval-valued function

Fig. 4 . 3 .

 43 Fig. 4.3. The updating operator (two steps).

Figure 4 .

 4 4 represent the first 3 iterates of f n when the IVP is Equation (4), with i = 2, k 1 = k 2 = 1, v open and x ≤ h. The black curve is the real solution and the gray lines represent respectively f 1 , f 2 and f 3 . The semantics of the continuous subsystem κ = F, {F k } , y 0 is the function mapping f ∈ D 0 with the least fix-point of Γ F,y0 starting from f : κ

Fig. 4 . 4 .

 44 Fig. 4.4. Example of iterations of ΓF,y 0 .

Fig. 6 . 1 .

 61 Fig. 6.1. Simplified version of the one-tank controller.

Table 6 .

 6 max) act.k!1; F → F0 F → F0 F → λt.(t <2)?F0; F1 First three iterations of the semantics computation.

  Definition 3 (Maximal solution of an ODE ). If two solutions f 1 , f 2 of the IVP (1) defined over two intervals i 1 ⊆ i 2 are equal at some t ∈ i 1 , then they are equal for all t ∈ i 1 . f 2 is then said to be an extension of f 1 . A solution of Equation (1) is said to be maximal if it cannot be extended.

	An important class of IVPs are the ones where F is (at least locally) Lipschitz
	in y. We recall that a function F : R × R + → R is globally α-Lipschitz in its first
	coordinate if for all y 1 , y 2 ∈ R, it holds that |F (y 1 , t) -F (y 2 , t)| ≤ α|y 1 -y 2 |. So,
	Lipschitz functions are functions with a bounded growth rate. For such functions,
	the existence of solutions to Equation (

Definition 2 (Solution of an IVP). A solution to the IVP (1) on the (open, semi-open or closed) interval (a, b) that contains t 0 is a continuous, continuously differentiable function f : (a, b) → R such that: ∀t ∈ (a, b), ḟ (t) = F (f (t), t) and f (t 0 ) = y 0

  Listing 1. Controller for a one-tank system.

	1 i n t main ( ) { 2 s e n s o r x ;	// s e n s o r s d e c l a r a t i o n
	3	a c t u a t o r k ;	// a c t u a t o r s d e c l a r a t i o n
	4 5	while ( t r u e ) { s e n s . x?h ;
	6	i f ( h>h max )
	7	a c t . k ! 1 ; throw ( alarm ) ;
	8	h i n 2 s e c s = a n t i c i p a t e ( h ) ;
	9	i f ( h i n 2 s e c s > h max )
	10	a c t . k ! 1 ;
	11	w a i t ( 0 . 0 1 ) ;	// d e l a y a c t i o n
	12 13 }	}

Table 4 .

 4 y. Hybrid denotations for hybrid statements.

	(	σκ.Fc(y, t) otherwise σ δ .F (y, t) if t ≤ σ δ .time	#

Table 6

 6

	shows the beginning