Francois Hild
email: hild@lmt.ens-cachan.fr

Stephane Roux

Nestor Guerrero

Maria Eugenia Marante

Julio Florez-Lopez

François Hild

Stéphane Roux

Néstor Guerrero

Julio Flórez-López

Calibration of constitutive models of steel beams subject to local buckling by using Digital Image Correlation

Keywords: Digital Image Correlation, Euler-Bernoulli kinematics, lumped damage mechanics, plastic hinge, steel beam

It is proposed to identify the behavior of steel beams prior to and after the inception of local buckling by using Digital Image Correlation. Full field measurements are used to evaluate kinematic and static fields for determining constitutive laws. It enables for the detection of local buckling inception and the evaluation of the postbuckled behavior. Constitutive models are tuned by using measured Euler-Bernoulli kinematics.

Introduction

The description of the local behavior of steel beams in buildings, bridges, off-shore platforms or other civil engineering structures is desirable when designed against in-service or earthquake loadings. This task is performed by utilizing various numerical techniques. The finite element method [START_REF] Zienkievicz | The Finite Element Method[END_REF] is one of the classical tools to analyze civil engineering structures. 2D [START_REF] Kwak | Nonlinear FE analysis of R/C structures under monotonic loads[END_REF][START_REF] Ile | Non-linear response and modelling of RC walls subjected to seismic loading[END_REF] or even 3D [START_REF] Rashid | Finite element analysis of reinforced concrete in bridge seismic design practice[END_REF][START_REF] Kwon | Three-dimensional finite element analyses of reinforced concrete columns[END_REF] codes are run. Very detailed analyses are possible and require full 3D constitutive models. Simplified or semi-global analyses are another class of methods in which the kinematic fields are described by resorting to generalized degrees of freedom (e.g., displacements and section rotations in beams). The (non linear) constitutive laws are then integrated over the height of the element. Special, so-called multi-fiber, beam elements are then implemented [START_REF] Owen | Finite elements in plasticity: Theory and practice[END_REF][START_REF] Guedes | A fiber Timoshenko beal element in CASTEM 2000[END_REF][START_REF] Davenne | Efficient approaches to finite element analysis in earthquake engineering[END_REF][START_REF] Kotronis | Simplified Modelling Strategies to Simulate the Dynamic Behaviour of R/C Walls[END_REF]. Lumped damage mechanics (LDM) is another way to describe the local behavior of steel beams. It is based on an extension of the concept of plastic hinges in beam calculations. For instance, it is able to account for local buckling [START_REF] Guerrero | Model of local buckling in steel hollow structural elements subjected to biaxial bending[END_REF]. Up to now, the parameters of the constitutive law of hinges, and more generally of beams, relied upon global data such as displacements at few prescribed measurement points [START_REF] Marante | Three-dimensional analysis of reinforced concrete frames based on lumped damage mechanics[END_REF]. It is proposed to use full-field measurement techniques tailored for the description of these structures as a set of beams and joints to determine the constitutive behavior of steel beams.

Digital Image Correlation (DIC) is a photomechanical technique [START_REF] Rastogi | Photomechanics[END_REF] allowing for the measurement of displacement fields based on a series of digital images of the surface of a specimen subjected to a specific loading history [START_REF] Chu | Applications of Digital-Image-Correlation Techniques to Experimental Mechanics[END_REF]. Recent advances have been achieved through a novel formulation that enables one to decompose the searched displacement field onto a suited library of such fields when dealing with beams (e.g., directly measuring the degrees of freedom associated with Euler-Bernoulli kinematics [START_REF] Hild | Displacement Measurement Technique for Euler-Bernoulli Kinematics[END_REF]). The interest of this experimental tool is that it provides full kinematic fields expressed in standard form for beam theories. Due to the fact that beam flexure is a statically determinate problem, static fields are also accessible when the behavior of the analyzed region is elastic. In particular, the exact loading conditions are obtained directly, and not inferred from the information given by the stroke and load transducers of the jack. The kinematics used herein is based upon an Euler-Bernoulli hypothesis applied to different discretizations of the region of interest. This hypothesis was also made in models, for instance developed by Sohal and Chen [START_REF] Sohal | Local buckling and sectional behavior of fabricated tubes[END_REF] to analyze local buckling of tubes by using inertia variations.

In the following, the procedure is illustrated by analyzing a flexural test on a steel beam. In Section 2, the general principle used in digital image correlation is briefly summarized and then particularized to an Euler-Bernoulli kinematics. A priori measurement uncertainties of the correlation algorithm are evaluated when applying a constant vertical displacement to the actual analyzed region. Kinematic and static fields are deduced by considering two different regions of interest in Section 3. Constitutive laws associated with local buckling are then determined by using two different descriptions (Section 4), namely, a global model in terms of generalized degrees of freedom and a non-local model accounting for inertia variations.

Kinematic measurements by DIC

Figure 1a shows a reference picture of a cantilever beam loaded at its end section by an actuator. The beam has a length of 1.5 m, a square cross-section of outer size 120 mm and inner size 112 mm. It is made of a conventional construction steel (ASTM-A-500). The pictures were shot with a digital CMOS camera (resolution: 3888 × 2592 pixels, digitization: 8 bits). Figure 1b corresponds to the last deformed shape of the considered beam. A random texture was applied onto the observed surface of the beam prior to the experiment to improve the measurement uncertainty by creating local gray level fluctuations.

General principle

DIC allows for the measurement of displacement fields from the registration (i.e., matching) of two pictures (Figure 1). The reference image, f (gray level as a function of position x x x), and that of the beam in a given deformed state g are related by

g(x x x + u u u(x x x)) = f (x x x) + b(x x x) (1)
where b(x x x) is noise induced by image acquisition, and u u u(x x x) an in-plane displacement field. In the sequel, it is assumed that the noise level, b, is negligible either because of its low amplitude with respect to those of f and g, or because of its scale separation with significant components of the displacement field.

When b(.) = 0, Equation ( 1) is the local form of the "brightness conservation."

The problem to address is the identification of the displacement field u u u from the sole knowledge of pictures f and g. As such, the problem is ill-posed, unless additional assumptions are made on the regularity of the displacement field so that the information is sufficient to determine u u u with a reasonable accuracy.

Let us introduce the following objective functional Φ operating on a priori

chosen displacement fields v v v Φ 2 (v v v) = [g(x x x + v v v(x x x)) -f (x x x)] 2 dx x x (2)
In the present case, the trial displacement v v v will be chosen as that corresponding to an Euler-Bernoulli kinematics [START_REF] Hild | Displacement Measurement Technique for Euler-Bernoulli Kinematics[END_REF]. Functional Φ is non linear with respect to the unknown displacement field u u u. Therefore, an iterative procedure is followed to evaluate u u u. A Taylor expansion of g up to the first order is introduced in Equation ( 2)

Φ 2 lin (v v v) = [g(x x x) -f (x x x) + v v v(x x x).∇ ∇ ∇g(x x x)] 2 dx x x (3)
Equation ( 3) corresponds to the linearized correlation residuals associated with the brightness conservation. The displacement field is decomposed as a linear combination of basis functions η η η

i (x x x) v v v(x x x) = v i η η η i (x x x) ( 4
)
where Einstein's convention is used, so that Φ 2 lin is a quadratic form in the unknown amplitudes v i . The extremality condition thus dictates, for all j,

(∇ ∇ ∇g.η η η j )(x x x)(∇ ∇ ∇g.η η η k )(x x x)dx x x v k = (f -g)(x x x)(∇ ∇ ∇g.η η η j )(x x x)dx x x ( 5
)
This system is written in a matrix form as

[M ]{v} = {m} ( 6
)
where {v} is a vector containing all the unknown components v i , [M ] and {m} are known quantities dependent upon f , g, and η η η. Successive iterations consist in evaluating the displacement field v v v, correcting the deformed picture g by using the current estimate v v v until no significant change of the degrees of freedom is observed. The evaluation of deformed images g(x x x +v v v(x x x)) requires gray level interpolations, which in the present case are chosen to be bilinear.

Euler-Bernoulli Kinematics: Beam-DIC

In the following, the kinematics of a single beam is addressed. Let us consider a straight bar (i.e., a beam element) of uniform cross section and length , which is loaded by axial forces and flexural moments about one axis of its cross section. Six degrees of freedom are considered for the bar, namely, two axial displacements (v 1 , v 4 ), two vertical displacements (v 2 , v 5 ) and two rotations (v 3 , v 6 ) about one axis of the cross section. The local coordinate system (x, y, z) coincides with the principal axes of the cross section, with the x-axis representing the centroidal axis of the beam element, and the z-axis corresponding to the direction of the flexural moment.

The (chosen) displacement field in a beam element then reads

v v v(x x x) = [N N N e (x x x)]{v} (7)
where N N N e are the shape functions (N 1 , . . . N 6 ) associated with the degrees of

freedom {v} t = {v 1 , . . . v 6 } N 1 (x) = 1 - x , N 2 (x) = (2x 3 -3 x 2 + 3 )/ 3 N 3 (x) = (x 3 -2 x 2 + 2 x)/ 2 , N 4 (x) = x N 5 (x) = -(2x 3 -3 x 2 )/ 3 , N 6 (x) = (x 3 -x 2 )/ 2 (8)
The rotation field θ is only caused by flexure

θ(x) = d N dx (x) {v} (9)
where vt = {v 2 , v 3 , v 5 , v 6 } and [ N (x)] = [N 2 (x) , N 3 (x) , N 5 (x) , N 6 (x)], and the corresponding curvature κ reads

κ(x) = d 2 N dx 2 (x) {v} (10)
Last, the longitudinal strain field is expressed as

ε xx (x, y) = [B e (x, y)]{v} ( 11
)
where

B e = {B 1 , . . . B 6 } reads B 1 (x, y) = - 1 , B 2 (x, y) = - y 3 (12x -6 ) B 3 (x, y) = - y 2 (6x -4 ) , B 4 (x, y) = 1 B 5 (x, y) = y 3 (12x -6 ) , B 6 (x, y) = - y 2 (6x -2 ) (12)
Therefore, the generalized degrees of freedom {v} give access to the displacement, rotation, curvature and strain fields at any point of the element without any additional post-processing step.

In practice, a region of interest (ROI) is chosen on the reference picture by the user. The ROI is then subdivided into smaller elements. The proposed approach is based upon first order Taylor expansions [START_REF] Ile | Non-linear response and modelling of RC walls subjected to seismic loading[END_REF]. When the (vertical)

displacements are large, it will not be robust. An initial field is needed to start the calculation. A first evaluation of the vertical displacement field is obtained by performing a classical correlation analysis in which, for each correlation window, a uniform displacement is sought. An FFT algorithm is used and a sub-pixel value is determined by interpolating the correlation func-tion in the vicinity of its maximum [START_REF] Hild | Multi-Scale Displacement Field Measurements of Compressed Mineral Wool Samples by Digital Image Correlation[END_REF]. At least four windows are used so that the displacement field is interpolated by a cubic polynomial, or equivalently by using decomposition [START_REF] Guedes | A fiber Timoshenko beal element in CASTEM 2000[END_REF]. Each pixel of the ROI is then moved by the estimated displacement. The subsequent displacement residuals are small so that the first order approximation used in Equation ( 3) is robust enough. The linear system (6) is implemented and solved. Convergence is reached when the correction of each measured degree of freedom

