M Goldman
email: goldman@mis.mpg.de

B Zwicknagl
email: zwicknagl@iam.uni-bonn.de

Scaling law and reduced models for epitaxially strained crystalline films

A variational model for the epitaxial deposition of a film on a rigid substrate in the presence of a crystallographic misfit is studied. The scaling behavior of the minimal energy in terms of the volume of the film and the amplitude of the misfit is considered, and reduced models in the various regimes are derived by Γ-convergence methods. Depending on the relation between the thickness of the film and the amplitude of the misfit, the surface or the elastic energy contribution dominates, and in the critical case the two contributions balance. In particular, the formation of islands is proven if the amplitude of the misfit is large compared to the volume of the film.

Introduction

We study a free energy functional introduced in [START_REF] Spencer | Asymptotic derivation of the glued-wetting-layer model and contact-angle condition for stranski-krastanow islands[END_REF] (see also [START_REF] Bonnetier | Computing the equilibrium configuration of epitaxially strained crystalline films[END_REF][START_REF] Fonseca | Equilibrium configurations of epitaxially strained crystalling films: Existence and regularity results[END_REF][START_REF] Fusco | Equilibrium configurations of epitaxially strained elastic films: Second order minimality conditions and qualitative properties of solutions[END_REF]) to model the epitaxial deposition of a film on a rigid substrate when there is a crystallographic misfit between the two solids. The energy consists of the stored elastic energy in the film and the interfacial energy of its free surface. Precisely, we consider

F d,e 0 (u, h) := ∫ Ω h W (∇u) dx dy + ∫ 1 0 √ 1 + |h | 2 dx, (1)
where the Lipschitz function h : [0, 1] → [0, ∞) describes the profile of the deposited film, Ω h := {(x, y) : 0 ≤ x ≤ 1 , 0 ≤ y ≤ h (x)}, and u ∈ W 1,p (

Ω h ; R 2 )
is the planar displacement. Note that we restrict ourselves to two-dimensional morphologies which correspond to three-dimensional configurations with planar symmetry (see Section 5 for some results in the higher-dimensional setting). We consider film profiles of fixed volume d > 0, i.e., ∫ 1 0 h (x) dx = d, and impose the boundary conditions h(0) = h(1) = 0 (see Figure 1).

The parameter e 0 ∈ R stands for the amplitude of the crystallographic misfit between the film and the rigid substrate, and is introduced in this model via the boundary condition u (x, 0) = e 0 (x, 0). This condition forces the film to be strained. The free energy density W is nonnegative and satisfies a p-growth condition (see Section 2.3). We note that the 1) is normalized by setting a typical surface energy per unit length to one, i.e., the material parameters are all collected in W .

1 x y 1 0 h Ω h Figure 1: A height profile h functional (
It has been observed experimentally and numerically that the qualitative shape of the optimal profile depends on the volume d of the film and on the amplitude of the misfit e 0 (see [START_REF] Bonnetier | Computing the equilibrium configuration of epitaxially strained crystalline films[END_REF][START_REF] Gao | Surface roughening of heteroepitaxial thin films[END_REF][START_REF] Gray | Formation of one-dimensional surface grooves from pit instabilities in annealed SiG/ Si (100) epitaxial films[END_REF][START_REF] Spencer | Asymmetry and shape transitions of epitaxially strained islands on vicinal surfaces[END_REF]). If the volume is small then the film typically forms a flat layer. If the volume of the film is sufficiently large then the flat configuration is no longer stable and atoms often tend to rearrange in such a way that part of the bulk energy is released. The competition between elastic and surface energy then gives rise to the formation of islands on the substrate surface. Such island formation is used for many optical and optoelectronic applications, such as quantum dot lasers.

In recent years, the mathematical analysis of the model [START_REF] Adams | Sobolev spaces[END_REF] has been devoted to the geometrically linear small strain approximation (see [START_REF] Fonseca | Equilibrium configurations of epitaxially strained crystalling films: Existence and regularity results[END_REF][START_REF] Fusco | Equilibrium configurations of epitaxially strained elastic films: Second order minimality conditions and qualitative properties of solutions[END_REF][START_REF] Bonnetier | Computing the equilibrium configuration of epitaxially strained crystalline films[END_REF]), corresponding to small deformations, in which W depends only on the symmetrized gradient E(u) := ∇u+∇ T u 2 . Since we are mainly interested in the regime of large mismatch e 0 , the small strain hypothesis is questionable and instead we focus on the geometrically nonlinear case. We point out that our analysis can be easily carried over to the geometrically linear setting with only very minor modifications. However, in the limit of large strains or large volumes, the model becomes physically less justified since dislocations, fracture, and other plastic effects are more likely to appear. Also, the hypothesis that the film remains a subgraph seems to be rather restrictive. Our aim is thus not to give a quantitative prediction of the formation of islands, but to show how the latter is encoded in this classical model and to highlight the underlying scales. We try in particular to better understand how the relation between the misfit and the volume of the deposited film drives the pattern formation. Our main result is the following scaling law for the energy (see Theorem 3.1): There are positive constants C 1 and C 2 such that for all choices of parameters d and e 0 , } .

Subsequently, we consider the scaling regimes separately and derive reduced limiting func-tionals in the spirit of Γ-convergence in the three scaling regimes and for the transition regime d e p 0 . Our results agree qualitatively with the experimentally observed morphologies. Consider first large volumes d → +∞. If the amplitudes of the misfits e 0 → +∞ are such that e p 0 d → 0, i.e., inf F d,e 0 d, then the surface energy dominates, and the main energy contribution comes from the non-horizontal parts of the boundary. Indeed, in this case the limiting reduced functional does not depend on the elastic strain and charges only the vertical parts of the boundary of Ω h (see Proposition 4.2). The limit problem is minimized by the flat configuration (see Lemma 2.6). In the transition regime in which d e p 0 → +∞, surface and elastic contributions compete (see Section 4.3). Consequently, the minimizer of the reduced model is either the flat configuration or an island, depending on the elastic properties of the material. Finally, if the amplitudes of the misfits are large compared to the volumes, i.e., if e 0 → +∞ and

e p 0 d → +∞, then inf F d,e 0 e p/3 0 d 2/3
, and the main contribution to the energy comes from the elastic part. Precisely, the limiting functional is now defined on the space of (at most) countable sums of Dirac masses. Using a compactness argument (see Proposition 4.7), this proves that in this regime, low-energy sequences have to converge to sums of Dirac masses. This shows that the formation of islands is energetically favorable in this regime. To the best of our knowledge, this work is the first rigorous mathematical justification of the formation of islands in relation to the amplitude of the mismatch between crystallographic lattices in epitaxially strained films. For small volumes d → 0 and small amplitudes of the misfits e 0 → 0 such that e p 0 d 2 → 0, we have inf F d,e 0 1, and the limiting reduced functional is simply a constant (see Proposition 4.1). In particular, for low-energy sequences in this regime neither the elastic energy nor the non-horizontal parts of the boundary contribute significantly to the energy. If, however, e p 0 d 2 → +∞, then inf F d,e 0 e p/3 0 d 2/3 , and, as discussed above for the case of large volumes, low-energy sequences converge to sums of Dirac masses, and the formation of islands is energetically favorable. Notice that our proof makes fundamental use of the fact that we are on a bounded domain. However, building on the techniques developed here, we investigate with P. Bella the same type of problems on unbounded domains and obtain similar results (see [START_REF] Bella | Study of island formation in epitaxially strained films on unbounded domains[END_REF]).

In the last part of the paper we adapt our method to prove the scaling law in higher dimension for the Dirichlet elastic energy (see Proposition 5.1). Even though our method seems to be quite flexible, the richness of the geometry makes the extension to more general energy functionals difficult (see also [START_REF] Chambolle | Interaction of a bulk and a surface energy with a geometrical constraint[END_REF] for some results). We finally note that in higher dimension, the elastic part of the energy can be seen as a repulsive nonlocal term which relates the problem to the Ohta-Kawasaki model that has recently attracted a great deal of attention (see [START_REF] Knüpfer | On an isoperimetric problem with a competing nonlocal term I: The planar case[END_REF][START_REF] Cicalese | Droplet minimizers of an isoperimetric problem with long-range interactions[END_REF][START_REF] Choksi | Small volume fraction limit of the diblock copolymer problem: I. Sharp-interface functional[END_REF][START_REF] Goldman | The Γ-Limit of the Two-Dimensional Ohta-Kawasaki Energy. I. Droplet Density[END_REF][START_REF] Alberti | Uniform energy distribution for an isoperimetric problem with long-range interactions[END_REF]).

We note that in the regimes in which the elastic energy is not dominated by the surface energy, the recession function of W at infinity plays an essential role in the limit. The latter is defined by

W ∞ (A) := lim sup t→+∞ W (tA) t p for A ∈ R 2×2 ,
and appears naturally in problems involving functionals with linear growth (see [START_REF] Fonseca | Quasiconvex integrands and lower semicontinuity in L 1[END_REF][START_REF] Fonseca | Relaxation of quasiconvex functionals in BV(Ω, R p ) for integrands f (x, u, ∇u)[END_REF]).

Previous work, starting with [START_REF] Chambolle | C ∞ regularity of the free boundary for a two-dimensional optimal compliance problem[END_REF], has been devoted to regularity and other qualitative properties of islands, once they are formed. In [START_REF] Fonseca | Equilibrium configurations of epitaxially strained crystalling films: Existence and regularity results[END_REF] the authors prove that minimizing configurations are smooth outside of a finite number of cusps and cuts. Subsequently, it is proven in [START_REF] Fusco | Equilibrium configurations of epitaxially strained elastic films: Second order minimality conditions and qualitative properties of solutions[END_REF] that for small values of the amplitude of the mismatch, the flat configuration is always minimizing no matter how thick is the film. Further, they proved that for larger (but fixed) values of e 0 , there are increasing thresholds for the volume d such that the flat configuration changes from being an absolute minimizer to being only a local minimizer, and such that it is no longer a local minimizer above a certain threshold for d. Finally, they showed that even though the flat configuration is no longer minimizing, there exists another threshold below which minimizers are smooth.

