B Darbois Texier

A Seguin

Successive re-intrusions in a granular medium

We measure and analyze the drag force experienced by a rigid rod that penetrates vertically into a granular medium, partially withdraws before sinking again. The drag during the successive reintrusions is observed to be significantly smaller than the force experienced in the first run. Two force regimes are evidenced depending on how the re-intrusion depth compares with the withdrawal distance ∆. These two regimes are characterized by a force curve of positive and negative curvature and are separated by an inflection point which is characterized experimentally. We approach the difference between the first intrusion and the following re-intrusions by considering a modification in the stress field of the granular material after the partial extraction of the rod. A theoretical model for the stress modification is proposed and allows to rationalize all the experiments realized for different withdrawal distances ∆. This framework introduces a crossover length λ above which the stress modification in the granular medium is maintained and that is shown to depend linearly on ∆. Finally, the model provides a prediction for the location of the inflection points in reasonable agreement with observations.

I. INTRODUCTION

Intrusion in a non-cohesive soils is a problem of primary importance for civil engineering, geophysical surveys and animals living in sandy grounds. The development of efficient drilling or probing techniques [1] requires a detailed understanding of the interaction between the intruder and the soil. The survival of animals in sandy environments such as sandfish lizards or sea clams also depends on their capacity to hide beneath the sand surface [2,3]. In all these situations, the burial of the intruder causes a flow of material [4] and leads to a large vertical resistance that can be seen as a drag force. This drag force has been extensively studied in dry granular media which provide an easy-to-use model soil for modelling these problems.

The drag applied on a rod when it experiences a continuous vertical penetration or extraction in a granular medium at slow speed has already been studied [5]. The force measured during intrusion is an order of magnitude larger than that experienced during extraction. To rationalize these observations, a power law is proposed to describe the quasi-static drag force F in both directions of motion with the following form F/ρgπD 3 = C(z/D) λ where z is the depth of the tip of the intruder, D its diameter, ρ the material bulk density, g the gravity. C and λ are two non-dimensional coefficients that depend on the direction of motion. For a rod, they measured C 9.5 and λ 1.6 in penetration, C -0.66 and λ 1.3 in extraction. In the case of penetration alone, another model has been proposed considering that the drag force comes from the contribution of two terms: one coming from the hydrostatic-like pressure at the tip of the rod F ∝ z and another resulting from the friction applying on the lateral surface F ∝ z 2 [6]. Recently, the penetration of objects at shallow depths has shown the presence of a particular regime where the drag force is closely related to the Archimedean force with a pre-factor that strongly increases with the effective friction coefficient of the granular medium [7,8]. This hydrostatic-like regime is not dominant as soon as the depth of the intruder becomes large enough, i.e. after a few object diameters (z 2D). In the case of extraction, the force corresponds approximately to the weight of the granular column above the object. The asymmetric behaviour of the drag force between intrusion and extrusion phases has also been demonstrated in other experimental studies [9,10]. This difference is explained by the fact that in extraction the drag force corresponds essentially to friction on the surface of the rod, unlike penetration where most of the force comes from the compression of the packing under the rod, i.e. the increase of the volume fraction under the rod. The geometry of the object has been modified and this difference between penetration and extraction remains similar [11].

Nonetheless, all these studies focus on a single and continuous intrusion or extrusion of the intruder in a granular medium. However, the motion of intruders in practical applications and natural conditions are often more complex than a continuous motion and may include vibrations of small amplitude, rotations and back and forth movements. This is the case in ground drilling where penetration/extraction cycles are required to remove the excess of material and in anchoring problems where the anchor must resist periodic loads [12]. In nature, sea clams use a cyclical movement strategy called "push and pull" to penetrate up to two meters deep into the sediment [3,13]. On earth, the burrowing worms employ peristaltic waves to progress into non-cohesive substrates [14]. The presence of mechanical vibrations at the surface of the intruder has been proved to fluidize locally the granular medium and to reduce significantly the intrusion force [15,16]. Adding a rotational component to the progressive motion has been shown to be an effective strategy for reducing the resistance to intrusion [17] and the drag force of an object moving horizontally [18]. The case of back and forth motions was studied by examining the response of granular materials in a shear cell subjected to repeated cycles [19][20][21][22][23] and to cyclic horizontal motion of an object [24]. These experiments reveal that after shear reversal, the shear stress follows an exponential evolution towards its nominal value which is due to the reorientation of force chains in the medium. However, the effect of back and forth motions on the intrusion force to penetrate a granular medium is under-explored while this configuration cannot be inferred from previous studies because the orientation of gravity changes the flow of material and the structure of the force network. The goal of this study is to fill this gap and consider the force experienced by an intruder in a granular medium has it undergoes a succession of vertical intrusion and extrusion phases.

In this paper, we study experimentally the reintrusion of a rigid rod after a first intrusion step and a partial extraction. By performing successive cycles of extrusion and re-intrusion of asymmetric amplitude, we evidence two different regimes for the drag force during re-intrusions. Depending on the depth of reintrusion and the withdrawal distance, the drag can either increase supralinearly or sublinearly with depth. The transition between these two behaviors is characterized by an inflection point in the evolution of the drag force with depth. We first detail the experimental procedure followed to measure the drag force. Then, we present the results that demonstrate the existence of two regimes. Finally, we propose a model based on regularization of the stress in the granular medium after the passage of the intruder and that captures our observations.

II. EXPERIMENTAL SETUP

The experiments consist in plunging downwards a vertical rigid rod into a dry granular medium (Fig. 1). The rod has a diameter D = 12 mm, a length L = 300 mm and is ended by a conical tip of angle 60 • . The rod is made of steel and its surface has been polished to reduce the effect of surface roughness. Granular matter is made of sieved glass beads of diameter d = 1 mm and density ρ = 2.5 × 10 3 kg.m -3 . The dispersion in size for these beads is smaller than 10%. The grains are poured in a cylindrical container of diameter D c = 80 mm and height 250 mm. In all our experiments, a minimal distance of 50 mm is let between the tip of the rod and the bottom of the container in order to avoid the influence of the bottom wall [25]. The initial prepara-

Load Cell + Translation Stage Rod D z ' z 0
Granular Medium tion of the granular medium is realized by tapping the containers at least ten times before each experiment, a procedure that permits to reach an initial packing fraction of φ 0.63 with a good reproducibility. The rod is mounted on a translation stage that allows a precise control of the vertical displacement of the rod. In our experiments, the intruder velocity V 0 is maintained constant between 0.1 and 1 mm/s which insures to lay in the quasi-static regime where granular forces does not depend on the velocity of the intruder [26,27]. The vertical force experienced by the rod during its motion is measured with a force sensor placed at the base of the rod and that has a resolution of 10 mN. A typical experiment consists in placing the tip of the intruder just above the horizontal granular surface and plunging the rod up to a given depth z 0 below the surface and then extracting the rod by a withdrawal distance ∆ before plunging again the rod up to larger depths. Note that the variation of the filling level of the grains corresponds to the volume of immersed rod. This intrusion/extrusion cycles can eventually be repeated several times at different depths z 0 and for different cycle amplitudes ∆.