{ṽ} t = {v 1 , v 2 , v 3 , v 4 , v 5 , v 6
} is less than 10 -3 pixel between two iterations.

Performances of Beam-DIC

One way of evaluating the performance of a correlation algorithm (i.e., displacement, rotation, curvature uncertainties) is to artificially move the ROI by translation increments of sub-pixel value, and to assess the standard uncertainty of measured quantities. By using the shift / modulation property of Fourier transforms [START_REF] Périé | Analysis of a Multiaxial Test on a C/C Composite by Using Digital Image Correlation and a Damage Model[END_REF], sub-pixel values are prescribed. In the present case, three quantities are evaluated, namely, the displacement, rotation and curvature fields. The same ROI (ROI 2 of Figure 1, size: 2048 × 256 pixels) is analyzed with different discretizations (i.e., the length of the element is varied, and its height is constant) and for a vertical displacement of 0.5 pixel.

This last value generally leads to higher uncertainties when compared to other sub-pixel values [START_REF] Besnard | Finite-element" displacement fields analysis from digital images: Application to Portevin-Le Châtelier bands[END_REF].

Figure 2 shows the standard uncertainties for the three considered quantities.

In the present case, the displacement uncertainty σ u is independent of the element length and reaches very low values (of the order of 10 -3 pixel). This is due to the fact that many pixels are available to measure the displacement field described by very few degrees of freedom. The rotation uncertainty σ θ decreases as the element size increases. Being the first derivative of the vertical displacement [see Equation [START_REF] Kotronis | Simplified Modelling Strategies to Simulate the Dynamic Behaviour of R/C Walls[END_REF]], this result is to be expected by dimensional analysis (σ θ ∝ σ u / ). The linear fit shown in Figure 2 confirms this result.

Similarly, the curvature uncertainty σ κ decays with the square of the element size. This is due to the fact that the curvature is the second derivative of the displacement field [see Equation [START_REF] Guerrero | Model of local buckling in steel hollow structural elements subjected to biaxial bending[END_REF]] and therefore σ κ ∝ σ u / 2 (this trend is depicted by the straight solid line in Figure 2). These results illustrate the fact that it is not possible to capture very fine kinematic details (i.e., displacement changes) with a high accuracy. There is always a trade-off between displacement uncertainty and spatial resolution (i.e., element size), provided the measured kinematics is well captured by the chosen kinematic basis [START_REF] Réthoré | Extended digital image correlation with crack shape optimization[END_REF].

Kinematic and static fields

The experiments are performed in such a way that the stroke of the jack is controlled. The applied force is also measured by a load cell close to the jack.

Eleven pictures are shot, namely a reference picture and 10 load levels are recorded. Figure 3a shows the corresponding global data. Since the present situation is statically determinate, a first use of the correlation technique, ironically, will yield the change of the flexural moment along the longitudinal direction of the beam. This result is obtained by analyzing a ROI close to the load application point (ROI 1, see Figure 1a). In a second step, by analyzing a ROI containing the weld (ROI 2, see Figure 1a), the different fields introduced in Section 2.2 are evaluated prior to and after local buckling inception.

Elastic analysis: Load gauge

The measured displacement field, and more importantly, the curvature field enable us to evaluate the flexural moment for any considered section of the beam (as for any classical load cell). This is possible provided the behavior of the region of interest remains elastic. In that sense, it is a "stress gauge" as already developed to analyze a Flamant problem [START_REF] Roux | A stress scale in full-field identification procedures: A diffuse stress gauge[END_REF]. Consequently, a first analysis consists in considering a ROI close to the zone where the load is applied (ROI 1, see Figure 1a). The chosen kinematics corresponds to the exact solution of a cantilever beam when the local behavior remains elastic.

In the present case, a single element (height: 256 pixels, length: 2048 pixels) is considered. The advantage is that the measurement uncertainty is minimal (see Figure 2) and therefore the sought degrees of freedom are estimated more accurately. The curvature field then gives access to the flexural moment M as a function of the local coordinate x M (x)

EI 0 = κ(x) ( 13
)
where E is the Young's modulus of the material, and I 0 the inertia moment of the cross-sectional area. When the six degrees of freedom {v} t = {v 1 , . . . v 6 } are measured, the curvature field is obtained directly by using Equation [START_REF] Guerrero | Model of local buckling in steel hollow structural elements subjected to biaxial bending[END_REF].

Furthermore, the results are extrapolated outside the ROI by assuming that the beam behavior is elastic everywhere. This hypothesis is not necessarily true, and some deviations will be observed especially after local buckling inception.

Figure 3b shows the change of the curvature field for the ten load levels. Two regimes are observed. For the first six levels, there is a gradual increase in the slope of the curvature. Thereafter, the latter levels off and decreases. This phenomenon is in direct relationship with the change of the applied load with the stroke (Figure 3a). The derivative of the curvature field is proportional to the applied load normal to the beam. In Figure 4a, the latter is compared with the force measured by the load cell. Even though there is a good correlation, a non-linear relationship exists between the two quantities. This first result shows that the closer the measurement region to the sample, the more relevant the information obtained by a transducer, be it a load cell or a "stress gauge" associated with a Beam-DIC procedure.

Two other outputs of this first analysis are given. First, the location of the point for which the flexural moment vanishes is sought. Figure 4b shows the change of the axial location of that point with the applied load. There is a general correlation between the two data. However, the location clearly moves and neglecting this effect would over-estimate the value of the flexural moment by a factor up to about 10%. The average correlation residual is shown in Figure 5 for the ten analyzed pictures. Even though there is a gradual degradation of its level, the order of magnitude remains the same. Therefore, the previous measurements are deemed trustworthy.

Hinge detection

The rotation and deflection fields are analyzed in the sequel. One of the features that will be analyzed concerns the results at the junction of the beam with its base. This point corresponds to the location of the weld. Figure 6a shows the change of the rotation field for the ten analyzed pictures. Two regimes are observed. For the first five pictures, the rotation level close to the weld is vanishingly small. Conversely, for the five last levels, there is a discontinuity of the extrapolated rotation at the junction. This phenomenon corresponds to the effect of local buckling that is not fully captured by the chosen kinematics. The displacement field is shown in Figure 6b. Again two regimes are observed. The extrapolated displacement close to the junction is first very small, i.e., continuous with respect to the kinematics of the base.

Later on, a deviation is observed and the point for which the extrapolated displacement vanishes is shifted about 200 pixels away from the junction.

Kinematic field: Analysis of local buckling

The considered ROI is now moved close to the junction (ROI 2, see Figure 1a)

to analyze local buckling. The left edge of the ROI now coincides with the estimated location of the junction (i.e., weld) between the beam and the base.

To discuss the choice of the discretization used hereafter, the last loading case is first analyzed; local buckling has already occurred. First, only one element is chosen and the kinematic field is sought. By analyzing the correlation residual field (Figure 7), there is a clear deviation from the average level for the first 250 pixels. This is an indication that the measurement results in that zone are not reliable. The main reason is that the kinematic hypothesis is not consistent with the experimental phenomenon (i.e., local buckling) in this localized region. When studying the rotation field (Figure 8a), a discontinuity is again observed as in the case of extrapolated quantities of Section 3.1.

The reason for the observed discrepancy between measured and actual displacements is mainly due to the fact that the chosen (Euler-Bernoulli) kinematics (with uniform elastic and geometric properties) is not able to properly describe the phenomena occurring close to the junction. One alternative is then to only use measurements outside of this zone, as shown in Section 3.1, and extrapolate the results up to the junction. Another choice is to resort to more detailed analyses of the local field by using stereovision [START_REF] Sutton | Advances in Two-Dimensional and Three-Dimensional Computer Vision[END_REF][START_REF] Garcia | A combined temporal tracking and stereo-correlation technique for accurate measurement of 3D displacements: Application to sheet metal forming[END_REF] since out of plane motions may cause in-plane distorsions. It was followed to analyze buckling in composite materials [START_REF] Melin | Buckling behaviour and delamination growth in impacted composite specimens under fatigue load: An experimental study[END_REF]. A last choice is to still use Euler-Bernoulli kinematics, but not with the usual constraints related to the assumption of elastic behavior. The last route is followed herein. It consists in discretizing the ROI by using more than one element. Consequently, more degrees of freedom are measured, i.e., the displacement field is richer.

However, the measured displacement field does not necessarily satisfy static admissibility. The latter is recovered when the curvature and its derivative are continuous from one element to the next one. Let us emphasize that the correlation algorithm only enforces continuities of the displacements and rotations thanks to the chosen degrees of freedom. The curvature, derivative of the curvature and normal strains are not necessarily continuous functions when more than one beam element is considered in the ROI.

In the following, the measured displacement field will be regularized by enforcing the continuity of the curvature field over the whole ROI. Moreover, a continuity of the rotation and displacement at the weld is prescribed for a discretization with more than two elements. This is possible by measuring the rigid body motion of the base with the same type of correlation scheme as that discussed in Section 2.1. Last, over one part of the ROI where elasticity is likely to occur, additional constraints are prescribed to describe the continuity of the curvature derivative and normal strains. The regularization of any quantity is performed by using Lagrange multipliers. All the choices discussed above have to be validated.

The performance of the correlation algorithm is evaluated by following the same procedure as in Section 2.3, namely, for a constant vertical displacement of 0.5 pixel. In Figure 2, the results show that the same level of uncertainty is achieved for displacements, rotations and curvature, irrespective of the element size . This is to be expected since the additional constraints lead to an equivalence of any discretization when the continuity of the curvature, its first derivative and the normal strains are continuous over the whole length of the ROI. The fact that this property is recovered validates the implemented regularization. Last, when only the curvature is constant over the whole ROI, the displacement uncertainty level is virtually constant. The rotation uncertainty decays approximately with the square root of the element size (σ θ ∝ 1/ √ ), and the curvature with the element size raised to the power -1.2 (σ κ ∝ 1/ 1.2 ).

Both uncertainties reach the same level as in the two other analyzed cases when the element length is equal to 2048 pixels. Therefore, an intermediate response is observed between the two limit cases analyzed previously. These last results are not shown in Figure 2 for the sake of clarity. It is concluded that the higher the number of implemented continuity conditions, the less uncertain the measurements, provided the kinematic basis contain the field to be evaluated.

The first analysis concerns the choice of the discretization when the displacement field is not "regularized" over the whole length of the ROI. This is a crucial step since the smaller the element, the better the description of a complex displacement field, yet the higher the uncertainty level (Figure 2). Figure 8b shows the rotation field when the ROI is discretized with 1 to 16 elements.

When less than two elements are used, no regularization is implemented. The consequence is that the rotation at the left end of the ROI is not equal to the value corresponding to the rotation of the base. Moreover, the derivative of the rotation (i.e., the curvature) is not continuous at the middle of the ROI when two elements are used. When 4 or 8 elements are used, virtually the same rotation field is obtained. Last, when 16 elements are used, fluctuations occur, thereby indicating that the evaluation is no longer trustworthy. When the correlation residuals are analyzed (Figure 9), there is a continuous decrease of the average residual over the whole ROI. Conversely, there is a slight increase when the average is performed over the first 256 pixels for 4 elements.