Our analysis bears similarities with dimension reduction problems (see [START_REF] Anzellotti | Dimension reduction in variational problems, asymptotic development in Γ-convergence and thin structures in elasticity[END_REF][START_REF] Maso | Nonlocal character of the reduced theory of thin films with higher order perturbations[END_REF][START_REF] Friesecke | A theorem on geometric rigidity and the derivation of nonlinear plate theory from three-dimensional elasticity[END_REF][START_REF] Friesecke | A hierarchy of plate models derived from nonlinear elasticity by gamma-convergence[END_REF][START_REF] Hornung | A Γ-convergence result for thin martensitic films in linearized elasticity[END_REF][START_REF] Dret | The nonlinear membrane model as variational limit of nonlinear three-dimensional elasticity[END_REF]).

In contrast to these works, we study the behavior for small and for large volumes. Furthermore, the reference configuration is not given but is one of the unknowns. Another feature of (1) is the absence of regularizing second order terms which are often used to obtain scaling laws in elasticity (see [START_REF] Kohn | Surface energy and microstructure in coherent phase transitions[END_REF][START_REF] Conti | A lower bound for a variational model for pattern formation in shape-memory alloys[END_REF][START_REF] Bella | Wrinkles as a relaxation of compressive stresses in an annular thin film[END_REF]). Notice also that our proof of the lower bound for the scaling law in dimension two does not rely on interpolation inequalities.

Here, we deal only with the stationary setting, but we refer to [START_REF] Fonseca | Motion of elastic thin films by anisotropic surface diffusion with curvature regularization[END_REF][START_REF] Piovano | Evolution of elastic thin films with curvature regularization via minimizing movements[END_REF] for recent results on the time evolution problem. Finally, as pointed out above, it would be also interesting to investigate the model without the hypothesis that the domain of the film is a subgraph (see [START_REF] Braides | A relaxation result for energies defined on pairs set-function and applications[END_REF]). We expect to observe a qualitatively similar behavior where typical shapes of islands are not rectangles but balls.

The plan of the paper is as follows: In Section 2 we set the notation and collect some preliminary results concerning both the surface energy and the elastic energy. In Section 3 we establish the scaling law for F d,e 0 , and in Section 4 we derive and discuss reduced models in the various scaling regimes. Finally in Section 5, we present a partial extension of our results to higher dimensions.

Notation and preliminary results

Set I := [0, 1], and throughout the text denote by C and c constants that may vary from expression to expression. For Ω ⊂ R

Γ-convergence

We briefly recall the definition and some of the main properties of Γ-convergence (see [START_REF] Maso | An introduction to Γ-convergence[END_REF][START_REF] Braides | Γ-convergence for beginners[END_REF]).

Definition 2.1. Let X be a topological space. We say that a sequence of functions {F n },

F n : X → R, (sequentially) Γ-converges to F : X → R and write F n Γ -→ F if the following two conditions are satisfied. (i) If {x n } ⊂ X satisfies sup F n (x n ) < +∞ then there exists a subsequence (not relabeled) such that x n → x ∈ X and lim inf n→+∞ F n (x n ) ≥ F (x) .
(ii) For every x ∈ X there exists a sequence {x n } ⊂ X such that x n → x and

lim sup n→+∞ F n (x n ) ≤ F (x).
The main property of Γ-convergence is the following:

Theorem 2.2. Suppose that a sequence {F n } with F n : X → R Γ-converges to F and that there is some

C > 0 such that inf x∈X F n (x) ≤ C for all n ∈ N. Then inf x∈X F n (x) → inf x∈X F (x).
Moreover, if x n is a minimizer of F n then there is a subsequence of {x n } that converges to a minimizer of F .

The Surface Energy

We review some results from [START_REF] Fonseca | Equilibrium configurations of epitaxially strained crystalling films: Existence and regularity results[END_REF][START_REF] Bonnetier | Computing the equilibrium configuration of epitaxially strained crystalline films[END_REF] adapted to our setting. If h : I → [0, +∞) is lower semicontinuous, then we set

Ω h := {(x, y) : 0 ≤ x ≤ 1, 0 ≤ y < h (x)} ,

and denote the pointwise variation of h by

Var h := sup

{ n ∑ i=1 |h (x i ) -h (x i-1 )| : {x 1 , . . . , x n } is a partition of I } .
If Var h is finite then h is said to be of bounded pointwise variation (see [START_REF] Ambrosio | Functions of bounded variation and free discontinuity problems[END_REF]). If h is a function of bounded pointwise variation then we define

h -(x) := min { h ( x + ) , h ( x -)} = lim inf z→x h (z) , h + (x) := max { h ( x + ) , h ( x -)} = lim sup z→x h (z) ,
where h (x ± ) := lim z→x ± h (z). Further, let

∫ 1 0 h := Var h + h ( 0 + ) + h ( 1 -) .
We denote by Γ cuts the at most countable collection of vertical cuts,

Γ cuts := { (x, y) : x ∈ (0, 1) ∩ S (h) , h (x) ≤ y ≤ h -(x) } ,
where S (h) := {x ∈ (0, 1) :

h (x) < h -(x)}.
sup n ∫ 1 0 √ 1 + h n 2 dx + ∫ 1 0 h n dx < +∞.
Then there exists a subsequence (not relabeled) such that

(i) R 2 \Ω hn converges in the Hausdorff metric to R 2 \Ω h where h(x) := inf { lim inf n→+∞ h n (x n ) : x n → x }
is lower semicontinuous and of bounded pointwise variation;

(ii) h n → h in L 1 (I);

(iii) for every sequence

{a n } ⊂ R + with a n → 0 lim inf n→+∞ ∫ 1 0 √ a n + h n 2 dx ≥ ∫ 1 0 h + 2H 1 (Γ cuts ) .
Conversely, if h is nonnegative, lower semicontinuous and of bounded pointwise variation, then there exists a sequence {h n } of Lipschitz functions such that 0 ≤ h n ≤ h, R 2 \Ω hn converges in the Hausdorff metric to R 2 \Ω h , and

lim n→+∞ ∫ 1 0 √ a n + h n 2 dx = ∫ 1 0 h + 2H 1 (Γ cuts )
for every sequence {a n } ⊂ R + with a n → 0.

By Proposition 2.3, following the argument of [20, Theorem 2.8], we obtain the following result.

Proposition 2.4. For every nonnegative, lower semicontinuous function h of bounded pointwise variation, and for every

u ∈ W 1,p ( Ω h ; R 2 )
, there exist a sequence {h n } of nonnegative Lipschitz functions with h n (0) = h n (1) = 0 and

∫ 1 0 h n dx = ∫ 1 0 h dx such that lim n→+∞ ∫ 1 0 √ a n + h n 2 dx = ∫ 1 0 h + 2H 1 (Γ cuts )
for every sequence {a n } ⊂ R + with a n → 0, and a sequence

{u n } ⊂ W 1,p ( Ω hn ; R 2 ) which converges strongly (locally) to u in W 1,p .
Proof. By Proposition 2.3, there exists a sequence {h n } of Lipschitz functions such that h n ≤ h and

lim n→+∞ ∫ 1 0 √ a n + h n 2 dx = ∫ 1 0 h + 2H 1 (Γ cuts )
for every sequence a n → 0. Set

ε n := ∫ 1 0 (h (x) -h n (x)) dx and hn := h n + 2ε n . For a > 0 such that {y = hn (x)} ∩ {y = ax} = ∅, let (x a , ax a ) = ( x a , hn (x a )
) be the first point of the intersection between

{ y = hn (x)
} and {y = ax} (see Figure 2), i.e.,

x a := inf

{ x ∈ (0, 1) : ax = hn (x) } .
Choose a > 0 such that Ω hn ∩ {(x, y) : 0 ≤ x ≤ x a , y ≥ ax} = εn 2 . Notice that since εn 2 ≥ x a ε n (the area of the shaded region on the left of Figure 2 is larger than the area of the triangle of height 2ε n and width x a ), we have x a ≤ 1 2 . Similarly, define b > 0 and

x b ≥ 1 2 ≥ x a such that Ω hn ∩ {(x, y) : x b ≤ x ≤ 1, y ≥ b (1 -x)} = εn 2 . Then hn (x) :=      ax if 0 ≤ x ≤ x a , hn (x) if x a ≤ x ≤ x b , b (1 -x) if x b ≤ x ≤ 1,
and

