Marc Durand

Mechanical approach to surface tension and capillary phenomena

Many textbooks dealing with surface tension favor the thermodynamic approach (minimization of some thermodynamic potential such as free energy) over the mechanical approach (balance of forces) to describe capillary phenomena, stating that the latter is flawed and misleading. Yet, mechanical approach is more intuitive for students than free energy minimization, and does not require any knowledge of thermodynamics. In this paper we show that capillary phenomena can be unmistakably described using the mechanical approach, as long as the system on which the forces act is properly defined. After reminding the microscopic origin of a tangential tensile force at the interface, we derive the Young-Dupré equation, emphasizing that this relation should be interpreted as an interface condition at the contact line, rather than a force balance equation. This correct interpretation avoids misidentification of capillary forces acting on a given system. Moreover, we show that a reliable method to correctly identify the acting forces is to define a control volume that does not embed any contact line on its surface. Finally, as an illustration of this method, we apply the mechanical approach in a variety of ways on a classic example: the derivation of the equilibrium height of capillary rise (Jurin's law).

Surface tension and capillary phenomena encompass phenomena in which the interface between to immiscible fluids acts as a thin elastic sheet [START_REF] De Gennes | Capillarity and Wetting Phenomena: Drops, Bubbles, Pearls, Waves[END_REF] . This is a standard topic taught at the undergraduate level. Despite its apparent simplicity and its many manifestations in everyday life, this subject is not exempt from traps and misunderstandings [START_REF] Berry | [END_REF]3 .

In particular, there are two standard issues that students (and teachers) must face when addressing this topic: i) how to explain the tangential orientation of surface tension force from a microscopic perspective ? ii) How to properly identify the capillary forces acting on a given system ? In most textbooks these points are eluded, and the thermodynamic approach (minimization of suited thermodynamic potential) is favored over the mechanical approach (balance of forces) to describe capillary phenomena. In some of them students are even warned against mechanical approach, questioning the interpretation of surface tension as a force per unit length [START_REF] Champion | Properties of matter, Blackie and son limited[END_REF][START_REF] Adam | The Physics and Chemistry of Surfaces[END_REF] . However, without using the concept of a tensile force parallel to the surface, it is very difficult to explain how objects which are significantly more dense than water (e.g. a paperclip or a pin) can "float" on the water surface [START_REF] Vella | [END_REF] .