This effect is due to the regularization that is performed starting with four elements. The average residual then decreases again. Both averages level off for discretizations with more than 8 elements when the curves showing the trends are studied. Consequently, the number of elements is chosen equal to 8 elements in all subsequent analyses to limit spurious fluctuations.

Another question to address concerns the zone where the regularization is applied. On the one hand, if the zone is too large, a deviation is to be expected.

On the other hand, if the zone is too small, the measurements might be noisier.

In the present case, 8 elements are considered and different lengths of the right part of the ROI are regularized, namely, the curvature, its derivative and the normal strains are continuous. In that part, it is assumed that the beam behavior is elastic. Over this zone, it would be equivalent of using a single Euler-Bernoulli beam element. Figure 10a shows the measured rotation field as a function of the fraction of regularized ROI. The results are very close when up to 75% of the ROI is regularized. Beyond this value, there is a clear change of the measured rotation field. The corresponding correlation residuals also start to increase, especially in the left part of the beam. In the following, a regularization over 75% of the ROI is chosen.

The rotation field is now studied for the ten analyzed load levels (Figure 10b).

As the stroke increases, a gradual deviation from an elastic response is observed. For the last four levels, there is a rotation localization induced by local buckling. This result illustrates the fact that the rotation capacity of steel beams is undermined by the inception and development of local buckling. The measured rotation fields are now used to identify different constitutive laws.

To perform the analysis, two inputs are needed, namely, the rotation field and extrapolated curvature field in an elastic region, which is proportional to the flexural moment.

Constitutive law of a beam subject to local buckling

The previous measurements are now used to identify two different constitutive equations depending on the type of hypothesis made to describe local buckling.

First model: Lumped constitutive law

If the experiments are performed in order to analyze the beam behavior when used in frames, a simple yet powerful model consists in "lumping" all the non-linear processes induced by plasticity and local buckling onto the weld section. This type of assumption is made in the framework of Lumped Damage Mechanics [START_REF] Cipollina | A simplified damage mechanics approach to nonlinear analysis of frames[END_REF][START_REF] Marante | model of damage for RC elements subjected to biaxial bending[END_REF][START_REF] Armero | Numerical modeling of softening hinges in thin Euler-Bernoulli beams[END_REF]. It corresponds to an extension of the concept of plastic hinges for which constitutive laws describe the flexural moment / section rotation relationship. This analysis is possible in the present case by using the extrapolated rotation (Figure 6a) and the corresponding curvature fields (Figure 3b). For the section rotation at the weld, the value of the base rotation is subtracted from its extrapolated value. The corresponding flexural moment is proportional to the value of the extrapolated curvature field at the location of the weld.

M = M u (1 -D) when Θ > 0 (15)
with

D = ∆ Θ -Θ 0 (16)
where . are Macauley's brackets. By using a least squares fit, the following values are determined: M u /EI 0 = 26.2 × 10 -6 ± 0.4 × 10 -6 pixel -1 , Θ 0 = 0.02 ± 0.004, and ∆ = 9 ± 4. The identification result is shown in Figure 11. The lumped model is able to capture the main features observed experimentally.

Second model: Piece-wise constant inertia

In the present approach, it is assumed that local buckling is described by a change of the beam inertia, to be determined, over an unknown length lb close to the weld (Figure 12). An Euler-Bernoulli hypothesis is made to analyze the experiments. It is assumed that the rotation and curvature fields are both continuous, in a similar way as during the measurement stage. Some of these hypotheses can also be found in Refs. [START_REF] Sohal | Local buckling and sectional behavior of fabricated tubes[END_REF][START_REF] Challamel | Non-local behavior of plastic softening beams[END_REF]. In the first part of the beam where the inertia is denoted by Ĩ ≤ I 0 (i.e., 0 ≤ x ≤ lb ), the rotation field reads

θ(x) = P E Ĩ L p x - x 2 2 + θ 0 (17)
where θ 0 denotes the rotation of the base, and L p the length leading to a continuous curvature field. In the second part (x > lb ), the rotation field becomes

θ(x) = P EI 0 L(x -lb ) - x 2 -2 lb 2 + P E Ĩ L p lb - 2 lb 2 + θ 0 (18)
where the continuity of the curvature when x = lb yields the additional constraint

L -lb I 0 = L p -lb Ĩ (19)
For each load level, two unknowns ( Ĩ and lb ) are tuned by least squares minimization between the measured rotation field (Figure 10b) and that described by Equation [START_REF] Besnard | Finite-element" displacement fields analysis from digital images: Application to Portevin-Le Châtelier bands[END_REF]. The length L is deduced from the static analysis of Section 3.1, see Figure 4b, and the value P/EI 0 from the analysis of the rotation in the zone where it is assumed to be elastic. In the present case, the value for lb varies from 0.26L ROI for the fifth load level to 0.24L ROI for the last one, where L ROI denotes the length of the region of interest (here 2048 pixels).

This last value is assumed to be valid for the whole analysis, and is about twice the distance of the skeletal point shown in Figure 6b.

Figure 13a shows the results obtained with the present procedure. There is a very good agreement between the measured and identified rotation fields. The results obtained so far are recast as a non-local damage model for which the inertia degradation is directly described by a damage parameter D

Ĩ = I 0 (1 -D) (20)
so that when D = 0, there is no buckling, and when D = 1, the rotation capacity of the beam is completely degraded. The quantity lb is then the "internal length" of the non-local model, here assumed to be constant. Within this new framework, it is also possible to identify the change of the damage parameter D with the average curvature κ over the length lb (Figure 13b).

Moreover, the following law is used to fit the data

D = 1 -exp - κ -κ th κ 0 m ( 21
)
where κ 0 is a scale parameter, and κ th a threshold value below which no degradation (i.e., local buckling) occurs. A very good description of the experimental data is obtained by using this expression when κ 0 = 2.2 × 10 -6 ± 10 -6 1/pixel, κ th = 1.9 × 10 -5 ± 2 × 10 -6 1/pixel, and m = 0.34 ± 0.05.

The latter ones were determined by resorting to a least squares fit.

Summary

The The definition of a suited library (i.e., with mechanical content as close as possible to the real experiment) of displacement field reveals to be a key ingredient for an accurate and reliable evaluation of the beam kinematics in terms of generalized degrees of freedom. When applied to a real experiment, the feasibility is demonstrated by using pictures obtained with a semi-professional camera. It is also shown that when one departs from the kinematic hypotheses made herein, the correlation residuals are a good error indicator. In present case, it allows for the detection of local buckling and its effect on the rotation capacity of steel beams. By moving artificially pictures, a displacement uncertainty of the order of one µm is achieved with the chosen parameters.

The same approach can be applied to other types of structures such as frames, or other types of materials such as reinforced concrete or wood. When departing from beam kinematics, the approach developed herein is generic and is applicable to cases where closed-form solutions exist [START_REF] Hild | Digital image correlation: From measurement to identification of elastic properties -A review[END_REF][START_REF] Roux | Stress intensity factor measurements from digital image correlation: Post-processing and integrated approaches[END_REF], or numerical solutions [START_REF] Leclerc | Integrated Digital Image Correlation for the Identification of Mechanical Properties[END_REF] are computed.

The key ingredient is to taylor the measured kinematics as closely as possible to the experiment, and to the (non linear) constitutive law.

List of Figures

Figure 11 shows

 11 Figure11shows the results obtained with the present procedure. Two regimes are observed. For the first five load steps, the rotation level is very small and believed to be in the uncertainty range associated with the extrapolation procedure. Conversely, for the last five load levels, there is a clear change of the rotation level induced by local buckling. With this type of information, there is no clear indication of a plastic regime prior to local buckling. However, it clearly shows the degradation of the rotation capacity of steel beams induced by local buckling. When compared with Figure3a, there is a significant difference in terms of behavior, in particular for the load levels where local buckling occurs.

1 30 3Fig. 1 .Fig. 3 .Fig. 4 .

 30134 Fig. 1. Cantilever beam in its reference (a) and deformed (b) state for the last load level. The two regions of interest (ROIs) analyzed herein are shown on the reference picture. The picture resolution is 3888 × 2592 pixels with an 8-bit digitization. The physical size of 1 pixel is 0.39 mm.

Fig. 5 .Fig. 6 .Fig. 7 .

 567 Fig. 5. Average correlation residuals Φ as a function of the applied load.

Fig. 10 .

 10 Fig. Average (in gray levels) as a function of number of beam elements. Two zones are considered, the first 256 pixels and the whole 2048-pixel ROI to evaluate the average value. The curves depict trends in terms of change of the correlation residual with the chosen discretization.

6 Fig. 11 .

 611 Fig. 11. Normalized flexural moment M/EI 0 vs. corrected section rotation Θ for the analyzed experiment. The dashed line shows the identification result with the lumped model [Equations (14-16)].

12 .Fig. 13 .

 1213 Fig. 13. Rotation fields for the ten analyzed load levels (b). Comparison between experimental and predicted rotations when a constant inertia degradation is assumed in the left part of the beam (b). Damage parameter D vs. average curvature κ. The dashed line corresponds to the best fit with the damage law (21).

  analysis of Euler-Bernoulli displacement fields based on digital image correlation is used to identify constitutive models of steel beams prior and after the inception of local buckling. When the local behavior is elastic, it allows one to measure the flexural moment. Otherwise, this kinematics is able to describe local buckling, in particular in terms of rotation field. With this information at hand, two models are identified. The first one corresponds

	to a "lumped" point of view that may be used to model frames within the
	framework of lumped damage mechanics. The second model is non-local for
	which the growth law of the damage variable is determined, as well as the
	internal length, which is virtually constant during the whole development of
	local buckling.

Acknowledgements

This work is part of an ECOS-Nord / CNRS project entitled "Detection and prediction of the damage state in frames subjected to earthquakes."


Benoît Caillaud
email: benoit.caillaud@inria.fr

Jean-Baptiste Raclet
email: jean-baptiste.raclet@irit.fr

Ensuring Reachability by Design

Keywords: component-based design, compositional reasoning, interface theories, modal specifications

Modular design aims at decomposing systems as a set of distinct components that can be independently developed and then assembled all together. Interfaces are then attached to components; they abstract implementation details while exposing to the environment relevant information about cross-component interactions. Whereas state-of-the-art on interfaces essentially consider independent implementability of safety properties, we consider in this paper reachability properties, which are in general not compositional. The approach we advocate consists in controlling the design flow of components, that is, the evolution of their interfaces through combinations and refinements, in order to ensure a reachability property by construction. Modal specifications are widely acknowledged as a suitable specification formalism for interfacebased design. In order to obtain the required expressivity, we extend them with marked states to model states to be reached. We then develop an algebra with both logical and structural composition operators ensuring reachability properties by design.

Garantir l'atteignabilité par construction