u n (x) := { e 0 (x, 0) if 0 ≤ y ≤ 2ε n , u (x, y -2ε n ) if y ≥ 2ε n ,
satisfy the required properties.

Remark 2.5. The Dirichlet boundary condition is often relaxed. Precisely, instead of restricting ourselves to Lipschitz functions h with h(0) = h(1) = 0, we can equivalently consider arbitrary Lipschitz functions h if the surface energy term is replaced by

∫ 1 0 √ 1 + |h | 2 dx + h (0) + h (1) . x y 1 0 hn xa x b h n Figure 2: Construction of h n from hn (see proof of Proposition 2.4)
This kind of relaxation is very classical for functionals with linear growth (see [START_REF] Giaquinta | Functionals with linear growth in the calculus of variations[END_REF]).

Finally, we state an isoperimetric inequality which will be used throughout the paper.

Lemma 2.6. Let h : [a, b] → R be a Lipschitz function on the segment [a, b] with h (a) = h (b) = 0, and let ∫ b a h (x) dx =: d. Then ∫ b a √ 1 + |h | 2 dx ≥ 2 d b -a . ( 2
)
Proof. Let x be a point where h attains its maximum on [a, b] and set h :

= h (x). Then ∫ b a √ 1 + |h | 2 dx ≥ ∫ x a h dx + ∫ b x h dx = 2 h ≥ 2 d b -a .

The Strain Energy

In this section we collect assumptions and basic properties of the strain energy term.

Definition 2.7. A Borel measurable function

W : R 2×2 → R is quasiconvex if for every A ∈ R 2×2 and every bounded domain Ω ⊂ R 2 W (A) ≤ 1 |Ω| ∫ Ω W (A + ∇φ) dxdy for all φ ∈ W 1,∞ 0 ( Ω; R 2 ) . ( 3
)
Remark 2.8. It is well known that in the definition of quasiconvexity one can equivalently suppose that (3) holds only for the unit cube (0, 1) 2 (see [START_REF] Giusti | Direct methods in the calculus of variations[END_REF]).

We assume that the energy density W : R 2×2 → R satisfies the following hypotheses:

(H1) W ≥ 0;

(H2) W is quasiconvex;

(H3) there exist α > 0 and 1 < p < ∞ such that

α (|A| p + 1) ≥ W (A) ≥ 1 α (|A| p -1) for all A ∈ R 2×2 .
In case of geometrically linear elasticity, (H3) is replaced by the condition (H3') there exist α > 0 and 1 < p < ∞ such that

α ( A + A T p + 1 ) ≥ W (A) ≥ 1 α ( A + A T p -1 ) for all A ∈ R 2×2 .
We note that we assume (H2) only to simplify notation. Indeed, the analysis goes through exactly in the same way provided that in the results the function W is replaced by its quasiconvex envelope, i.e., the largest quasiconvex function which is below W . Hypothesis (H3) does not allow for potentials that blow-up when det y → 0 + , which corresponds to the noninterpenetration condition (see [START_REF] Belgacem | Relaxation of singular functionals defined on Sobolev spaces[END_REF] for a discussion of this issue). By (H3) and a classical result of Marcellini (see [

( Ω; R 2 ) .
We consider the recession function of W at infinity defined by

W ∞ (A) := lim sup t→+∞ W (tA) t p for A ∈ R 2×2 .
By definition, W ∞ is p-homogeneous and satisfies the growth condition α |A| p ≥ W ∞ (A) ≥ 1 α |A| p , and similarly in the case of linear elasticity. Using the quasiconvexity of W and the Fatou Lemma, we see that W ∞ is quasiconvex, and therefore also locally p-Lipschitz continuous. The recession function arises naturally in relaxation and Γ-convergence problems for functionals with linear growth (see [START_REF] Fonseca | Quasiconvex integrands and lower semicontinuity in L 1[END_REF][START_REF] Fonseca | Relaxation of quasiconvex functionals in BV(Ω, R p ) for integrands f (x, u, ∇u)[END_REF]). We will need the following additional assumption on the rate of convergence of W (tA)

t p
to W ∞ (A) (see [START_REF] Fonseca | Relaxation of quasiconvex functionals in BV(Ω, R p ) for integrands f (x, u, ∇u)[END_REF]):

(H4) There exist 0 < m < p, γ > 0 and L > 0 such that for

t |A| ≥ L, W ∞ (A) - W (tA) t p ≤ γ |A| p-m t m .
In the case of linear elasticity, this condition becomes:

(H4') There exist 0 < m < p, γ > 0 and L > 0 such that for

t A + A T ≥ L, W ∞ (A) - W (tA) t p ≤ γ A + A T p-m t m .
Remark 2.9. For p > 1 the functions W (•) := dist p (•, SO 2 ) satisfy (H4).

The main geometrical objects that will appear in the analysis are rectangles [0, ] × [0, L] for some , L > 0. We will use the following rescaling estimate.

Lemma 2.10.

If u ∈ W 1,p ( [0, ] × [0, L] ; R 2 ) , with u (x, 0) = e 0 (x, 0), then ∫ [0, ]×[0,L] W (∇u) dxdy ≥ e p 0 2 min v(x,0)=(x,0) ∫ [0,1]×[0,L/ ] W (e 0 ∇v) e p 0 dx dy, ( 4
)
where here, and in the sequel, the minimum is taken among all

v ∈ W 1,p ( [0, 1] × [0, L/ ] ; R 2 ) that satisfy the boundary condition v (x, 0) = (x, 0). Proof. For u ∈ W 1,p ( [0, ] × [0, L] ; R 2 ) set ũ (x, y) := 1 u ( x, y). Then ũ ∈ W 1,p ( [0, 1] × [0, L/ ] ; R 2 ) with ∇ũ (x, y) = ∇u ( x, y), and thus min u(x,0)=e 0 (x,0) ∫ [0, ]×[0,L] W (∇u) dx dy = 2 min ũ(x,0)=e 0 (x,0) ∫ [0,1]×[0,L/ ] W (∇ũ) dx dy = 2 min v(x,0)=(x,0) ∫ [0,1]×[0,L/ ]
W (e 0 ∇v) dx dy.

Notice that for every e 0 , the function

φ (t, e 0 ) := min v(x,0)=(x,0) ∫ [0,1]×[0,t]
W (e 0 ∇v) e p 0 dx dy is non-decreasing in t, and bounded above by some constant independent of e 0 (take any smooth function with bounded support and use (H3) or (H3')).

Remark 2.11. We recall that Korn-type inequalities or related rigidity results in the geometrically non-linear setting, degenerate if the Lipschitz constants of the domain blow-up, or if L → +∞ in strips of the form [0, ] × [0, L[ (see [START_REF] Kondrat | Boundary value problems for a system in elasticity theory in unbounded domains. Korn inequalities[END_REF][START_REF] Friesecke | A theorem on geometric rigidity and the derivation of nonlinear plate theory from three-dimensional elasticity[END_REF]).

The following lemma describes the behavior of the elastic energy for small thickness of the film. It can be seen as a special case of a dimension reduction argument (see [START_REF] Dret | The nonlinear membrane model as variational limit of nonlinear three-dimensional elasticity[END_REF][START_REF] Anzellotti | Dimension reduction in variational problems, asymptotic development in Γ-convergence and thin structures in elasticity[END_REF]).

Lemma 2.12. There holds

lim ε→0 + min v(x,0)=(x,0) 1 ε ∫ [0,1]×[0,ε] |∇v| p dx dy = 1, (5)
and similarly

lim ε→0 + min v(x,0)=(x,0) 1 ε ∫ [0,1]×[0,ε] |E(v)| p dx dy = 1, ( 6
)
where

E(v) = ∇v+∇ T v 2 .
Proof. We prove only (5) since the proof of ( 6) is very similar. The inequality

min v(x,0)=(x,0) 1 ε ∫ [0,1]×[0,ε]
|∇v| p dx dy ≤ 1 being easily obtained by taking v(x, y) = (x, 0), we are left to prove the reverse inequality.

In order to work on an ε-independent domain, we make a classical change of variables (see [15, Chapter 1, Section 1

.3]), i.e., for v = (v 1 , v 2 ) ∈ W 1,p ( [0, 1] × [0, ε] ; R 2 ) we set w (x, y) := (v 1 (x, εy) , εv 2 (x, εy)) ∈ W 1,p ( [0, 1] 2 ; R 2
) . Notice that if v (x, 0) = (x, 0), then also w (x, 0) = (x, 0). The rescaled functional to be considered then reads

J ε (w) := ∫ [0,1] 2 ( ∂w 1 ∂x 1 ε ∂w 1 ∂y 1 ε ∂w 2 ∂x 1 ε 2 ∂w 2 ∂y ) p dx dy.
If w ε is a minimizer of J ε subject to the condition w ε (x, 0) = (x, 0) then w ε W 1,p is bounded above uniformly in ε. In particular, up to a subsequence, {w ε } converges weakly in W 1,p to a function w with ∂w 1 ∂y = ∂w 2 ∂x = ∂w 2 ∂y = 0. Furthermore, w (x, 0) = (x, 0) since for p > 1 the space

W 1,p ([0, 1] 2 ; R 2 ) is compactly embedded in some L q ( [0, 1] 2 ; R 2 ) (see [1, Theorem 6.3]). Thus lim inf ε→0 + J ε (w ε ) ≥ ∫ [0,1] 2 ∂w 1 ∂x p dx dy = 1.
We next examine the scaling of the elastic energy when the thickness of the film tends to infinity.

Lemma 2.13. Let W satisfy (H2), (H3) and (H4). If

f : R + → R + is such that f (t) → +∞ for t → +∞, then lim e 0 →+∞ min v(x,0)=(x,0) ∫ [0,1]×[0,f (e 0 )] W (e 0 ∇v) e p 0 dx dy = min v(x,0)=(x,0) ∫ [0,1]×[0,+∞)
W ∞ (∇v) dx dy.

(7) Similarly, let W satisfy (H2), (H3') and (H4'). If

f : R + → R + is such that f (t) → +∞ for t → +∞, then lim e 0 →+∞ min v(x,0)=(x,0) ∫ [0,1]×[0,f (e 0 )] W (e 0 E(v)) e p 0 dx dy = min v(x,0)=(x,0) ∫ [0,1]×[0,+∞) W ∞ (E(v)) dx dy. ( 8
)
Proof. As before, we only prove ( 7) since ( 8) can be very similarly obtained. Set

G e 0 (v) := ∫ [0,1]×[0,f (e 0 )]
W (e 0 ∇v) e p 0 dx dy and

G (v) := ∫ [0,1]×[0,+∞) W ∞ (∇v) dx dy.
By Theorem 2.2, it suffices to show that G e 0 Γ -→ G with respect to the (sequential) weak topology of W 1,p loc

( [0, 1] × [0, +∞) ; R 2 )
as e 0 → +∞. Consider first {v e 0 } such that v e 0 (x, 0) = (x, 0) and sup G e 0 (v e 0 ) < +∞. Then by (H3), for every M > 0 the functions v e 0 are uniformly bounded in

W 1,p ( [0, 1] × [0, M ] ; R 2 )
, and thus there exists a subsequence converging weakly in W 1,p loc to a function v.

We now show that for M > 0 fixed lim inf

e 0 →+∞ ∫ [0,1]×[0,M ]
W (e 0 ∇v e 0 ) e p 0 dx dy ≥

∫ [0,1]×[0,M ] W ∞ (∇v) dx dy. ( 9
)
The proof of ( 9) is an adaptation of the semicontinuity proof for quasiconvex functionals (see [START_REF] Giusti | Direct methods in the calculus of variations[END_REF]Thm. 5.4]), and we sketch it only for the reader's convenience. Set

R := [0, 1] × [0, M ].
For simplicity of notation, let x := (x, y) T .

Step 1. If v is affine, i.e., v = Ax + b for some A ∈ R 2×2 and some b ∈ R 2 , and v e 0 = v on ∂R, then v e 0 = v + φ e 0 for some

φ e 0 ∈ W 1,p 0 ( R; R 2 )
, and by ( 3) and (H4), for e 0 |A| ≥ L or

A = 0 we have ∫ R W (e 0 ∇v e 0 ) e p 0 dx dy ≥ M W (e 0 A) e p 0 ≥ M ( W ∞ (A) -γ |A| p-m e m 0 ) , (10)
and ( 9) follows as e 0 → +∞ by quasiconvexity of W ∞ .

Step 2. If v is affine but v e 0 = v on ∂R, then we modify v e 0 near ∂R. Precisely, for R 0 R, K ∈ N and i = 1, . . . , K, consider the sets

R i := { x ∈ R : dist (x, R 0 ) < i K ρ }
where ρ := 1 2 dist (R 0 , ∂R), and introduce cut-off functions

ψ i ∈ C 1 0 (R i ) with 0 ≤ ψ i ≤ 1, ψ i = 1 in R i-1 ,
and

|∇ψ i | ≤ 2(K + 1) ρ . Set w i e 0 := v + ψ i (v e 0 -v). Notice that |∇w i e 0 | p ≤ C ( |∇v| p + |∇v e 0 | p + (K + 1) p ρ p |v e 0 -v| p ) . ( 11
)
Since w i e 0 = v on ∂R, by [START_REF] Braides | Γ-convergence for beginners[END_REF] we have

∫ R W ( e 0 ∇w i e 0 ) e p 0 dx dy ≥ ∫ R W ∞ (∇v) dx dy -M γ |A| p-m e m 0 . Therefore, ∫ R W ∞ (∇v) dx dy -M γ |A| p-m e m 0 ≤ ∫ R\R i W (e 0 ∇v) e p 0 dx dy + ∫ R i \R i-1 W ( e 0 ∇w i e 0 ) e p 0 dx dy + ∫ R i-1
W (e 0 ∇v e 0 ) e p 0 dx dy Since v e 0 v weakly in W 1,p (R), using (H3) and ( 11) we can bound the penultimate integral in the above inequality. Summing the inequalities over i, dividing by K and letting e 0 → +∞, we find that for some

≤ ∫ R\R 0 W ∞ (∇v) dx dy + M γ |A| p-m e m 0 + ∫ R i \R i-1 W ( e 0 ∇w i
C > 0 ∫ R 0 W ∞ (∇v) dx dy ≤ lim inf e 0 →+∞ ∫ R W (e 0 ∇v e 0 ) e p 0 dx dy + C K which for K → +∞ and R 0 → R implies (9).
Step 3. Consider then a countable family of squares Q i with pairwise disjoint interiors that cover R. We apply Step 2 in each square to the functions z i , • , where

z i := 1 |Q i | ∫ Q i ∇v dx dy, lim inf e 0 →+∞ ∫ Q i W ( e 0 ∇w i e 0 ) e p 0 dx dy ≥ ∫ Q i W ∞ (z i ) dx dy.
Let Z be the function that in every cube Q i is equal to the constant z i . If the diameters of the squares tend uniformly to zero then Z tends to Dv in L p (R) from which we get that for every ε > 0 there is a covering W ∞ (∇v) dx dy.

Q i such that ∫ R W (e 0 ∇v e 0 ) e p 0 dx dy - ∑ i ∫ Q i W ( e 0 ∇w i e 0 ) e p 0 dx dy ≤ Cε and ∫ R W ∞ (∇v) dx dy - ∑ i ∫ Q i W ∞ (z i ) ≤ Cε,
We let M → +∞ to get lim inf G e 0 (v e 0 ) ≥ G (v).

On the other hand

, if v ∈ W 1,p ( [0, 1] × [0, +∞) ; R 2 )
, then v can be approximated in energy by functions with compact support and for these functions, using the growth conditions (H3) and the reverse Fatou Lemma, we conclude that lim sup

e 0 →+∞ G e 0 (v) ≤ G (v) . Define C W := min v(x,0)=(x,0) ∫ [0,1]×[0,+∞) W ∞ (∇v) dx dy. ( 12
)
Remark 2.14.

If W (•) = |•| 2
, one obtains by Fourier methods that (see [START_REF] Conti | A lower bound for a variational model for pattern formation in shape-memory alloys[END_REF]Appendix])

C W = 1 π 3 ∑ k>0 1 k 3 (1 + (-1) k+1 ) 2 .

Scaling law

In this section we consider the qualitative behavior of the minimal energy in terms of its scaling regimes. } .

Proof. We give the proof only for the nonlinear elasticity since the geometrically linear case can be treated analogously.

Upper bound.

For ≤ 1 and 0 < δ 2 set h := 2d 2 -δ , and consider (see Figure 3(a))

h (x) :=            2 h δ x if 0 ≤ x ≤ δ 2 , h if δ 2 ≤ x ≤ -δ 2 , -2 h δ x + 2 h δ if -δ 2 ≤ x ≤ , 0 if ≤ x ≤ 1.
Let u be the restriction to Ω h of ũ :

I × [0, ∞) → R given by ũ (x, y) = { (e 0 x ( 1 -1 y ) , 0) if 0 ≤ y ≤ , 0 else. 0 δ/2 -δ/2 h (a) Upper bound construction y 0 a 1 b 1 a 2 b 2 1 2

1

(b) Geometry for the lower bound Then

F d,e 0 (u, h) ≤ ∫ Ω h W (∇u) dx dy + 1 + 4d 2 -δ ≤ Ce p 0 ∫ 0 ∫ 0 ( (1 - 1 y) p + ( 1 x) p ) dx dy + αd + 1 + 4d 2 -δ ≤ C
i := |Ω h ∩ ([a i , b i ] × [y 0 , +∞))|. Then ∑ +∞ i=1 i = and ∑ +∞ i=1 d i ≥ d -y 0 ≥ Cd. If i ≤ ( d e p 0 ) 1/3
for all i ∈ N, then by (2) applied to h -y 0 we obtain

F d,e 0 (u, h) ≥ +∞ ∑ i=1 ∫ b i a i √ 1 + |h | 2 dx ≥ +∞ ∑ i=1 d i i ≥ ( e p 0 d ) 1/3 +∞ ∑ i=1 d i ≥ Ce p/3 0 d 2/3 .
Otherwise, the largest connected component of I , say

I 1 , satisfies 1 ≥ ( d e p 0 ) 1/3
. By Lemma 2.12 there exists a small constant ε 0 < 1 such that for ε ≤ ε 0 , min u(x,0)=(x,0)

1 ε ∫ [0,1]×[0,ε] |∇u| p dx dy ≥ 1 2 .
Since ε 0 > 0 is a universal constant, and since e p/3 0 d 2/3 ≥ C max {1, d}, we may, without loss of generality, by changing C, assume that e 4) and (H3),

p/2 0 ≥ 4 ε 0 . If ( d e p 0 ) 1/3 ≤ 1 ≤ y 0 ε 0 , then, by (
F d,e 0 (u, h) ≥ ∫ [a 1 ,b 1 ]×[0,y 0 ] W (∇u) dx dy ≥ 1 α ( d e p 0 ) 2/3 e p 0 min v(x,0)=(x,0) ∫ [0,1]×[0,ε 0 ] |∇v| p dx dy - 1 α 1 y 0 ≥ ε 0 2α e p/3 0 d 2/3 - 1 α y 0 ≥ ε 0 2α e p/3 0 d 2/3 - 1 α d √ e p/3 0 d 2/3 ≥ ε 0 4α e p/3 0 d 2/3 ,
where we used that

d √ e p/3 0 d 2/3 ≤ ε 0 4 e p/3 0 d 2/3 , since e p/2 0 ≥ 4 ε 0 .
Otherwise, if 1 ≥ y 0 /ε 0 , then, by ( 4), (H3), ( 5), and since

1 y 0 = d (e p/3 0 d 2/3 ) 1/2 1 ≤ e p/3 0 d 2/3 , F d,e 0 (u, h) ≥ 1 α 2 1 e p 0 min v(x,0)=(x,0) ∫ [0,1]×[0,y 0 / 1 ] |∇v| p dx dy - 1 α 1 y 0 ≥ 1 2α 2 1 e p 0 y 0 1 - 1 α e p/3 0 d 2/3 ≥ 1 2ε 0 α (e p/3 0 d 2/3 ) 2 - 1 α e p/3 0 d 2/3 ≥ ce p/3 0 d 2/3 ,
where the last inequality holds since e p/3

0 d 2/3 > C for C large enough.

Reduced models

To study the asymptotic behavior of F d,e 0 in the various regimes determined in Theorem 3.1, we set h := h/d, Ω h := {(x, y) : (x, d y) ∈ Ω h }, and u (x, y) = u (x, d y). Dropping the tildes, the energy now reads

F d,e 0 (u, h) = d [ ∫ Ω h W ( ∂u ∂x , 1 d ∂u ∂y ) dx dy + ∫ 1 0 √ 1 d 2 + |h | 2 dx ] for (u, h) such that h(0) = h(1) = 0, ∫ 1 0 h dx = 1, and u ∈ W 1,p (Ω h ) with u (x, 0) = e 0 (x, 0).
In the regime in which F d,e 0 1, the limiting functional is constant (see Proposition 4.1), while for F d,e 0 d, the main contribution to the reduced energy comes from the surface part (see Proposition 4.2), and the flat configuration is optimal. Notice, however, that as proven in [START_REF] Fusco | Equilibrium configurations of epitaxially strained elastic films: Second order minimality conditions and qualitative properties of solutions[END_REF], for large but finite mismatch e 0 > 0 and for volume d large enough, the flat configuration is never a global minimizer of the energy. We believe that this is a higher order effect that cannot be captured by our first order analysis. In the transition regime, in which d e p 0 → +∞, elastic and surface energy compete (see Proposition 4.3), and the minimizer of the reduced model is either the flat configuration or an island, depending on the elastic properties of the material, in particular on the constant C W in [START_REF] Chambolle | C ∞ regularity of the free boundary for a two-dimensional optimal compliance problem[END_REF]. Finally, in the regime in which F d,e 0 e p/3 0 d 2/3 , the elastic energy dominates. By a corresponding compactness result (see Proposition 4.7), we conclude that in this regime the formation of islands is energetically favored. )

The trivial regime

, then F d,e 0 1, and the limit functional is a constant. In this regime, the non-horizontal parts of the surface and the elastic part of the energy do not contribute significantly. Given an absolutely continuous probability measure µ := h dx, let

h i := d i i .
We finally let h d,e 0 be a Lipschitz approximation of

∑ N i=1 h i χ [c i -i 2 ,c i + i 2 ]
and u d,e 0 be the minimizer of the elastic energy in Ω h d,e 0 so that

F d,e 0 (u d,e 0 , h d,e 0 ) ≤ 1 + 2 N ∑ i=1 dd i i + C N ∑ i=1 e p 0 2 i ≤ 1 + Ce p/3 0 d 2/3
from which the upper bound follows. If d ≥ Ce p 0 , we then replace in the previous construction i by i := d 1/2 from which we similarly obtain

F d,e 0 (u d,e 0 , h d,e 0 ) ≤ 1 + 2 N ∑ i=1 dd i i + C N ∑ i=1 e p 0 2 i ≤ 1 + 2d 1/2 + Ce p 0 d 2 .
F d (u, h) := ∫ Ω h W ( ∂u ∂x , 1 d ∂u ∂y ) dx dy + ∫ 1 0 √ 1 d 2 + |h | 2 dx.
In this regime, the surface energy dominates, and the limit functional turns out to be

F (h) := ∫ 1 0 h + 2H
F d (u d , h d ) ≥ F (h) .
Further, for every nonnegative lower semicontinuous function h with bounded pointwise variation and

∫ 1 0 h (x) dx = 1, there exists a sequence {(u d , h d )} such that h d : I → R are non-negative Lipschitz functions with ∫ 1 0 h d (x) dx = 1, h d (0) = h d (1) = 0, and u d ∈ W 1,p ( Ω h d ; R 2 ) , R 2 \Ω h d converge to R 2 \Ω h , and
lim sup d→+∞ F d (u d , h d ) ≤ F (h) .
Proof. The compactness and the liminf inequality follow from Proposition 2.3. For the limsup inequality, we may assume that h is Lipschitz continuous with h(0) = h(1) = 0 (see Proposition 2.4). Choose h d := h and

u d (x, y) := { e 0 (x (1 -d y) , 0) if y ≤ 1 d , 0 if y ≥ 1 d .
Then by (H3), ∫

Ω h W ( ∂u d ∂x , 1 d ∂u d ∂y ) dx dy ≤ ∫ 1 0 ∫ 1/d 0 α (e p 0 |(1 -d y, -x)| p + 1) dy dx ≤ α ( e p 0 d ∫ 1 0 ∫ 1 0 |(1 -y, x)| p dx dy + 1 d ) ,
and thus lim sup d→+∞

∫ Ω h W ( ∂u d ∂x , 1 d ∂u d ∂y
) dx dy = 0.

The borderline case d e p

0 We now focus on the limit case d e p 0 → +∞. In this regime, elastic and surface energy compete and interplay in the limit. Rescaling the energy by d, we obtain

F d (u, h) := ∫ Ω h W ( ∂u ∂x , 1 d ∂u ∂y ) dx dy + ∫ 1 0 √ 1 d 2 + |h | 2 dx.
We first give a compactness and lower-bound result.

Proposition 4.3. Suppose that W satisfies (H1)-(H4). If sup F d (u d , h d ) < +∞ then there is a subsequence with the following properties: { R 2 \Ω h d } converges in the Hausdorff topology to R 2 \Ω h , where h (x) := inf {lim inf h d (x d ) : x d → x}.

Denote the boundary layers by

BL h := { (x, y) : (x, y) ∈ [0, 1] × R + , 0 < h (x) } and BL d h := {(x, y) : (x, y) ∈ BL h , y ≤ d h d (x)} . Then { BL d h } converges in the local Hausdorff topology to BL h . Moreover, if v d : BL d h → R 2 is defined by v d (x, y) := 1 e 0 u d ( x, y d ) , then there exists v ∈ W 1,p ( BL h ; R 2 ) with v (x, 0) = (x, 0), v d χ BL d h v locally weakly in W 1,p loc ( BL h ; R 2 )
, and

lim inf d→+∞ F d (u d , h d ) ≥ ∫ BL h W ∞ (∇v) dx dy + ∫ 1 0 h + 2H 1 (Γ cuts ) . Proof. Since |Ω h d | = 1 and { ∫ 1 0 √ 1 d 2 + h d 2 dx
} is uniformly bounded, the compactness and lower-semicontinuity for the surface part follow from Proposition 2.3, and the convergence of

{ BL d h } follows from the Hausdorff convergence of R 2 \Ω h d .
We now focus on the elastic energy. Changing variables z = d y and dividing by e 0 , we get

∫ BL d h W (e 0 ∇v d ) e p 0 dx dy ≤ C
which, by the p-growth condition (H3), implies that ∇v d L p (BL d h ∩{y≤M }) is bounded for every M . Hence, as in Lemma 2.12, v d L p (BL d h ∩{y≤M }) is also bounded, and so there exists a subsequence that converges locally to v ∈ W 1,p loc (BL h ) with v (x, 0) = (x, 0). The liminf inequality follows from the weak convergence, as in Lemma 2.13.

We are now in position to prove the limsup inequality:

Proposition 4.4. Suppose W satisfies (H1)-(H4). For every pair (v, h) with v ∈ W 1,p loc ( BL h ; R 2 )
, v (x, 0) = (x, 0), and h : I → R a nonnegative lower semicontinuous function of bounded pointwise variation with

∫ 1 0 h (x) dx = 1, there exists a sequence {u d } ⊂ W 1,p loc ( Ω h ; R 2 ) with u d (x, 0) = e 0 (x, 0), such that 1 e 0 u d ( x, y d ) v locally weakly in W 1,p loc ( BL h ; R 2 ) and lim d→+∞ F d (u d , h) = ∫ BL h W ∞ (∇v) dx dy + ∫ 1 0 h + 2H
F d (u d , h) = ∫ BL h W ∞ (∇v) dx dy + ∫ 1 0 h .
We now characterize the minimizers of the limiting functional.

Proposition 4.5. Assume that W satisfies (H1)-(H4), and let C W be as in [START_REF] Chambolle | C ∞ regularity of the free boundary for a two-dimensional optimal compliance problem[END_REF].

If C W ≥ 1, then the minimum of ∫ BL h W ∞ (∇v) dx dy + ∫ 1 0 h + 2H 1 (Γ cuts ) is attained for h = 1 min χ [0, min ] with min = ( 1 C W ) 1/3
, and v the minimizer of the elastic energy in the corresponding boundary layer BL h . If C W < 1, then the flat configuration is minimizing.

Proof. Note first that h is constant on each connected component of {h = 0}. Indeed, given an interval [a, b] and a volume d, the rectangle is the shape with least vertical perimeter (i.e., minimal ∫ b a |h |) for a given volume d. In the boundary layer, v has to be chosen to be the minimizer of the elastic energy.

If h = ∑ h i χ [a i ,b i ] , then set i := b i -a i .
The minimal energy is given by min

∑ i h i i =1 C W 2 ∑ i 2 i + ∑ i h i .

20

Assume, for the sake of contradiction, that two of the i are non-zero, say

1 ≥ 2 > 0. For η ∈ [ -h 1 , 2 1 h 2 ] consider h 1 + η and h 2 -η 1 2 . Since ( i , h i ) is minimizing and (h 1 + η) 1 + ( h 2 -η 1 2 ) 2 = h 1 1 + h 2 2 , we find that η -η 1 2 ≥ 0 for all η ∈ [ -h 1 , 2 1 h 2 ] ,
and hence 1 = 2 , from which we deduce that i = for every i. The minimization problem then reduces to min

≤1 C W 2 N 2 + 1 ,
where N is the number of intervals where h = 0. The minimum is attained for N = 1 and

min = min { 1,
(

1 C W ) 1/3 } . Remark 4.6. If W ∞ (A) = |A| 2 , then C W ≤ min u(x,0)=(x,0) ∫ 1 0 ∫ +∞ 0 |∇u| 2 dy dx ≤ ∫ 1 0 ∫ 1 0 (1 -y) 2 + x 2 dx dy = 2 3 < 1,
where where the second inequality follows by choosing u (x, y) := (x (1 -y) χ y≤1 , 0). In particular, min = 1, and the flat configuration is optimal. We now turn to the case in which e 0 → +∞,

F η (u, h) := η [ ∫ Ω h W ( ∂u ∂x , 1 d ∂u ∂y ) dx dy + ∫ 1 0 √ 1 d 2 + |h | 2 dx ] .
We first give a compactness and a liminf inequality result.

lim inf η→0 F η (u η , h η ) ≥ 3C 1/3 W +∞ ∑ i=1 d 2/3 i .
Proof. Since µ η is a probability measure for every η, there exists a subsequence (not relabeled) and a probability measure µ such that µ η weakly- * converges to µ. We use the notation from the proof of Theorem 3.1 (see Figure 3 , and :=

H 1 ( Ω hη ∩ (I × {y 0 }) ) . Let I η := Ω hη ∩ (I × {y 0 }), I η = ∪ +∞ i=1 [a η i , b η i ], be the decomposition into connected components, η i := b η i -a η i , d η i := Ω hη ∩ ([a η i , b η i ] × [y 0 , +∞)) ,
i ∈ [0, 1], a η i → c i and b η i → c i . Let Ω η i := Ω hη ∩ ([a η i , b η i ] × [0, +∞)) and F η (u η , h η , Ω η i ) := η ∫ b η i a η i √ 1 d 2 + h η 2 dx + η ∫ Ω η i W ( ∂u η ∂x , 1 d ∂u η ∂y ) dx dy.
Then for every i (see ( 2))

F η (u η , h η , Ω η i ) ≥ η ∫ b η i a η i h η dx + η ∫ [a η i ,b η i ]×[0,y0] W ( ∂u η ∂x , 1 d ∂u η ∂y ) dx dy ≥ 2η d η i η i + η d min u(x,0)=e 0 (x,0) ∫ [a η i ,b η i ]×[0,dy0] W (∇u) dx dy ≥ 2η d η i η i + η d e p 0 ( η i ) 2 min v(x,0)=(x,0) ∫ [0,1]× [ 0, dy 0 η i ] W (e 0 ∇v) e p 0 dx dy ≥ 2η d η i η i + η d e p 0 ( η i ) 2 min v(x,0)=(x,0) ∫ [0,1]× [ 0, √ e p/3 0 d 2/3 ] W (e 0 ∇v) e p 0 dx dy = 2η d η i η i + η d e p 0 ( η i ) 2 C W (1 -ψ (η)) ≥ 3C 1/3 W (1 -ψ (η)) 1/3 (d η i ) 2/3 ,
where ψ (η) → 0 as η → 0. Summing over i and letting η → 0, we obtain the liminf inequality. Now, for every ε > 0, let

V ε := {i ∈ N : d η i < ε}. Then ∑ i∈V ε d η i = ∑ i∈V ε (d η i ) 1/3 (d η i ) 2/3 ≤ ε 1/3 ∑ i∈V ε (d η i ) 2/3 ≤ Cε 1/3 ∑ i∈V ε F η (u η , h η , Ω η i ) ≤ Cε 1/3 F η (u η , h η ) ≤ Cε 1/3 .
The number of islands with d η i > ε is uniformly bounded by some constant

N ε ≤ 1 ε . For fixed ε > 0 let I ε := ( ∪ i∈V ε [a η i , b η i ] ) c and µ ε η := h η χ I ε dx. Then { µ ε η } converges weakly- * to µ ε := ∑ Nε i=1 d i δ c i . Finally µ ε → µ since for every φ ∈ C (I) |(µ ε -µ) (φ)| = lim η→0 ∫ I ε h η φ dx ≤ C φ ∞ ε 1/3 .
Since µ ε weakly- * converges ∑ i∈N d i δ c i , this ends the proof.

Remark 4.8. In contrast to [START_REF] Choksi | Small volume fraction limit of the diblock copolymer problem: I. Sharp-interface functional[END_REF], the structure of the limiting measure seems not to follow directly from the Second Concentration-Compactness Lemma by P.L. Lions (see [START_REF] Lions | The concentration-compactness principle in the calculus of variations. The limit case[END_REF]), but rather from the scaling of the energy.

We finally prove the corresponding limsup inequality.

Proposition 4.9.

If µ := ∑ +∞ i=1 d i δ c i then there exist a sequence {(u η , h η )} of functions u η ∈ W 1,p ( Ω hη ; R 2 )
, and nonnegative Lipschitz functions h η such that µ η := h η dx are probability measures that weakly- * converge to µ, and

lim sup η→0 F η (u η , h η ) ≤ 3C 1/3 W +∞ ∑ i=1 d 2/3 i .
Proof. Every measure µ = ∑ +∞ i=1 d i δ c i can be approximated in energy by the measures µ N := ∑ N i=1 d i δ c i , and by slightly moving the points c i , we may assume that c i / ∈ {0, 1}. For such measures, we construct a recovery sequence as follows: Set i :=

( d i C W ) 1/3 η, h i := d i i , and let h η a Lipschitz function close to ∑ N i=1 h i χ (c i -i /2,c i + i /2)
. Finally, choose u η to be the minimizer of the elastic energy in Ω hη .

Note that the minimizer of the limit functional, min

{ +∞ ∑ i=1 d 2/3 i : +∞ ∑ i=1 d i = 1 } ,
is given by a single Dirac mass, i.e., d 1 = 1 and d i = 0 for i > 1.

Remark 4.10. (i) The limiting energy charges only Dirac masses. This can be interpreted as a confirmation of the formation of islands in case that the amplitude of the mismatch is large compared to the thickness of the film.

(ii) The limit functional is not defined on a function space, but on a space of measures. The idea to consider limits in such a way has been used, e.g., in the study of the Ohta-Kawasaki model (see [START_REF] Choksi | Small volume fraction limit of the diblock copolymer problem: I. Sharp-interface functional[END_REF][START_REF] Goldman | The Γ-Limit of the Two-Dimensional Ohta-Kawasaki Energy. I. Droplet Density[END_REF]), in the study of vortices in Ginzburg-Landau model (see [START_REF] Jerrard | The Jacobian and the Ginzburg-Landau energy[END_REF][START_REF] Sandier | Vortices in the magnetic Ginzburg-Landau model[END_REF]), and is also behind the idea of the blow-up method of Fonseca and Müller (see [START_REF] Fonseca | Relaxation of quasiconvex functionals in BV(Ω, R p ) for integrands f (x, u, ∇u)[END_REF]).

Scaling law in dimension three for the Dirichlet energy

In this section, we show that in higher dimension, a scaling law similar to the one of Theorem 3.1 holds. Let D = D(0, 1) ⊂ R 2 be the unit disk (but it could be replaced by any smooth bounded domain) and consider } .

Proof. The upper bound is very similar to the two dimensional case, replacing rectangles by cylinders.

For the lower bound, we proceed along the lines of the proof of Theorem 3.1. We assume that e )

, ( 13
)
where λ 1 (Ω) is the Cheeger constant of Ω defined as (see for instance [START_REF] Alter | Uniqueness of the Cheeger set of a convex body[END_REF]) Let us notice that by reducing Ω we can assume that λ 1 (Ω) = P (Ω) |Ω| i.e., that Ω is calibrable (see for example [START_REF] Alter | Uniqueness of the Cheeger set of a convex body[END_REF]) since it would only lower the energy. Notice that Ω is then a connected set. We then consider the minimizer u of this problem which satisfies,      -∆u = 0 in Ω × (0, 1) u(x, 0) = (x, 0)

λ
in Ω ∂u ∂ν = 0 in ∂Ω × (0, 1) ∪ Ω × {1}.

Let µ 2 k be the increasing eigenvalues of the Laplacian in Ω with Neumann boundary conditions (so that µ 1 = 0) and let φ k be the associated eigenfunctions (normalized so that ∫ Ω φ 2 k = 1). We can then decompose u with respect to the basis φ k , i. We then get that (using that

∫ Ω |∇φ k | 2 dx = µ 2 k ) ∫ Ω×[0,1] |∇u| 2 dx dy = ∑ k≥1 ∫ 1 0 |u k (y)| 2 + µ 2 k |u k (y)| 2 dy = ∑ k≥2 1 -exp(-2µ k ) 1 + exp(-2µ k ) µ k |u k | 2 . ( 14
)
By Cheeger's inequality (see [START_REF] Ledoux | A simple analytic proof of an inequality by P. Buser[END_REF]), for k ≥ 2

µ k ≥ µ 2 ≥ 1 4 λ 1 (Ω)
and since Ω ⊂ D, we also have λ 1 (Ω) ≥ λ 1 (D) and thus

∫ Ω×[0,1]
|∇u| 2 dx dy ≥ 1 -exp(-λ 1 (D) 2 ) 1 + exp(-λ 1 (D)

2 )

λ 1 (Ω) 4 ∑ k≥2 |u k | 2 .
By Plancherel formula, there holds For that, we employ the interpolation inequality (recall that λ 1 (Ω) = P (Ω) |Ω| ) P (Ω) 4/5 (∫ Ω×Ω |x -z| 2 dx dz

∑ k≥2 |u k | 2 = ∫ Ω |x| 2 dx - 1 |Ω| n ∑ i=1 (∫ Ω x i dx ) 2 . Since ∫ Ω |x| 2 dx - 1 |Ω| n ∑ i=1 (∫ Ω x i dx
) 1/5 ≥ C|Ω|, ( 15
)
which corresponds to [34, (5.3)] with α = -2, since their proof carries over verbatim to this choice. Finally, dividing (15) by |Ω|, raising it to the power 5/4, and multiplying it by e

|∇u| 2 dx dy |(x, 0)| 2 H 1/2 (Ω) = ∑ i ∫ Ω i ×Ω i 1 |x -z| dx dz,
where the sets Ω i are the connected components of Ω. Hence (at least formally), the right handside of (13) looks very similar to the Ohta-Kawasaki functional which has received a lot of attention in the last few years (see [START_REF] Knüpfer | On an isoperimetric problem with a competing nonlocal term I: The planar case[END_REF][START_REF] Cicalese | Droplet minimizers of an isoperimetric problem with long-range interactions[END_REF][START_REF] Choksi | Small volume fraction limit of the diblock copolymer problem: I. Sharp-interface functional[END_REF][START_REF] Goldman | The Γ-Limit of the Two-Dimensional Ohta-Kawasaki Energy. I. Droplet Density[END_REF][START_REF] Alberti | Uniform energy distribution for an isoperimetric problem with long-range interactions[END_REF]).

(ii) The proof of Theorem 5.1 can be extended similarly to any space dimension.

(iii) In order to remove the condition d ≥ 2π, we would need the reverse of Cheeger's inequality. Unfortunately, it is known that Buser's inequality does not hold for problems with Neumann boundary conditions (see [START_REF] Ledoux | A simple analytic proof of an inequality by P. Buser[END_REF]).

0 d 2/ 3 } 1 ,

 31 ≤ inf F d,e 0 ≤ C 2 max {

and ( 9 )

 9 follows. In conclusion, for every M > 0, lim inf e 0 →+∞ G e 0 (v e 0 ) ≥ lim inf e 0 →+∞ ∫ [0,1]×[0,M ] W (e 0 ∇v e 0 ) e p 0 dx dy ≥ ∫ [0,1]×[0,M ]

Theorem 3 . 1 .0 d 2/ 3 } 1 ,

 3131 Suppose that W satisfies (H1) and (H3), or (H1) and (H3'). Then there are constants C 1 , C 2 > 0 such that, for all d, e 0 > 0, ≤ inf F d,e 0 ≤ C 2 max {

Figure 3 :

 3 Figure 3: Constructions in the proof of Theorem 3.1

3 0 d 2 /3 if e p/ 3 0 d 2 / 3 ≥√ e p/ 3 0 d 2/ 3 , := H 1 (

 32323331 If e p 0 ≤ d, then we choose := 1, and if e p 0 ≥ d we choose := d 1/3 e the proof the of the upper bound. Lower bound: By definition of the surface energy, F d,e 0 (u, h) ≥ 1, and by Lemma 2.6 F d,e 0 (u, h) ≥ 2d. It remains to show that F d,e 0 (u, h) ≥ Ce p/C max {1, d} for some fixed constant C > 0. Let y 0 := d Ω h ∩ (I × {y 0 })) and I := Ω h ∩ (I × {y 0 }). Denote by [a i , b i ] the countably many (pairwise disjoint) maximal connected components of I (see Figure 3(b)), i.e., I = ∪ +∞ i=1 [a i , b i ], and for i ∈ N, set i := b i -a i and d

F d,e 0 1 If d → 0 and e p 0 = o ( 1 d 2

 112

GProposition 4 . 1 . 1 d 2 )

 4112 d,e 0 (µ) := min u(x,0)=e 0 (x,0) F d,e 0 (u, h). Suppose that W satisfies (H1) and (H3), d → 0 and e p 0 = o ( , then {G d,e 0 } Γ-converges with respect to the weak- * convergence of measures to the constant functional equal to 1 on probability measures.Proof. The compactness follows from the weak- * compactness of sequences of probability measures on compact sets. Since the energy is always bounded from below by 1, the lower bound is immediate. For the upper bound, by density of finite sums of Dirac masses in the set of probability measures, it is enough to assume that µ = ∑ N i=1 d i δ c i , and we can further assume that for every i = 1, .., N , c i / ∈ {0; 1}. If d

4. 2

 2 The surface dominant regime F d,e 0 d If d → +∞ and e p 0 = o (d), then F d,e 0 d. Hence, we rescale the energy by d, and consider

4. 4 3 0 d 2/ 3

 433 The elastic dominant regime F d,e 0 e p/

e p 0 d → +∞ and e p 0 d 2 →

 02 +∞. Note that this allows also for d → 0. In this regime, the main contribution to the energy comes from the elastic part. Define η := ( so that F d,e 0 d η . We thus rescale the energy F d,e 0 (u, h) by d η , and consider

  (b)), i.e., y 0 :=

F 1 +Proposition 5 . 1 . 2 0 d 3/ 4 } 1 ,

 151241 d,e 0 (u, h) |∇h|2 dx,whereΩ h := {(x, y) : x ∈ D, 0 ≤ y ≤ h(x) }, u(x, 0) = e 0 (x, 0) for all x ∈ D, and ∫ D h dx = d. Let d ≥ 2π. There exist constants C 1 , C 2 > 0 such that C 1 max { 1, d, e 1/≤ inf F d,e 0 ≤ C 2 max {

1 / 2 0 d 3 / 4 ≥F|∇u| 2

 12342 C max{1, d}. Let Ω := {x ∈ D : h(x) > 1}. Then |Ω h ∩ {y ≥ 1}| ≥ d -π and thus dx dy + d λ 1 (Ω)

h

  = d and h = 0 on ∂Ω } , where P (E) denotes the perimeter of the set E. For a fixed domain Ω ⊂ D, we want to estimate from below min u(x,0)=(x,0) ∫ Ω×[0,1]|∇u| 2 dx dy.

  e., u(x, y) = ∑ k≥1 u k (y)φ k (x)where u k is a vector valued function. From the equation we getu k -µ 2 k u k = 0 u k (0) = u k u k (1) = 0where u k = ∫ Ω u(x, 0)φ k dx and thus u k (y) = α exp(µ k y) + β exp(-µ k y) so that we findu k (y) = exp(-2µ k ) 1 + exp(-2µ k ) u k exp(µ k y) + 1 1 + exp(-2µ k ) u k exp(-µ k y)

z| 2

 2 dx dz + dλ 1 (Ω) ≥ Ce

1 / 2 0 d 3 / 4 ,Remark 5 . 2 .

 123452 yields the desired lower bound. (i) Notice that min u(x,0)=(x,0) ∫ Ω×[0,1]

  1 (Γ cuts ).Proof. We may assume that h is Lipschitz continuous (see Proposition 2.4), and that v has bounded support. Define the recovery sequence by u d (x, y) := e o v(x, dy). Then 1 e 0 u d

	v locally weakly in W 1,p loc	(	BL h ; R 2 )	and	(	x, y d	)
	lim d→+∞

  Proposition 4.7. Let {(u η , h η )} be such that sup F η (u η , h η ) ≤ C, and set µ η := h η dx. Then there exists a subsequence (not relabeled) such that {µ η } weakly- * converges to µ :=

	where d i > 0 satisfy	∑ +∞ i=1 d i = 1. Moreover, there holds	∑ +∞ i=1 d i δ c i

  and assume that the d η i are in descending order. The latter can be assumed since d i → 0 as i → +∞. Indeed, otherwise, for every n > 0 there would exist η n → 0 such that 1 ≥ nη n , and hence inf F d,e 0 ≥ Cne

	Note that 1 -	∑	i d η i ≤ y 0 , and thus lim η→0	∑ i d η i = 1. Let finally d i := lim η→0 d η i (which
	we can assume exists for every i ∈ N up to further extraction of a subsequence). Since
	F d,e 0	e	p/3 0 d 2/3 , by Theorem 3.1, we deduce that max i	η i ≤ Cη and thus (b η i -a η i ) → 0 for
	all i. p/3 0 d 2/3 which contradicts the upper bound. Therefore, we may assume
	that for some c

Acknowledgments

Both authors thank I. Fonseca and G. Leoni for bringing this problem to their attention, for helpful discussions and for their constant support. They thank G. De Philippis and H. Knüpfer for interesting discussions concerning the last part of the paper, and warmly thank the Center for Nonlinear Analysis (NSF Grant No. DMS-0635983), where this research was carried out. The second author was partly funded by a postdoctoral fellowship of the National Science Foundation under Grant No. DMS-0905778. The final stages of this work were carried out while the first author was funded by a Von Humboldt postdoctoral fellowship.


Alban Rasse
email: alban.rasse@uha.fr

Jean-Marc Perronne
email: jean-marc.perronne@uha.fr

Pierre-Alain Muller
email: pierre-alain.muller@irisa.fr

Bernard Thirion
email: bernard.thirion@uha.fr

Using Process Algebra to Validate Behavioral Aspects of Object-Oriented Models

We present in this paper a rigorous and automated based approach for the behavioral validation of control software systems. This approach relies on metamodeling, model-transformations and process algebra and combines semi-formal object-oriented models with formal validation. We perform the validation of behavioral aspects of objectoriented models by using a projection into a well-defined formal technical space (Finite State Process algebra) where model-checkers are available (we use LTSA; a model checker for Labeled Transition Systems). We then target an implementation platform, which conforms to the semantics of the formal technical space; in turn, this ensure conformance of the final application to the validated specification.

Inroduction

The increasing complexity of control software systems makes their comprehension and their construction more and more difficult [START_REF] Sanz | Software for Complex Controllers In: Control Of Complex Systems[END_REF]. The approach proposed in this paper (figure 1) simplifies the reliable design of these software systems through a complete software development cycle (from the specification to the code) in a coherent and automated way. It is based on existing techniques, from different fields of software engineering, and integrates:

a specification phase based on object-oriented decomposition.

a validation phase based on formal methods and model-checking tools, so as to provide software designers with checking techniques that improve their design quality.

an implementation phase to ensure the coherence of the generated code according to both the validation and specification phases. a model-based software engineering process in accordance with Model-Driven Engineering (MDE) [START_REF] Bézivin | In search of a Basic Principle for Model-Driven Engineering[END_REF], which allows -through a metamodel architecture -the integration of the specification, the validation and the implementation phases into a coherent software development cycle. Moreover, model transformation -a key concept in MDE -helps to go from one modeling field to another, which, in turn, helps to obtain automatically, from a source model, models that are adapted to a particular technical space. These transformations make the software designer's tasks easier by hiding, as far as possible, the complexity of formal tools which often require an important learning effort.

As the whole approach cannot be described in this paper, only the specification and validation phases, with the associated transformations, will be considered here (dark gray in figure 1).

Figure 1. Projection of the behavioral aspects into a process algebra technical space

The approach is based on a specification model which represents an abstraction of the control software. This model is specified using classes, objects and Finite State Machines (FSM) so as to describe the different aspects (structure, behavior, and configuration) of the system under study. FSMs have been chosen as this formalism is based on known semantics [START_REF] Magee | Concurrency. State Models & Java Programs[END_REF] which can be interpreted in terms of Labeled Transition System (LTS) [START_REF] Arnold | Finite Transition System[END_REF]. The precisely defined semantics is necessary -on one hand -to allow the easier use of model transformation techniques and -on other hand -to ensure the coherence of the approach, since the behavioral aspects of the proposed models (specification, validation and implementation) are also based on semantics that can be described in term of LTS. The FSMs are translated into a process algebra [START_REF] Bergstra | Handbook of Process Algebra[END_REF] called Finite State Processes (FSP) [START_REF] Magee | Concurrency. State Models & Java Programs[END_REF]. This leads to a validation model which can be analyzed with the Labeled Transition System Analyzer (LTSA) model checking tool [START_REF] Magee | Concurrency. State Models & Java Programs[END_REF].

This paper is divided into four parts. The first part presents the running example which will be used to illustrate the proposed approach. The second and third sections describe an overview of the specification model and the validation model respectively. Finally, the

Running Example

The system used to illustrate the present approach is a control software whose role is to manage the locomotion function of an hexapod robot [START_REF] Thirion | Concurrent programming for the Control of Hexapode Walking[END_REF] (figure 2 To ensure flexible and robust locomotion, this system must satisfy a set of liveness and safety properties. As an example, one of these liveness properties says that all the legs must always execute their walking cycle, whatever the possible execution trace of the system. and in accordance with the safety properties, one leg can only be raised if its two neighbors remain on the ground (static stability). The control software of this robot is a typical example of the software systems which must be validated to avoid severe dysfunctions at runtime.

Specification Model

The specification model, based on object-oriented models, represents an abstraction of the control software and includes three complementary aspects which represent, respectively, its structure, its behavior and its configuration.

Specification of the structural aspects

To describe the different types of entities present in control systems, we specify the structural aspects in the form of two conceptual levels [START_REF] Perronne | A Modeling Framework for Complex Behavior Modeling and Integration[END_REF]. The first level models the passive objects which must be controlled, while the second level corresponds to behavioral objects (active entities) whose role is to control passive objects in their state space (figure 3.a). This explicit representation of behaviors allows these to be considered as full objects and so, to be manipulated and organized within an object-oriented architecture. Moreover, the systematic separation of passive objects from behavioral objects helps to abstract and isolate them and thus to simplify their specification. This organization can also be generalized since a passive/behavior association can be considered as a new (passive) object which is, itself, supervised by another behavior (figure 3.a).

Specification of the behavioral aspects

We model the dynamic aspects of control systems by associating each behavioral class with a Finite State Machine (figure 3.b). Figure 3.b models the discrete behavior of a leg controlled by its local controller, which is itself coordinated by its local supervisor. Once specified in this way, the behavioral objects execute an elementary task, in an autonomous and independent manner, and their concurrent execution describes the entire state space of six legs. ensure reliable locomotion, some of these states for example the state in which all the legs are raised at the same moment -must be prohibited. To restrict the entire statespace to the allowed state-space, we allow (or not) some transitions to be fired by synchronizing the actions of the LC instances with those of the LS instances. These synchronizations (or shared actions) are detailed in the configuration aspects. Moreover, we propose to combine behavioral and passive objects together in a composite object (figure 3.a), so as to explicitly represent a modeled software function (here the Locomotion). To make design easier and development effort profitable these composite can be manipulated and (re)used to model more complex software functions in a hierarchic and modular way.

Configuration aspects

The previously described behavioral and structural aspects specify a set of possible configurations of a family of software systems in terms of classes, interactions and behaviors. Consequently, modeling a particular software system of this family requires the description of a particular configuration. This particular configuration, which is represented with an object diagram (figure 3.c) helps to better define the structural aspects by specifying the topology and interactions of the instances which make up the software system. Moreover, it also helps to better define the behavioral aspects by specifying -in the form of relabeling annotations [START_REF] Magee | Concurrency. State Models & Java Programs[END_REF], (instance1.actionA /instance2.actionB) -the actions which are shared between these instances. These shared actions allow to synchronize instances in order to obtain the desired behavior. The object diagram in figure 3.c illustrates part of the configuration of the mobile platform. This diagram shows, in accordance with the previously mentioned safety property, how the local supervisor ls3 allows the evolving of local controller lc3 according to the position of the two neighboring legs l2 and l4. Indeed if legs l2 and l4 are raised (lc2 and lc4 receive the privilege to do their protraction: ls3.privilege/lc4.transfer or ls3.privilege/lc2.transfer) then leg l3 can only be in the Down state (figure 3.b). Conversely, if the legs l2 and l4 remain on the ground, leg l3 can be allowed to rise (ls3.up/lc3.transfer) which will then preempt the privilege of its neighbors. This last specification phase helps to complete the specification model whose global behavior (Locomotion function) must be validated so as to make sure that its specification respects the expected properties.

« behavior » Local Controller (LC)

Validation Model

Simulation and model-checking techniques aim to make software reliable by ensuring designers that their models meet their requirements [START_REF] Bérard | Systems and Software verification[END_REF][START_REF] Clarke | Model checking[END_REF]. The integration of these complementary methods into object-oriented constructions seems pertinent as they allow the efficient validation of software systems. In the proposed approach, the validation model is described in the form of process algebra called Finite State Process (FSP) [START_REF] Magee | Concurrency. State Models & Java Programs[END_REF] in order to use LTSA [START_REF] Magee | Concurrency. State Models & Java Programs[END_REF]. The advantage of LTSA is that it allows both the simulation and the checking of behavioral models.

Specification of the validation model using FSP

In LTSA, a system is structured using a set of primitive processes, whose behavior is modeled in FSP in the form of expressions combining local processes and actions. The representation of the global behavior of systems is obtained with the composition of instances of these processes (instance: Process) and with the representation of their interactions through shared actions within a composite process. So similarly to the specification model, modeling a composite process allows the specification of a complex system in a modular, hierarchic way; the instances of composite processes are potentially reused in another composite. To specify the validation model, we collect the entities contained in the specification model (states, actions, relabeling annotations, …) to transform these entities into FSP (i.e. section 5). Thus, as shown in figure 4.a, for the local controller (LC), the behavior of a behavioral class, graphically described by its FSM (figure 3.b), is used to obtain the primitive process (LC) in FSP. a second step, the composite type instances which are presented in the configuration aspects (figure 3.c) are used to generate the composite processes in FSP (figure 4.b). As an example, the Locomotion behavior is obtained from a set of six instances (lci) of the primitive process local controller (LC) and six instances (lsi) of primitive processes local supervisor (LS). These instances are composed in a parallel way ( || ), then synchronized ( / ) using their shared actions -thanks to the annotation (ls3.privilege/lc2.transfer, ls3.up/lc3.transfer, etc…) -included in the Locomotion composite object (figure 3.c). This Locomotion behavioral model is then checked using LTSA.

Analysis of the validation model

LTSA allows the interactive simulation of the different execution traces of the specified model to ensure that the latter satisfies the expected behavior. Simulation, which is a nonexhaustive validation, can be completed with a search for violation of liveness and safety properties. In the validation model proposed here, only the liveness properties will be presented. A liveness property asserts that « something good eventually happens » [START_REF] Bérard | Systems and Software verification[END_REF]. In LTSA, liveness properties are expressed with the keyword progress. The liveness property mentioned earlier (at the end of section 2) consists in checking that each local controller (lci) can always execute its walking cycle, which results in the recurrent detection of the transfer action for each local controller (figure 5)

Figure 5. Liveness properties in FSP

If a property is violated by the validation model, LTSA produces the sequence of actions leading to this violation. The designer can then modify his/her model according to the obtained results.

Model

Engineering [START_REF] Bézivin | In search of a Basic Principle for Model-Driven Engineering[END_REF] aims to unify software activities from the specification down to the executable code production, through the integration of heterogeneous models into coherent software developments. This coherent integration is only possible -according to MDE -through a formally defined metamodeling architecture which allows -through different levels of abstraction (models, metamodels, metametamodel) -the precise definition of the concepts used to characterize a particular type of (meta)model. architecture, metamodels describe all the concepts necessary for the definition of a specific type of models, while the metametamodel specifies the concepts that are common to the metamodels used. So, from these common concepts, a set of relations between the entities of the metamodels can be deduced. Figure 6.a describes the correspondence of the concepts of the specification metamodel and those of the validation metamodel. The transformation rules which can be deduced from these relations are applied to the entities of a source model (here, the specification model) in order to obtain the entities of the target model (here, the validation model) in a systematic way. Moreover, the explicit representation of the metamodels and transformation rules allows the use of model transformation tools for the automated generation of specific target models (figure 6.b). In accordance with MDE, the present approach is based on the concepts of models, metamodels and model transformations and has been prototyped with a metamodeling environment MetaEdit [START_REF]Domain Specific Modeling with MetaEdit+[END_REF] -in order to transform the specification model into a validation model (FSP code). The FSP code obtained in this way can directly be analyzed with the LTSA tool. As the proposed models respect the LTS semantics, the semantic gap between these models is reduced, which makes the transformation between models easier. Moreover, the use of model transformation tools makes the proposed approach even more reliable by avoiding the errors that would be caused by manual transcriptions.

Figure 6.a). Correspondence between the specification and validation metamodel, b) Conceptual representation of metamodeling

As said in the introduction, the aim of the present approach is to produce an executable code for the implementation of validated control software. However, even if the joint use of object-oriented techniques, checking tools and model transformation techniques makes software development easier and more reliable, it does not guarantee that the implementation conforms with the validation. That is why, the approach presented in this paper is part of a global software development (figure 1) in which the use of a framework and a runtime platform -also in conformity with LTS semantics -helps to reduce the semantic gap between the models and thus allows the easier generation of a code in accordance with the specification and validation models [START_REF] Rasse | Toward a Validated Object-Oriented Design Approach to Control Software[END_REF]. So, this approach allows the creation of a coherent software development cycle that integrates specification, validation and implementation phases.

Conclusion and Perspective

This paper has presented an approach combining object-oriented techniques with formal validation and MDE, to ensure the validated specification of control software. In a first step, it proposes an object-oriented specification completed with FSM for the modeling of software systems. The specification model thus obtained is sufficiently precise to be used as a source model for automated software generation. It can be transformed into a process algebra so as to be validated with a model-checking tool. This approach which has been applied on a locomotion software system has the advantage of making the conception of software systems easier while increasing their reliability and also of being integrated in a coherent global development ranging the specification to the implementation. We will continue this work, in a first step, by the checking of other liveness and safety properties to validate more effectively the Locomotion function of the robot. In a second step, we plan to implement the approach on a number of various applications to test its robustness.

  .a). A leg moves in a cyclic way between two positions aep (anterior extreme position) and pep (posterior extreme position) (figure 2.b). The control architecture is based on decentralized control [7]; the walking cycle of a leg (L) is obtained with local controllers (LC) and the global behavior is obtained with six local supervisors (LS) which coordinate the local controllers (figure 2.c).

Figure 2 .

 2 Figure 2. a) Mobile platform, b) Walking cycle, c) Control architecture

Figure 3 :

 3 Figure 3: Specification model of the Locomotion function: a) structural aspects, b) behavioral aspects, c) configuration aspects

  / lc2.transfer ls3.up / lc3.transfer, ls3.down / lc3.aep :Locomotion

Figure 4 .

 4 Figure 4. Behavioral description in FSP, a) of the LC primitive process, b) of the Locomotion composite process

  In this progress Leg1_Cycle = {lc1.transfer },…, progress Leg6_Cycle = {lc6.transfer }( lc1 : LC || lc2 : LC || … || ls1 : LS || ls2 : LS || … ) / { ls3.privilege / lc2.transfer, ls3.up / lc3.transfer,