In this paper we show that capillary phenomena can be undoubtedly described using mechanical approach. Indeed, mistakes do not result from the mechanical approach per se, but rather from the ambiguity as to the delimitation of the system under study, and thus in the identification of the forces exerted on it. After reminding the microscopic origin of the tangential orientation of surface tension force, a point which is often overlooked, we derive the Young-Dupré equation which relates the contact angle to the three surface tensions at play on the contact line (the common frontier to three immiscible media), emphasizing that this relation should be interpreted as a continuity equation rather than a force balance equation. This reinterpretation eliminates many mistakes made on the identification of forces acting on the system. Moreover, we show that a safe strategy for the correct identification of acting forces consists in defining a control volume whose surface is close to the contact line but does not contain it. We can then apply the force balance on this volume control, and then stretch its surface until it touches the contact line. Finally, we illustrate this approach in a variety of ways on a standard problem: the equilibrium height of capillary rise (Jurin's law).

I. SURFACE TENSION: A FORCE TANGENT TO THE INTERFACE

A. Macroscopic perspective

We start our analysis by giving an experimental evidence that the restoring force associated with the creation of an elementary surface area between two immiscible fluids is tangent to it, without any knowledge on the microscopic origin of this force. We denote by A the area of the interface, and consider a process whereby this area undergoes a reversible change by an infinitesimal amount dA. The energetic cost associated with this process corresponds to the work to bring molecules from bulk to the interface. Assuming that the surface concentration remains constant, this work is then directly proportional to dA, and so can be written as: δW = γδA, which defines the surface tension γ between the two fluids. A detailed thermodynamic treatment shows that the surface tension is defined as a surface contribution to the grand potential Ω 7 , although the confusing term free energy is used in most textbooks and scientific papers.

To illustrate the tangential nature of the restoring force, the experimental setup sketched in Fig. 1 is commonly invoked: it consists of a U-shaped wire frame, on which is mounted a wire that can slide with negligible friction. The frame and sliding wire support a thin film 1 of liquid. Because surface tension causes the liquid surface to contract, a force F is needed to keep the slider at fixed distance l from the opposite edge. Then, the work associated with a small displacement δl = δlt of the slider (where t is the unit vector tangent to the film) is δW = F•δl = F δl. This work is also equal to the increase of surface energy, δW = 2γδA, with δA = hδl. The factor 2 reflects the two liquid-air interfaces of the film. Identifying the two expressions of δW yields F = 2γht. From the Newton's third law of motion, we conclude that the magnitude of the restoring force per unit length and per interface is γ. However, the demonstration with this experiment of the tangential orientation of the force acting on each interface is questionable: F is in fact the resultant of the forces acting on both liquid-air interfaces, which by symmetry must be tangent to the film, independently of the orientation of the force acting on each interface. A more convincing experimental evidence of the tangential nature of this force is the one shown in Fig. 2: a loop of thread is deposited on the surface of a water tank, with an arbitrary shape. Now delicately put a drop of soap on the surface circled by the thread. Immediately the loop adopts a regular circular shape, which results from the action of an isotropic force acting tangentially to the water surface on every point of the thread. Incidentally, this experience also highlights the fact that surface tension is an interfacial property that depends on the two fluids in contact: in Fig. 2(a), every elementary piece of thread experiences capillary forces from both the inner and outer surfaces, which have equal magnitude but opposite directions. In Fig. 2(b), the addition of soap decreases the magnitude of the inner tensile force, so that every piece of thread experiences a centrifugal force.

FIG. 1: Experimental evidence of the existence of a tensile force opposed to the creation of interface. The magnitude of the force is related to the surface tension γ defined as the work to create a unit surface area.

B. microscopic perspective

The molecular origin of the phenomenon of surface tension evidently lies in the intermolecular cohesive forces. The usual explanation for the origin of surface tension from a microscopic perspective is a lack (for an interface between a liquid and its vapour) or a mismatch (for an interface between two immiscible liquids) of cohesive molecular bonds, as illustrated in Figure 3, a picture which is found in most textbooks. This description yet suggests that a molecule at the interface experiences a net force oriented normally to the interface. But then why is the surface tension force oriented tangentially to it ? A misleading justification is that the competition between all molecules pushing inwards results in a macroscopic tangential force. For instance, Adamson and Gast 8 uses the mechanical analogy of a weight acting on a rope and pulley to illustrate how the normal force is converted to a tangential tension. Yet, it is not clear what part plays the role of a pulley here. Moreover, with such an argument the surface tension of a solid should be zero, since its constituents cannot freely move inwards like for a liquid.

FIG. 3: Picture found in most textbooks to illustrate the origin of surface tension. This picture wrongly suggests that a molecule at the interface experiences a force perpendicular, and not tangential, to it.

Actually, the microscopic description above is incomplete, as it considers only the static part of the molecular interactions. The full microscopic interpretation of sur-FIG. 4: Microscopic origin of surface tension: the pressure force acting surface element dS parallel to the liquid-gas interface is constant, as the decrease of its kinetic contribution is exactly compensated by its static counterpart. The pressure force acting on the surface element dS ⊥ perpendicular to the liquid-gas interface is negative in the vicinity of the interface, because the positive kinetic contribution decreases on a length scale around the interface comparable to the interatomic distance while the negative static contribution increases on a lengthscale comparable to the range of attractive interactions between molecules.

face tension has been clearly exposed by M. V. Berry 2 . We resume here his illuminating arguments. Let p (z) and p ⊥ (z) be the pressure acting on surface elements dS and dS ⊥ , centered on a distance z from the interface, and oriented parallel and normal to it, respectively (Fig. 4). By pressure, we mean here the normal component of stress acting on these surface elements. Each of these pressures has two contributions: the first is the static contribution which arises because of the interactions between molecules. It is usually negative (so this contribution is indeed a tension), because the long-range attractive interactions between molecules take over their short-range repulsive interactions. This is the contribution which is mentioned in the partial microscopic description above. The second is the kinetic contribution which comes from the transport of momentum by molecules moving across the surface because of thermal agitation, and is always positive:

p (z) = p s (z) + p k (z), p ⊥ (z) = p s ⊥ (z) + p k ⊥ (z). (1)
The kinetic pressure is the only pressure in an ideal gaz.

As its value depends only on the local number density and temperature, it is isotropic: p k (z) = p k ⊥ (z). However it is not homogeneous. If, for simplicity, one considers from now on an interface between a liquid and a gas; the kinetic pressure then continuously decreases when passing from the liquid to the gas phase. The static part, on the other hand, is strongly anisotropic when approaching the liquid-gas interface, because of the long-range character of molecular interactions: for the surface element dS , when approaching the interface, a molecule of the liquid phase interacts with fewer and fewer molecules located at the other side of the surface, because of the local density decrease. Thus, p s (z) increases from its (negative) liquid bulk value to its (slighlty negative, or zero for an ideal gas) gas bulk value when crossing the liquid-gas interface, and the increase occurs over a distance comparable to the range of a few interatomic distances. Actually, the vertical balance of forces requires that the increase of p s (z) exactly compensates the decrease of p k (z) so that the total pressure p is a positive constant p 0 , which is also the isotropic pressure far from the interface (we neglect here the pressure gradient caused by the gravity). Hence, p s , p k and p k ⊥ all three change significantly over a same spatial distance of a few intermolecular distances For the element of surface dS ⊥ , a molecule of the liquid phase still interacts with many molecules across the test surface when approaching the interface, and p s ⊥ (z) remains close to its (negative) bulk value except in the extreme vicinity of the liquid-gas interface: the increase from the liquid bulk to gas bulk value occurs on a distance much shorter than for p s (z). Therefore, there is a domain in the vicinity of the interface in which p ⊥ (z) < p 0 . The surface tension is defined as the difference between p (z) = p 0 and p ⊥ (z) integrated over all z:

γ = +∞ -∞ (p 0 -p ⊥ (z)) dz.
(

) 2
This equation simply states that a real interface can be replaced with an ideal interface where pressure is isotropic and uniform on both sides, plus a tensile force acting tangentially to the interface.

II. YOUNG-DUPR É EQUATION: AN INTER-FACE CONDITION AT THE CONTACT LINE

We now focus our attention on the Young-Dupré equation and its interpretation. When two immiscible fluids (e.g. a liquid and a gas) and a solid are brought in contact, the geometry of their connection is dictated by the Young-Dupré equation. The contact angle is conventionally defined as the angle that the liquid-gas interface makes with the solid at the contact line (the locus of points at the frontier between the three media). The Young-Dupré equation relates the contact angle θ c to the three surface tensions at play:

γ LG cos θ c + γ SL -γ SG = 0. (3)
Young-Dupré equation is a source of much confusion for the students: first, it is inevitably introduced as the balance of forces acting on the contact line. This definition is indeed quite confusing: physical forces act on material systems, not on mathematical lines. Moreover, in many textbooks the Young-Dupré equation is derived using arguments based on "free energy" minimization, and thus the support reaction R is even not mentioned or represented, yielding an unbalance of forces in the vertical direction.

Most importantly, the misinterpretation of Young-Dupré equation as a balance of forces blurs the identification of capillary forces acting on a system. To illustrate this point, consider the meniscus formed by a liquid at the vicinity of a vertical wall, as illustrated in Fig. 6. To the question what is the force exerted on the liquid-gas interface at the contact line ?, the following (wrong) answers usually come out: Answer #1: since Young's law Eq. 3 precisely expresses the balance of forces at the contact line, and the contact line is precisely located at the end of the liquid-gas interface, the net force acting at the contact line at this position is 0. Answer #2: the force acting on the liquid-gas interface at the contact line is caused by the wall. In virtue of the Newton's fundamental law of action-reaction, the exerted force must be R = -γ LG sin θ c n, where n is the unit vector normal to the wall. No one of these reasonings lead to the correct answer, which is -γ LG . To understand why in Fig. 5 four forces act on the contact line, which is at the end of the liquidgas interface, while only one must be considered to answer correctly to the question, we derive in the following the Young-Dupré equation using a mechanical approach, and emphasizing that it should be interpreted as an interface condition rather than a balance of forces on a immaterial line. This point of view will be helpful to unambiguously determine the capillary forces acting on a system.

Let us consider a control volume with square section dl×dl enclosing the contact line, as shown in Fig. 5a. For simplicity, we suppose that the geometry is invariant by translation in the direction perpendicular to the figure. The (per length) acting on this volume control can be divided in three categories:

• forces acting on the volume, like the weight ρ eff dl 2 g, where ρ eff is the effective density of the enclosed system. We express them using the generic form

ρ eff f v dl 2 .
The key point is that they scale as dl 2 .

• forces acting on the four faces: pressure is uniform in the gas and in the liquid, with respective values P 0 and P l .The pressure within the solid has two contributions: the first one, noted P s , equilibriates the pressure in the two fluids above and so its value continuously increases from P 0 in the region under the gas to P l under the liquid. The associated pressure forces acting on the contour can be expressed using the generic form i P i dl, and scale as dl 1 . The second contribution to the pressure within the solid is caused by the elastic response to the punctual normal force γ LG sin θ c n pulling on its surface. Usually surface tensions force are much weaker than the cohesive forces in the solid, and the deformations of the solid are imperceptible. Nevertheless, components of stress are finite: they spread through the solid material from the source point [START_REF] Landau | [END_REF] .

Conversely, when approaching the contact line, the stress conscentrates on a very localized zone, so its integration over segment DC tends to a constant R independent of dl.

• capillary forces γ LG , γ SL , γ SG acting tangentially to the interfaces between the liquid, gas, and solid phases. These forces also scale as dl 0 .

Application of Newton's second law yields:

i P i dl + ρ eff f v dl 2 + (γ LG + γ SL + γ SG + R) = ρ eff a cm dl 2 (4)
where the right-hand side term represents the inertia of the enclosed system; a cm is the acceleration of its center of mass. Taking this equation to the limit dl → 0 finally yields:

γ LG + γ SL + γ SG + R = 0. (5)
The vertical projection R + γ LG sin θ c = 0 simply reflects the law of action-reaction (Newton's third law). The horizontal projection of this equation yields the Young-Dupré equation (Eq. 3). This derivation is enlightening in two aspects: first, it shows that rather a balance of forces on a immaterial line, the Young-Dupré equation is an interface condition, as there exist in other domains of physics (but here at the boundary between three medias), e.g. such as the (disc)continuity of the tangential and normal components of the electric field at the interface between two media. As such, Young-Dupré equation dictates the geometry in the vicinity of the contact line: the contact angle is imposed by the values of the three surface tensions at play. Second, our derivation shows that in theory the Young-Dupré equation is not restricted to the static case; it applies to a moving contact line (with non uniform motion) as well. However, it is well documented that on real substrates the contact angle is not the same for an advancing or receding contact line, because of the surface imperfections 1 , a feature which is not captured by the Young-Dupré equation.

We now come back to the question of the force exerted on the liquid-gas interface at the contact line that we discussed at the beginning of this Section. First we can simply explain why the reasoning leading to answers #1 and #2 is wrong: in answer #1 the insidious assumption was to consider the contact line as a material part of the liquid-gas interface, and that Young-Dupré equation expresses the balance of forces on it. As we stressed out, the contact line is an immaterial line, and thus does not experience or exert forces. The fallacy in answer #2 is in considering that the system can be split in two independent subsystems: the solid wall in one hand, and the liquid and gas phases in the other hand. But this is wrong: the of two systems create new interfaces and so new capillary forces acting tangentially on them.

To answer to the initial question, let us consider a control volume Γ which encloses the liquid and gas phases, except for a thin layer at the vicinity of the wall (see Fig. 6). It is then clear that the capillary force exerted by this thin layer on the system at point M tends to -γ LG as the layer thickness decreases to 0. More generally, to avoid any mistakes in the identification of forces acting on a system containing contact lines, we recommend to define first a control volume whose surface comes sufficiently close to, but does not embed the contact lines. We illustrate this approach in the next section.

III. APPLICATION: CAPILLARY RISE (JU-RIN'S LAW)

We are now equipped to study capillary phenomena with the mechanical approach. In this section we use it to derive the expression for the equilibrium height of capillary rise, known as Jurin's law: when the lower end of a narrow tube is placed in a liquid such as water, a concave meniscus forms and the liquid climbs up to an equilibrium height h which depends on the tube radius r and the surface tension between liquid and air γ LG . The usual derivation based on thermodynamic approach is as follows: the change of surface "free energy" (grand potential, precisely) for an ascension at height h corresponds by the replacement of a solid-gaz interface by a solidliquid interface on that height: F s = (γ SL -γ SGV ) 2πrh. According to Young-Dupré equation, it can rewritten as F s = -γ LG cos θ c 2πr. The change of gravitational energy is F w = πr 2 h O ρgzdz = πr 2 ρgh 2 /2. At Equilibrium, the total free energy F tot = F s + F w must be at a minimum: dF tot /dh = 0 10 . This yields the famous Jurin's law

h = 2γ LG cos θ c ρgr . (6)
Let us now turn to the mechanical approach: the equilibrium configuration is derived from the balance of forces acting on the system. To avoid misidentification of capillary forces acting on the system, we follow the recommendation set out in Section II, and choose a control volume whose surface does not include the contact line. As a practice, we apply the force balance over various control volumes which satisfy this property, and show that they all lead to the expression (6).

FIG. 7: Derivation of Jurin's law using mechanical approach (balance of forces) on four different control volumes.

a. Control volume Γ 1 (Fig. 7a) -We first consider the axisymmetric control volume Γ 1 inside the capillary tube, whose cross-sectional area is delimited by the rectangle ABCD (see Fig. 7a). The segment AB is located just above the meniscus (i.e. at height h + with → 0), segments BC and AD inside the capillary tube, close from the walls, and segment CD at the same height as liquid level in the pool far from the capillary tube. As before, we identify the volume, surface and boundary (capillary) forces acting on this control volume: the first one is the weight of the liquid column, -ρghπr 2 e z . The pressure forces acting on segments AD and BC cancel each other by symmetry. Similarly the pressure on segments AB and CD are both equal to the atmospheric pressure P 0 and so the associated forces cancel each other. The boundary forces are the capillary forces acting tangentially all along the meniscus contour, with constant norm γ LG . Integration over that contour leads to the vertical force 2πrγ LG cos θ c e z . Finally, balance of weight and capillary forces immediately lead to Jurin's law Eq. 6.

b. Control volume Γ 2 (Fig. 7b) -We now consider the control volume Γ 2 , which is defined similarly to Γ 1 except that segment CD is located just below the meniscus, i.e. at height h -with → 0 11 . The weight of the system is then negligible. Pressure forces on segments AD and BC still cancel each other (and are also negligible in the limit → 0). As before, the resulting capillary force is equal to 2πrγ LG cos θ c e z . It is balanced by the pressure forces acting on both sides of the interface, (P CD -P AB )πr 2 e z . Incidentally, introducing the radius of curvature R of the meniscus and the geometrical relation R = r/ cos θ c , one simply recovers Laplace's law. One has P AB = P 0 , while from hydrostatic law P CD = P 0 -ρgh. Hence resulting pressure forces are -ρghπr 2 e z , and their balance with capillary forces finally leads to Jurin's law.

c. Control volume Γ 3 (Fig. 7c) -We then consider the volume control Γ 3 delimited by contour ABCD, where segment AB is just below the meniscus, segments BC and AD lie within the walls of the capillary tube, in the vicinity of the solid-liquid interface, and segments CD is positioned at the same height as the liquid level in the pool far from the capillary tube. As for the control volume Γ 1 , the weight is -ρghπr 2 e z . Pressure forces on segments AD and BC still cancel each other by symmetry, but pressure on segment AB and CD are different: P CD = P 0 , and according to Laplace law, P AB = P 0 -2γ/R, where R is the meniscus radius of curvature: R = r/ cos θ c . Capillary forces acting on segment AB are located at the solid-liquid interface and are oriented tangentially to it. Integration over the contour gives 2πrγ SL e z . This resulting force is balanced by the exact same force with opposite direction acting on seg-ment CD. Finally, Jurin's law results from the balance of weight and pressure forces.

d. Control volume Γ 4 (Fig. 7d) -Finally, we consider the volume control Γ 4 which is identical to the previous one except that now segments AD and BC are in the liquid-side of the solid-liquid interface. Weight and pressure forces remain the same, while no capillary forces act on this control volume. Hence, as in the previous case, balance of weight and pressure forces yields Jurin's law.

IV. CONCLUSION

To summarize, in this paper we discussed from a macroscopic and microscopic point of views the origin of the tangential orientation of the surface force. We then derived the Young-Dupré equation using the mechanical approach, and stressed out that it should be interpreted as a surface condition at the contact line, rather than a balance of forces: this equation dictates the geometry at the vicinity of the contact line by relating the contact angle to the three surface tension at play. This interpretation allows a proper identification of the capillary forces acting on a system, which is the primary mistake in the mechanical treatment of capillary phenomena. In particular, we stressed out that the studied system must not contain any contact line on its surface. Finally, applications of the mechanical approach using this methodology are given on a standard example: the capillary rise. We hope this work will be useful to the undergraduate students that find the mechanical approach more intuitive than the thermodynamic approach. Beyond that, this is one of the fascinating feature of physics that a same phenomenon can be described using alternative approaches. Understanding and mastering these different approaches is certainly a strength when facing new physics problems.

FIG. 2 :

 2 FIG. 2: Experimental evidence of the tangential orientation of surface tension force: (a) a loop of thread is deposited on the surface of a water tank, with arbitrary shape. By symmetry, the forces (in red) acting on both sides of a thread element cancel each other. (b) After the addition of a drop of soap on the surface of the enclosed area, the thread forms a regular circular loop, because of the unbalance of inner and outer capillary forces.

FIG. 5 :

 5 FIG. 5: Young-Dupré equation derivation obtained from Newton's second principle : a) Forces acting on a vanishing control volume surrounding the contact line. b) Young-Dupré equation is an interface condition at the contact line: it relates the contact angle θc to the three surface tensions γSG, γLG, γSL.

FIG. 6 :

 6 FIG. 6: Misconception of Young-Dupré equation: what is the force acting on the liquid-gas interface at the contact line ?

Acknowledgments I thank J. Derr and L. Viennot for many useful discussions, and the undergraduate physics students from the University of Paris whose many valuable questions have nourished this work.


Ismail Berrada

Patrick F Élix

R Castanet -P

Félix

FROM THE FEASIBILITY ANALYSIS TO REAL-TIME TEST GENERATION

Testing real-time systems is an important and not obvious step in the validation process of critical systems. This paper proposes an efficient ¡ £¢ ¤¢ ¦¥ ¨ § © algorithm for solving the feasi- bility problem corresponding to a path of length ¥ in a timed automaton, with © clocks. The given solution, combined with synchronous product, allows in particular, generating both the fastest and the slowest timed test cases for a given test purpose.

¡ 37 T © T 3W 0`¥ ! is the wanted suite

Proof. 4 : From the definition of an execution, reached values and the defini- tion 7, the suite ¡ ¢¡ ¡ ¨T ' ¥¤ © © T 3W `¥ verifies the theorem.

: If there is a suite ¡ C7 T

Introduction

The behavior of a real-time system is highly dependent on the temporal performances of target hardware platforms used for the implementation. These temporal constraints should be taken into account at the earliest stage of development process. But, we should notice the increasing implementations complexity, due to their algorithms and time constraints. Since systems must be delivered faultless, one way to increase their security is through conformance testing.

Conformance Testing

A general definition of conformance is to compare the implementation behavior with the specification one, in order to find errors. This verification consists in the definition of some test sets, their submission to the system under test (IUT), and the observation of their executions with a verdict (oracle) based on the specification, whether they are successful or not. The definition of the test set can be based on the specification (black-box), on the structure of the implementation (glass-box), or both. Usually, the development of conformance testing procedures is mostly based on the designers experience. A potential improvement that is being examined is to make testing a formal method and to provide tools that automate test cases generation.

Studia Informatica Universalis

"main" 2004/3/5 page 2 2 I. Berrada -R. Castanet -P. Félix

Test Based Approach

The most known approaches to test selection in the black-box conformance testing framework are:

Coverage Criteria. The most used coverage criteria are based on the specification model. In the case of timed automata, some authors proposed transition, state or variable coverage approaches.

Test Assumptions. Various test assumptions can be formulated and combined until a finite test set is obtained. In the case of input/output timed automata, some authors assume that the specification and the IUT are deterministic, output enabled, and deadlock and livelock free.

Test Purposes. The user chooses behaviors which have to be analyzed, hence the specification exploration reduction. Using the specification and test purposes, a finite number of test cases are generated.

Our Contribution

Generating a test case for a path assumes that we are already able to decide the reachability of some states for this path. In this paper, we consider the following feasibility problem: if a given path of the automaton has executions, we wish to determinate which constraints, every execution of this path has to verify. Our motivation for studying this problem is test cases generation: once the feasibility conditions over a path are calculated, they allow in particular, generating both the fastest and the slowest timed executions. While these executions are not unique, we will identify two versions for each fastest and slowest timed executions. The contributions of this paper are: a ¡ ¢¡ ¤£ ¦¥ ¨ § © © time solution for the feasibility problem, generation of the slowest and the fastest timed executions for a path, introduction and formalization of the strong/weak feasibility concept, and an application to test cases generation.

Related Work

An extension of test theory for Mealy machines in the case of dense real-time systems was proposed by Springintveld et al. [START_REF] Springintveld | Testing Timed Automata[END_REF]. The authors suggested to preform a kind of discretization of the region graph model. The discretization step size takes into account the number of clocks as well as the timing constraints. From the generated model, they derive test cases. This extension yields to a finite and complete set of test but the method is highly exponential and is not usable in practice. Another result generating test sequences for a discretized deterministic timed automaton is given by En-Nouaary et al. in [START_REF] En-Nouaary | Timed test cases generation based on state characterization technique[END_REF]. The authors propose to build a grid automaton from the region graph, and SIU 2003 use a Wp method for the generation assuring a good coverage of the initial specification, but the number of generated test cases can be large. In [START_REF] Koumsi | An approach for testing real time protocols[END_REF], the authors have chosen as model temporized automata with discrete time. The model is transformed into automaton without time, but with two special events on clocks: set and expire. The advantage of the method is combinatorial explosion limitation. A drawback of this approach is the possibility of generating some test cases that contain non-executable sequences with the events set and expire.

In [START_REF] Cardell-Oliver | Conformance Testing of Real-Time Systems with Timed Automata Specifications[END_REF], an implicit clock is used, the time is discrete and the proposed model is a temporized transition system. The test concerns only time domains(not events coming at a precise time). In [START_REF] Clarke | Automatic Test Generation for the Analysis of a Real-Time System: Case Study[END_REF], the system specification is based on a constraint graph. From a fault model, the authors define test criteria and generate test cases according to the test criteria. Since constraint graph is used as a model, only delays can be expressed between two successive events, and the coverage of faults cannot be complete. In [START_REF] Mandrioli | Generating Test Cases for Real-Time Systems from Logic Specifications[END_REF], the generation of test cases is produced from logic formula (time is expressed by using two constructors: future and past). A unique clock is used and the temporal domain is discrete. This model is not sufficient to represent complex real-time systems and the generated test suite covers only integer values of time.

We also mention another interesting contribution [START_REF] Higashino | Generating Test Cases for a Timed I/O Automaton model[END_REF] that proposes a generation method based on must/may traceability. The authors propose to test first, the correctness of the implementation of states and transitions. For that, they transform the specification into a FSM, and use the UIOv-method to derive test cases. For the correctness of the implementation of transition conditions, they assume that faults are restricted to some typical ones and use the must/may traceability method to generate test cases.

In [START_REF] Bloch | Some issues on testing real time systems[END_REF][START_REF]Adapted test cases for timed systems[END_REF][START_REF] Petitjean | Etude des méthodes de test sur les systèmes temporisés[END_REF], the authors propose first to enlarge the regions of the graph and to build dynamically the region graph according to test purposes. Our approach [START_REF] Koné | On the Fly Test Generation for Real Time Protocols[END_REF] uses timed automata model and a synchronous product between the specification and a test purpose as in [START_REF] Kaiser | Interopérabilité temporelle d'automates temporisés[END_REF]. A reachable path is dynamically calculated by resolving inequalities on time constraints. This method avoids combinatorial explosion of the region graph, but don't give a complete coverage of faults.

The remainder of this paper is structured as follows: After the introduction of timed automata with global clock (TAGC) model, and formalization of the feasibility problem, chapter 2 and 3, we will present, in chapter 4, a solution for reached values computation of the global clock. The identification of both, the fastest/slowest timed execution, and strong/weak feasibility is done in chapter 5. In chapter 6, the reached values computation algorithm for any clock is exposed. An application, of the results proposed in this paper, to test cases generation is presented in chapter 7. The last chapter summarizes the contributions of the paper and presents future works.

Timed Automaton Modeling

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] were introduced as a formal notation to model the behavior of real-time systems. This section presents the timed automaton model and some basic definitions in order to specify notations.

Preliminaries

Let ¡ denote the set of reals, ¡ £¢ the set of nonnegative reals, and ¡ £¢ the set of nonnegative reals with the single element ¤ . We extend the standard partial ordering ¥ , the addition operator ¦ , and the subtraction operator § over ¡ ¢ to ¡ ¢ in the usual way: for every © ¡ ¢ , ¥ ¤ , ¦ ¤ ¤ ¦ ¤ and ¤ ! § "# $¤ . An interval I of ¡ ¢ is a dense set over ¡ ¢

¡ ¢ . For ¡ CD E' GF © © ¡ , H I4 £ ¡ CD E' GF © (resp. H & BP ¡ 3D Q' GF © ) is the smallest (resp. greatest) of D and F . For R S ¡ R £T VU © T 3W YX abU cW ed , R gf h ¡ R if T pU © T bW YX aqU cW ed and r s© s ¡ ¢ : r ¥ R t ¡ r ¥ R
£T pU © T bW YX abU cW ed , and R u¦ vR f ¡ R wT VU x¦ yR f T pU © T bW YX aqU cW ed . For a finite set , the & B EF ¡ © is the number of elements of .

Clocks, Constraints and Interpretations.

A clock is a variable that allows to record the passage of time. It can be set to a certain value and inspected at any moment to see how much time has passed.

In the Alur-Dill model [START_REF] Alur | A theory of timed automata[END_REF], clocks increase at the same rate, they are ranged over ¡ ¢ and the only assignments that are allowed are clocks reset of the form P t . For a set C of clocks, the set ¡ © of clocks constraints is defined by the grammar: P ¥ D aD ¥ P s I where x is a clock in C and c is a constant in . A clock interpretation for a set C of clocks is a mapping from C to ¡ ¢ that assigns a real value to each clock. .

Timed Automaton Definition 1 (Timed Automaton). A timed automaton (TA) A is a tuple

Definition 2 (TA with Global Clock). A timed automaton with global clock (TAGC) A is: A timed automaton.

There is a clock h of A without reset in any transition except for a transition which leads to the initial state. The notion of the clock h is implicit in the Alur-Dill model and explicit in the P-automaton [START_REF] Bérard | Automates temporisés calife[END_REF]. The choice of TAGC model is justified by the context of black-box testing in which all events are seen according to a global clock, and by comprehension and clarity reasons.

1 C2[2,6] 2 3 4 5 6 R(C2) !a !c ?d R(C1) !x !y ?b h[0,2] C2[0,1] C1[0,2]
h [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Cardell-Oliver | Conformance Testing of Real-Time Systems with Timed Automata Specifications[END_REF] C1 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bérard | Automates temporisés calife[END_REF] h [START_REF] Alur | Membership problems for timed and hybrid automata[END_REF][START_REF] Koné | On the Fly Test Generation for Real Time Protocols[END_REF] h [START_REF] Bérard | Automates temporisés calife[END_REF][START_REF] Koné | On the Fly Test Generation for Real Time Protocols[END_REF] C2 [START_REF] Alur | Membership problems for timed and hybrid automata[END_REF][START_REF] Cardell-Oliver | Conformance Testing of Real-Time Systems with Timed Automata Specifications[END_REF] C1 [START_REF] Alur | Membership problems for timed and hybrid automata[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] h [START_REF] Clarke | Automatic Test Generation for the Analysis of a Real-Time System: Case Study[END_REF][START_REF] En-Nouaary | Timed test cases generation based on state characterization technique[END_REF] C2[0,1] R(C1) h [START_REF] Bloch | Some issues on testing real time systems[END_REF][START_REF] Koumsi | An approach for testing real time protocols[END_REF] C2[0,1] C1 [START_REF] Bérard | Automates temporisés calife[END_REF][START_REF] Clarke | Automatic Test Generation for the Analysis of a Real-Time System: Case Study[END_REF] Let A be the automaton with global clock h of Fig. 2.1. This automaton has 6 states, 8 transitions and 3 clocks. R(C1) means that clock C1 is reset in this transition. Each transition has some clock's constraints and events. For this automaton, ¡ £¢ ' ' ¥¤ §¦ , ¡ ¨ ¥© © ¤ 6' £¢ ' ¦ , ¡ © © ¤ 6' ¦ , ¡ ¨ ¥© ' £¢ © % ' ¤ E1 , and ¡ © ' © % ' E1 . Definition 3 (Timed Execution). Let A be a TA. A path ! $0 #" $" ¨¥ of A is a suite of transitions that form an arc in the graph associated with A. A timed execution (TE) R of ! is a two-dimensional real array of size

h[4,+INF] C1[0,2] h[3,6] C1[0,2]
P © § R ¡ ¨T ' GP © R ¡ ¨T ¢ ' (' © § R ¡ ¨T ' (' © . -If y alone is reset in ¨T , then R ¡ ¨T ¢ ' GP © § R ¡ ¨T ' GP © R ¡ ¨T ¢ ' (' © . -If x alone is reset in ¨T , then R ¡ ¨T ¢ ' GP © R ¡ ¨T ¢ ' (' © § R ¡ ¨T ' (' ©
.

-If both x and y are reset in ¨T , then R

¡ ¨T ¢ ' P © R ¡ ¨T ¢ ' )' © .
While all clocks increase at the same rate, these four rules ensure this hypothesis. From now on, we assimilate execution and timed execution.

Notation 2.1. For a path ! ¨ " ¨ " $" 0" ¨¥ of a TAGC 1 , ! T ¨ " ¨ " 0" $" ¨T is a sub- path of ! . R ¡ ! ©
is the set of all executions of ! . If for every 4 in % ¢ ' ¢£ 1

, & T is the event associated to ¨T , then: ¡ 3F ' G& © " ¡ 3F ' 2& © " 0" $" ¡ 3F ¥ ' 2& ¥ © , such that F T © ¡ ,
is the execution R defined by: For every 4 in % ¢ ' ¢£ 1

, R ¡ ¨T ' ¤ © F T .

For every 4 in % ¢ ' ¢£ 1

, for every clock

P in ¡ ¨T © last reset in (2 , R ¡ ¨T ' P © F T § F 2 .
In the reset of the paper, we assume that ! 2 #" $" ¨¥ is a path of a given TAGC A from the initial state, and £ is the last state of this path.

Feasibility of a Path

In the feasibility problem, we wish to determine the reachability of transition ¨¥ . That is, we are interested in the computation of suitable constraints over ! for firing ¨¥ . Section 3.1 formalizes this problem by introducing the reached values concept and Section 3.2 introduces well-formed (WF) suites, out reach intervals and some properties of these intervals.

3 )4 ¢ $5 £ is the set of clocks that appear in 5 .

SIU 2003

"main" 2004/3/5 page 7

A Formal Approach for Real-Time Test Generation

1. For every r © ¥ ¦¡ ¡ ¨T ' GP © §£ , there is an execution R © R ¡ ! © such that: R ¡ ¨T ' P © r . 2. For every execution R © R ¡ ! © , R ¡ ¨T ' GP © is in ¢¡ ¡ ¨T ' P © ¤£ .
The reached values of a constraint in a given transition depend on the chosen path. The feasibility problem consists then, in the reached values computation for every clock in every transition of this path. When there is no confusion on the path ! , ¢¡ ¡ ¨T ' GP © £ will be noted ¦¡ ¡ ¨T ' GP © .

Corollary 1. The state £ is a reachable state of ! iff for every 4 in % ¢ ' ¢£ 1 , ¢¡ ¡ ¨T ' ¥¤ ©
is a non empty set. In this case, we say that ! is a feasible path.

Lemma 2. For every 4 in % ¢ ' ¢£ 1

, for every

P in ¡ GT © , ¦¡ ¡ ¨T ' P © is an interval over ¡ ¢ .
Proof. From the definition of an execution and the grammar constraints (a constraint over a clock is a dense set), it is easy to see that from two executions of ! , R and R , and a given © % ' ¢ 1 , the execution E defined by:

% (4 © % ¢ ' £ 1 ' % P © y ¡ ¨T © c' R ¡ ¨T ' P © ©¨¥ R ¡ ¨T ' GP © ¦ ¡ ¢ § ¥¨© ¥ R ¡ ¨T ' GP © is an execution of ! . Then % (4 © % ¢ ' £ 1 , % P © " ¡ GT © , ¢¡ ¡ ¨T ' GP © is a dense set over ¡ ¢ . Remark 3.1. If ! f is a path of a TA where the clock h is implicit, and R is an execution of ! f , then the clock ¤ values of R in every transition can be com- puted. In fact, % (4 © % ¢ ' £ 1 , % P © ¡ ¨T © : R ¡ ¨T ' ¥¤ © T U ¤ ¤ § ¨ § ! @`" $# R ¡ ¨U ' GP ©
, where &% E8 $% ¨¡ ¨U ' GP © means that the clock x is last reset in transition ¨U with ' )( 4 . Now, if for two executions of ! f , R and R , there is ï© % ' ¢ 1 such that

% (4 © % ¢ ' ¢£ 1 , % P 10 ¤ © v ¡ ¨T © , R ¡ ¨T ' GP © 2¨¥ R ¡ ¨T ' GP © ¦ ¡ ¢ w § 1¨© ¥ R ¡ ¨T ' GP © , then: R ¡ ¨T ' ¤ © 3 T U ¤ ¤ § ¨ § ! a`" $# ¡ ¨¥ R ¡ ¨U ' P © ¦ ¡ ¢ § ©¨© ¥ R ¡ ¨U ' GP © ¢© ¦4 R ¡ ¨T ' ¥¤ © 5¨¥ R ¡ ¨T ' ¤ © ¦ ¡ ¢ § 6¨© ¥ R ¡ ¨T ' ¤ © . Conclusion, ¦¡ ¡ ¨T ' ¤ © is also a dense set over ¡ ¢ if h is implicit.

Out Reach Intervals

Definition 5. Let

7 % & ' 0) 21 and 7 % D E' GF Y1
be two intervals of ¡ ¢ . The sum 7 98 7 of 7 and 7 is the interval defined by: 7 98 First, we add a new transition ¨ in which all clocks are reset: ¤ ¡ ¨ © % ' 1

7 s % & ¦ D Q' 2) ¦ F Y1
¤ ¡ ¡ © % ' 1 1 ' ¤ % " ¤ ¡ ¨T © ¢ " QW § ¤£ # ¤ ¡ ¨2 ¦¥ © 8 ¡ ¨T ' P © where x is last reset in )2 ¥ ¡ § " ( 4 ),
1 5 4 3 2 h[0,2] C1[0,2] C2[0,1] !a R(C1) h[2,7] C1[2,5] C2[2,6] ?b R(C2) t1 t2 t3 t4 !c ?d h[3,13] h[5,13] C1[3,6] C2[3,7]
.

For G , all clocks are reset in ¨ , then:

¤ ¡ G © ¡ ¤ ¡ ¨ © 8 % ' 1 © ¨ § ¡ ¤ ¡ ¨ © 8 % ' 1 © ¨ § ¡ ¤ ¡ ¨ © 8 % ' ¢ 1 © % ' ¢ 1 " For ¨ , C1 is reset in G , then: ¤ ¡ ¨ © ¡ ¤ ¡ ¨ © 8 % ' © 1 © ¨ § ¡ ¤ ¡ ¡ © 8 % ' ¦ 1 © % ' ) Q1
.

For , C2 is reset in ¨ , then:

¤ ¡ © ¡ ¤ ¡ ¨ © 8 % ' E1 © ¨ § ¡ ¤ ¡ ¡ © 8 % ' ¢ E1 © % ' ¢ E1
. At the end, in ¡ , C2 is reset in ¨ and C1 in ¨ then:

¤ ¡ ¡ © ¡ ¤ ¡ ¨ © 8 % ' E1 © ¨ § ¡ ¤ ¡ ¨ © 8 % ' ¦ 1 © ¨ § ¡ ¤ ¡ ¡ © 8 % © ' ¢ E1 © % © ' ¦ 1
. Definition 7 (Well-formed Suite). Let ¡ C7 T © T 3W 0`¥ be a suite of non empty inter- vals over ¡ , 7 T % 4 £ 65 ¡ 37 T © ' 8 a9 eA ¡ 37 T © 1

.

¡ C7 T © T 3W `¥ is a well-formed (WF) suite if for every 4 in % ¢ ' £ § ¢ 1 , 4 £ 65 ¡ 37 T © ¥ 4 £ 65 ¡ C7 T ¢ © , 8 a9 eA ¡ 37 T © ¥ "8 a9 BA ¡ C7 T ¢ © .

Definition 8.

¡ 37 T © T bW `¥ accepts a WF sub-suite

¡ 7 T © T 3W `¥ if for every 4 in % ¢ ' ¢£ 1
, 7 T 7 T , and ¡ 7 T © T bW `¥ is WF.

The next lemma gives a relation between ¡ ¢¡ ¡ ¨T ' ¥¤ © © T 3W `¥ intervals, con- sequence of path clocks reset.

Lemma 3. ! is feasible iff there is a suite of intervals ¡ 37 T © T 3W 0`¥ ! such that:

1. For every r U in 7 U , there is r T in 7 T such that r T § r U © ¡ ¨T ' GP © .

¡ C7 T © T 3W 0`¥ is a WF suite. 2. For every 4 in % ¢ ' ¢£
For every r T in 7 T , there is r U

in 7 U such that r T § r U © ¡ ¨T ' GP © . Moreover, if for every 4 in % ¢ ' ¢£ 1 , 7 T ¤ ¡ ¨T ©
is the largest interval verifying the third condition, then suite that verifies 3) is the suite

¡ ¢¡ ¡ GT ' ¤ © ¢© T bW `¥
Corollary 4 gives a necessary condition for the feasibility of the path, consequence of lemma 3.

Corollary 4.

If ! is feasible then the suite of the complementary of out reach intervals of ! has a WF sub-suite.

Computation of the Reached Values of Clock h

In the preceding section, we have introduced the reached values of a constraint. We showed that path feasibility depends on the reached values of the global clock. Section 4.1 presents the constraints graph associated to a two variables inequalities system, Section 4.2 develops an algorithm for the computation of the reached values of the clock ¤ , and Section 4.3 discusses the complexity of this algorithm.

Constraints Graph.

For a two variables inequalities system, we associated a constraints matrix. For example, ¤ is the constraints matrix associated to system .

¥ ¦ § ¥ P ¥ P § ¥ ' ' ©¨© ¤ § § © ¤ ¤
A system of inequalities can be represented as a graph where every node is a variable and every edge is a constraint over these variables.

¤ ¡ " © ¥ ¦¢ ¦ e' 1 ¦
defined by: §¢ ¦ is the graph vertexes set.

1 ¡ ¥ ¦¢ ¦ ¥ ¥ ¡ ¨¢ ¦ © ¦ ©
is the graph edges set. We denoted by P © P f every edge of 1 .

P © P f © 1 4 ¡ bP § P f ¥ D © 4

& " ¤% H

A two variables inequalities system admits a solution if its constraints graph does not contain a negative cycle.

Algorithm

Given a TAGC A and a path ! 2 #" $" ¨¥ of A from an initial state, the computation algorithm of the suite ¡ ¢¡ ¡ ¨T ' ¥¤ © © T 3W 0`¥ is outlined in Fig. 4.3. The input of the algorithm is a path ! 2 #" $" ¨¥ , an empty system £ and a vector r of £ reals. The algorithm consists in three steps: First, a checking step in which we compute ¡ ¤ ¡ ¨T © © T 3W `¥ . If ¡ ¤ ¡ ¨T © ¢© T bW `¥ does not have a WF sub-suite then the path is not feasible (Corollary 4). Second, a system construction step in which the relations between clocks are formulated (Lemma 3). Finally, a solving step of the system constructed £ .

Complexity Analysis: Modified Timestamps Generation Algorithm

The algorithm Fig. 4.3 introduces a linear system of inequalities. In [START_REF] Alur | Membership problems for timed and hybrid automata[END_REF], the authors give an efficient algorithm, of complexity ¡ ¤£ ¥ § © , for generating a possible sequence of time values at which the individual edges are traversed. The algorithm computes the shortest cost path 8 ¤ ¤% E8 a ¡ ' 4 © from node to node 4 in the digraph ¤ associated to the system £ . This solution can be modified to solve the feasibility problem. In fact, the shortest cost path 8 ¤ ¤% E8 a ¡ ' 4 © in our case corresponds to 4 £ 65 ¡ ¢¡ ¡ ¨T ' ¥¤ © © : 4 £ 65 ¡ ¢¡ ¡ ¨T ' ¤ © ¢© § £8 ¤ ¤% E8 @ ¡ ' 4 © .

If now we consider the digraph ¤ f obtained from ¤ by reversing edges, by ap- plying the same algorithm to ¤ f , we have 8 ¤ ¤% E8 @¨ f

& @9 ) A0 Add ¥ § B 3 @C ¥ § To ¢ £ ; Add & ¦ $D © ¢ E2 4© § 6 7¡ C ¥ § C GF IH QP © ¢ E2 4© § 6 7¡ To ¢ £ ; For R TS T2 4© § Add To ¢ ¤£ /* x was last reset in U */ & ¦ $D © ¢ E2 4© § 6 R C ¥ § ¤V ¥ U C GF WH XP © ¢ E2 4© § 6 R ;
End For End For /* Solving step */ Phase Three: Solve ¢ £ . Solve ¢ ¤£ ;

End;

Figure 4.3:

¡ ¦¡ ¡ ¨T ' ¥¤ © © T 3W 0`¥ computation algorithm.

Fastest and Slowest Accumulate Delay Executions

Generating the fastest and the slowest accumulate delay executions are interesting for several reasons. Firstly, they allow testing the implementation behavior in critical situations. Secondly, it is generally useful that regression testing can be executed as quickly as possible in order to improve the turn around time between changes [START_REF] Hessel | Time-optimal Real-time Test Case generation using UPPAAL[END_REF]. Since these executions are not unique, in this section, we will identify two versions for each fastest and slowest timed execution: the fastest and the slowest timed executions according to every transition crossed (Section 5.1), and the fastest and the slowest timed executions according to every clock of a transition (Section 5.3). Section 5.2 introduces and formalizes the strong/weak feasibility concept. Recall. For a path ! ¨ " ¨ " 0" $" ¨¥ of a TAGC 1 , ! T ¨ " 0" 0" ¨T is a sub-path of ! .

R

¡ ! © is the set of all executions of ! .

Fastest and Slowest Timed Executions According to every Transition Crossed

One way to reach a state of a path in an early (resp. late) time is to reach every state between this one and the initial state as soon (resp. late) as possible. This observation is formulated below.

Lemma 6. Let us assume that ! is a feasible path.

1. If for every 4 in % ¢ ' £ 1 , ¢¡ ¡ ¨T ' ¥¤ © is bounded, then there is a single execution R ¡ © R ¡ ! © such that: for every 4 in % ¢ ' ¢£ 1 , R ¢ ¡ ¨T ' ¤ © 8 a9 BA ¡ ¦¡ ¡ ¨T ' ¤ © ¢© . 2.
There is a single execution R ¡£ such that: for every

4 in % ¢ ' ¢£ 1 , R ¤£ ¡ ¨T ' ¥¤ © 4 £ 65 ¡ ¦¡ ¡ ¨T ' ¤ © ¢© .
Proof. See Appendix A.

Weak and Strong Feasibility

Problem 5.1. The problem treated here is: under what constraints over a feasible path, if a transition is fired, the next transition can be also fired until the last transition of this path. Let us take the example of Fig. 5.4. If the transition ¨¢ is fired at moment 2, and ¨ at 4, we notice that ¨ can not be then fired according to its path constraints. Now, let us take the example of Fig. 5.5. For this path, each time a transition is fired respecting its constraints, the next transition can be fired. Definition 10. The feasible path ! s ¨ " ¨ " 0" $" ¨¥ is said to be strongly feasible if for every natural 4 © % ¢ ' ¢£ 1

, and for every execution

R f © R ¡ ! T © , there is an execution R © R ¡ ! © that meets R f . On the opposite (i.e. there is R f © yR ¡ ! T © , such that for every R © yR ¡ ! © , R does not meet R f ), ! is said
to be weakly feasible.

SIU 2003 Typically, ! is strongly feasible if: for every 4 in % ¢ ' £ 1 , for every execution R gf in R ¡ ! BT © , there is R in R ¡ ! © such that: for every ' in % ¢ ' 4 1 , for every P

1 3 2 h[0,1] C1[0,1] C2[0,1] a R(C1) h[2,4] C1[2,4] C1[4,5] b R(C2) t1 t2 t3 c h[4,5] C2[2,4] C2[1,2]
in ¡ ¨U © , R ¡ ¨U ' P © R if ¡ ¨U ' GP © .
The strong feasibility allows deciding at advance if the running behavior of the system will reach the needed target behavior. The latter is capital during test applications on real implementations. The tester will be then able to decide stopping, at each time, the implementation execution, and not to await the end of the test case. Lemma 7 gives a necessary and a sufficient condition for the strong feasibility. Lemma 7. Let ! y ¨ " ¨ " $" 0" ¨¥ be a feasible path. ! is strongly feasible iff for every 4 in % ¢ ' £ 1

, for every clock

P in ¡ ¨T © , ¨T is fired in ¢¡ ¡ ¨T ' P © ¤£ .
The idea of the proof is to replace the specification constraints by the reached values and to proceed by induction.

Proof. See Appendix B.

Fastest and Slowest Executions According to every Clock of a Transition

As the fastest and slowest executions are not unique, in this subsection, we will present other executions that also allow computation of the fastest and slowest delay for reaching a path target state. Let be the path of Fig. 5.6. We can verify that, % (4 #© % ¢ ' E1 , % P © ¡ ¨T © , ¢¡ ¡ ¨T ' P © ¡ ¨T ' GP © . The slowest execution according to every transi- tion crossed R corresponding to this path is ¡ ¢ ' G& © " ¡ ' 2) © " ¡ ¡ ' 2D © . For this execution, R ¡ ' © £¢ , R ¡ ' © , and R ¡ ' ¥¤ © . Let us now consider R , the execution given by ¡ ' 2& © " ¡ ' 0) © " ¡ ¡ ' GD © . This execution is also a slowest execution, and we have R

1 3 2 h[0,1] C1[0,1] C2[0,1] a R(C1) h[2,6] C1[2,6] C1[4,9] b R(C2) t1 t2 t3 c h[4,9] C2[2,6] C2[2,3]
¡ ) ' © , R ¡ ' ©
, and R ¡ ¨ ' ¤ © . As we can see, R takes simultaneously the 8 @9 BA ¡ ¢¡ ¡ ¨ ' © © , 8 a9 eA ¡ ¢¡ ¡ ¨ ' © ¢© and 8 @9 BA ¡ ¢¡ ¡ ¨ ' ¤ © ¢© . Next, we will prove that this result holds for every path in every transition.

P in ¡ ¨¥ ©
. The proof of the lemma is done by induction over the number of transition clocks, using the constraints graph associated to a path.

Proof. See Appendix C.

We have showed that there is an execution that takes simultaneously the ¡ 4

£ 65 ¡ ¢¡ ¡ ¨¥ ' P © ¢© ¢© " QW § ¥¤ # (resp. ¡ 8 a9 BA ¡ ¦¡ ¡ ¨¥ ' GP © © ¢© " YW ¨ § ¥¤ # ), for transition ¨¥ .

In fact, this result holds for every transition of ! . Lemma 9. Let us assume that ! is feasible. For all ' in % ¢ ' ¢£ 1

we have :

1. If for every 4 in % ¢ ' ' 1 , ¢¡ ¡ ¨T ' ¤ © ¤£ is bounded, then there is an execution of ! that takes simultaneously the 8 a9 eA ¡ ¢¡ ¡ ¨U ' P © ¤£ © , for every

P in ¡ ¨U © . 2.
There is an execution of ! that takes simultaneously the 4 £ 65 ¡ ¢¡ ¡ ¨U ' P © ¤£ © , for every

P in ¡ ¨U © .
Proof. Let us consider the path ! U , such that: for every § in % ¢ ' ' 1 , and for every P in ¡ ¨2 © , ¡ ¨2 ' P © ¢¡ ¡ ¨2 ' GP © §£ . According to lemma 8, for ! U , there is an execution R © yR ¡ ! eU © that takes simultaneously the 8 a9 eA ¡ ¢¡ ¡ ¨U ' P © £ © , for every clock P in ¡ ¨U © . Now, according to lemma 7, this execution can be extended to an execution of ! due to the strong feasibility of ! (every transition of ! QU is fired according to the reached values sets of ! ).

We have proved the existence of an execution R (resp. R f ) of ! that takes simultaneously the maximal (resp. minimal) values of ¢¡ ¡ ¨U ' GP © , for every ' in % ¢ ' ¢£ 1 . Let R (resp. R ) be an execution that meets R (resp. R f ), for

! is feasible. Let R © R ¡ ! © (resp. R © R ¡ ! ©
) be the execution that takes simultaneously the maximal (resp. the minimal) values of ¢¡ ¡ ¨U ' GP © , for a ' in % ¢ ' ¢£ 1

, and for every

P in ¡ ¨U ©
, while making the possible minimum (resp. maximum) delay between transitions after ¨U . Then, for every execution R © R ¡ ! © :

1. For every 4 , ' ¥ 4 , R ¡ ¨T ' ¤ © § R ¡ ¨U ' ¥¤ © ¥ "R ¡ ¨T ' ¥¤ © § R ¡ ¨U ' ¥¤ © . 2. For every 4 , ' ¥ 4 , R ¡ ¨T ' ¤ © § R ¡ ¨U ' ¥¤ © ¥ "R ¡ ¨T ' ¤ © § R ¡ ¨U ' ¥¤ © . Proof. See Appendix D.

Computation of the Reached Values of any Clock

In this section we will introduce a computation method of the reached values of any clock by using the two versions of each fastest and slowest timed executions.

Algorithm:

We assume that used clocks are ¤ , P , P ,..., P ¡ £¢ ¥¤ £ # # . The algorithm for computing the reached values for every clock is outlined in Fig. 6 Compute © © § 6 7¡ 5£ % § 3 ! #" ;

For & (' ) 10

To ¦ Do For every R S 2 4© , if R is last reset in the initial state Then ¤ ¥ & "! # £ ! ' ) 8& ¦ $D © © 5 § 56 7¡ ; ¤ ¦ § $ & ! # £ ! ' ) F IH QP © © § 56 7¡ ;
Phase Two: Filling ¤ ¥ and ¤ § with the other reached values.

For & (' ) 10 To ¦ Do If there is clocks reset in § Then

For 3 : % R & S 2 4© , ¢ E2 4© § 56 R ' ) ' ¤ ¥ ( & "! # £ ! 6 )¤ ¥ 0 & "! # £ ! ¢! ; For : % R & S 2 4© , ¢ E2 4© § 6 R ' ) ' ¤ § & ! # £ ! 6 )¤ § & "! 1 £ ! ¢! ;
/* The feasibility of 3 and are ensured by lemma 9.*/ Compute © © § 56 7¡ £ 32 § 3 ! #" Once the reached values of ¤ for ! and ! are computed, for every clock P 2 in ¡ ¨U © , such that ' is greater than 4 , and P 2 last reset in the current transition ¨T , then 4

; Compute © © § 6 7¡ 5£ 54 X § 3 ! #" ; For 6 ' ) 8& To ¦ Do For every R S 2 4© Do /* Updating ¤ ¥ and ¤ ¦ § */ If R S U is last reset in § Then: ¤ ¥ 6 7! # £ ! ' ) 8& ¦ $D © © U 6 7¡ 5£ )4 % V & ¦ $D © © § 6 7¡ 5£ 54 # ; ¤ ¦ § $ 6 7! # £ ! ' ) F IH QP © 8 © U 6 ¡ £ ¡2 V F IH QP © © § 56 7¡ £ 32 ; End;
£ 65 ¡ ¢¡ ¡ ¨U ' P 2 © £ © "4 £ 65 ¡ ¦¡ ¡ ¨U ' ¥¤ © £ 4 © § i4 £ 65 ¡ ¢¡ ¡ ¨T ' ¤ © £ 4 © , and 8 a9 eA
¡ ¢¡ ¡ ¨U ' GP 2 © £ © 8 a9 eA ¡ ¢¡ ¡ ¨U ' ¤ © £ 4 © § 8 a9 BA ¡ ¢¡ ¡ ¨T ' ¥¤ © £ 4 © .
This result is a consequence of lemma 10. At the end, ¦ ¨ § and ¦ © contain the minimum and the maximum reached values of any clock.

In every transition having clocks reset, the complexity of computing the reached values of this transition clocks is ¡ £ ¥ § © , then the complexity of the algorithm is

¡ ¡ £ ¥ § © ¢ © .
Theorem 11. Given a path ! from the initial state of a TAGC 1 , with £

transitions and § clocks, the computation of the reached values for every clock can be solved in time

¡ ¡ £ ¥ § © ¢ © . SIU 2003

Test Generation: Test Purpose Based Approach

Protocol testing consists in checking that some implementations conform to a given specification. We assume the determinism of the specification and the IUT. The latter are given as timed I/O automata. The architecture of the test is given in Fig. 7.8. The tester takes the place of the environment and controls the IUT by injecting test cases via control and observation points (COP).

IUT {Test cases}

Tester COP

Test Purpose

A test purpose is a temporal property that one would like to observe in implementation behaviors. In the case of real-time systems, such property may include real-time features where time constraints appear explicitly. We also model test purpose with I/O automaton.

Definition 11. A Test purpose

© ¡ is a deterministic, acyclic automaton with a distinguished non empty set of accepting states.

Synchronous Product

T ¨¥ YT § ¡ ¤£ © ¢© ¡ ¡ T ¨¥ QT ¨ § ¡ ¡ A % D © ' T ¦¥ QT § ¡ © ¥ © © . ¡ ¡ ¤£ © ¡ A % D © ¥ ¡ © ¥ © . ¡ ¡ ¤£ © ¡ ¡ A % D © ¢ ¡ © ¥ © . ¢ ¡ ¡ ¦£ © ¢ ¡ ¡ A % D © ¢ ¢ ¡ © ¥ © .

Example

Let the automaton of Fig. 2.1 be an example of a specification, and let us consider the test purpose of Fig. 7.9. In this test purpose, we want to test if after receiving an event "a" in a delay between 0 and 1 (X[0,1]), the IUT can send an event "d" in a delay between 1 and 3 (Y [START_REF] Floyd | Algorithm 97 (shortest path)[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF]) . By using the synchronous product, the path of Fig. 3.2 syn- chronizes with this purpose. By adding the constraints of test purpose to this path we have Fig. 7.10:

X[0,1] !a R(Y) Y[1,3] ?d Accept
1 5 4 3 2 C1[0,2] C2[0,1] !a R(C1) C1[2,5] C2[2,6] ?b R(C2) t1 t2 t3 t4 !c ?d C1[3,6] C2[3,7] h[5,13] X[0,1] R(Y) h[0,2]
h [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Cardell-Oliver | Conformance Testing of Real-Time Systems with Timed Automata Specifications[END_REF] h [START_REF] Alur | Membership problems for timed and hybrid automata[END_REF][START_REF] Koné | On the Fly Test Generation for Real Time Protocols[END_REF] Y [START_REF] Floyd | Algorithm 97 (shortest path)[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] Figure 7.10: Synchronous Product 1.

¡ ¡ © £¢ ) ' ¤ 6 ¤ ! . ¡ ¡ © 3 ) A© ¡ © ¢ ¦¥ ¤ 6 ¨ § ! ¦© © ¡ © ¢ ¦¥ ¤ 6 ¨ § ! ¦© © ¡ © ¢ ¦¥ ¤ 6 I0 )! ¦© © ¡ $© ¢ ¦¥ ¤ 6 0 3! ) ¤ 6 W0 3!
After reseting the clock Y when receiving "a".

SIU 2003

"main" 2004/3/5 page 19

¡ ¡ © ) A© ¡ © 3 ¥ § 6 ¡ ! © © ¡ © ¢ ¥ § 6 £¢ ! ) ' § 6 ¥¤ ! . ¡ ¡ © ¦ ) A© ¡ © ¥ § 6 ¥¤ ! © © ¡ © ¢ ¥ ¦ 6 W0 §¦ ! ) ' ¨6 W0 § ! . ¡ ¡ © § ) A© ¡ © 3 ¥ ¦ 6 ¥¤ ! © © ¡ © ¥ ¦ 6 £¢ ! © © ¡ $© ¢ ¥ ¡ 6 I0 §¦ ! © © ¡ © 3 ¥ 0 X6 ©¦ ! ) ¡ 6 ¥¦ ! ) ' 6 ! .
We notice that the out reach interval of transition ¨ is empty. We know immediately that, this path does not respect the test purpose. Let us now consider the test purpose of Fig. 7.11. The suite of out reach intervals of the synchronous product of this path are:

X[0,1] !a R(Y) Y[1, 5] ?d Accept
¤ ¡ ¨ © % ' 1 , ¤ ¡ ¨ © % ' ¢ 1 , ¤ ¡ ¨ © % ' ) Q1 , ¤ ¡ ¨ © % ' ¢ E1
and ¤ ¡ ¨ © % © ' E1 . The constraints system associated to this path after removing redundant constraints is:

¥ ¦ § ¤ C ¥ 3 C 0 § C ¥ C ¤ ¨C ¥ ¦ C 0 § ¡ C ¥ § C ¤ § C ¥ V ¥ 3 C ¡ § C ¥ ¦ V ¥ C ¤ ¦ C ¥ § V ¥ 3 C ¡ ¦ C ¥ § V ¥ C ¢ 1 5 4 3 2 C1[0,1] C2[0,1] !a R(C1)
C1 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bérard | Automates temporisés calife[END_REF] C2 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] ?b

R(C2) t1 t2 t3 t4 !c ?d C1[3,6] C2[3,7] Y[1,5] Y[0,1] R(Y)
X [START_REF] Bérard | Automates temporisés calife[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] h[0,1] C2 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] h [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] X [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] X [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] h [START_REF] Bérard | Automates temporisés calife[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF]] X[0,1] h [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] Figure 7.12: Phase one algorithm application.

The solution of this system is: ¢¡ ¡ ¨ ' ¤ © % ' ¢ 1 , ¢¡ ¡ ¨ ' ¤ © % ' E1 , ¢¡ ¡ ¨ ' ¤ © % ' ) E1 , and ¢¡ ¡ ¨ ' ¤ © % © ' E1 . The reached values of clocks last reset in the initial state (Phase One) are given in Fig. 7.12.

For the computation of the maximum reached values of £¢ and , we consider the path ! of Fig. 7.13. In this path, we have changed ¡ 0 ' P © by 4 £ 65 ¡ ¢¡ ¡ G ' P © ¢© for every clock of 2 .

The reached values of ¤ for this path are:

¢¡ £ 2 ¡ G ' ¤ © % ' 1 , ¢¡ £ 2 ¡ ¨ ' ¤ © % ' Q1 , ¦¡ £ 2 ¡ ¨ ' ¤ © % ' © 1 , and ¢¡ £ 2 ¡ ¨ ' ¤ © % © ' © 1 . It means that: 8 @9 BA ¡ ¢¡ £ ¡ ¨ ' £¢ © ¢© 8 @9 BA ¡ ¢¡ £ 2 ¡ ¨ ' ¥¤ © © § 8 a9 BA ¡ ¦¡ £ 2 ¡ G ' ¤ © ¢© . SIU 2003
"main" 2004/3/5 page 20 20 I. Berrada -R. Castanet -P. Félix

1 5 4 3 2 C1[0,0] C2[0,0] !a R(C1)
C1 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bérard | Automates temporisés calife[END_REF] C2 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] ?b