Résumé : Les méthodes de conception modulaire procèdent par décomposition d'un système en un ensemble de composants qui seront, dans un premier temps, réalisés indépendamment les uns des autres, pour être par la suite combinés de façon à former un système complet. Il est alors utile d'associer aux composants des interfaces qui servent à abstraire les détails de réalisation, tout en exposant les aspects cruciaux concernant les interactions avec les autres composants et l'environnement. Alors que l'état de l'art sur les interfaces concerne en premier lieu l'implémentation indépendante de propriétés de sureté, ce rapport porte sur la prise en compte de propriétés d'atteignabilité, qui sont en général non compositionnelles. L'approche défendue ici consiste 'a contrôler le flot de conception d'un systèmes, c'est 'a dire, l'évolution des interfaces tout au long des étapes de composition et de raffinement, de telle manière qu'une propriété d'atteignabilité est garantie par construction. Les spécifications modales sont reconnues comme un formalisme d'interface approprié. Elles sont ici étendues par ajout de marquage des états, servant a modéliser l'atteignabilité de certains états. L'algèbre d'interfaces modales marquée, avec ses opérateurs de composition logique et structurelle, permet d'assurer par construction l'atteignabilité de certains états.

Mots-clés : conception par composants; raisonnement compositionnel; théories d'interfaces; spécifications modales

Introduction

In order to face the intrinsic complexity of automotive, aeronautic and consumer electronics embedded systems, but also of web-based service oriented architectures, modular design aims at organizing systems as a set of distinct components that can be developed independently and then assembled together. This is best achieved using interfaces which abstract superfluous implementation details of a component and expose cross-component protocol informations that are essential to a correct use of a component. Component reuse in different contexts is thus made possible, not only reducing design time, but also enabling the amortization of design costs over several different projects.

Component interoperability or compatibility is then a major issue: when can we safely compose two (or more) components? Compatibility is often considered at a signature level. In this simple case, interfaces consist in function or method types and compatibility consists in a typechecking, performed either at compile-time or at run-time. This paper deals with a richer notion of interfaces capable of capturing behavioral properties.

The first work on behavioral compatibility of interfaces has been proposed in [START_REF] De Alfaro | Interface automata[END_REF]. This paper considers an automata-based formalism for interfaces in which transitions are labeled with output (produced by the component) or input (produced by the environment) actions. Then, a run-time error occurs whenever a component produces an output that is not accepted as input by one of its peers. The fact that a runtime error may occur does not necessarily lead to deem the interfaces incompatible. Indeed, the authors promotes an optimistic approach of composition in which two interfaces are compatible if there exists a restriction of the permitted actions of the environment in order to prevent the reachability of a runtime error. They show that this form of compatibility is preserved in the design flow provided alternating refinement [START_REF] Alur | Alternating refinement relations[END_REF] is used. More precisely, starting from initial interfaces whose product satisfies a particular safety property (i.e., a runtime error cannot be reached), they can be refined independently and then composed, their product will also satisfy the same safety property. This principle, called independent implementability, is of key importance [START_REF] Henzinger | The discipline of embedded systems design[END_REF] and enables the concurrent design of systems that are then assembled in a bottom-up manner.

This paper now studies the case of reachability properties and proposes results regarding their satisfaction by design. Basically, a reachability property states that some particular situation can be reached. Examples abound in practice. For instance, consider Service Oriented Architectures (SOA) formed of several interacting services; they should always have the possibility to reach a termination state, by delivering a response to all service activation. However, termination is in general not preserved by service composition. Although reachability properties are easy to verify in this context [START_REF] Bérard | Systems and Software Verification. Model-Checking Techniques and Tools[END_REF], model-checking may not be an appropriate solution. First, because it requires to construct the reachability graph of a system which may lead to a state explosion problem. Moreover, in case model-checking reveals a violation of the reachability property, designers have to iterate the design cycle by re-coding and re-validating their components, therefore extending time to market. The alternative approach advocated in this paper consists in controlling the design flow of components, that is, the evolution of interfaces through compositions and refinements, in order to ensure a reachability property by construction.

Now, what specification formalism capturing some behavioral aspects of components is convenient for interface-based design? Modal specifications [START_REF] Larsen | A modal process logic[END_REF][START_REF] Larsen | Automatic Verification Methods for Finite State Systems[END_REF][START_REF] Antonik | 20 years of modal and mixed specifications[END_REF] are widely acknowledged as a suitable proposal [START_REF] Larsen | Modal I/O automata for interface and product line theories[END_REF][START_REF] Raclet | Modal interfaces: unifying interface automata and modal specifications[END_REF][START_REF] Raclet | A modal interface theory for component-based design[END_REF]. Basically, they consist in labeling interface transitions with modalities, either must if the transition has to be enabled in any refinement, or may if the transition is allowed. Recently, they have been extended to a timed setting [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] and also to a quantitative one [START_REF] Juhl | Modal transition systems with weight intervals[END_REF]. In [START_REF] Larsen | Modal I/O automata for interface and product line theories[END_REF][START_REF] Raclet | Modal interfaces: unifying interface automata and modal specifications[END_REF][START_REF] Raclet | A modal interface theory for component-based design[END_REF], modal specifications are shown to have many benefits comparing the specification formalism introduced in [START_REF] De Alfaro | Interface automata[END_REF]; they are not only equipped with an optimistic compo-sition operator and a refinement relation but also with a conjunction and a quotient operator. The role of these operators in a design flow will be motivated later in the paper. As reachability properties cannot be expressed, in general, with modal specifications, we first consider in this paper modal specifications enriched with marked states, in the same fashion as it is done in [START_REF] Darondeau | Supervisory control for modal specifications of services[END_REF]. We show that, in this framework, we can develop a theory ensuring reachability properties by design.

2 Modeling with marked modal specifications

Background on automata

Let Σ be a finite alphabet of actions, a deterministic automaton over Σ is a tuple M = (R, r 0 , Σ, λ, G) where R is a finite set of states, r 0 ∈ R is the unique initial state, λ is a partial map from R × Σ to R called the labeled transition map and G ⊆ R is a non-empty set of marked states. The set of firable actions from r ∈ R is ready

(r) = {a ∈ Σ | λ(r, a) is defined}.
Transition map λ is extended to its transitive and reflexive closure: let denote the empty word, for all r ∈ R, λ(r, ) = r and for all u

∈ Σ * , a ∈ Σ, r 1 , r 2 , r 3 ∈ R, λ(r 1 , u) = r 2 and λ(r 2 , a) = r 3 imply λ(r 1 , u.a) = r 3 . Define L M = {u ∈ Σ * |∃r ∈ R, λ(r 0 , u) = r }
to be the language of M. If λ(r, u) = r for some u then r is said to be reachable from r. The natural projection of a word v ∈ L M on Σ ⊆ Σ is defined inductively with pr Σ ( ) = and, if v = u.a, pr Σ (v) = pr Σ (u) .a when a ∈ Σ and pr Σ (v) = pr Σ (u) otherwise.

Given P ⊆ R, define pre * (P ) and post * (P ) to be the set of states that are respectively coreachable and reachable from any state r ∈ P : it is the least set such that for r ∈ P , r ∈ pre * (P ) and r ∈ post * (P ) and for every λ(r , a) = r , if r ∈ pre * (P ) then r ∈ pre * (P ) and if r ∈ post * (P ) then r ∈ post * (P ). With a slight abuse, we may write pre * (r) and post * (r) for pre * ({r}) and post * ({r}).

If modeling a service, it is desirable to set that a service session eventually terminates; this is often refered in SOC as weak termination. To capture this kind of requirement, we define terminating automata: an automaton M is said to be terminating whenever R = pre * (G) meaning that it is always possible to reach a marked state from any state of the automaton. In other words, M is terminating if and only if for any u ∈ L M , there exists a v such that uv ∈ L M and λ(r 0 , uv) ∈ G. In the temporal logic CTL, this property can be written AG(EF G).

Given two automata

M 1 = (R 1 , r 0 1 , Σ 1 , λ 1 , G 1 ) and M 2 = (R 2 , r 0 2 , Σ 2 , λ 2 , G 2 ), their product is the automaton M 1 × M 2 = (R 1 × R 2 , (r 0 1 , r 0 2 ), Σ 1 ∪ Σ 2 , λ, G 1 × G 2 ) where λ((r 1 , r 2 ), a) is defined as (λ 1 (r 1 , a), r 2 ) for a ∈ Σ 1 \ Σ 2 , (r 1 , λ 2 (r 2 , a)) for a ∈ Σ 2 \ Σ 1 and (λ 1 (r 1 , a), λ 2 (r 2 , a)) for a ∈ Σ 1 ∩Σ 2 . As a consequence, the language of M 1 ×M 2 is the mixed language L M1 L M2 = {u ∈ (Σ 1 ∪ Σ 2 ) * | pr Σ1 (u) ∈ L M1 and pr Σ2 (u) ∈ L M2 }.

Marked modal specifications

Following [START_REF] Darondeau | Supervisory control for modal specifications of services[END_REF], we enrich modal specifications [START_REF] Larsen | A modal process logic[END_REF][START_REF] Larsen | Automatic Verification Methods for Finite State Systems[END_REF][START_REF] Antonik | 20 years of modal and mixed specifications[END_REF] with marked states in order to model states to be reached. For instance, if a designer specifies a service, this enables to represent session terminations. The obtained formalism allows to specify a (possibly infinite) set of automata called implementations.

Definition 1 (Marked Modal Specification) A marked modal specification over Σ is a tuple C = (Q, q 0 , Σ, δ, must, may, F ), where Q is a finite set of states, q 0 ∈ Q is the unique initial state, δ : Q × Σ → Q is a partial labeled transition map; must, may : Q → 2 Σ map to each state q the set of required and allowed actions from q, F ⊆ Q is a non-empty set of marked states.

Inria

It is assumed that a transition is associated to any allowed action, that is for every state q ∈ Q and every action a ∈ Σ, a ∈ may(q) if and only if δ(q, a) is defined. The mapping may : Q → 2 Σ can thus be reconstructed from the transition relation δ. However, this distinction simplifies the definition of satisfaction and refinement relations and compositions operators.

In this paper, marked modal specifications are taken deterministic, that is: for any a ∈ Σ and any state q there is at most one state q such that δ(q, a) = q . The reason for this will be given later in Sec. [START_REF] Antonik | 20 years of modal and mixed specifications[END_REF].

The underlying automata associated to C is Un(C) = (Q, q 0 , Σ, δ, F ). The language L C is then L Un(C) . As previously for automata, we extend δ to words by taking its transitive and reflexive closure. Moreover, we define pre * M (P ) and pre * m (P ) with P ⊆ Q as the set of states that are coreachable from any state q ∈ Q by following transitions labeled by required and allowed actions, respectively: pre * m (P ) corresponds to pre * (P ) in Un(C); pre * M (P ) is the least set such that for r ∈ P , r ∈ pre * M (P ) and for every λ(r , a) = r with a ∈ must(r ) and r ∈ pre * (P ) then r ∈ pre * M (P ). Last, post * m (P ) is post * (P ) in Un(C). Any terminating automaton can be seen as a marked modal specification with no design choice left open, that is, for any state r, the optional action set may(r) \ must(r) is empty. More formally, the embedding of a terminating automaton M = (R, r 0 , Σ, λ, G) into the class of the marked modal specifications is Em(M) = (R, r 0 , Σ, λ, must, may, G) with, for all r ∈ R, may(r) = must(r) = ready(r). Now, the semantics of marked modal specifications is given in terms of terminating automata:

Definition 2 (Satisfaction) A terminating automaton M = (R, r 0 , Σ, λ, G) satisfies the marked modal specification C = (Q, q 0 , Σ, δ, must, may, F ), denoted M |= C, if an only if there exists a simulation relation π ⊆ R × Q such that (r 0 , q 0 ) ∈ π
and for all pairs (r, q) ∈ π:

1. must(q) ⊆ ready(r) ⊆ may(q); 2. r ∈ G implies q ∈ F ; 3. for every a ∈ Σ and every r ∈ Q, λ(r, a) = r implies r , δ(q, a) ∈ π.

The set of models (or implementations) of C is denoted C . A marked modal specification if said satisfiable if and only if C = ∅. Two marked modal specifications C and C are said equivalent, written C ≡ C , if and only if they admit the same implementations: C = C . Any unsatisfiable specification is mapped on a special specification marked modal specification denoted C ⊥ , with C ⊥ = ∅.

Example 3 Consider the terminating automaton M in Fig. 1(a) and the marked modal specification C in Fig. 1(b) where transitions from q labeled by a are dashed when a ∈ may(q) \ must(q) and plain when a ∈ must(q); marked states are double-circled. M satisfies C because of the simulation relation π = {(0, 0 ), (1, 1 ), (2, 2 ), (3, 1 )}.

Observe that, in state 2 , although none of the two outgoing transition is must, at least one of the two has to be present in any model in order to preserve the reachability of a marked state. Such restricted disjunction cannot be expressed with traditional unmarked modal specifications. Observe also that, according to the second item of the Def. 2, the reachability of a marked state may be delayed: 1 is marked, (3, 1 ) ∈ π but 3 is not marked; however, a marked state can be eventually reached from 3 thanks to the state 1.

According to Def. 2, only reachable states of C are semantically meaningful. We thus suppose from now on, and without loss of generality, that C is reachable, that is: ∀q ∈ Q, q 0 ∈ pre * (q).

A marked state q ∈ F is said delayable if q can be reached again, that is, there exists a word u = such that δ(q, u) = q; it is said undelayable otherwise. Denote by D the set of delayable states of a marked modal specification.

(c) Must-saturation of C Figure 1: M is a model of C A marked state q ∈ F is a bottleneck of C if it is the only marked states reachable from some state q ∈ Q that is, post * m (q ) ∩ F = {q}.
Intuitively, this notion allows to identify the states that will be marked in any model of the specification.

Lemma 4 Given a terminating automaton M and a marked modal specification C s.t. M |= C then: L M ⊆ L C , and, for all u ∈ L M , λ(r 0 , u), δ(q 0 , u) ∈ π.

Proof: The language inclusion is a direct consequence of the third item of Def. 2. Moreover, as modal specifications are assumed deterministic, the relation π is unique, when it exists, and thus, for any u ∈ L M , λ(r 0 , u), δ(q 0 , u) ∈ π.

The introduced semantics induces some simplifications in the structure of the marked modal specifications that we discuss now. At the end of this section, this will leads to the definition of an associated normal form.

Must-saturation. Observe that any terminating automaton model of the marked modal specification in Fig. 1 includes the starting transition labeled by a stemming from the initial state. It is thus a required transition that can be assigned a must modality in the specification. We therefore introduce the must-saturation of marked modal specifications.

Definition 5 (Must-saturation) A marked modal specification is must-saturated if for all q / ∈ F such that there is a unique a ∈ may(q), we have a ∈ must(q). Such a must-mapping is then said to be saturated. Lemma 6 Any must-mapping can be saturated without changing the set of marked implementations.

Proof: Let (r, q) ∈ π. If q / ∈ F then r / ∈ G.
As M is terminating, it is then possible to reach a marked state from r and: card(ready(r)) ≥ 1. As card(may(q)) = 1, we have: card(ready(r)) = 1 for any M and it is not different than to have card(must(q)) = 1.

Inria

Consistency and attractability. Given a marked modal specification C = (Q, q 0 , Σ, δ, must, may, F ) and a state q ∈ Q, C is said consistent in q if and only if must(q) ⊆ may(q). C is said attracted in q if and only if q ∈ pre * m (F ).

Lemma 7 If M |= C then C is consistent and attracted in every state δ(q 0 , u) with u ∈ L M .

Proof: Let u ∈ L M , by Lem. 4 we have λ(r 0 , u), δ(q 0 , u) ∈ π. Thus, from the first item of Def. 2, must(δ(q 0 , u)) ⊆ ready(λ(r 0 , u)) ⊆ may(δ(q 0 , u)) and C is consistent in δ(q 0 , u).

We now prove that C is attracted in δ(q 0 , u) that is, δ(q 0 , u) ∈ pre * (F ). Since M is terminating λ(r 0 , u) ∈ pre * (G). As a result, there exists a suffix v of u such that uv ∈ L M and λ(r 0 , uv) ∈ G. By Lem. 4, uv ∈ L C and λ(r 0 , uv), δ(q 0 , uv) ∈ π. Now if λ(r 0 , uv) ∈ G then δ(q 0 , uv) ∈ F by item 2 of Def. 2 and thus δ(q 0 , u) ∈ pre * (F ).

As a consequence, only consistent and attracting states of C are semantically meaningful. This now leads us to define a reduced form: Definition 8 (Reduced marked modal specification) C is reduced iff every state is reachable and it is consistent and attracted in every state q ∈ Q.

Proposition 9 (Reducibility) Every satisfiable marked modal specification is equivalent to a reduced marked modal specification.

Proof of this proposition is by construction of a reduced marked specification ρC and then proving that C and ρC are equivalent. This construction makes use of a pruning operation. We denote by Q Ψ ⊆ Q the set of all states q ∈ Q such that q is inconsistent or unattracting, that is: must(q) may(q) or q / ∈ pre * (F ).

Definition 10 (Reduction operation) Given a marked modal specification C = (Q, q 0 , Σ, δ, must, may, F ):

if q 0 ∈ pre * M (Q Ψ ) then the reduction of C is C ⊥ ; otherwise, it is the marked modal specification (Q \ pre * M (Q Ψ ) , q 0 , Σ, δ , must , may , F \ pre * M (Q Ψ ))
where: δ (r, a) = r if and only if δ(r, a) = r and r, r / ∈ pre * M (Q Ψ ); as indicated in right after Def. 1, may can be recovered from δ whereas must is the restriction of must to the domain

Q \ pre * M (Q Ψ ).
We now prove Prop. 9: Proof: We first show : C ⊆ ρC . We prove that M |= ρC can be established with the same simulation relation π that states M |= C:

• Let (r, q) ∈ π ⊆ R × Q. Observe first that q / ∈ Q Ψ according to Lem. 7. Moreover, q / ∈ pre * M (Q Ψ ) otherwise, there would exist q ∈ Q Ψ coreachable from q by following transitions labeled by must-actions and thus we would have (r , q ) ∈ π with q ∈ Q Ψ for some r ∈ R which is not possible by Lem. 7. As a result, π stating

M |= C is more precisely defined over R × Q \ pre * M (Q Ψ ) .
• Moreover, we can show that if λ(r, a) is defined and q / ∈ pre * M (Q Ψ ) then δ (q, a) is also defined. By contradiction, suppose that δ (q, a) is not defined then δ(q, a) ∈ pre * M (Q Ψ ) by construction of δ . However, λ(r, a) defined implies δ(q, a) defined and λ(r, a), δ(q, a) ∈ π as M |= C and, by Lem. 7, δ(q, a) / ∈ pre * M (Q Ψ ) which is in contradiction with the previous sentence. Consequence from the two previous items is that any pair (r, q) ∈ π which states M |= C can also be seen as pair of states of M and ρC. We now show that F , must and may satisfies the constraints of a model relation:

• First, as M |= C, we have r ∈ G implies q ∈ F . As previously shown, q / ∈ pre * M (Q Ψ ) and thus q ∈ F \ pre * M (Q Ψ ); • Next, if must(q) ⊆ ready(r) then, as ∈ Q \ pre * M (Q Ψ )
, by construction we have must (q) = must(q) and thus must (q) ⊆ ready(r); • Last, if ready(r) ⊆ may(q), we can show that ready(r) ⊆ may (q). By contradiction, suppose ready() ∩ (may(q) \ may (q)) = ∅. Then there exists a for which λ(r, a), δ(q, a) are defined and q / ∈ pre * M (Q Ψ ) but δ (q, a) is not defined. We have shown above that this situation is not possible. As a result, M |= ρC which concludes the first part of the proof. We now prove : C ⊇ ρC . It is clear that the graph associated with Un(ρC) is a sub-graph of Un(C) as ρC is built from C by removing some edges. As a result, all pairs (r, q) in the simulation relation π stating that M |= ρC can also be seen as a pair of states of M and C. We now show that π also defines a suitable simulation relation in order to establish M |= C as G, may and must of C satisfies the constraints of a model relation. Let (r, q) ∈ π:

• If r ∈ G then q ∈ F \ pre * M (Q Ψ )
and thus, in particular, q ∈ F ; • By construction, must (q) = must(q) and may (q) ⊆ may(q). As a result, if must (q) ⊆ ready(r) ⊆ may (q) then must(q) ⊆ ready(r) ⊆ may(q). As a result, M |= C which concludes the proof.

Normal form. This now leads us to define the normal form of any marked modal specification: Definition 11 (Normal form) A marked modal specification is in normal form if it is both must-saturated and reduced.

According to Lem. 6 and Prop. 9, any marked modal specification C can be put in normal form ηC without altering its set of models. As a result, from now on, we always suppose that marked modal specifications are in normal form.

At this point, the reader may wonder why must-saturation, consistency and attractability are not fully part of the definition of marked modal specification (as it is the case for the consistency requirement in the original papers on unmarked modal specifications [START_REF] Larsen | A modal process logic[END_REF][START_REF] Larsen | Automatic Verification Methods for Finite State Systems[END_REF]). The reason for this is because, in what follows, we propose composition operators on marked modal specifications and it is easier to define these constructions without trying to preserve these different requirements. Now if the combination of two marked modal specifications (which are now implicitly supposed to be in normal form) gives rise to the a specification violating one of the above requirements then a step of normalization has to be applied on the result in order to have an iterative process.

Refinement of marked modal specifications

A refinement relation aims at relating interfaces at different stages of their design. Basically, it should correspond to refine the set of allowed implementations of an interface. Moreover, we shall see later that refinement should entail substitutability, meaning that the substitution of an interface C 2 by a refined version C 1 must not impact the possible and actual cooperation with other components, that have been previously declared as legal for C 2 .

Definition 12 (Refinement) Given two marked modal specifications

C 1 = (Q 1 , q 0 1 , Σ, δ 1 , must 1 , may 1 , F 1 ) and C 2 = (Q 2 , q 0 2 , Σ, δ 2 , must 2 , may 2 , F 2 ), C 1 is a refinement of C 2 , noted C 1 ≤ C 2 ,
if and only if there exists a simulation relation Π ⊆ Q 1 ×Q 2 such that (q 0 1 , q 0 2 ) ∈ Π and, for all pairs (q 1 , q 2 ) ∈ Π:

1. may 1 (q 1 ) ⊆ may 2 (q 2 ) and must 1 (q 1 ) ⊇ must 2 (q 2 ); Inria 2. q 1 ∈ F 1 implies q 2 ∈ F 2 ; 3. for every a ∈ may 1 (q 1 ), we have: δ 1 (q 1 , a), δ 2 (q 2 , a) ∈ Π.

Intuitively, refining an interface corresponds to possibly changing a transition with a may modality into either a required or a proscribed transition while potentially delaying the reachability of a marked state. This relation is reflexive and transitive and is thus a preorder.

Theorem 13 Given two marked modal specifications

C 1 and C 2 , C 1 ≤ C 2 if and only if, C 1 ⊆ C 2 .
Theorem 13 holds provided the marked modal specifications are deterministic. If nondeterminism is allowed, refinement becomes correct but not fully abstract (the implication from right to left in Theorem 13 is not true in general). This is discussed for unmarked modal specifications in [START_REF] Larsen | On modal refinement and consistency[END_REF]; their counterexample can be immediately adapted to our context. Moreover, as argued in [START_REF] Fecher | On the expressiveness of refinement settings[END_REF], nondeterministic modal specifications are not really suitable to characterize a set of deterministic automata.

To prove this Theorem, the two following intermediate Lemmata are necessary. We first define the maximal implementation associated to a marked modal specification: Lemma 14 (Maximal Implementation) Given a marked modal specification C = (Q, q 0 , Σ, δ, must, may, F ), the automaton M C = (Q, q 0 , Σ, δ, F ) satisfies C and moreover, L M = L C .

Proof: Take equality as the simulation relation. For all q ∈ Q, we have for M C : ready(q) = may(q). Since C is in normal form, we have must(q) ⊆ may(q). Hence, must(q) ⊆ ready(q) ⊆ may(q). Normal form implies that Q = pre * (F ). Hence M C is a terminating automaton satisfying C and such that L M = L C .

Remark also that the simulation relation can be chosen to be a least relation defined as follows:

Definition 15 (Least Simulation Relation) Given C 1 = (Q 1 , q 0 1 , Σ, δ 1 , must 1 , may 1 , F 1 ) and C 2 = (Q 2 , q 0 2 , Σ, δ 2 , must 2 , may 2 , F 2 ) two marked modal specifications, define Γ ⊆ Q 1 × Q 2 to be the least relation such that:

1. (q 0 1 , q 0 2 ) ∈ Γ; 2. For all (q 1 , q 2 ) ∈ Γ, if a ∈ may 1 (q 1 ) ∩ may 2 (q 2 ) then δ 1 (q 1 , a), δ 2 (q 2 , a) ∈ Γ.

Lemma 16 Given two marked modal specifications C 1 and C 2 , C 1 refines C 2 implies that any (q 1 , q 2 ) ∈ Γ satisfies the items of Def. 12.

Proof: Assume C 1 ≤ C 2 , meaning that there exists Π satisfying the items of Def. 12. Lets prove that Γ ⊆ Π. The pair of initial states are in both relations: (q 0 1 , q 0 2 ) ∈ Γ ∩ Π. If (q 1 , q 2 ) ∈ Γ ∩ Π, then for every a ∈ may 1 (q 1 ) ⊆ may 2 (q 2 ), δ 1 (q 1 , a), δ 2 (q 2 , a) ∈ Γ∩Π. This proves that Γ = Γ∩Π, and hence Γ ⊆ Π. This implies that any (q 1 , q 2 ) ∈ Γ also satisfies the items of Def. 12.

We can now prove Theorem 13: Proof: (⇒) Suppose that M |= C 1 and C 1 ≤ C 2 , meaning that there exists simulation relations

π ⊆ R × Q 1 and Π ⊆ Q 1 × Q 2 ,
witnesses of the satisfaction and refinement relations. Hence we assume that π satisfies the items of Def. 2 and the Π satisfies the items of Def. 12.

We now prove that M |= C 2 . This is done by proving that relation π

• Π = {(r, q 2 ) ∈ R × Q 2 | ∃q 1 ∈ Q 1 st. (r, q 1 )
∈ π and (q 1 , q 2 ) ∈ Π} satisfies the items of Def. 2. (r 0 , q 0 1 ) ∈ π and (q 0 1 , q 0 2 ) ∈ Π imply (r 0 , q 0 2 ) ∈ π • Π. Given (r, q 2 ) ∈ π • Π, there exists q 1 ∈ Q 1 such that (r, q 1 ) ∈ π and (q 1 , q 2 ) ∈ Π. Take any q 1 ∈ Q 1 such that (r, q 1 ) ∈ π and (q 1 , q 2 ) ∈ Π. (i) must 2 (q 2 ) ⊆ must 1 (q 1 ) ⊆ ready(r) ⊆ may 1 (q 1 ) ⊆ may 2 (q 2 ); (ii) r ∈ G implies q 1 ∈ F 1 implies q 2 ∈ F 2 ; And (iii) for every a ∈ Σ and every r ∈ R such that λ(r, a) = r , r , δ 1 (q 1 , a) ∈ π and (δ 1 (q 1 , a), δ 2 (q 2 , a)) ∈ Π. Hence (r , δ 2 (q 2 , a)) ∈ π • Π.

(⇐) We proceed by contraposition; we prove that if C 1 C 2 then there exists a model M of C 1 that is not a model of C 2 . Consider the least simulation Γ. Since C 1 C 2 , (i) C 1 is satisfiable and (ii) there exists (q 1 , q 2 ) ∈ Γ such that at least one of the items of Def. 12 is not satisfied:

• Assume may 1 (q 1 ) may 2 (q 2 ). By construction

M C1 |= C 1 , while M C1 |= C 2 .
• Assume may 1 (q 1 ) ⊆ may 2 (q 2 ) for all (q 1 , q 2 ) ∈ Γ and must 1 (q 1 ) must 2 (q 2 ). Hence there exists a ∈ must 2 (q 2 )\must 1 (q 1 ). Construct M = (Q 1 , q 0 1 , Σ, λ, G 1 ) such that λ(q, b) = q of and only if δ 1 (q, b) = q and q = q 1 or b = a. Recall C 1 is in normal form, hence M |= C 1 . However, a ∈ must 2 (q 2 ) and a / ∈ ready(q 1 ). Hence M |= C 2 . • Assume may 1 (q 1 ) ⊆ may 2 (q 2 ) and must 1 (q 1 ) ⊇ must 2 (q 2 ) for all (q 1 , q 2 ) ∈ Γ. Assume

q 1 ∈ F 1 and q 2 / ∈ F 2 . M C1 |= C 1 , while M C1 |= C 2 .
When the left counterpart is ultimately refined, the refinement relation coincide with the implementation relation: given a terminating automaton M and a marked modal specification C, M |= C if and only if Em(M) ≤ C.

Conjunction of marked modal specification

It is a current practice, when modeling complex systems, to associate several specifications with a same system, sub-system, or component, each of them describing a different aspect of it. These so-called viewpoints may be engineered independently, and possibly by different teams. It is then natural to question whether different viewpoints are not contradictory and how to realize all of them. This leads to define a conjunction operator. Moreover in [START_REF] Doyen | Interface theories with component reuse[END_REF], the authors point out that, during the design cycle, a designer may be tempted to merge two interfaces which share some similarities in order to use a same implementation for the two interfaces. More formally, this corresponds to look for a shared refinement of the interfaces, if it exists.

We now define a conjunction operator which enjoy the expected properties to solve the two above problems.

Definition 17 (Conjunction) Given two marked modal specifications

C 1 = (Q 1 , q 0 1 , Σ, δ 1 , must 1 , may 1 , F 1 ) and C 2 = (Q 2 , q 0 2 , Σ, δ 2 , must 2 , may 2 , F 2 ), the conjunction of C 1 and C 2 , noted C 1 ∧ C 2 , is the normal form η(C 1 & C 2 ) of C 1 & C 2 = (Q, q 0 , Σ, δ, must, may, F ) with: 1. Q = Q 1 × Q 2 and q 0 = (q 0 1 , q 0
2 ); 2. for any q 1 ∈ Q 1 , q 2 ∈ Q 2 and a ∈ Σ, δ (q 1 , q 2 ), a = (q 1 , q 2 ) if and only if δ 1 (q 1 , a) = q 1 and δ 2 (q 2 , a) = q 2 ; 3. may(q 1 , q 2 ) = may 1 (q 1 ) ∩ may 2 (q 2 ) and must(q 1 , q 2 ) = must 1 (q 1 ) ∪ must 2 (q 2 ); 4. (q 1 , q 2 ) ∈ F if and only if q 1 ∈ F 1 and q 2 ∈ F 2 .

Considering the manipulations done on the may/must-maps and on the transition map to obtain C 1 & C 2 , the must-saturation and the consistency may not be respected. We thus impose a normalization step in order to have an iterative process as explained at the end of Sec. 2.

Theorem 18 Given some marked modal specifications C 1 , C 2 , C 3 and C:

•

C 1 ∧ C 2 = C 1 ∩ C 2 ; Inria b (a) M 1 a b (b) C 1 a (c) M 2 a b (d) C 2 Figure 2: Reachability is not compositional • C 1 ∧ C 2 is the greatest lower bound of C 1 and C 2 for the refinement relation: C ≤ C 1 and C ≤ C 2 iff C ≤ C 1 ∧ C 2 ; • ∧ is associative: C 1 ∧ (C 2 ∧ C 3 ) ≡ (C 1 ∧ C 2 ) ∧ C 3 .
Proof: The proof of the second item is a direct consequence of the first one: if C ≤ C i for i ∈ {1, 2} then, by Theorem 13: C ⊆ C i . As a result, we have:

C ⊆ C 1 ∩ C 2 . By the first item of Theorem 18, this is equivalent to: C ⊆ C 1 ∧ C 2 . Last, we deduce from Theorem 13 that C C 1 ∧ C 2 .

Product of marked modal specifications

Reachability is not preserved by product in general. Fig. 2 shows a simple example: M 1 |= C 1 and M 2 |= C 2 ; however the product of M 1 × M 2 is a single non-marked state, hence the reachability of a marked state is not possible. This leads us to consider the following problem: given two marked modal specifications, can they be implemented concurrently i.e., such that the product of any model of the first specification with any model of the second one will always have the ability to reach a marked state of the product?

Similarly to [START_REF] De Alfaro | Interface automata[END_REF], we distinguish a pessimistic from an optimistic view of composition and solve the previous problem in this two contexts.