III. RESULTS

In this study, we consider as a reference case the intrusion of the rod at a constant and low velocity without cycles. A previous study has shown that this force results from two contributions: the hydrostatic-like pressure applying on the tip of the rod and the frictional force exerting along its length [6]. They provided the following expression for the vertical force F 0 experienced during a continuous intrusion:

F 0 πφρgD 3 /4 = C 1 z D + C 2 z D 2 (1)
where C 1 and C 2 are non-dimensional coefficients that are determined experimentally. In our system, the vertical force F 0 experienced by the rod as a function of depth z is shown in figure 2 by the way of a black solid line. The best fit of our data with Eq. ( 1) is found for

C 1 = 10 ± 2 and C 2 = 19 ± 1.
These values lay in the same range as previous estimations for flat-ended rods penetrating into glass beads [6]. Due to the finite size effect of the container, possible wall effect generated by friction may be expected [28][29][30]. However, the effective friction due to the presence of these walls is contained in the value of the coefficients C 1 and C 2 of the equation 1. We therefore expect that the dimensions of the container will influence these two coefficients. We always keep the same container dimensions for all measurements.

A. Successive re-intrusions at constant ∆ We are first interested in the resistance experienced by the rod as it undergoes successive intrusion/extrusion cycles for given z 0 and ∆. Figure 2 shows the vertical force F as a function of the intrusion depth z for the first (black solid line) and nine successive extrusion/intrusion cycles (color solid lines). We observe that when the rod moves upwards, the force decreases over a very short distance, of the order of a millimeter, the diameter of a grain. This behavior is related to the fact that the surface of the rod is smooth and would be different for rough surfaces. Since the extrusion force remains at a very low level during all the extrusion phase, we did not focus on this phase in the following of the study. When the rod moves downwards again (blue solid line), the depth-force curve follows a very different path than the first intrusion and finally recovers the nominal value, F 0 , at the initial depth, z z 0 . The evolution of the force F with z during the successive re-intrusions is clearly below the initial force. In term of energy, the work necessary to re-intrude on a distance ∆ is about 36 % lower than the initial work required to penetrate on the same distance during the first intrusion. Importantly, we note that all the following cycles do superimpose. This observation is confirmed by the inset of Fig. 2 . This graph shows that ( -0 )/D increases with N before saturating towards a constant value. Finally, the variation of ( -0 )/D after the first re-intrusion remains small (less than 5 % in relative value) and the most significant changes occur during the first intrusion/extrusion cycle. For this reason, we will only consider the first cycle in the following of the article.

B. Re-intrusions at different values of ∆

In this section, we focus on the drag force F as the rod undergoes successive re-intrusion cycles with different amplitudes ∆ but constant initial intrusion depth z 0 . These results are shown in figure 3 for z 0 = 170 mm and extrusion distances ∆ ranging from 3 mm to 100 mm. As noted previously, one can notice the significant differences between the first intrusion and the second reintrusions. For each withdrawal distance ∆, the path followed by the re-intrusion force is different and the curves only superimpose when the depth reaches approximately z 0 . At this depth, the re-instrusion force recovers the nominal value experienced during the first intrusion. We remark that the beginning of the re- intrusion force curve has a similar shape to the curve of the first intrusion with a supralinear growth, corresponding to a positive curvature. At larger re-intrusion depths, the force curve changes in behavior to tangent the initial curve and recovers the same level as during the first intrusion. In this domain, the curvature of the force curve is negative. These two regimes are separated by an inflection point of the force curve, whose depth is noted z i . We estimate the location of the inflection point by calculating the curvature of the experimental force curve and determining the depth at which the curvature changes its sign. The results of this procedure are indicated with crosses in Fig. 3. These results are also presented separately in Fig. 4 which shows the normalized depth of the inflection point z i /z 0 as a function of the normalized withdrawal distance ∆/z 0 . We observe a decrease of the depth of the inflection point as the withdrawal distance increases before the data become dispersed at large ∆. Note that we do not present the extreme case ∆ = 170 mm since the curve obtained is similar to the curve of the first run. To summarize, the re-intrusion curves show two regimes: a first regime where the force growth is similar to the first intrusion and that takes place at the beginning of the re-intrusion (z 0 -∆ < z < z i ) and a second regime where the force inflects toward the initial curve which occurs when z gets closer to z 0 (z i < z < z 0 ). Overall, this behavior describes the fact that the effort to partially plunge back into a granular material is weaker at shallow reintrusion depths but ultimately, the initial force level is recovered as soon as the the intruder returns to z 0 . 3. The circles represent the measurements where the force curvature at z = zr is lower than signal fluctuations and thus the determination of zi is uncertain. The prediction of Eq. ( 5) for λ = 0.70∆ is represented by solid line for short withdrawal distances and dashed line for large withdrawal distances.

As a consequence, it is illusory to attempt reducing the drag force on a intruder by realizing non-symmetric intrusion/extrusion cycles since the force always recover its nominal value F 0 at the initial depth.

IV. DISCUSSION