R(C2) t1 t2 t3 t4 !c ?d C1[3,6] C2[3,7] Y[1,5] Y[0,0] R(Y)
X [START_REF] Bérard | Automates temporisés calife[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] h[0,0] C2 [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] h [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] X [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Membership problems for timed and hybrid automata[END_REF] X [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] h [START_REF] Bérard | Automates temporisés calife[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF]] X[0,0] h [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] Figure 7.13: Phase two algorithm application.

8 a9 BA ¡ ¦¡ £ ¡ ¨ ' £¢ © © 8 a9 BA ¡ ¦¡ £ 2 ¡ ¨ ' ¤ © ¢© § 8 a9 BA ¡ ¢¡ £ 2 ¡ G ' ¤ © ¢© © . 8 a9 BA ¡ ¦¡ £ ¡ ¨ ' £¢ © © 8 a9 BA ¡ ¦¡ £ 2 ¡ ¨ ' ¤ © ¢© § 8 a9 BA ¡ ¢¡ £ 2 ¡ G ' ¤ © ¢© © .
In the same way, after computing the reached values of this path, we obtain Fig. 7.14.

1 5 4 3 2 C1[0,1] C2[0,1] !a R(C1) C1[2,3] C2[2,3] ?b R(C2) t1 t2 t3 t4 !c ?d C1[5,5] C2[3,3] Y[5,5] Y[0,1] R(Y) X[5,6] h[0,1] C2[2,3] h[2,3] X[2,3] h[4,6] h[5,6] X[0,1] Y[2,3]
X [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bloch | Some issues on testing real time systems[END_REF] C1 [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bérard | Automates temporisés calife[END_REF] Y [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Bérard | Automates temporisés calife[END_REF] Figure 7.14: The reached values of the synchronous product.

We note by : FETC / SETC: Fastest/Slowest execution according to every transition crossed. FECT / SECT: Fastest/Slowest execution according to every clock of transition.

Table 7.15 summarizes the FETC, SETC, FECT and SECT of this path. For this example, the FETC for every transition is the same as the FECT. Transition ¨ has a SETC different from the SECT one. The total number of different executions of FETC, SETC, FECT and SECT, is between 1 and £ . The number the We notice that for ! © % ' ¢ 1 , and for two executions R and R f of executions given in table 7.15,

! ¥ R ¦ ¡ ¢ § ! © ¥ R f
is also an execution of this path. All these executions can be used as test cases.

SIU 2003

Transitions FETC FECT

3 ¢ ¢¡ ¤£ ¦¥ ¨ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ ¢ ¢¡ ¤£ ¦¥ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ ¢ ¢¡ ¤£ ¦¥ ¨ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ ¢ ¢¡ ¤£ ¦¥ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ ¦ ¢ ¢¡ ¤£ ¦¥ ¨ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ ¢ ¢¡ ¤£ ¦¥ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ § ¢ ¢¡ ¤£ ¦¥ ¨ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ ¢ ¢¡ ¤£ ¦¥ ¨ § ¢ © ¤£ ¦ § ¢ £ ¥ ¨ § ¢ ¢ ¤£ Transitions SETC SECT 3 ¢ "! #£ ¦¥ ¨ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£ ¢ "! #£ ¦¥ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£ ¢ "! #£ ¦¥ ¨ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£ ¢ ¢¡ ¤£ ¦¥ ¨ § ¢ $ ¤£ ¦ § ¢ ¤£ ¥ ¨ § ¢ ¢ ¤£ ¦ ¢ "! #£ ¦¥ ¨ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£ ¢ "! #£ ¦¥ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£ § ¢ "! #£ ¦¥ ¨ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£ ¢ "! #£ ¦¥ ¨ § ¢ $ ¤£ ¦ § ¢ % ¤£ ¥ ¨ § ¢ ¢% ¤£

Discussion and Future Work

In this paper, we have presented a solution to the feasibility problem for a path in time ¡ ¢¡ ¤£ ¥ § © © . By introducing a global clock to a given timed automaton & , the analysis of the feasibility problem becomes easier to solve. The use of this clock allows us to compute both the two versions of the fastest and slowest timed executions ' ,and to introduce the strong/weak feasibility concept. Standard algorithms [START_REF] Aspvall | A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with two Variables per Inequalities[END_REF][START_REF] Floyd | Algorithm 97 (shortest path)[END_REF] solve a two-terms inequalities in ¡ ¡ £ ¥ § © © time, and not allow the computation of the reached values for every clock except the global clock.

Applying our method to a synchronous product of the specification and the test purpose, we can have all test verdicts: conformance to specification and test purpose (pass verdict), conformance to specification but not to the test (inconclusive verdict) and conformance to test purpose but not to the specification or no conformance to specification and test purpose (fail verdict).

The test generation method proposed is potentially inefficient, because many paths may have to be synthesized and thereafter rejected by the feasibility analysis. The solution here is to modify the synchronous product by adding a checking step that consists in applying the method to every new node added to the already calculated path, and rejecting nodes that made this path unfeasible.

Our real-time model is quite restrictive and a generalization will be of benefit for real-time systems: especially the use of invariants and assignments. For the invariant of a state s, this invariant can be seen as the guard of a transition t that lead to s. If the specification includes constraints in the form P § ' ¥ D ( If this automaton does not have already one.

) If bounded intervals.

SIU 2003

Let us assume that

% R if i© R ¡ ! T §# £ © 4 ¡ R © R ¡ ! © such that % ' © % ¢ ' 4 § ¢ 1 , % P © ¡ ¨U © , R ¡ ¨U ' GP © R f ¡ ¨U ' P © , and let us prove that % R f f © R ¡ ! BT £ © ¢4 ¡ R © R ¡ ! © such that % ' © % ¢ ' 4 1 , % P © ¡ ¨U © , R ¡ ¨U ' P © R gf ¡ ¨U ' P © . While R ¡ ! BT £ © R ¡ ! T §# £ © , according to the induction assumption, there is R © R ¡ ! © such that % ' © % ¢ ' 4 § ¢ 1 , % P © ¡ ¨U © , R ¡ ¨U ' GP © R gf f ¡ ¨U ' P © .
Let us define the paths ! G " 0" 0" ¨¥ and ! G " 0" $" ¨¥ such that: For ! : %

P © ¡ ¨T © , ¡ ¨T ' GP © % R ¡ ¨T ' GP © c' R ¡ ¨T ' GP © 1 . For ! : % P © ¡ ¨T © , ¡ ¨T ' GP © % R gf f ¡ ¨T ' GP © ' R gf f ¡ ¨T ' GP © 1 .
For these paths, we have changed the specification constraints over clocks in transition ¨T . R is an execution of ! , then the constraints graph ¤ £ If passes by r aT . Let r U and r 2 be the neighbor nodes of r T in . Let us assume that there is an edge form r cU to r @T of weight A U GT and an edge from r @T to r 2 of weight A (T 2 . We have the following cases:

-If ' 6( 4 and § ( 4 . From the construction of the constraints graph, A U GT is negative and A T 2 is positive. Now if we consider the cycle f from ¤ £ 2 which has the same nodes as , then and f differ only on the weight of the two edges from r U to r T and from r T to r 2 . Let be A f U 2 and A (f T 02 the weights of this two edges in ¤ £ 2 . From the construction of the execution R , there is a F © ¡ such that % P © ¡ ¨T © , R ¡ ¨T ' GP © R gf f ¡ ¨T ' P © ¦ F or R ¡ ¨T ' GP © R gf f ¡ ¨T ' P © § F

(because R and R if f have the same values in every ¨U , ' less than 4 ).

Then A U GT Y¦ #A T 2 A f U 2 ¦ #A f T 2 . As f is positive then is also positive.

-If ' ( 4 ( § or § ( 4 ( 1' . Let P be the clock such that ¡ ¨T ' P © % § A U GT ' A U GT 1 . If is a negative cycle. Let ! f g G " 0" $" ¨¥ be the path such as:

¡ ¨T ' P © % § A U GT ' A U GT 1 . Then is negative cycle of ! f . It means that R gf f ¡ ¨T ' GP © A U GT 0 © ¢¡ £ ¡ ¨T ' P © is not a reached values of P in ¨T of ! . Then is positive.
We have showed that ¤ £ 4 does not have negative cycles, then ! is feasible. Let R be an execution of ! . The execution R defined by: For every ' in % ¢ ' 4 1 , and for every clock P in ¡ ¨U © : R ¡ ¨U ' GP © R gf f ¡ ¨U ' P © .

SIU 2003

Let ' ( 4 be the greatest index such that £ U ¥ H 4 £ ¡ 3& ' 0) © and . Then: 1. The suite ¤ converges to Proof. Let P and ' be the two clocks of ¡ ¨¥ © . There are two executions of ! , R and R , such that: R ¡ ¨¥ ' P © 8 a9 BA ¡ ¦¡ ¡ ¨¥ ' P © ¤£ © , R ¡ ¨¥ ' )' © 8 a9 eA ¡ ¢¡ ¡ ¨¥ ' (' © ¤£ © . Let ¡ T © T be the suite of execution defined by: R , w R . hT ¢ ¢¡ ¥ xT ¨ E¦ ¢ ¢¡ ¥ U , hT ¡ ¨¥ ' GP © £ hT ¡ ¨¥ ' P © ¦ ¡ T , and xT ¡ ¨¥ ' (' © hT ¡ ¨¥ ' )' © ¦ ¡ T such that:

¡ T H 4 £ ¡ ¥ 2 £¢ £ ¥¤ 2 £¦ ¢ ¥ 2 § £ T §# ' ¥ 4 §¢ £ ¥¤

¡ T H I4

£ ¡ hT ¡ ¨¥ ' GP © § £ £ ©¤ 2 § ¥¤ `" # ¢ £ § ¥¤ `" $# ' U ¡ ¨¥ ' (' © § £ ¢ £ ¥¤ 2 £¦ ¨ § ¤ `¤ # ¢ £ 4 ¨ § ¤ `¤ # © , if T ¡ ¨¥ ' GP © 8 @9 BA ¡ ¢¡ ¡ ¨¥ ' GP © ¢© . ' ( 4 is the greatest index such that 6U

¡ ¨¥ ' P © ( 8 a9 BA ¡ ¦¡ ¡ ¨¥ ' P © £ © .

¡ T H I4 £ ¡ U

¡ ¨¥ ' P © § £ £ ¥¤ 2 § ¥¤ B`" $# ¢ £ § ¥¤ `" $#

, hT ¡ ¨¥ ' (' © § £ ¢ £ ¥¤ 2 £¦ ¨ § ¤ `¤ # ¢ £ 4 ¨ § ¤ `¤ # © otherwise. ' ( 4 is the greatest index such that U ¡ ¨¥ ' )' © ( 8 a9 eA ¡ ¢¡ ¡ ¨¥ ' (' © ¤£ © .

According to lemma 12, the suite converges to an execution R such that R ¡ ¨¥ ' P © 8 a9 BA ¡ ¦¡ ¡ ¨¥ ' GP © ¤£ © and R ¡ ¨¥ ' (' © 8 a9 eA ¡ ¢¡ ¡ ¨¥ ' (' © ¤£ © . We have a similar proof for the second result.

After proving the result of this lemma, we will use the induction to generalize to H used clocks.

Proof of Lemma 8. We present here the proof of the lemma in the case of & B EF ¡ ¡ ¨¥ © © . For any H less than the number of clocks, the same proof holds by induction. We assume that the clocks of ¡ £¥ © are respectively P , ' and ¤ . Let us note by: 1 8 a9 eA ¡ ¢¡ ¡ ¨¥ ' ¤ © £ © ¦¥ 8 a9 eA ¡ ¢¡ ¡ ¨¥ ' P © £ © 8 a9 BA ¡ ¦¡ ¡ ¨¥ ' )' © £ © Let R , R and R be three executions of ! such that: R ¡ ¨¥ ' ¤ © ¡1 , R ¡ ¨¥ ' GP © ¥ and R ¡ ¨¥ ' )' © S . Now we define three paths ! , ! and ! such that: ! is the path ! without the constraint over ¤ , and ¡ £¥ ' GP © w % ¥ ' ¥ 1 , ¡ ¨¥ ' )' © % ' 1 . ! is the path ! without the constraint over P , and ¡ ¨¥ ' ¤ © w % 1 ' 1 1 . ¡ ¨¥ ' )' © % ' 1 . ! is the path ! without the constraint over ' , and ¡ ¨¥ ' ¤ © w % 1 ' 1 1 , ¡ ¨¥ ' GP © % ¥ ' ¥ 1 .