First, in order to represent the cooperation between subsystems, a signature over Σ is now associated to any terminating automaton or marked modal specification over Σ: Definition 19 (Signature) Given a set of actions Σ, a signature over Σ is a mapping µ : Σ → {?, !} which associates to any action either ? when the action is an input or ! when it is an output. Now, transitions are either labeled !a (for µ(a) = !) when the entity responsible for the occurrence of a is the system, or ?a (for µ(a) = ?) if a stems from the environment of the system. The resulting formalism is thus suited to model protocols between a system and an unknown partner belonging to the system environment. Contrarily to the input/output automata of [START_REF] Lynch | An introduction to Input/Output automata[END_REF] and following the interface automata of [START_REF] De Alfaro | Interface automata[END_REF], terminating automata and marked modal specifications are not required to be input-enabled, meaning that some actions ?b of the environment may not be permitted in some state q. More formally, this situation occurs in state q if there is no outgoing transition from q labeled by ?b. This allows to restrict, from the point of view of the system, the behavior of its environment.

Example 20 Fig. 3(a) depicts the specification of a service which can receive requests ?r from an unidentified subsystem in its environment and then answers by producing !a untils it is stopped C 1 over {?r, ?e, ?f, !a, !b}

0 1 2 !r ?a ?a !t (b) C 2 over {?a, ?b, !r, !f } 0, 0 1, 1 2, 2 q 6, 2 !r !a ?e !f (c)
C1 C2 over {?e, !r, !f, !a, !b} with ?f . It may also produce !b when set in an enhanced mode by ?e. Fig. 3(b) depicts the specification of a client which expects to receive ?a as an answer to any request !r and is ready to receive remitted ?a. Although ?b is in the signature of C 2 , there is no transition labeled ?b meaning that the client rejects this inputs.

We write Σ ? and Σ ! for the set of input and output actions, respectively, thus forming a partition of Σ. A system is then closed if its associated signature is such that Σ ? = ∅ and open otherwise. In this paper, we assume that if M |= C then the signature associated to M and C is identical. Similarly, if C 1 ≤ C 2 then C 1 and C 2 have the same signature 1 .

A first condition to product is the composability of signatures. Given two signatures µ 1 and µ 2 over Σ 1 and Σ 2 respectively, defining two partitions Σ ? 1 , Σ ! 1 and Σ ? 2 , Σ ! 2 , they are composable if no output actions is shared: Σ ! 1 ∩Σ ! 2 = ∅. For composable signatures, we let the communication actions be the set Σ co (µ 1 , µ 2 ) = (Σ ? 1 ∩ Σ ! 2 ) ∪ (Σ ? 2 ∩ Σ ! 1 ) which corresponds to the shared actions on which a synchronization will be possible. The complement is called the set of private actions and is denoted Σ pr (µ

1 , µ 2 ) = (Σ 1 ∪ Σ 2 ) \ Σ co (µ 1 , µ 2 ).
Definition 21 (Product of signatures) The product of two composable signatures µ 1 and µ 2 is µ = µ 1 × µ 2 defined over Σ 1 ∪ Σ 2 such that:

Σ ? = (Σ ? 1 ∪ Σ ? 2 ) \ Σ co (µ 1 , µ 2 ) and Σ ! = Σ ! 1 ∪ Σ ! 2 .
The product of two terminating automata M 1 and M 2 with respective composable signatures µ 1 and µ 2 is then M 1 × M 2 as defined in Sec. 2.1 with signature µ 1 × µ 2 .

Pessimistic composition of marked modal specifications

We first consider the case of pessimistic2 composition; we define a sufficient and necessary condition such that two marked modal specification can be independently implemented, the product of any of their implementations being terminating.

This condition corresponds to the existence of a joint path to a marked state, for every reachable state of the product of arbitrary implementations. We then consider the less cooperative situation in which any optional behavior is disabled and check if such paths exist. However, the minimal behavior associated to a state of a marked modal specification is not unique in general. Consider C 1 in Fig. 2(b), the minimal number of outgoing transition stemming from the initial state among all the models of C 1 is 1 and can be either a transition label by a or by b. To represent the different minimal possibilities, we thus use an intermediate structure called minimal constraint automaton. First we define the set of minimal constraints associated to a state: Definition 22 (Minimal constraints) For any state q of a marked modal specification C defined over Σ, we associate the set ζ(q) ∈ 2 2 Σ defined by:

ζ(q) =    { must(q) } if must(q) = ∅ { {a} | a ∈ may(q) } if must(q) = ∅ and q / ∈ F { ∅ }
if must(q) = ∅ and q ∈ F Definition 23 (Minimal constraints automaton) Given a state q of a marked modal specification C over Σ, the minimal constraints automaton Min(C, q) is the automaton over Σ whose initial state is q; its labeled transition map is λ Min such that λ Min (q , a) = q if and only if a ∈ X with X ∈ ζ(q ) and δ(q , a) = q ; its set of final states G Min is the set of undelayable bottlenecks of C.

We identify potential dead-ends, that is pairs of states of two marked modal specifications C 1 and C 2 to be composed from which no outgoing transition may be available in a product of two respective implementations: Definition 24 (Dead-end) Given q 1 and q 2 two states respectively from the marked modal specifications C 1 and C 2 defined over Σ 1 and Σ 2 , the pair (q 1 , q 2 ) is a dead-end if:

1.