In order to understand the origin of the force reduction during re-intrusion, we look for a change in the packing fraction of the granular medium along the successive cycles . We deduce the mean packing fraction of the medium by tracking the height of the free surface during intrusion/extrusion cycles. These experiments show that the volume change detected at the free-surface is equal to the volume of the intruder that plunges or retracts from the medium within measurements uncertainties. Thus, the change in the forcecurve between first and following intrusions is unlikely to be the result of dilatancy effects but should rather result from stress modification in the medium [31,32]. The modeling of the drag force on objects in granular media is most often based on the granular resistive force theory [18,[33][34][35][36][37]. In the current experiment, the extraction generates a local decrease of the packing fraction at the end of the stem, creating a flow of grains from dense to less dense zones. Thus, the reorganization of the medium during extraction causes a modification of the initial stress in the granular medium and it is dif- ficult to place oneself in the framework of this theory.

In the following, we develop a description of the stress σ zz in the granular material along the successive reintrusions. During the first intrusion up to a depth z 0 , the stress σ zz in the granular column has a hydrostaticlike dependency such that σ zz ∼ φρgz. During the extraction, the intruder returns to a depth z r = z 0 -∆ and granular avalanches fill the wake left by the object during its ascension [38], thus creating a new column of grains. When stopping at a depth z r , a free surface is created just below the tip of the intruder, which is compatible with a zero force measured on the intruder at this position (Fig. 2). During re-intrusion, the intruder should experience a new stress that writes σ zz (r) ∼ φρg (z -z r ), since the free surface is now lo-cated at z r = z 0 -∆. However, in the depths of the medium, the stress σ zz still respects σ zz (i) ∼ φρgz. These two states of stress field are not compatible and should be reconciled at intermediate depths. For short extrusion distances ∆ and large depths z 0 , the depthforce curve is sub-linear and is a concave function (inset of Fig. 3). On the contrary, for large extrusion distances and small depths, the depth-force curve is supra-linear with a positive curvature (Fig. 3). In order to unify the two stress profiles, we suggest a continuous transition between them that is accounted by introducing an effective depth z eff which is a weighted average between z and z -z r :

z eff = (z -z r ) e - z -z r λ + z   1 -e - z -z r λ   , ( 2
)
where λ is the characteristic length of this transition. Note that the two exponential terms in this relation correspond to an arbitrary choice of weighting functions and do not correspond to a Janssen saturation of the stress in the granular medium. With this definition, the effective depth z eff is equals to z -z r at small re-intrusion depths (z -z r λ) and tends to z at large depths (z -z r λ). Implementing the regularized stress profile φρ g z eff in the equation 1, we get the following expression for the re-intrusion drag force:

F (z eff ) πφρgD 3 /4 = C 1 z eff D + C 2 z eff D 2 , (3)
where z eff is given by Eq. ( 2). This expression can be re-expressed preferably by normalizing the drag force by the initial force at a depth z = z 0 , F 0 (z 0 ), resulting in:

F (z eff ) F 0 (z 0 ) = C1 z eff z 0 + C2 z eff z 0 2 , (4)
where C1 = πφρgD 2 C 1 F 0 (z 0 )z 0 /4 and C2 = πφρgDC 2 F 0 (z 0 )z 0 /4. This prediction can be compared with our observations realized for different cycle amplitudes (Fig. 3). For this purpose, we consider the crossover length λ as a free parameter and we look for the values that provide the best fit of our data. Figure 5(a) presents the experimental result of the drag force F (z eff ) normalized by the nominal force at a depth z 0 , F 0 (z 0 ) as a function of the effective depth z eff normalized by the initial depth z 0 . The normalization with respect to the length z 0 is justified by the fact that the reintrusion force recovers its nominal value around this depth. It can be seen that all the curves of Fig. 3 collapse on a master curve which is the prediction of Eq. ( 3) with the coefficients C 1 and C 2 determined for the first intrusion (see section III). This collapse proves the validity of the proposed model over the range of parameters investigated in this study. In addition, the characteristic length λ estimated through this procedure is shown as a function of the withdrawal distance ∆ in Fig. 5(b). We observe a linear relation between λ and ∆ over two decades which is consistent with the qualitative observations made previously. The best fit of these data with a linear trend provides a slope of 0.70 ± 0.05.

Besides, this model also gives a prediction for the depth z i at which the inflection occurs. The inflection point corresponds mathematically to d 2 F/dz 2 z=zi = 0 which can be calculated from Eqs. ( 2) and (3). It leads to an implicit relation for z i :

2e - z i -z r λ + λ -z i z r - C 1 D 2C 2 z r + λ z r 2 e z i -z r λ = 0
(5) with z r = z 0 -∆. The previous relation has no trivial solution and we solve it numerically. The numerical solution of Eq. ( 5), z i , is plotted in Fig. 4 as a function of ∆ with a black line where we have assumed that λ = 0.70 ∆ consistently with the fit of our data. We observe that the predicted depth of the inflection point coincides with z 0 for zero withdrawal distances ∆ and moves closer to the surface when ∆ increases before falling back z 0 for larger ∆ (dashed portion of the line in Fig. 4). In addition, no inflection points are expected above a critical withdrawal distance of ∆ 0.34 z 0 . The predictions of the model are in very good agreement with our measurements for small withdrawal distances (∆ < 0.25 z 0 ). For larger withdrawal distances, we do not observe experimentally the increase of z i with ∆, showing the range of application of this model. Concerning the large shrinkage distances ∆ > 0.34 z 0 , we are not able to rule out experimentally the presence of an inflection point because of the existence of experimental noise. However, we distinguish in figure 4, the measurements of z i where the initial curvature d 2 F/dz 2 z=zr is larger than the mean fluctuations of the force curvature (this situation is indicated by crosses) and where it is smaller (indicated by circles) and the existence of the inflection point is not certain. With this distinction, the disappearance of the inflection point predicted theoretically for ∆/z 0 > 0.34 is not incompatible with our measurements. Finally, the proposed model is accurate to rationalize our observations at small withdrawal distances ∆/z 0 < 0.25 and give potential trends for large ∆.

V. CONCLUSION

In this paper, we focus on the drag force during the re-intrusion of an object into a granular material after its partial extraction. Experiments show that the re-intrusion force at the beginning is significantly lower than the force experienced during the first penetration. When the object regains its initial depth in the medium, this behavior fades and the drag force returns to its nominal level. We evidence two force regimes: a first regime where the re-intrusion force starts from zero and increases rapidly with depth adopting a positive curvature and a second regime where the force bends back to the initial intrusion curve and exhibits a negative curvature. These two regimes are separated by an inflection point which has been characterized experimentally. The transition between these two regimes is rationalized by the introduction of a crossover length λ. This length ensures a continuous transition between the two stress profiles present in the granular packing: the stress profile existing before the initial penetration and the stress profile created during the extraction by the filling of the wake of the object. The predictions of this model compare well to our observations both in term of force curve and location of the inflection point. The crossover length λ is shown to scale linearly with the withdrawal distance ∆.

The understanding of the transition between two force regimes during re-intrusion relies on the microscopic properties of the material and the internal structure of the packing. This should motivates future numerical simulations to establish how the stress field in the granular medium evolves during the partialextrusion and the successive intrusions of an object. Also, it would be interesting to extend the present study in specific regimes where the intruder motion should be faster than the characteristic avalanche time at the tip of the rod and to immersed granular medium where the interstitial fluid flow add further physical ingredients to the problem.

Figure 1 .

 1 Figure 1. Sketch of the experimental setup and notations.

Figure 2 .

 2 Figure 2. Drag force F experienced by a rod of diameter D = 12 mm as a function of the depth z for successive intrusion/extrusion cycles realized for z0 = 170 mm and ∆ = 80 mm. The rod is displaced at constant velocity V0 = 0.3 mm.s -1 in glass beads of mean diameter d = 1 mm. The gray solid line corresponds to the force experienced during the first continuous intrusion. Color solid lines from blue to red represent the following nine extrusion/intrusion cycles. The dark dashed line corresponds to the best fit of the first intrusion with Eq. (1). The horizontal dash line indicates F = 10 N which intersects the force curves in 0 and for the first and successive intrusions respectively. Inset: ( -0)/D as a function of the cycle number N .

Figure 3 .

 3 Figure 3. Drag force F on the rod as a function of the penetration depth z for different cycle amplitudes ∆ and a constant initial depth z0 = 170 mm. Color code spans from blue to red for 3 ≤ ∆ ≤ 100 mm respectively. The black line represents the initial run. Inset: Zoom in of the same data around z0. Crosses indicate the inflection points where d 2 F/dz 2 = 0.

Figure 4 .

 4 Figure 4. Normalized depth of the inflection point zi/z0 as a function of the normalized withdrawal distance ∆/z0. The inflection points (crosses) are deduced from the re-intrusion curves presented in figure3. The circles represent the measurements where the force curvature at z = zr is lower than signal fluctuations and thus the determination of zi is uncertain. The prediction of Eq. (5) for λ = 0.70∆ is represented by solid line for short withdrawal distances and dashed line for large withdrawal distances.

Figure 5 .

 5 Figure 5. (a) Normalized drag force F/F0(z0) as a function of the normalized effective depth z eff /z0. Color code spans from blue to red for 3 ≤ ∆ ≤ 100 mm respectively. The black line correspond to Eq. (3). (b) Crossover length λ as a function of the re-intrusion depth ∆. The dashed line corresponds to the equation λ/z0 = 0.70 ∆/z0 and correspond to the best fit of the data.

ACKNOWLEDGMENTS

We are grateful to L. Auffray, J. Amarni, A. Aubertin, C. Manquest and R. Pidoux for the development of the experimental setup. This work is supported by ANR PIA funding: ANR-20-IDEES-0002.


Marius Bozga

Jean-Claude Fernandez

Lucian Ghirvu Z Z ,

Susanne Graf

Jean-Pierre Krimm

Laurent Mounier

Joseph Sifakis

IF: An Intermediate Representation for SDL and its Applications

Keywords: Sdl, Static Analysis, Validation, Model-Checking, Test, Test Generation

We present work of a project for the improvement of a speci cation/validation toolbox integrating a commercial toolset Objectgeode and di erent validation tools such as the veri cation tool cadp and the test sequence generator tgv.

The intrinsic complexity of most protocol speci cations lead us to study combination of other techniques such as static analysis and abstraction together with the classical modelchecking techniques. Experimentation and validation of our results in this context motivated the development of an intermediate representation for sdl called if. In this intermediate representation, a system is represented as a set of timed automata communicating asynchronously through a set of bu ers or by rendez-vous through a set of synchronization gates. The advantage of the use of such a program level intermediate representation is that it is easier to interface with various existing tools, such as static analysis, abstraction and compositional state space generation. Moreover, it allows to de ne for sdl di erent, but mathematically sound, notions of time.

We illustrate the use of if on a small example, a distributed leader election algorithm, on which we perform experimentation using static analysis and compositional generation.

1 Introduction sdl and related formalisms such as msc and ttcn are at the base of a technology for the specication and the validation of telecommunication systems. This technology will be developing fast due to many reasons, institutional, commercial and economical. sdl is promoted by Itu and other international standardization bodies. There exist commercially available tools and most importantly, there are increasing needs for description and validation tools covering as many aspects of system development as possible. These needs motivate the work for enhancement of the existing standards undertaken by Itu and Etsi, in particular.

Among the work directions for improvement of sdl, an important one is the description of non functional aspects of the behavior, such as performance and timing. Finding a \reasonable" notion of time is a central problem which admits many possible solutions depending on choices of semantic models. This is certainly a non trivial question and this is re ected by the variety of the existing proposals.

Choosing an appropriate timed extension for sdl should take into account not only technical considerations about the semantics of timed systems but also more pragmatic ones related to VERIMAG-Centre Equation, 2 avenue de Vignate, F-38610 Gi eres, e-mail: Marius.Bozga@imag.fr y LSR/IMAG, BP 82, F-38402 Saint Martin d'H eres Cedex, e-mail: Jean-Claude.Fernandez@imag.fr z Work partially supported by R egion Rhône-Alpes, France 1 the appropriateness for use in a system engineering context. We believe that the di erent ideas about extensions of the language must be validated experimentally before being adopted to avoid phenomena of rejection by the users. Furthermore, it is important to ensure as much as possible compatibility with the existing technology and provide evidence that the modi ed standard can be e ciently supported by tools.

Another challenge for the existing technology for sdl to face the demand for description and validation of systems of increasing size, is to provide environments that allow the user to master this complexity. The existing commercial tools are quite satisfactory in several respects and this is a recognized advantage of sdl over other formalisms poorly supported by tools. However, it is necessary to improve the existing technology to avoid failing to keep up. Mastering complexity requires a set of integrated tools supporting user driven analysis. Of course, the existing tools such as simulators, veri ers, automatic test generators can be improved. Our experience from real case studies shows that another family of tools is badly needed to break down complexity. All the methods for achieving such a goal are important ranging from the simplest and most \naive" to the most sophisticated.

In this paper we present work of a project for the improvement of a speci cation/validation toolbox interconnecting Objectgeode Ver96] and di erent validation tools such as cadp FGK + 96] developed jointly with the Vasy team of Inria Rhône-Alpes and tgv FJJV97] developed jointly with the Pampa team of Irisa. The project has two complementary work directions. The rst is the study and the implementation of timed extensions for sdl; this work is carried out in cooperation with Verilog, Sema Group and Cnet within a common project. The second is coping with complexity by using a combination of techniques based on static analysis, abstraction and compositional generation. Achieving these objectives requires both theoretical and experimental work. Experimentation and validation of our results in this context motivated the development of an intermediate representation for sdl called if. if is based on a simple, and semantically sound model for distributed timed systems which is asynchronously communicating timed automata (automata with clocks). A translator from a static subset of sdl to if has been developed and if has been connected to di erent tools of our toolbox. The use of such an intermediate representation confers many advantages.