All these paths are feasible. In fact, if ! f is the path ! without the constraint over ¤ , then R and R are executions of ! f . According to lemma 13, for this path there is an execution R if of ! f such that : R if ¡ ¨¥ ' P © ¥ and R if ¡ ¨¥ ' (' © © © is the path such that § ! #" %$ '& )( 10 2 3 #2 54 , § 6 ! 87 %$ 9& )( 10 @ A #@ B4 and § C" D$ '& )( E0 § F # § G4 .

4 I

 4 . Berrada -R. Castanet -P. Félix

Figure 2 . 1 :

 21 Figure 2.1: Timed automaton A with global clock h.

6 I

 6 . Berrada -R. Castanet -P. Félix

7 3. 1 .Definition 4 .

 714 Reached Values of a Constraint in a Transition Let ¢¡ ¡ ¨T ' P © ¤£ denote a subset of ¡ ¨T ' P © . ¢¡ ¡ ¨T ' P © ¤£ is the reached values set of the clock P in transition ¨T if:

.Example 3 . 1 .

 31 Fig. 2.1.

Figure 3 . 2 :

 32 Figure 3.2: Out reach intervals.

10 I

 10 . Berrada -R. Castanet -P. Félix Definition 9 (Constraints Graph.). Let be a set of variables and " a con- junction of atomic terms of the form P § P f ¥ D , with ¡ 3P 6' P f © © ¡ £¢ ¦ and D © . The constraints graph associated to " is a valuated directed graph

Theorem 5 .

 5 Given a path ! from the initial state of a TAGC 1 , with £ transitions and § clocks, the computation of the reached values of the global clock ¤ can be solved in time ¡ ¤£ ¥ § © . SIU 2003 Input: A timed path . Output: The reached values of clock ¡ . Data Structure: A system ¢ ¤£ , and a vector ¥ of ¦ variables ¥ ¨ § . Begin Phase One: Checking the feasibility of . /* ¢ £ is empty at the beginning*/ /* Checking if© ¡ © § § 3 ! #" has a WF suite * / Compute the suite © ¡ © § § 3 ! #" ; If © ¡ $© § § 3 ! %" does not have a WF sub suite Then exit; For & (' ) 10 To ¦ Do ¢ 32 4© 5 § 56 7¡ ' ) ¡ © 5 § ; End For Phase Two: Filling ¢ £ . /* Adding relation inequalities (Lemma 3) */ For & (' ) 8¦ To 0 Do If

12 I

 12 . Berrada -R. Castanet -P. Félix

4 Figure 5 . 4 :

 454 Figure 5.4: A weakly feasible path.

4

 4

Figure 5 . 5 :

 55 Figure 5.5: A strongly feasible path.

4

 4

Figure 5 . 6 :

 56 Figure 5.6: Temporal path example.

  .7. At the beginning of the algorithm, ¦ ¨ § % § B1 % ' 1 contains the lower bound of the specifi- § B1 % ' 1 the upper bound of the specification constraint over P (i.e. 8 a9 BA ¡ ¡ ¡ ¨ 2 ' GP U © ¢© ). In the first phase, the algorithm computes the reached values of the global clock. For every clock P in a transition ¨T , last reset in the initial state, its reached values are the one of the clock ¤ (i.e. ¢¡ ¡ ¨T ' GP © © ¢¡ ¡ ¨T ' ¥¤ © ). ¦ § and ¦ © are then updated.The second phase consists in a loop on transitions starting from ¨ . For every transition, we check the emptiness of the set of associated clocks reset. If it is empty then we increase the current transition index ¨T . In the opposite, we start computing the maximal and the minimal delay from the currant transition to any transition of the path. This is done by computing the reached values of ¤ for paths ! and ! . We notice that ! and ! are defined such that R ¡ ! © and R ¡ ! © contain all executions that take simultaneously, re- spectively the maximal and minimal reached values over clocks of the current transition ¨T (Sets R ¡ ! © and R ¡ ! © are non empty according to lemma 9).

16 I

 16 . Berrada -R. Castanet -P. Félix Input: A feasible timed path ) G 3 ¡ ¢ ¢ ! with ¦ states and £ clocks. Output: Computation of reached values for every clock. Data Structure: ¤ ¦¥ and ¤ ¦ § a two dimensional arrays of size ¦ ©¨£ . Temporary Variables: Two paths 3 ) G 3 ¢ ¢ ! and ) G 3 ¡ ¢ ! Begin: Phase One: Filling ¤ ¦¥ and ¤ § with reached values of clocks last reset in the initial state.