q 1 ∈ (F 1 \ D 1 ) or q 2 ∈ (F 2 \ D 2 ) and, 2. there exists X 1 ∈ ζ 1 (q 1 ) and X 2 ∈ ζ 2 (q 2 ) such that: (X 1 ∪ (Σ 2 \ Σ 1 )) ∩ (X 2 ∪ (Σ 1 \ Σ 2 ) = ∅.
Example 25 The minimal constraints associated to the initial states of C 1 and C 2 from Fig. 2 and defined over the same alphabet of actions {a, b} are respectively {{a}, {b}} and {{a}}. The pair formed by this two states is thus a dead-end as for X 1 = {b} and X 2 = {a}, we have

X 1 ∩ X 2 = ∅.
This now leads us to a definition of exception state pairs from which a joint path to a marked state pair cannot be ensured independently of the implementation choices to be made: Definition 26 (Exception state pair) Given q 1 and q 2 two states respectively from two marked modal specifications C 1 and C 2 , the pair (q 1 , q 2 ) is an exception, noted Ex(q 1 , q 2 ) if:

• Min(C 1 , q 1 ) × Min(C 2 , q 2 ) is not terminating or,

• there exists a reachable dead-end3 (q 1 , q 2 ) in Min(C 1 , q 1 ) × Min(C 2 , q 2 ).

Then we can define the following criterion characterizing marked modal specifications having compatible reachability: Definition 27 (Compatible reachability) Two marked modal specifications C 1 and C 2 have a compatible reachability, noted C 1 ∼ T C 2 , if there is no exception state pair that is reachable in Un(C 1 ) × Un(C 2 ).

The soundness and the completeness of the previous definition is then stated by the following Theorem:

One important principle in modular and concurrent design of systems is the fact that a property checked on a primary version of some system artifacts remains true on any refined version of them. This is what allows to guarantee that the system parts corresponding to compatible interfaces can be designed concurrently. This is respected for compatible reachability:

Proposition 34 For all marked modal specifications C

1 , C 1 and C 2 , if C 1 ∼ T C 2 and C 1 C 1 then C 1 ∼ T C 2 and C 1 ⊗ C 2 C 1 ⊗ C 2 . Proof: Let M 1 and M 2 be models of C 1 and C 2 . As C 1 C 1 , by Theorem 13, M 1 is also a model of C 1 . Moreover, the product M 1 × M 2 is terminating as C 1 ∼ T C 2 , by Theorem 28. As a result, by Theorem 28, C 1 ∼ T C 2 .
Last, the product is a commutative and associative operator, meaning that interfaces can be assembled in any order without affecting the result.

Proposition 35 The product of marked modal specifications is commutative and associative. Given three marked modal specifications C 1 , C 2 and C 3 :

C 1 ⊗ C 2 ≡ C 2 ⊗ C 1 and C 1 ⊗ (C 2 ⊗ C 3 ) ≡ (C 1 ⊗ C 2 ) ⊗ C 3 .
Remark 36 If a bottleneck q 1 of C 1 belongs to a cycle in Min(C 1 , q 1 ) then for any q 2 of C 2 , Min(C 1 , q 1 ) × Min(C 2 , q 2 ) will not be terminating, that is C 1 T C 2 .

Optimistic composition of marked modal specifications

Consider again C 1 and C 2 from Fig. 3. They do not have a compatible reachability as (4, 1) is a reachable dead-end and thus an exception state pairs in the sense of Def. 26. It is however pessimistic to declare C 1 and C 2 as not composable. Indeed, the system potentially formed by any model of C 1 and C 2 would not be closed as the occurence of ?e would still be under the control of the environment. Now by preventing the environment from producing !e when C 1 and C 2 are in their initial state, the reachability of the exception state pairs (4, 1) can be avoided 4 . In this section, let us now be optimistic and declare composable any C 1 and C 2 if there exists at least one environment, closing the system and preventing the reachability of bad states of C 1 and C 2 in which the reachability property cannot be guaranteed.

Definition 37 (Legal environment) Given M and E two terminating automata, E is said to be a legal environment for M, if and only if: the signature of M and E are composable; M × E is closed; Em(M) ∼ T Em(E), that is M × E is terminating.

Next, we identify unusable states from which the reachability of an exception state pair cannot be prevented regardless of the environment. This corresponds to pairs of state that can autonomously reach an exception state pair by a sequence of output actions: Definition 38 (Unusable pair of states) Given C 1 and C 2 two marked modal specifications with respective signature µ 1 and µ 2 , the set of unusable pair of states U ⊆ Q 1 × Q 2 is the least set such that:

• if Ex(q 1 , q 2 ) then (q 1 , q 2 ) ∈ U ;

• if, for a ∈ Σ co (µ 1 , µ 2 ), δ 1 (q 1 , a), δ 2 (q 2 , a) ∈ U then (q 1 , q 2 ) ∈ U ;

• if, for a ∈ Σ pr (µ 1 , µ 2 ) ∩ Σ ! 1 , δ 1 (q 1 , a), q 2 ∈ U then (q 1 , q 2 ) ∈ U ; • if, for a ∈ Σ pr (µ 1 , µ 2 ) ∩ Σ ! 2 , q 1 , δ 2 (q 2 , a) ∈ U then (q 1 , q 2 ) ∈ U .

Proposition 45 For all marked modal specifications C 1 , C 1 and

C 2 , if C 1 ∼ O C 2 and C 1 C 1 then C 1 ∼ O C 2 and C 1 C 2 C 1 C 2 .
Proposition 46 The optimistic product of marked modal specifications is commutative and associative. Given three marked modal specifications C 1 , C 2 and C 3 :

C 1 C 2 ≡ C 2 C 1 and C 1 (C 2 C 3 ) ≡ (C 1 C 2 ) C 3 .

Related works and conclusion

Marked modal specifications can be used to express, in a modular manner, that a system should be capable of reaching one or several marked states representing either the completion of a composition of services or the quiescence of a network of interacting agents. They improve the expressive power of deterministic modal specifications that corresponds to the conjunctive ν-calculus [START_REF] Feuillade | Modal specifications for the control theory of discrete-event systems[END_REF] which does not allow to capture reachability properties.

The same goal can be achieved with automata-theoretic specifications in which states are annotated with propositional formulas expressing implementation variants and, possibly, an obligation of progress. This is the case of annotated automata [START_REF] Wombacher | IPSI-PF -a business process matchmaking engine based on annotated finite state automata[END_REF] and operating guidelines [START_REF] Massuthe | Operating guidelines -an automata-theoretic foundation for the service-oriented architecture[END_REF][START_REF] Lohmann | Compact representations and efficient algorithms for operating guidelines[END_REF]. While both formalisms have a product (or parallel) composition operator, they are missing the optimistic view of composition and also the conjunction operator that turns out to be instrumental as soon as components are described according to several distinct but interacting viewpoints [START_REF] Raclet | A modal interface theory for component-based design[END_REF].

The disjunctive variants of modal specifications [START_REF] Larsen | Equation solving using modal transition systems[END_REF][START_REF] Fecher | Comparing disjunctive modal transition systems with an oneselecting variant[END_REF] allows to constraint progress and thus to inductively express reachability. However no implementation relations including marked states nor optimistic composition have been proposed for these variants of modal specifications.

Marked modal specifications look similar to the modal specifications with marked states introduced in [START_REF] Darondeau | Supervisory control for modal specifications of services[END_REF]. However, these two formalisms are very different because the satisfaction relation in [START_REF] Darondeau | Supervisory control for modal specifications of services[END_REF] admits implementations having final states corresponding to a state of the specification that is not final. This is appropriate in the context of supervisory control synthesis. However, this semantics does not seem well-suited to a specification algebra with a refinement preorder, which explains why a different satisfaction relation is used for marked modal specifications.

Figure 3 :

 3 Figure 3: Example of composition

RR n°7928

This assumption is taken to simplify the presentation. Refinement of signature as defined in[START_REF] Raclet | A modal interface theory for component-based design[END_REF] can be handled in the presented theory.

The pessimistic view of this approach will be made clearer in the next section.Inria

As the set of states of Min(C i , q i ) is a subset of these of C i , we can refer to (q 1 , q 2 ) in Min(C 1 , q 1 )×Min(C 2 , q 2 ) as a pair of states of C 1 and C 2 and then test if it is a dead-end in the sense of Def. 24.RR n°7928

A similar pruning on the outputs of input complete specifications was proposed in[START_REF] Dill | Trace theory for automatic hierarchical verification of speed-independent circuits[END_REF], ealier than in[START_REF] De Alfaro | Interface automata[END_REF].Inria

Inria

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Caillaud & Raclet

Theorem 28 (Independent implementability) Given two marked modal specifications C 1 and C 2 , C 1 ∼ T C 2 if and only if for any M 1 |= C 1 and M 2 |= C 2 , the product M 1 × M 2 is terminating.

To prove this Theorem, we need the two following intermediate Lemmata.

Lemma 29 For any M |= C and pair (r, q) ∈ π, there exists a set X ∈ ζ(q) such that X ⊆ ready(r).

Proof: If must(q) = ∅ then ζ(q) = {must(q)}. As (r, q) ∈ π, we have must(q) ⊆ ready(r). Thus, for X = must(q) ∈ ζ(q), we have X ⊆ ready(r).

If must(q) = ∅ and q / ∈ F then ζ(q) = {{a} | a ∈ may(q)}. As q / ∈ F , we have r / ∈ G and there exists a path from r to a marked state. Thus, there exists at least an a ∈ may(q) such that λ(r, a) is defined. For X = {a} ∈ ζ(q), we then have X ⊆ ready(r).

Last, if must(q) = ∅ and q ∈ F then ζ(q) = {∅}. Thus, for X = ∅ ∈ ζ(q), we have X ⊆ ready(r).

Lemma 30 If a state q of a marked modal specification C is a bottleneck and is not delayable then may(q) = ∅.

Proof: Suppose that may(q) = ∅ then as C is supposed to be in normal form, there exists a marked state reachable from q. As q is a bottleneck, the only reachable marked state from q is q. However, as q is not delayable, q cannot be reached again. As a result, may(q) = ∅.

We can now prove Theorem 28: Proof: (⇒) We assume C 1 ∼ T C 2 and we prove that, for M 1 |= C 1 and M 2 |= C 2 , M 1 × M 2 is terminating. We thus fix a u ∈ L M1 L M2 and we show that there exists a v such that λ((r 0 1 , r 0 2 ), uv) ∈ G 1 × G 2 . The word u corresponds to u 1 = pr Σ1 (u) in M 1 and to u 2 = pr Σ2 (u) in M 2 . Let r 1 = λ 1 (r 0 1 , u 1 ) and r 2 = λ 2 (r 0 2 , u 2 ). By Lem. 4, u 1 ∈ L C1 and u 2 ∈ L C2 . Let q 1 = δ 1 (q 0 1 , u 1 ) and q 2 = δ 2 (q 0 2 , u 2 ). As C 1 ∼ T C 2 and as (q 1 , q 2 ) is reached in Un(C 1 ) × Un(C 2 ) after u, (q 1 , q 2 ) is not an exception state pair. Thus Min(C 1 , q 1 ) × Min(C 2 , q 2 ) is terminating and no potential dead-end is reachable in Min(C 1 , q 1 ) × Min(C 2 , q 2 ).

From Lem. 29, we know that u 1 and u 2 can be extended with actions belonging to the minimal constraints sets of C 1 and C 2 respectively. More precisely, we construct a word w in Min(C 1 , q 1 )× Min(C 2 , q 2 ) such that w = a 0 ...a n with a

In any case, we eventually reach a marked state as Min(C 1 , q 1 ) × Min(C 2 , q 2 ) is terminating. Let w 1 = pr Σ1 (w) and to w 2 = pr Σ2 (w) and let (q 1 , q 2 ) be the marked state reached after w in Min(C 1 , q 1 ) × Min(C 2 , q 2 ). Note that, by construction, q 1 and q 2 are undelayable bottlenecks in C 1 and C 2 . Now by Lem. 30, may 1 (q 1 ) = ∅ and may 2 (q 2 ) = ∅. As a result,

If C 1 T C 2 then there exists u ∈ L C1 L C2 such that the state (q 1 , q 2 ) reached after u is an exception pair of state. Two cases are possible:

• Min(C 1 , q 1 )×Min(C 2 , q 2 ) is not terminating, that is: there exists v ∈ L Min(C1,q1) L Min(C2,q2) for which there is no w such that vw ∈ L Min(C1,q1) L Min(C2,q2) and the state reached after vw is marked, that is, by construction, is a pair of bottleneck of C 1 and C 2 .

We consider M i |= C i for i ∈ {1, 2} such that pr Σi (u) ∈ L Mi and the possible suffix of pr Σi (u) are the words in L Min(Ci,qi) . We can choose the marked state of M i such that there is no word w such that pr Σi (uvw) is marked in both M 1 and M 2 as a pair of bottleneck from C 1 and C 2 cannot be reached in Min(C 1 , q 1 ) × Min(C 2 , q 2 ). As a consequence, for uv ∈ L M1 L M2 , there is no suffix w such that the state reached in M 1 × M 2 after uvw is marked. As a result, M 1 × M 2 is not terminating. • (q 1 , q 2 ) is a dead-end, reached in Min(C 1 , q 1 ) × Min(C 2 , q 2 ) after a word v, that is:

, and there exists X 1 ∈ ζ 1 (q 1 ) and X 2 ∈ ζ 2 (q 2 ) such that:

We consider M i |= C i for i ∈ {1, 2} such that pr Σi (uv) ∈ L Mi and such that λ(r 0 , pr Σi (uv)) ∈ G if and only if q i ∈ F i \ D i and ready i (pr Σi (uv)) = X i . The automaton M 1 × M 2 is not terminating as the pair of state reached after uv ∈ L M1 L M2 is not final and has no outgoing transition by construction.

We now define the product of two marked modal specifications with compatible reachability.

Definition 31 (Product) Given two marked modal specifications

with compatible reachability, the product C 1 ⊗ C 2 is the normal form of the marked modal specification (Q, q 0 , Σ 1 ∪ Σ 2 , δ, must, may, F ) with:

1. Q = Q 1 × Q 2 and q 0 = (q 0 1 , q 0 2 ); 2. for any q 1 ∈ Q 1 , q 2 ∈ Q 2 and a ∈ Σ 1 ∪ Σ 2 , δ (q 1 , q 2 ), a is defined as (δ 1 (q 1 , a), δ 2 (q 2 , a))

for a ∈ Σ 1 ∩ Σ 2 , (δ 1 (q 1 , a), q 2 ) for a ∈ Σ 1 \ Σ 2 and (q 1 , δ 2 (q 2 , a)) for a ∈ Σ 2 \ Σ 1 ; 3. may((q 1 , q 2 )) = may 1 (q 1 ) ∪ (Σ 2 \ Σ 1 ) ∩ may 2 (q 2 ) ∪ (Σ 1 \ Σ 2 ) ; 4. must((q 1 , q 2 )) = must 1 (q 1 ) ∪ (Σ 2 \ Σ 1 ) ∩ must 2 (q 2 ) ∪ (Σ 1 \ Σ 2 ) ; 5. (q 1 , q 2 ) ∈ F if and only if q 1 ∈ F 1 and q 2 ∈ F 2 .

Now, the product of any models

Proposition 32 Given two marked modal specifications

Moreover, C 1 ⊗ C 2 gives the most precise characterization of the behavior of the product of any models M 1 of C 1 and M 2 of C 2 :

Proposition 33 Given two marked modal specifications C 1 and C 2 , if C 1 ∼ T C 2 and if there exists a marked modal specification C such that for any

A pair of states is said usable if it is not unusable.

Definition 39 (Optimistic compatible reachability) Two marked modal specifications C 1 and C 2 have an optimistic compatible reachability, noted

This criterion is sound and complete as stated by the following Theorem:

Theorem 40 (Independent implementability) Given two marked modal specifications

Definition 41 (Optimistic product) Given two marked modal specifications

over composable signatures µ 1 and µ 2 and with optimistic compatible reachability, the optimistic product C 1 C 2 is is the normal form of the marked modal specification (Q, q 0 , Σ 1 ∪ Σ 2 , δ, must, may, F ) over µ 1 × µ 2 with:

if a ∈ Σ pr (µ 1 , µ 2 ) ∩ Σ 1 : δ (q 1 , q 2 ), a = (δ 1 (q 1 , a), q 2 ) if (δ 1 (q 1 , a), q 2 ) / ∈ U and q otherwise;

• may(q ) = Σ 1 ∪ Σ 2 and must(q ) = ∅; • (q 1 , q 2 ) ∈ F if and only if q 1 ∈ F 1 and q 2 ∈ F 2 .; q ∈ F . This construction is very similar to the product ⊗ of Def. 31 except that unusable states are pruned away. Transitions labeled by an action ?a that would lead to an unusable state if performed by the environment are rerouted to a fresh state q on which all constraints on the future are relaxed.

Example 42 The optimistic product of C 1 and C 2 from is depicted in Fig. 3(c). The transition labeled by ?e is rerouted from the unusable (3, 0) to q . Optimistic compatible reachability is preserved by refinement hence allowing concurrent design of sub-systems. Moreover, the optimistic product is monotonic with respect to the refinement relation and is also associative which guarantees independence in the design flow.