It is possible to implement and evaluate di erent semantics of time for sdl as the underlying model of if is general enough to encompass a large variety of notions of urgency, time non determinism and di erent kinds of real-time constructs. if allows a attened description of the corresponding sdl speci cation with the possibility of direct manipulation, simpli cation and generally application of analysis algorithms which are not easy to perform using commercial tools which, in general, are closed. if can be considered as a common representation model for other existing languages such as Promela or for the combination of languages adopting di erent description styles.

Related work

After its standardization in the eighties, a lot of work has been done concerning the mathematical foundations of sdl. The rst complete semantics was given by the annex F to the recommendation Z.100 and is based on a combination of csp and Meta-iv. Even if it is the reference semantics of sdl (about 500 pages), it is far from being complete and contains many inconsistencies and obscure points.

In Bro91] is given a semantics for sdl based on streams and stream processing functions. It deals with a subset of sdl and the timing aspects are simpli ed. An operational semantics which covers sdl systems, processes, blocks and channels is given in God91]. It de nes a method to build labeled transition systems from sdl speci cations. The approach is relatively complete, however in this case too, time is not handled in a satisfactory manner. An important work is done in [START_REF] Bensalem | Computing Abstractions of In nite State Systems Compositionally and Automatically[END_REF][START_REF] Bergstra | Process Algebra Semantics of 'SDL[END_REF] which gives a semantics based on process algebra to a rather simple subset of sdl, called ' ? sdl. A method is given, for translating each sdl system into a term of PA ? drt -ID which is a discrete time process algebra extended with propositional signals and conditions, counting process creation operator, and a state operator. Finally, we mention the work of MGHS97] which proposes an axiomatic semantics based on Duration Calculus and the work of GK97] which uses abstract real time machines.