Figure 6 . 7 :

 67 Figure 6.7: Reached values computation algorithm.

Figure 7 . 8 :

 78 Figure 7.8: Test specification.

Definition 12 .

 12 Let A % D be a specification and © ¢ a test purpose. The synchronous product of A % D and © is the I/O automaton ¤£ defined as follows.

Figure 7 . 9 :

 79 Figure 7.9: Test purpose 1.

Figure 7 . 11 :

 711 Figure 7.11: Test purpose 2.

Figure 7 . 15 :

 715 Figure 7.15: Test cases.

  Figure C.16: Constraints graph associated to ¢¡ .

Figure

  Figure C.19: Constraints graph associated to © © . Let us prove that © © is feasible. In fact, let IH QP , RH CS , RH CT and H © © be the constraints systems obtained from the algorithm of Fig. 4.3 respectively for paths ¤£ , ¡ , ¢¥ and © © . Let U BH QP , U BH CS , U BH CT and U H © © be the constraints graphs respectively associated to IH QP , RH CS , RH CT and H © © . The graphs U BH QP , U BH #S , U BH CT

  1

						"main"
						2004/3/5
						page 9
	A Formal Approach for Real-Time Test Generation			9
	3. For every 4 in % ¢ ' ¢£ 1 , for every	P in	¡ ¨T ©	being last reset in	¨U ' ' )( 4 :
	,	7 T " ¤ ¡ ¨T © .
	According to the clock h.
		SIU 2003

Lemma 8 .

 8 Let us assume that ! is feasible. If & e EF ¡ ¡ ¥ © ¢© H :

	1. If for every 4 in % ¢ ' ¢£ 1 , ¢¡ ¡ ¨T ' ¥¤ © §£ that takes simultaneously the 8 a9 BA 2. There is an execution that takes simultaneously the 4 is bounded. Then there is an execution ¡ ¦¡ ¡ ¨¥ ' GP © §£ © , for every P in ¡ ¨¥ © . £ 65 ¡ ¢¡ ¡ ¨¥ ' P © ¤£ © ,
	for every

  , and fires as soon (resp. late) as possible transitions after ¨U (the existence of R and R are ensured by the strong feasibility of ! ). For these executions, the delay between the instant of firing ¨U and the instant of firing every transition ¨T , ' ¥ 4 , is less (resp. more) than the delay between ¨U and ¨T for any other execution of this path. This result is proved in the next lemma.

	every 4 g¥ ' Lemma 10. Let us assume that
	¦ See lemma 6. § m less than 4 ©	¢ 4	¢ 05 £ ¤ .
			SIU 2003

  obtained from the algorithm of Fig.4.3 for ! , does not have negative cycles. Let us prove that the constraints graph ¤ £ does not have negative cycles. In fact, these two graphs differ only for edges weight between vertexes r T and r U , for ' less than 4 . For each cycle which passes only once by a vertex of ¤ £

	to the system £	2 , associated