The paper is organized as follows. In the next section, we present an example used throughout the paper to illustrate our work. Then, we describe the main features of the if formalism used as an intermediate representation for sdl. Finally, we present an open validation environment for sdl speci cations and illustrate its usefulness by means of some experimental results.

2 An example: a distributed leader election algorithm We present a simple example used throughout the paper to illustrate the introduced formalisms and veri cation methods. We consider a token ring, that is a system of n stations S 1 , : : : , S n , connected through a circular network, in which a station is allowed to access some shared resource R only when it \owns" a particular message, the token. If the network is unreliable, it is necessary to recover from token loss. This can be done using a leader election algorithm Lan77, CR79] to designate a station responsible for generating a new token.

Formal speci cations and veri cations of these algorithms already exist and we consider here an sdl version of the one described in GM96]. Figure 1 All stations S i are identical and modelled by the sdl process of Figure 2. On expiration of the timer worried token loss is assumed: this timer is set when the station waits for the token, and reset when it receives it. The \alternating bit" round is used to distinguish between valid claims (emitted during the current election phase) and old ones (cancelled by a token reception). In the idle state, a station may either receive the token from its neighbour (then it reaches the critical state and can access the resource) and receive the timer expiration signal (then it emits a claim stamped with its address and the current value of round) or receive a claim. A received claim is \ ltered" if its associated address is smaller than its own address and transmitted unchanged if it is greater. If its own valid claim is received, then this station becomes elected and generates a new token. To complete this speci cation, message loss should be modelled explicitly (for instance by introducing a non deterministic choice when a token or claim is emitted by a station). However, using the intermediate representation if, message loss can be expressed directly using lossy bu ers.

IF: An intermediate representation for SDL

In the following sections, we give a brief overview of the intermediate representation if, its operational semantics in terms of labeled transition systems and the translation of a rather extended subset of sdl into if. A more complete description of if and its semantics can be found in BFG + 98]. In particular, we do not present the rendez-vous communication mechanism here.

An overview on IF

In if, a system is a set of processes communicating asynchronously through a set of bu ers (which may be lossy/reliable and bounded/unbounded). The timed behaviour of a system can be controlled through clocks (like in timed automata ACD93, HNSY94]) and timers (sdl timers, which can be set, reset and expire when they reach a value below 0).

IF system de nition

A system is a tuple Sys = (glob-def,procs) where glob-def = (type-def,sig-def,var-def,buf-def) is a list of global de nitions, where type-def is a list of type de nitions, sig-def de nes a list of parameterized signals (as in sdl), var-def is a list of global variable de nitions, and nally, buf-def is a list of bu ers through which the processes communicate by asynchronous signal exchange. procs de nes a set of processes described in section 3.1.2.

IF process de nition

Processes are de ned by a set of local variables, a set of control states and a set of control transitions. A process P2procs is a tuple P= (var-def, Q, cTrans), where:

var-def is a list of local variable de nitions (including timers and clocks)

Q is a set of control states on which the following attributes are de ned:

{ stable(q) and init(q) are boolean attributes, where only stable states are visible on the semantic level.

{ for stable states, the tpc(q) attribute is a predicate on any variable \visible" in the process (global variables and local variables of P), de ning when time is allowed to progress. In non stable states, time cannot progress.

{ save(q), discard(q) are lists of filters of the form signal-list in buf ] if cond]. save(q) is used to implement the save statement of sdl; its e ect is to preserve all signals of the list in buf, whenever the condition cond holds. discard(q) is used to implement the implicit discarding of unconsumable signals of sdl. When reading the next input signal in buf, all signals to be discarded preceding it in buf are discarded in the same atomic transition.

cTrans is a set of control transitions, consisting of two types of transitions between two control states q,q'2Q:

{ input transitions which are triggered by some signal read from one of the communication bu ers as in sdl: q g 7 ! input ; body ?????????????! (u) q 0 { internal transitions depending not on communications: q g 7 ! body ???????! (u) q 0

Where in both cases:

g is a predicate representing the guard of the transition which may depend on variables visible in the process (including timers, clocks and and bu ers, where bu ers are accessed through a set of primitives).

body is a sequence of the following types of atomic actions:

{ outputs of the form \output sig(par list) to buf" have as e ect to append a signal of the form \sig(par list)" at the end of the bu er buf.

{ usual assignments. { settings of timers of the form \set timer := exp". This has the e ect to activate timer and to set it to the value of exp. An active timer decreases with progress of time. sdl timers expire when they reach the value 0, but in if any timer tests are allowed. Clocks are always active and they increase with progress of time.

{ resettings of timers and clocks, which have the e ect to inactivate timers and to assign the value 0 to clocks.

The attribute u2feager, delayable, lazyg de nes the urgency type of each transition. eager transitions have absolute priority over progress of time, delayable transitions may let time progress, but only as long as they remain enabled, whereas lazy transitions cannot prevent progress of time. These urgency types are introduced in BST98].

input is an input of the form \input sig(reference list) from buf if cond]" where { sig is a signal, { reference list the list of references 1 in which the received parameters are stored, { buf is the name of the bu er from which the signal should be read { cond is a \post guard" de ning the condition under which the received signal is accepted; cond may depend on received parameters.

Semantics of IF

Association of a model with a process

We show how with a process can be associated a labeled transition system, and then, how these process models can be composed to obtain a system model. Let P= (var-def, Q, cTrans) be a process de nition in the system Sys and:

Let TIME be a set of environments for timers and clocks (for simplicity of the presentation, we suppose that these environments are global, that is, applicable to all timers and clocks occurring in Sys, if necessary, using renaming). An environment T 2TIME de nes for every clock a value in a time domain T (positive integers or reals), and for every timer either a value in T or the value \inac" (which can be represented by a negative value) meaning that the timer is not active. Setting or resetting a timer or a clock a ects a valuation T in an obvious manner. Progress of time by an amount transforms the valuation T into the valuation T in which the values of all clocks are increased by , and the values of all timers are decreased by (where the minimal value is zero).

Let BUF be a set of bu er environments B, representing possible contents of the bu ers of the system, on which all necessary primitives are de ned: e.g. \get the rst signal of a given bu er, taking into account the save and the discard attribute of a given control state", \append a signal at the end of a bu er",...\time progress by amount ", denoted by B , is necessary for bu ers with delay. Let ENV be a set of environments E de ning the set of valuations of all other variables de ned in the system Sys.

1 that is an \assignable" expression such as a variable or an element of an array 6

The semantics of P is the labeled transition system P] = (Q VAL,Trans,Ttrans) where Q VAL is the set of states and VAL= ENV TIME BUF is the set of data states.

Trans is the set of untimed transitions obtained from control transitions by the following rule: for any (E,T ,B),(E',T ',B')2VAL and input transition (and simpler for an internal transition) q g 7 ! (sig(x 1 :::xn);buf;cond) ; body ?????????????????????????! (u) q 0 2cTrans implies (q; (E; T ; B)) ? ! (q'; (E 0 ; T 0 ; B 0 )) 2Trans, if { the guard g evaluates to true in the environment (E,T ,B) { the rst element of buf in the environment B| after elimination of appropriate signals of the discard attribute and saving of the signals of the save attribute | is a signal sig(v 1 :::v n ), and the updated bu er environment, after getting sig(v 1 :::v n ), is B" { E"=E v 1 :::v n /x 1 :::x n ] and T "=T v 1 :::v n /x 1 :::x n ] are obtained by assigning to x i the value v i of the received parameters, { the post guard cond evaluates to true in the environment (E",T ",B") { E' is obtained from E" by executing all the assignments of the body, { T ' is obtained from T " by executing all the settings and resettings occurring in the body, without letting time progress, { B' is obtained from B" by appending all signals required by outputs in the body, { `is an appropriate labeling function used for tracing.

Ttrans is the set of time progress transitions, which are obtained by the following rule: in any state (q,(E,T ,B)), time can progress by the amount , that is (q; (E; T ; B)) ? ! (q; (E; T ; B )) 2Ttrans if 1. q is stable 2. time can progress in the state (q,(E,T ,B)), and, 3. time can progress by steps until : whenever time has progressed by an amount 0 where 0 0 < , time can still progress in the reached state (q,(E,T 0 ,B 0 )).

Time can progress in a state (q,(E,T ,B)) if and only if the following conditions hold:

{ the time progress attribute tpc(q) holds in (E,T ,B) { no transition with urgency attribute eager is enabled in (q,(E,T ,B)) { for each delayable transition tr enabled in (q,(E,T ,B)), there exists a positive amount of time , such that tr cannot be disabled while time progresses by .

Composition of models

The semantics of a system Sys = (glob-def,procs) is obtained by composing the models of processes by means of an associative and commutative parallel operator k.

Let P i ] = (Q i VAL,Trans i ,Ttrans i ) be the models associated with processes (or subsystems) of Sys. Then, P 1 ] k P 2 ] = (Q VAL,Trans,Ttrans) where Q= Q 1 Q 2 where init((q 1 ,q 2 )) = init(q 1 ) ^init(q 2 ) stable((q 1 ,q 2 )) = stable(q 1 ) ^stable(q 2 ) Trans is the smallest set of transitions obtained by the following rule and its symmetrical rule:

(q 1 ; V) ? ! (q 0 1 ; V 0 ) 2 Trans 1 and :stable(q 1 ) _ stable(q 2 ) ((q 1 ; q 2 ); V) ? ! ((q 0 1 ; q 2 ); V 0 ) 2 Trans Ttrans is the smallest set of transitions obtained by the following rule (q 1 ; V) ? ! (q 1 ; V 0 ) 2 Ttrans 1 and (q 2 ; V) ? ! (q 2 ; V 0 ) 2 Ttrans 2 ((q 1 ; q 2 ); V) ? ! ((q 1 ; q 2 ); V 0 ) 2 Ttrans 3.3 Translation from SDL to IF 3.3.1 Structure sdl provides a complex structuring mechanism using blocks, substructures, processes, services, etc, whereas if systems are at, that is consisting of a single level of processes, communicating directly through bu ers. Therefore, a structured sdl system is attened by the translation into if. Also, the structured communication mechanism of sdl using channels, signal routes, connection points, etc is transformed into point to point communication through bu ers by computing for every output a statically de ned unique receiver process (respectively its associated bu er). All prede ned sdl data types, arrays, records and enumerated types can be translated. For abstract data types, only the signatures are translated, and for simulation, the user must provide an appropriate implementation.

In sdl all signals are implicitly parameterized with the pid of the sender process, therefore in if all signals have an additional rst parameter of type pid.

Processes

Basically, for each instance of an sdl process, we generate an equivalent if process and associate with it a default input queue. If the number of instances can vary in some interval, the maximal number of instances is created.

Variables: Each local variable/timer of an sdl process becomes a local variable/timer of the corresponding if process. We de ne also variables sender, offspring and parent which are implicitly de ned in sdl. Remote exported/imported variables declared inside an sdl processes become global variables, declared at if system level.

States: All sdl states (including start and stop) are translated into stable if control states.

As if transitions have a simpler structure than sdl transitions, we introduce also systematically auxiliary non stable states for each decision and each label (corresponding to a \join") within an sdl transition. For each stable if state we de ne the save and discard sets to be the same as for the corresponding sdl state.

Transitions: For each minimal path between two if control states, an if transition is generated. It contains the triggers and actions de ned on that path in the same order.

All the generated transitions are by default eager i.e. they have higher priority than the progress of time; this allows to be conform with the notion of time progress of the tool Objectgeode; more liberal notions of time progress can be obtained by using di erent translations from sdl to if ( The architecture still allows connections with many other speci cation languages or tools. Thus, even speci cations combining several formalisms could be translated into a single if intermediate code and globally veri ed. The use of an intermediate program representation where all the variables, timers, bu ers and the communication structure are still explicit, allows to apply methods such as static analysis, abstraction, compositional generation. These methods are crucial for the applicability of the model checking algorithms.

ObjectGEODE

Objectgeode is a toolset developed by Verilog supporting the use of sdl, msc and omt. It includes graphical editors and compilers for each of these formalisms. It also provides a C code generator and a simulator to help the user to interactively debug an sdl speci cation. The Objectgeode simulator also o ers some veri cation facilities since it allows to perform automatic simulation (either randomly or exhaustively), and behavioral comparison of the speci cation with special state machines called observers ALH95].

CADP and TGV

We have been developing for more than ten years a set of tools dedicated to the design and veri cation of critical systems. Some of them are distributed in collaboration with the Vasy team of Inria Rhône-Alpes as part of the cadp toolset FGK + 96, BFKM97]. We brie y present here two veri ers integrated in cadp (aldebaran and evaluator) and the test sequence generator tgv FJJV97] built upon cadp jointly with the Pampa project of Irisa. These tools apply model-checking on behavioral models of the system in the form of labeled transition systems (lts). aldebaran allows to compare and to minimize nite lts with respect to various simulation or bisimulation relations. This allows the comparison between the observable behavior of a given speci cation with its expected one, expressed at a more abstract level. evaluator is a model-checker for temporal logic formulas expressed on nite lts. The temporal logic considered is the alternating-free -calculus. tgv aims to automatically generate test cases for conformance testing of distributed systems. Test cases are computed during the exploration of the model and they are selected by means of test purposes. Test purposes characterize some abstract properties that the system should have and one wants to test. They are formalized in terms of lts, labeled with some interactions of the speci cation. Finally, an important feature of cadp is to o er several representations of lts, enumerative and symbolic ones based on bdd, each of them being handled using well-de ned interfaces such as open-caesar Gar98] and smi Boz97].

SDL2IF and IF2C

To implement the language level connection through the if intermediate representation we take advantage of a well-de ned api provided by the Objectgeode compiler. This api o ers a set of functions and data structures to access the abstract tree generated from an sdl speci cation. sdl2if uses this abstract tree to generates an if speci cation operationally equivalent to the sdl one.

if is currently connected to cadp via the implicit model representation feature supported by cadp. if programs are compiled using if2c into a set of C primitives providing a full basis to simulate their execution. An exhaustive simulator built upon these primitives is also implemented to obtain the explicit lts representation on which all cadp veri ers can be applied.

Static analysis

The purpose of static analysis is to provide global informations about how a program manipulates data without executing it. Generally, static analysis is used to perform global optimizations on programs ASU86, WZ91, Muc97]. Our goal is quite di erent: we use static analysis in order to perform model reductions before or during its generation or validation. The expected results are the reduction of the state space of the model or of the state vector.

We want to perform two types of static analysis: property independent and property dependent analysis. In the rst case, we use classic analysis methods such as live variable analysis or constant propagation, without regarding any particular property or test purpose we are interesting to validate. In the second case, we take into account informations on data involved in the property and propagate them over the static control structure of the program. Presently, only analysis of the rst type is implemented but, we are also investigating constraint propagation and more general abstraction techniques. For instance, through the connection with invest we will be able to compute abstract if programs using general and powerful abstraction techniques.

Live variables analysis

A variable is live in a control state if there is a path from this state along which its value can be used before it is rede ned. An important reduction of the state space of the model can be obtained by taking into account in each state only the values of the live variables.

More formally, the reduction considered is based on the relation live de ned over model states: two states are related if and only if they have the same values for all the live variables. It can be easily proved that live is an equivalence relation and furthermore, that it is a bisimulation over the model states. This result can be exploited in several ways. Due to the local nature of live it is possible to directly generate the quotient model w.r.t. live instead of the whole model without any extra computation. Exactly the same reduction is obtained when one modi es the initial program by introducing systematic assignments of non-live variables to a particular value. This second approach is presently implemented for IF programs.

Consider now the token ring protocol example. In the idle state the live variables are round and worried, in the critical state only round is live, while variables sender, adr and rnd are never live. The reduction obtained by the live reduction is shown in Table 1 (line 3).

Constant propagation

A variable is constant in a control state if its value can be statically determined in the state. Two reductions are possible. The rst one consists in modifying the source program by replacing constant variables with their value. Thus, it is possible to identify and then to eliminate parts of dead code of the program e.g. guarded by expressions which always evaluates to false, therefore to increase the overall e ciency of the program. The second reduction concerns the size of the state vector: for a control state we store only the values of the non-constant variables. The constant values do not need to be stored, they can always be retrieved by looking at the control state.

Note that, both of the proposed reductions do not concern the size of the model, they only allow to improve the state space exploration (time and space). However, this kind of analysis may be particularly useful when considering extra information about the values assigned to variables, extracted from the property to be checked.

Compositional generation

As shown in the previous section, e cient reductions are obtained by replacing a model M by its quotient w.r.t an equivalence relation like live . However, stronger reductions can be obtained by taking into account the properties under veri cation. In particular, it is interesting to consider a weaker equivalence R | which should be a congruence for parallel composition |, able to abstract away non observable actions. The main di culty is to obtain the quotient M=R without generating M rst.

A possible approach is based on the \divide and conquer" paradigm: it consists in splitting the program description into several pieces (i.e., processes or process sets), generating the model M i associated to each of them, and then composing the quotients M i =R. Thus, the initial program is never considered as a whole and the generated models can be kept small. This compositional generation method has already been applied for speci cation formalisms based on rendez-vous communication between processes, and has been shown e cient in practice GLS96, Val96, KM97]. Surprisingly, to our knowledge it has not been investigated within an sdl framework, may be, because bu ers raise several di culties or due to lack of suitable tools.

To illustrate the bene t of a compositional approach we brie y describe here its application to the token ring protocol:

1. We split the if description into two parts, the rst one contains processes S 1 and S 2 and the second one contains processes S 3 and S 4 . For each of these descriptions the internal bu er between the two processes is a priori bounded to two places. Note that, when a bounded bu er over ows during simulation, a special over ow transition occurs in the corresponding execution sequence. 2. The lts associated with each of these two descriptions are generated considering the \most general" environment, able to provide any potential input. Therefore, the over ow transitions appear in these lts (claim and token can be transmitted at any time). 3. In each lts the input and output transitions relative to the internal bu ers (Q 2 and Q 4 ) are hidden (i.e., renamed to the special action); then these lts are reduced w.r.t an equivalence relation preserving the properties under veri cation. For the sake of e ciency we have chosen the branching bisimulation vGW89], also preserving all the safety properties (e.g. mutual exclusion). 4. Each reduced lts is translated back into an if process, and these two processes are combined into a single if description, including the two remaining bu ers (Q 1 and Q 3 ). It turns out that the lts generated from this new description contains no over ow transitions (they have been cut o during this last composition, which con rms the hypothesis on the maximal size of the internal bu ers). The nal lts is branching bisimilar to the one obtained from the initial if description. The gain, obtained by using compositional generation in addition to static analysis, can be found in Table 1 (line 4).

Results

We summarize in Table 1 the size of the lts obtained from the token-ring protocol using several generation strategies. The di erence between the model generated by Objectgeode (line 1) and the one obtained from if (line 2) are due to the following reasons: the handling of timer expirations in Objectgeode involves two steps: rst the timeout signal is appended to the input bu er of the process, and later it is consumed, whereas in if these two steps are collapsed into a single one, bypassing the bu er. Objectgeode introduces \visible" states for each informal decision, whereas these states do not appear in the model obtained from if.

However, the abstraction from these extra states in if, preserves all relevant properties. The most spectacular reduction is obtained by the live-reduction: the reduced model is about 100 times smaller than the one obtained by direct generation, preserving all properties (models 2 and 3 are strongly bisimilar).

Finally, when considering as visible only the open and close signals all four lts are branching bisimilar to the one shown in Figure 4, which proves, in particular, the mutual exclusion property of the protocol.

Conclusion and perspectives

We have presented the formalism if which is an intermediate representation for sdl allowing the interconnection of tools such as Objectgeode, cadp, tgv and speci c designed for if. The use of if o ers several advantages: if has a clear, formal semantics of time, and an explicit notion of atomicity. Moreover, it has some powerful concepts which are interesting for speci cation, such as di erent urgency types of transitions, synchronous communication, various bu er types (bounded, unbounded, lossy, : : : ).

if makes veri cation easier from several points of view:

{ the models generated by state space enumeration are less complex, though equivalent, due to the elimination of certain transient states.

{ if is a \program level" connection between the toolsets. This allows to combine program analysis techniques (e.g., static analysis or compositional generation) and classical model checking techniques. We envisage to implement more sophisticated static analysis, such as constraints propagation and more general abstraction techniques. The semantics of time in if is general enough to implement and experiment di erent time semantics for sdl.

Figure 1 :

 1 Figure 1: The token-ring architecture

Figure 2 :

 2 Figure 2: The behaviour of station S i

Figure 4 :

 4 Figure 4: An open validation environment for sdl

Figure 5 :

 5 Figure 5: The reduced behavior of the token ring.

  see the example below). inputs: sdl signal inputs are translated directly into if inputs, where the sender parameter must be handled explicitly: each signal receives the rst parameter in the local variable sender.Spontaneous input none is translated by an assignment of the sender to the pid of the current process. No input part is generated in this case. timeouts expirations are not noti ed via timeout signals in if: each timeout signal consumption in an sdl process is translated into a transition without input, which tests if the corresponding timer evaluates to zero, followed by the reset of that timer. The reset is needed to avoid multiple consumption of the same timeout expiration. priority inputs: are translated into normal inputs by enforcing the guards of all low priority inputs and the save set of the source state. The guard of each low priority input is conjuncted with a term saying that \there is no higher priority signal in the bu er". All low priority signals are explicitly saved if \at least one input with higher priority exists in the bu er". Such tests can e ectively be expressed by prede ned predicates on bu ers. continuous signal: sdl transitions triggered by a continuous signal test, generate if transitions without input. They are translated by an if transition, whose guard is equivalent to the sdl continuous signal. enabling condition: an enabling condition following an sdl input signal is translated directly into a post guarded input where the received parameters can be tested. task: all sdl formal tasks are translated into if assignments. Informal tasks become comments in the if speci cation. set and reset: sdl timer sets become if timer sets, where an absolute value \now + T" becomes in if a relative value \T". sdl timer resets become if timer resets. output: sdl outputs become if outputs: if the to pid-expression clause is present in the sdl output, the same pid-expression is taken as destination for the if output. Otherwise, according to signal routes signature, via restrictions, connections, etc. we compute statically the set of all possible destinations. If this set contains exactly one process instance, it become the if destination, otherwise, this output is not translated. Every output contains as rst parameter the pid of the sending process. decision: each alternative of an sdl formal decision is translated into a guard starting an if-transition from the corresponding non stable state. create: the dynamic creation of processes is not yet handled. But we intend to translate this construction by using the rendez-vous mechanism of if: a new instance is created (an \inactive" instance is activated) by synchronizing its rst action with the process creating (activating) it. During this synchronization, parameters can be passed between the \creating" and the \created" processes, such as the the values of the parent and the offspring variables, etc. procedures: if does not directly support procedures. But we handle a relatively large class of sdl programs containing procedures by procedure inlining, which consists in directly inserting the procedure graph, instead of its call, in the process graph.

		SDL	Languages Specifications
	Object	GEODE
		Compiler		IF
			Static	Compositional	Validation
			Analysis	Generation	Tools
		Simulator	CADP	TGV
	Code Generator	Model
		Verifier	Aldebaran	Evaluator
	Implementation	Diagnostics	Test Cases

Table 1 :

 1 lts obtained for the token ring example

	Generation method 1 Objectgeode 2 if 3 if + live reduction 4 if + compositional generation	Number of states Number of transitions 3018145 7119043 537891 2298348 4943 19664 1184 4788

Example: translation of the token ring to IF

To illustrate if, we present the translation of the token ring introduced in Section 2. The translation of the structure is completely straightforward in this example. Figure ?? contains the if version of the process S 1 , where the additional non stable states are dotted. By default, all transitions are eager, which leads to the same behaviour as in Objectgeode.

Thus, time can only progress, and the timeout occur, if the token is really lost (that is, no transition is enabled), and therefore a leader election algorithm is only initiated if necessary. In if, a di erent notion of time, closer to reality, can be modeled, e.g. by considering the transition from the critical state as lazy, thus allowing time to pass there by an arbitrary amount. In order to limit the time that a process can remain in critical, one can introduce a clock cl crit which is reset when entering critical, add to the outgoing transition the guard cl crit some limit and consider this transition as delayable.

An open validation environment based on IF

One of the main motivations for developing if is to provide an intermediate representation between several tools in an \open" validation environment for sdl. Indeed, none of the existing tools provides all the validation facilities a user may expect. Therefore, we want to allow them to cooperate, as much as possible using program level connections. An important feature is the ability of the environment to be open: in particular connections with kronos Yov97] (a model checker for timed automata) and invest GS97, BLO98] (a tool computing abstractions) are envisaged.

In this section, we rst present the architecture of this environment and its main components. Then, we describe in a more detailed manner two more recent modules concerning static analysis (section 4.2) and compositional generation (section 4.3) which are based on if.

Architecture

The environment is based on two validation toolsets, Objectgeode and cadp, connected through the intermediate representation if. There exists already a connection between these toolsets at