2 4 , associated to the system £ 4 4 , we have: If does not pass by r T : is also a cycle of ¤ £ 2 , and can not be a negative cycle.

  2 £¦ ¢ ¥ 4 § £ U be the greatest index such that £ U ¥ H 4 £ ¡ 3& ' 0) © and £¢ £ ¥¤ 2 £¦ ¢ ¥ 2 § ¡ T ' ¥ 4 §¢ £ ¥¤ 2 £¦ ¢ ¥ 4 § ¡ T

	2. Else Let ' ( 4 ¡ T H 4 £ ¡ ¥ 2 £¢ £ ¥¤ 2 £¦ ¢ ¥ 2 Then T ¡ ¥ 2 Lemma 12. Let be ¡ 3& ' 2& © and	§ ¡ ) £ U ' 2) © © I ¡ ' § 4 ¢ £ ©¤ 2 ¦ ¢	§	4	§	© . £ T ¨ ¤# © .

© .

D ¥

P § ' , by adding the inequality r 2 § gr U ¥ D 0D ¥ r 2 § gr U to algorithm (Fig. 4.3), we obtain the same result for the computation of the reached values of the global clock. We are interested in building a finite and complete test set for real-time systems as in [START_REF] Springintveld | Testing Timed Automata[END_REF]. We are working to widen the assignments, such that for a clock x, we allow x=:a, to add variables and parameters to the model and to see how to apply the method in the case of systems interoperability.

Appendix A. Proof of Lemma 6

Proof. For 4 in % ¢ ' £ 1 , and a clock P © ¡ ¨T © , being last reset in (2 , § ( 4 , we notice that: 8 a9 eA ¡ ¢¡ ¡ ¨T ' ¤ © ¢© § 8 a9 eA ¡ ¢¡ ¡ (2 ' ¤ © ¢© © ¡ ¨T ' GP © " In fact, according to lemma 3:

For 8 a9 BA ¡ ¢¡ ¡ (2 ' ¥¤ © © , ¡ r @T © ¢¡ ¡ ¨T ' ¤ © such that r @T § 8 a9 eA ¡ ¢¡ ¡ (2 ' ¤ © ¢© © ¡ ¨T ' P © . Then 4 £ 65 ¡ ¡ ¡ ¨T ' P © ¢© ¥ "8 @9 BA ¡ ¢¡ ¡ ¨T ' ¤ © ¢© § 8 a9 eA ¡ ¢¡ ¡ (2 ' ¤ © ¢© . We construct then, the execution R ¢ defined by, for every 4 in % ¢ ' ¢£ 1 and every

The two-dimensional array R ¡ is an execution of ! that verifies the first as- sertion of the lemma. We use a similar proof for the second assertion of the lemma.

Appendix B. Proof of Lemma 7

Proof. Let us note by: for every 4 in % ¢ ' £ 1 , ! T £ G " 0" $" ¨T the sub-path of ! obtained while replacing ¡ ¨U ' GP © by ¢¡ ¡ ¨U ' P © £ for every ' in % ¢ ' 4 1 . As the lemma assumes the feasibility of ! , then ! T £ is also feasible. Now, by induction, let us prove that,

For every

§ in % 4 x¦ ¢ ' ¢£ 1 , and for every clock P in ¡ ¨2 © : R ¡ ¨2 ' P © R ¡ ¨U ' P © .

is an execution of ! that meets R f f . We use a similar proof for the second assertion of the lemma.

Appendix C. Proof of Lemma 8

Let

, and the suite ¤ and defined by: ) does not have either a negative cycle. In fact, if there is a negative cycle then there is at least one cycle which passes one time by some nodes of the graph. If passe by ¤ £ , then one of the graphs ¤ £ 2 , ¤ £ 4 , ¤ £ ¡ has a negative cycle. We use a similar proof for the second assertion of the lemma.

Appendix D. Proof of Lemma 10

Proof. Let R be in R ¡ ! © . Let us prove, by induction, % (4

For 4 ' ¦ ¢ , since R is making the minimum delay between transitions after ¨U , then it takes the minimum of the interval of a clock ' in ¨U ¢ .

If ' is last reset in ¨U , then we have

' © , we have then the result of the lemma.

Now, let us us assume the lemma for ' ©( 4 and let us prove the lemma for 4 ¦ ¢ . Since R is making the minimum delay between transitions after ¨U , then it takes the minimum of the interval of a clock ' in ¨T ¢

, ' is last reset in )2 , § ( ' . While R ¡ ¨U ' (' © ¥ R ¡ ¨U ' )' © and R ¡ ¨T ¢ ' )' © ¥ R ¡ ¨T ¢ ' )' © , then R ¡ ¨T ¢ ' (' © § "R ¡ ¨U ' (' © ¥ R ¡ ¨T ¢ ' )' © § wR ¡ ¨U ' )' © We use a similar proof for the second assertion of the lemma.

Authors addresses:

LaBRI -CNRS -UMR 5800 Université Bordeaux 1 33405 Talence cedex France berrada@labri.fr, castanet@labri.fr, felix@labri.fr SIU 2003