O Allix

P Gosselet

P Kerfriden

K Saavedra

Virtual delamination testing through non-linear multi-scale computational methods: some recent progress

. The method proposed in this paper introduces three additional features: (i) the adaptation of the macro-basis to situations where classical homogenization does not provide a good preconditioner, (ii) the use of non-linear relocalization to decrease the number of global problems to be solved in the case of unevenly distributed non-linearities, (iii) the adaptation of the approximation of the local Schur complement which governs the convergence of the proposed iterative technique. Computations of delamination and delamination-buckling interaction with contact on potentially large delaminated areas are used to illustrate those aspects.

Introduction

Despite the many studies since the beginning of the eighties, the prediction of delamination remains a challenge, both from a scientific and from an industrial point of view. Many difficulties encountered in this field are inherent to composite modeling. The interested reader will find a survey of the literature devoted to the modeling of composites in [START_REF] Herakovich | Mechanics of composites: A historical review[END_REF]. Simulating delamination requires to tackle specific difficulties (i) the complex 1 state of stress which leads to the initiation and the propagation of delamination (ii) the size and the complexity of the problem to be solved when dealing with composite structures. One of the industrial objectives is to replace some of the numerous physical tests required to assess the damage tolerance of composites by numerical simulations [START_REF] Allix | Mesomodeling of delamination: towards industrial applications[END_REF], or in other words to perform Virtual Delamination Testing (VDT).

It is today well accepted at an industrial level that a realistic VDT procedure should rely on a meso-scale description of the laminates. Such a fine-scale description requires a Finite Element discretisation whose characteristic size is at most the thickness of individual plies, which is of the order of a tenth of a millimetre. For the treatment of industrial parts, the size of the resulting model is therefore huge, which leads to considering the applicability of parallel computations to those large and complex nonlinear cases. Indeed, these problems potentially involve multiple delamination fronts, buckling or contact, and therefore instabilities.

The paper describes some attempts to deal with such problems within a multi-scale parallel framework when delamination is the only damage mode that is taken into account. Delamination is here modeled by means of a cohesive zone model. Several such models have been proposed in the literature, for example in [START_REF] Allix | Interlaminar interface modelling for the prediction of delamination[END_REF][START_REF] Xu | Numerical simulations of fast crack growth in brittle solids[END_REF][START_REF] Schellekens | Free edge delamination in carbonepoxy laminates: a novel numerical/experimental approach[END_REF][START_REF] Qiu | An interface element formulation for the simulation of delamination with buckling[END_REF][START_REF] Camanho | Mixed-mode decohesion finite elements for the simulation of delamination in composite materials[END_REF]. In this paper we make use of the model proposed in [START_REF] Allix | Modeling and simulation of crack propagation in mixed-modes interlaminar fracture specimens[END_REF] but similar results could be obtained with other models once calibrated. The main features of the model are briefly presented in Section 2.

In the remainder of the paper, the basics of the multi-scale strategy are described and test cases are presented to demonstrate its numerical efficiency. The contribution of the paper is the definition of a framework that encompasses different aspects of the strategy that have emerged separately in [START_REF] Ladevèze | On a mixed and multiscale domain decomposition method[END_REF][START_REF] Guidault | A two-scale approach with homogeneisation for the computation of cracked structures[END_REF][START_REF] Cresta | Nonlinear localization strategies for domain decomposition methods: Application to post-buckling analyses[END_REF][START_REF] Kerfriden | A three-scale domain decomposition method for the 3d analysis of debonding in laminates[END_REF][START_REF] Allix | A relocalization technique for the multiscale computation of delamination in composite structures[END_REF][START_REF] Saavedra | On a multiscale strategy and its optimization for the simulation of combined delamination and buckling[END_REF]. Indeed, our previous publications focussed on particular issues related to the present topic. It now appears that the set of tools that we have developed in the past can help formulate a general non-linear multi-scale approach that is adapted to the treatment of large laminated and damageable structures taking into account possible buckling and contact. Multi-scale refers here to a computational technique which involves different scales and which aims at finding the solution over the whole structure at the smallest scale of interest. In this domain, one of the main issues to be addressed is the transfer of information from one scale to another.

A large number of multiscale methods rely on classical homogenisation of heterogeneous media, which was initiated by [START_REF] Hill | Elastic properties of reinforced solids: some theoretical principles[END_REF]. For linear periodic media the most efficient method was initiated in [START_REF] Sánchez-Palencia | Non homogeneous media and vibration theory[END_REF]. Further developments and related computational approaches can be found in [START_REF] Tarek | Hierarchical modeling of heterogeneous bodies[END_REF][START_REF] Fish | Computational plasticity for composite structures based on mathematical homogenization: Theory and practice[END_REF][START_REF] Pellegrino | Numerical homogenization of periodic composite materials with non-linear material components[END_REF][START_REF] Kouznetsova | Multiscale constitutive modelling of heterogeneous materials with a gradient-enhanced computational homogenization scheme[END_REF][START_REF] Feyel | A multilevel finite element (fe2) to describe the response of highly non-linear structures using generalized continua[END_REF]]. An overview of these methods can be found in [START_REF] Tarek | An introduction to computational micromechanics[END_REF]. In computational homogenization approaches the resolution of the macro-problem leads to effective values of the unknowns; then, the micro solution is calculated locally based on the macro solution. The fundamental assumption, besides periodicity, is that the ratio of the characteristic length of the small scale to the characteristic length of the large scale must be small. All areas which do not satisfy the hypothesis of scale separation such as boundary zones or vicinity of cracks, where the material cannot be homogenized, require special treatment. Therefore a large amount of recent studies aim at applying enhanced homogenization schemes to localized failure, see for instance [START_REF] Massart | Structural damage analysis of masonry walls using computational homogenization[END_REF][START_REF] Belytschko | Multiscale aggregating discontinuities: A method for circumventing loss of material stability[END_REF][START_REF] Coenen | A multi-scale approach to bridge microscale damage and macroscale failure: a nested computational homogenization-localization framework[END_REF]. These extension, which are dedicated to overcome some of the difficulties for a given type of problem are not suited yet to deal with edge effects and large cracks and therefore not directly suitable to the treatment of delamination.

The proposed method is based on a Domain Decomposition approach. These methods have been developed initially for large linear problems for which they can now be considered mature. The most well-known methods are FETI [START_REF] Farhat | Optimal convergence properties of the feti domain decomposition method[END_REF] and BDD [START_REF] Mandel | Balancing domain decomposition[END_REF] which where designed for perfect interface and extended, in the case of FETI, to contact (with or without friction) [START_REF] Dostál | Feti-based algorithms for modelling of fibrous composite materials with debonding[END_REF] or prescribed displacement gaps [START_REF] Kruis | Reinforcement-matrix interaction modelled by feti method[END_REF]. FETI and BDD rely on a static condensation for each sub-domain. The resulting interface problem, which is large, is solved iteratively using a preconditioner which is associated to the balance of the rigid-body momentum of the sub-domains. In the case of heterogeneous media, the macro-space of rigid body is not necessarily the most appropriate one and a specific deflation can be performed [START_REF] Efendiev | A domain decomposition preconditioner for multiscale high-contrast problems[END_REF]. It is therefore interesting to define the macro-space as the space which is associated with the homogenized response of the subdomains. The use of homogenization in the context of a Domain Decomposition Method has been proposed in the micro-macro approach of [START_REF] Ladevèze | Une nouvelle stratégie de calcul micro/macro en mécanique des structures[END_REF].

Homogenization being a natural tool for composites, we base our approach on this micro-macro framework. The decomposition of the structure into subdomains is chosen to be compatible with the mesomodeling of the laminate. The micro-macro method relies on mixed interface conditions between subdomains, which allows to treat any kind of interfacial constitutive law directly at the interface level [START_REF] Ladevèze | On a mixed and multiscale domain decomposition method[END_REF]. Three types of interfaces are considered here: damageable interfaces and contact interfaces that are compatible with the mesomodeling, and perfect interfaces within the plies to split the problem into smaller pieces that are suited to parallelism. This leads to a large number of substructures, and therefore to a large macro-problem. A third scale is then introduced to perform a low cost and precise approximation of the homogeneized macro-problem by using a BDD preconditioner [START_REF] Kerfriden | A three-scale domain decomposition method for the 3d analysis of debonding in laminates[END_REF], as described in Section 3. Note that in this paper only unilateral contact is considered but the framework is well suited to friction [START_REF] Champaney | Adaptive multi-analysis strategy for contact problems with friction[END_REF].

In the context of non-linear problems, Domain Decomposition Methods are mainly used as a solver for the tangent problem to be solved at each iteration of a Newton-Raphson based algorithm [START_REF] Le | Domain decomposition methods in computational mechanics[END_REF][START_REF] Germain | High-performance parallel simulation of structure degradation using non-local damage models[END_REF][START_REF] Klawonn | Dual-primal iterative substructuring for almost incompressible elasticity[END_REF], with if required an arc-length control. Several problems can be encountered in this case. One of such problems is that the choice of the macro-space, and the implied homogenized behavior, is in general not adapted to a situation where a crack interacts with a subdomain. In other words, a preconditioner designed for a problem without crack can become ineffective in the presence of a crack. It has been shown in [START_REF] Guidault | A two-scale approach with homogeneisation for the computation of cracked structures[END_REF][START_REF] Guidault | A multiscale extended finite element method for crack propagation[END_REF], that for cracks crossing interfaces of the domain decomposition, a modification of the macro-basis that adds a few degrees of freedom only makes it possible to obtain the same convergence rate for a cracked domain and for an un-cracked one. Unfortunately such an adaptation is not possible in the case of cracks propagating at the interface between subdomains. We have therefore followed another line, the one of non-linear relocalization [START_REF] Cresta | Nonlinear localization strategies for domain decomposition methods: Application to post-buckling analyses[END_REF][START_REF] Pebrel | A nonlinear dual domain decomposition method: application to structural problems with damage[END_REF]. This approach aims at solving the problem of the strong deterioration of the convergence rate due to localized non-linear effect [START_REF] Cai | Nonlinearly preconditioned inexact newton algorithms[END_REF]. Following this line of thoughts, we have applied a non-linear relocalization approach on the set of subdomains that are connected to the front of delamination, which is described in Section 4 [START_REF] Allix | A relocalization technique for the multiscale computation of delamination in composite structures[END_REF]. Note that our approach naturally avoids to conduct useless nonlinear computations far from the delamination front which is the goal of the prediction procedure developped in [START_REF] Lloberas-Valls | Multiscale domain decomposition analysis of quasi-brittle heterogeneous materials[END_REF] for Newton-Schur strategies.

Having in mind the problem of the tolerance of laminates to compression after impact [START_REF] Mfsf De Moura | Modeling compression failure after low velocity impact on laminated composites using interface elements[END_REF] we have started to work on the question of the interaction between potentially large growing delaminated areas and buckling, taking into account the contact condition [START_REF] Saavedra | On a multiscale strategy and its optimization for the simulation of combined delamination and buckling[END_REF]. In order to reconnect the micro part of the solution, the iterative technique introduces parameters which are associated to the influence of neighboring subdomains. These so called "search directions" correspond to Robin parameters whose values were optimized for 3D structures. These parameters must be adapted to the aspect ratios of the slender structures by introducing well-chosen anisotropic coefficients. Moreover, in the case of contact between slender structures over large delaminated areas, the search directions should be optimized according to the interface's state (open or closed) in order to obtain a reasonable convergence rate of the iterative solver. These points are discussed in Section 5. However, changing these parameters requires a refactorization of the homogenized operators, which is computationally expensive. A compromise between convergence speed and unit cost of iterations must be found so that the total CPU time is minimised.

The interface model

The interface model relates the jump of displacements [u] = u pu p to the normal Cauchy stress t = σ p .n = σ p .n on the interface Γ between two plies p and p . Here, n denotes the outer normal to ply p on Γ pp . In this problem, large displacements are considered but the jump of displacement is assumed to be small prior to full delamination. The tractions t are uniquely defined and related to the displacement discontinuities by means of the following damageable constitutive relation:

t = K.[u] (1)
The expression of the stiffness operator K can be given in the reference frame (N 1 , N 2 , n) (as depicted in Figure [START_REF] Abisset | On the validation of a damage mesomodel for laminated composites by means of open-hole tensile tests on quasi-isotropic laminates[END_REF] with n = N 3 , p ≡ "Ply 1" and p ≡ "Ply 2"):

    (1 -d 1 )k 1 0 0 0 (1 -d 2 )k 2 0 0 0 1 -[u].n + d 3 k 3     (2)
< > + is here the positive indicator function. The local damage variables d i are introduced into the interface model in order to simulate its softening behavior when the structure is loaded. Their values range from 0 (healthy interface point) to 1 (completely damaged interface point). The parameters d i are related to the local energy release rates Y i of the interface's degradation modes as follows:

Y i = - ∂e d ∂d i where            Y 1 = 1 2 k 1 [u] 2 1 Y 2 = 1 2 k 2 [u] 2 2 Y 3 = 1 2 k 3 [u] 3 2 + , (3)
ψ(σ.N 3 , d i ) = 1 2 σ 33+ 2 k 3 (1 -d 3 ) + σ 33- 2 k 3 + σ 13+ 2 k 1 (1 -d 1 ) + σ 23+ 2 k 3 (1 -d 2 ) (1.15) avec 0 ≤ d i ≤ 1 FIG. 1.2: Repère lié à l'interface
L'énergie libre, exprimée en contraintes, est reliée à une expression en déplacement de l'énergie de déformation par la relation de comportement suivante :

σ.z = K.[u]
(1.16)

Avec [u] = u + -u -= [u 1 ].N 1 + [u 2 ].N 2 + [u 3 ].N 3 exprimé dans le repère (N 1 , N 2 , N 3 ) défnit sur la figure (1.
2) et la définition de l'opérateur de comportement

K =   k 1 (1 -d 1 ) 0 0 0 k 2 (1 -d 2 ) 0 0 0 k 3 (1 -d 3 .h(σ 33 ))   (1.17) où h est la fonction heavyside : ∀x < 0 h(x) = 0 (1.18) ∀x ≥ 0 h(x) = 1 (1.19)
On obtient l'expression de l'énergie de déformation volumique en déplacements suivante :

e d = 1 2 ((1 -d 1 )k 1 [u 1 ] 2 + (1 -d 2 )k 2 [u 2 ] 2 + k 3 (1 -d 3 )[u 3 ] 2 + + k 3 [u 3 ] 2 -) (1.20)
Biblio P. Kerfriden

Y |t = sup τ ≤t Y 3 α |τ + γ 1 Y 1 α |τ + γ 2 Y 2 α |τ 1 α (4)
Thus, the evolution law is defined by:

d 1 = d 2 = d 3 = w(Y ) (5)
where, in general, w(Y

) = n n + 1 Y Y c n .
This model has the advantage, using a single damage variable, to be able to recover different critical energy release rates for pure mode loading as well as to fit to classical mixed mode criteria. For example, setting α = 2 leads to the classical quadratic energy criteria.

Main features of the method

As presented in Figure 2, the structure is split into substructures which are connected by interfaces that have mechanical behaviors. In a second stage, the substructures are gathered into "super-substructures" which are assigned to independent processors. In order to ensure the scalability of the method, the interfaces are the support of a macro (homogenized) problem, the resolution of which requires the solution of a third scale (supermacro) problem on super-interfaces.

Micro-macro scale separation

The iterative LaTIn algorithm, which is designed to non-linear problems, is here applied to the solution of the geometrically non-linear substructured reference problem with "material" non-linearities (damage, contact) localized on the interfaces. The finite element method is used to discretize the governing equations. The aim of the method

W E 0 (displacement), F E 0 (interforces),
where index E ranges over all substructures and index 0 means that the quantity is given in the reference configuration (total Lagrangian approach).

In order to ensure the scalability of the method, a global and linear coarse grid problem is solved. The definition of the macroscopic fields required to construct this problem is done on the interface unknowns only. Whichever the interface behavior, action reaction principle F E 0 + F E 0 = 0 is verified; the principle of the macro-problem is to enforce this equation partially at any time of the iterative solution process:

∀W M E0 ∈ W M E0 , Γ E 0 E 0 (F E 0 + F E 0 ) • W M E0 dΓ 0 = 0 , (6)
where displacement macrospace W M E0 is a parameter of the method as well as its dual F M E0 . The definition of the macro-spaces is done through a projector Π, which is chosen L 2 -orthogonal (so that the same projector is used by the traction and displacement fields). We then have the following splitting of the interface quantities:

∀(F E 0 , W E 0 ) ∈ F E0 × W E0 , F E 0 = F M E0 + F m E0 with F M E0 = ΠF E 0 and W E 0 = W M E0 + W m E0 with W M E0 = ΠW E 0 ⇒ Γ E 0 E 0 F E 0 • W E 0 dΓ 0 = Γ E 0 E 0 F M E0 • W M E0 dΓ 0 + Γ E 0 E 0 F m E0 • W m E0 dΓ 0 (7)
Numerical tests showed that in order to ensure the numerical scalability of the method the macro-basis should extract at least the linear part of the interface forces. Indeed, this macro-space contains the part of the interface fields with the highest wavelength. Consequently, according to the Saint-Venant principle, the micro complement only has a local influence.

Iterative algorithm

It is now possible to split all the equations of the system into two groups:

• non-linear equations in the substructures and macroscopic admissibility of interfaces, whose solutions are elements of the manifold A d :

-non-linear kinematic admissibility of the substructures

E E0 = 1 2 ∇ 0 u E0 + t ∇ 0 u E0 + t ∇ 0 u E0 t ∇ 0 u E0 , on Ω E0 (8)
u E0 |∂Ω E 0 = W E 0 |Γ E 0 , on Γ E 0 E 0 (9)
-non-linear static admissibility of the substructures

∀(u E0 , W E0 ) ∈ U 0 E0 × W 0 E0 such that u E0 |∂Ω E 0 = W E0 |Γ E 0 , Ω E 0 π E0 : Ė(u E0 ) dΩ 0 = Ω E 0 ρ E 0 f d • u E0 dΩ 0 + Γ E 0 F E 0 • W E0 dΓ 0 (10)
-behavior of the substructures

π E0 = ∂ψ ∂E E0 , on Ω E0 , (11)
-macroscopic admissibility of the interfaces (6).

• local (non-linear) equations in the interfaces whose solutions belong to the manifold Γ:

-interface behavior (perfect, contact and cohesive interfaces) and boundary conditions (see Section 2).

The solution

s ref = (u E0 , π E0 , W E 0 , F E 0
) is such that:

s ref ∈ A d ∩ Γ (12)
Note that in the case of small perturbations, the admissibility equations are linear. In this case, the manifold A d is an affine space.

The resolution scheme consists in seeking the solution s ref alternatively in these two manifolds: first, one finds a solution s n in A d , then a solution s n+ 1 2 in Γ. In order for the two problems to be well-posed, search directions E + and E -linking the solutions s and s through the iterative process are introduced (see Figure 3).

• At the global stage, starting from fields ( W E0 , F E0 ) satisfying the interface equations (manifold Γ), we seek fields (W E 0 , F E 0 ) in A d (satisfying the subdomain equations) using the following closing relation:

k - E0 W E 0 -W E0 + F E 0 -F E0 = 0 (13)
k - E0 is the search direction associated to the global stage. • At the local stage, starting from fields (W E 0

, F E 0 ) satisfying the subdomain equations (belonging to manifold A d ), we seek fields ( W E0 , F E0 ) satisfying the interface equations (manifold Γ), using the following closing relation:

k + E0 W E 0 -W E0 -F E 0 -F E0 = 0 (14)
k + E0 is the search direction associated to the local stage.

s ref Γ E - E + A d s n+ 1 2 s n+1 s n

Third scale

The macro-problem being linear, discrete and sparse, it can be efficiently solved by a balancing domain decomposition algorithm [START_REF] Mandel | Balancing domain decomposition[END_REF]. To do so, substructures are gathered into super-substructures. The macro-problem is condensed at the super-interfaces and this condensed problem is solved by a conjugate gradient algorithm. The balance of super-structures requires the global solution of a third scale problem whose size is the number of rigid body motions of floating super-substructures. Figure [START_REF] Allix | Mesomodeling of delamination: towards industrial applications[END_REF] shows the convergence rate of the LaTIn algorithm when the conjugate gradient scheme for the condensed macroproblem is stopped after a fixed number of iterations. The test case is the holed plate under traction loading with the supersubstructuring pattern given in Figure [START_REF] Allix | Modeling and simulation of crack propagation in mixed-modes interlaminar fracture specimens[END_REF]. This problem is 3.4 10 6 degrees of freedom large, it is distributed in 520 subdomains with 1, 350 interfaces leading to a 12 10 3unknown macro-problem. 8 super-substructures are employed so that the condensed macro-problem on the super-interfaces has 1, 746 unknowns and the dimension of the third scale (associated to the rigid body motions of the super-substructures) is only 36.

It appears clearly that only very few iterations of the conjugate gradient scheme are required to get the necessary part of the macro-displacement Lagrange multiplier leading to the multiscale convergence rate of the LaTIn algorithm. Typically, the algorithm is stopped when the residual error (normalized by the initial error) falls below 10 -1 . The admissibility of the macro-forces is thus enforced on a third level, which is sufficient to determine the part of the solution which needs to be transmitted at each iteration of the resolution. In that case the time required to solve the macroproblem is divided by a factor 100.

Figure 6 presents a larger case where a direct computation of the macroproblem The previous examples allow us to make an important remark related to our vision of the problem of large-scale simulation of delamination. The reader will notice that we use a homogeneously fine finite element discretization to approximate the displacement field in the structure. Specifically, the mesh is sufficiently fine to handle the propagation of a delamination front at an arbitrary location in the structure, which The fact that we are not willing to remesh is a choice driven by the observation that error estimation, mesh adaptivity and field transfer are, for parallel problems and for problems with softening behaviors, a subject of research in themselves and no mature tool has emerged from pioneer investigations which can be found, for instance, in [START_REF] Ladevèze | Constitutive relation error estimators for (visco)plastic finite element analysis with softening[END_REF][START_REF] Huerta | Error estimation and adaptivity for nonlinear fe analysis[END_REF][START_REF] Larsson | Time finite elements and error computation for (visco)plasticity with hardening or softening[END_REF][START_REF] Allix | On the control of the load increments for a proper description of multiple delamination in a domain decomposition framework[END_REF][START_REF] Parret-Fréaud | Fast estimation of discretization error for fe problems solved by domain decomposition[END_REF]. Of course, the price that we pay for the expected robustness associated to this choice is a large number of arguably unnecessary degrees of freedom.

Relocalization for the propagation of delamination

Let us consider a simple DCB case, as illustrated in Figure 8. Figure 9 shows that the convergence of the classical approach (blue bars) is strongly deteriorated when • the singularity near the tip of the crack is very poorly represented by linear macro quantities. Therefore, the complementary part is not localized enough and many iterations are required to transmit them through the structure;

• the strong non-linearities require many iterations to converge, in particular the prediction of the location of the crack tip at a given time step requires the quasiconvergence of a large number of consecutive equilibrium states.

Using non-linear relocalization in a box containing the crack tip and the process zone is a way to deal with those two problems: after each linear stage, a subproblem is extracted around the crack tip (within the so-called relocalization box whose size is a parameter) as shown in Figure 8. This smaller problem is solved non-linearly with Robin boundary conditions satisfying the macro-equilibrium of the structure. Being far enough from the singularity, the macro quantities at the boundary of the box represent the global fields correctly and are then relevant for the prediction of the non-linear evolution of the crack. The resulting modifications only have a small-scale effect which can be transmitted by the upcoming local stage.

The other bars in Figure 9 show the influence of the size of the relocalization box on the convergence. Of course the larger the box, the best the filtering of the singularities on the boundary of the box, and the fastest the convergence. The counterpart is that the larger the box, the more expensive the non-linear computations associated to the relocalized solutions, which are obtained by a LaTIn method restricted to the box, are.

5 Further improvements for delamination/buckling and contact

Taking into account the structure's slenderness

Optimal search direction of one subdomain (for the global step) is known to be the Schur complement of the rest of the structure. In general a very coarse approximation, in practice a scalar, is sufficient to ensure good convergence of the LaTIn method. In [START_REF] Saavedra | On a multiscale strategy and its optimization for the simulation of combined delamination and buckling[END_REF] it was shown that for plates, the slenderness induces a structural anisotropy that has to be taken into account by the search directions. A dimensional analysis leads to the following relationship between the longitudinal (n) and transverse (t) search directions (L 0 is the characteristic length of the structure, h 0 is its thickness):

k m E0 n k m E0 t = L 0 h 0 2
Here superscript m stands for the micro part of the search direction. The macro part of the search direction has to be set to a large value on perfect interfaces so that the macro continuity of displacements is almost satisfied throughout the iterative process.

Figure 10 shows that these adaptations of the search directions (i.e. anisotropic search directions) are necessary to ensure the scalability of the method.

Update of the search directions

In the context of buckling and contact, the state of the structure can have large influence on its response. This implies that search directions which are optimal in one configuration can be unadapted to others, leading to a drop in the convergence rate.

Strategies to update the search directions according to the status of the interfaces must then be settled. Typically for cohesive interfaces, the optimal value is related to the current stiffness of the interface (which depends on the damage state); for fully delaminated interfaces, search directions should be large when contact occurs whereas they should be null when the crack is open. Figure 11 presents the effect of the updating of the search direction according to the damage state. In this simple DCB case, all strategies converge. Of course, the more frequent the updates the less iterations, but each update requires recomputation and factorization of the operators so that a compromise must be found to achieve minimal CPU time.

Figure 12 shows the evolution of the error for one time step of a opening contact problem: the plate is initially delaminated in its middle (large closed crack) and a compression loading is imposed. When the optimal search direction is chosen a priori, only 10 iterations are required. When the wrong one is chosen, the algorithm converges to a non-physical solution. Starting from an incorrect initial guess, a simple update procedure (every 10 iterations the parameters are adapted to current contact state) enables to converge to the solution. Note that the convergence is slow because of the unusual extension of the initial contact zone.

Pre-delaminated plate sensitive to imperfection

Let us consider the example of a pre-delaminated plate submitted to compression. The example is designed to be sensitive to imperfection. Indeed two buckling modes can be excited (Figure 13): a global buckling mode (closed interface -mode II delamination) and a local buckling (open interface -mode I delamination). The problem is split into 1280 substructures leading to 3248 interfaces with about 1.2 millions of d.o.f. The macro-problem involves 30,000 d.o.f. when the super-macro one only involves 132 d.o.f. When the imperfection is small, the response of the buckling mode of the plate is a global one (mode II delamination) and the delamination starts to propagate for a transversal displacement of about 0.75 mm (see Figure 14 -mode II curve).

When the level of the perturbation is at least ten times greater (F d = 2 N), a local buckling mode is excited, which leads to the propagation of the delamination for a transversal displacement of about 0.36 mm (see Figure 14 -mode I curve). Figure 15 shows the configuration and the crack propagation of the last time step.

Example of multiple delamination of a laminated plate in compression

The following example has been chosen because it involves all the difficulties discussed in this last section. Here, the delamination between plies and the possibility of contact and separation between delaminated surfaces in large displacements are studied (others ] s composite plate, submitted to compression (prescribed displacement u d ) and pre-delaminated (with the same initial length) on the central interface and on the upper one. A normal perturbation is applied F d at the level of the top ply (see Figure 16). The layers are assumed to be elastic and orthotropic with the following characteristics in the referenced basis (1-fiber direction, 2-transverse direction in the ply, 3-normal direction): E 1 = 185, 500 MPa, E 2 = E 3 = 9, 900 MPa, ν 12 = ν 13 = 0.34, ν 23 = 0.5, G 12 = G 13 = 6, 160 MPa, G 23 = 3, 080 MPa. The problem is split into 1,280 substructures leading to 3,248 interfaces, 2 millions of d.o.f. are involved. The macroproblem involves 30,000 d.o.f. when the super-macro one only involves 168 d.o.f. The time interval is discretized into 120 times steps and 30 processors have been used. On Figure 17, the force-normal displacement responses for the three groups of layers in the middle of the plate are plotted and Figure 18 shows three typical configurations. The top ply buckles first for an applied load of 80 N leading to a non symmetric configuration (configuration A). In this configuration a loss of contact between the two upper plies and the lower one is observed. When the applied load reaches 100 N, the central and lower plies buckle which leads to a recontact between the upper plies (configuration B). Finally, the configuration C is symmetric. For a value of the transverse displacement of about 0.5 mm, the delamination starts to propagate in the central interface leading to a decrease of the reaction forces.

k + E 0 = k - E 0 = 0 k + E 0 = k - E 0 = E/L Γ E 0 k + E 0 = k - E 0 = E/L Γ E 0 k + E 0 = k - E 0 = 0
Figure 12: Evolution of the error when using different updating strategies

Conclusion

In order to circumvent the numerous problems associated with the large scale simulation of delamination problems, we have developed a multi-scale framework, wherein a Domain Decomposition approach is optimized to deal with the severe non-linearities.

A lot of work is still required to make the approach more generic. The problem of code development is also an issue that needs to be taken into account when developing such dedicated methods. The challenge we would like to address is the one of the Virtual Delamination Testing, in a fully integrated sense. Nevertheless, those studies have been conducted by restricting the potential damage modes of the laminate to delamination. However, it is known that in many cases, like in the case of low-velocity impacts or in the case of the analysis of the tolerance to defects, lumping the damages onto the interfaces cannot reproduce the delamination patterns adequately. In fact, these patterns are often driven by the interaction between transverse cracking and delamination. Two main approaches are followed in this more general case. In [START_REF] Lubineau | Towards a bridge between the microand mesomechanics of delamination for laminated composites[END_REF] a micro analysis leading to a meso-scale model where a non-local coupling between the interface and the adjacent plies associated with transverse-cracking / delamination interaction has been developed. A validation of this approach by making use of open-holed tests, which exhibits very different delamination patterns due to scale effect [START_REF] Green | An experimental investigation into the tensile strength scaling of notched composites[END_REF] can be found in [START_REF] Abisset | On the validation of a damage mesomodel for laminated composites by means of open-hole tensile tests on quasi-isotropic laminates[END_REF]. The non-locality of the ply model requires to have all the information throughout the thickness of a given ply within a unique sub-domain. This is not a problem with the physical decomposition at the meso-scale proposed in the paper. However, it becomes an issue if one makes use of an automatic decomposition of the structure, as was addressed in [START_REF] Bordeu | A mesoscale model for damage, cracking and delamination prediction in composite materials[END_REF]. Another approach aims at introducing the transverse cracks explicitly, or at least the transverse cracks that have a strong influence on the delamination pattern [START_REF] Van Der Meer | Computational modeling of complex failure mechanisms in laminates[END_REF] by means of X-FEM like technique. In the framework proposed in this paper, following this direction requires to development an hybrid multi-scale X-FEM method, as was proposed in [START_REF] Guidault | A multiscale extended finite element method for crack propagation[END_REF]. However, the complexity and highly-intrusive character of such an approach is an issue in terms of code development.

A promising alternative is to perform a local enrichment by means of a non-intrusive coupling of the structural solver with specialized external solvers dedicated to specific failure modes, as was proposed in [START_REF] Gendre | Non-intrusive and exact global/local techniques for structural problems with local plasticity[END_REF]. For instance, one can couple the tools presented in this paper with the one developed to simulate a micro-model where all the cracks are introduced explicitly [START_REF] Violeau | Micromodel-based simulations for laminated composites[END_REF]. This idea was successfully applied in [START_REF] Daghia | A micro-meso computational strategy for the prediction of the damage and failure of laminates[END_REF].

Figure 1 :

 1 Figure 1: The mesomodel entities

Figure 2 :

 2 Figure 2: Decomposition of the problem and associated three computational scales

Figure 3 :

 3 Figure 3: Schematic representation of the iterative LaTIn algorithm

Figure 4 :

 4 Figure 4: LaTIn convergence curves for different numbers of macro iterations

Figure 5 :

 5 Figure 5: Different levels of substructuring

Figure 6 :

 6 Figure 6: Bolted joint, substructuring and super-substructuring

Figure 7 :Figure 8 :

 78 Figure 7: Final delamination state of the bolted joint

Figure 9 :

 9 Figure 9: Performance of the relocalization technique w.r.t. the size of the relocalization box

Figure 10 :

 10 Figure 10: Influence of the search directions and of the substructuration in a bending test case

Figure 11 :

 11 Figure 11: Iterations and CPU time to convergence when using different updating strategies

Figure 13 :

 13 Figure 13: Pre-delaminated plate with associated potential buckling modes

Figure 14 :

 14 Figure 14: Load displacement curves depending on the imperfection

Figure 15 :Figure 17 : 18 Figure 18 :

 15171818 Figure 15: Final state of the plate in case of local buckling

Acknoledgement: Part of the research leading to these results has received funding from the European Community's Seventh Framework Program FP7/2007-2013 under grant agreement n • 213371.


Dimitris Vekris
email: dimitrios.vekris@u-pec.fr

Frédéric Lang
email: frederic.lang@inria.fr

Catalin Dima
email: catalin.dima@u-pec.fr

Radu Mateescu
email: radu.mateescu@inria.fr

Verification of EB 3 Specifications using CADP

eb 3 is a specification language for information systems. The core of the eb 3 language consists of process algebraic specifications describing the behaviour of the entities in a system, and attribute function definitions describing the entity attributes. The verification of eb 3 specifications against temporal properties is of great interest to users of eb 3 . In this paper, we propose a translation from eb 3 to LOTOS NT (LNT for short), a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to the eb 3 and LNT specifications. We automated this translation with the eb 3 2lnt tool, thus equipping the eb 3 method with the functional verification features available in the CADP toolbox.

Introduction

The eb 3 method [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] is an event-based paradigm tailored for information systems (ISs). eb 3 has been used in the research projects selkis [START_REF] Milhau | Combining UML, ASTD and B for the formal specification of an access control filter[END_REF] and eb 3 sec [START_REF] Jiague | Model-Driven Engineering of Functional Security Policies[END_REF], whose primary aim is the formal specification of ISs with security policies. In the eb 3 sec project, real banking industry case studies have been studied, describing interaction with brokers, customers and external financial systems. The selkis project deals with two case studies from the medical domain. The first one draws data records from medical imaging devices. The access to these records is done via web-based applications. The second one deals with availability and confidentiality issues for medical emergency units evolving in a great mountain range, like the Alps in that case.

A typical eb 3 specification defines entities, associations, and their respective attributes. The process algebraic nature of eb 3 enables the explicit definition of intra-entity constraints, making them easy for the IS designer to review and understand. Yet, its particular feature compared to classical process algebras, such as CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], lies in the use of attribute functions, a special kind of recursive functions evaluated on the system execution trace. Combined with guards, attribute functions facilitate the definition of complex inter-entity constraints involving the history of events. The use of attribute functions simplifies system understanding, enhances code modularity, and streamlines maintenance. However, given that ISs are complex systems involving data management and concurrency, a rigorous design process based on formal specification using eb 3 must be completed with effective formal verification features.

Existing attempts for verifying eb 3 specifications are based on translations from eb 3 to other formal methods equipped with verification capabilities. A first line of work [START_REF] Gervais | Synthesizing B Specifications from eb 3 Attribute Definitions[END_REF][START_REF] Gervais | Refinement of eb 3 Process Patterns into B Specifications[END_REF] focused on devising translations from eb 3 attribute functions and processes to the B method [START_REF]The B-Book -Assigning programs to meanings[END_REF], which opened the way for proving invariant properties of eb 3 specifications using tools like Atelier B [START_REF] Clearsy | [END_REF]. Another line of work concerned the verification of temporal logic properties of eb 3 specifications by means of model checking techniques. For this purpose, the formal description and verification of an IS case-study using six model checkers was undertaken in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF][START_REF] Chossart | Évaluation d'outils de vérification pour les spécifications de systèmes d'information[END_REF]. This study revealed the necessity of branching-time logics for accurately characterizing properties of ISs, and also the fact that process algebraic languages are suitable for describing the behaviour and synchronization of IS entities. However, no attempt of providing a systematic translation from eb 3 to a target language accepted as input by a model checker was made so far.

In this paper, we aim at filling this gap by proposing a translation from eb 3 to LNT [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator -Version 5[END_REF], a new generation process algebraic specification language inspired from E-LOTOS [START_REF]ISO/IEC. Enhancements to LOTOS (E-LOTOS)[END_REF]. As far as we know, this is the first attempt to provide a general translation from eb 3 to a classical value-passing process algebra. It is worth noticing that CSP and LNT were already considered in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] for describing ISs, and identified as candidate target languages for translating eb 3 . Since our primary objective was to provide temporal property verification features for eb 3 , we focused our attention on LNT, which is one of the input languages accepted by the CADP verification toolbox [START_REF] Garavel | CADP 2010: A toolbox for the construction and analysis of distributed processes[END_REF], and hence is equipped with on-the-fly model checking for action-based, branching-time logics involving data.

At first sight, given that eb 3 has structured operational semantics based on a labelled transition system (LTS) model, its translation to a process algebra may seem straightforward. However, this exercise proved to be rather complex, the main difficulty being to translate a history-based language to a process algebra with standard LTS semantics. To overcome this difficulty, we considered alternative memory-based semantics of eb 3 [START_REF] Vekris | Efficient Operational Semantics for eb 3 for Verification of Temporal Properties[END_REF], which were shown to be equivalent to the original trace-based semantics defined for finite-state systems in [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF]. Another important ingredient of the translation was the multiway value-passing rendezvous of LNT, which enabled to obtain a one-to-one correspondence between the transitions of the two LTSs underlying the eb 3 and LNT descriptions, and hence to preserve strong bisimulation. The presence of array types and of usual programming language constructs (e.g., loops and conditionals) in LNT was also helpful for specifying the memory, the Kleene star-closure operators, and the eb 3 guarded expressions containing attribute function calls. At last,

= P (x) = E E ::= λ | α (v) | E1.E2 | E1 | E2 | E0 * | E1 |[∆]| E2 | |x : V : E0 | |[∆]|x : V : E0 | C ⇒ E | P (v)
Fig. 1. eb 3 syntax the constructed data types and pattern-matching mechanisms of LNT enabled a natural description of eb 3 data types and attribute functions. We implemented our translation in the eb 3 2lnt tool, thus making possible the analysis of eb 3 specifications using all the state-of-the-art features of the CADP toolbox, in particular the verification of data-based temporal properties expressed in MCL [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] using the on-the-fly model checker EVALUATOR 4.0.

The paper is organized as follows. Sections 2 and 3 give an overview of the eb 3 and LNT languages, respectively. Section 4 presents our translation from eb 3 to LNT, implemented by the eb 3 2lnt translator. Section 5 shows how eb 3 2lnt and CADP can be used for verifying the correctness requirements of an IS. Finally, Section 6 summarizes the results and draws up lines for future work.

2 The Language EB 3 The eb 3 method has been specially designed to specify the functional behaviour of ISs. A standard eb 3 specification comprises (1) a class diagram representing entity types and associations for the IS being specified, (2) a process algebra specification, denoted by main, describing the IS, i.e., the valid traces of execution describing its behaviour, (3) a set of attribute function definitions, which are recursive functions on the system execution trace, and (4) input/output rules to specify outputs for input traces, or SQL expressions used to specify queries on the class diagram. We limit the presentation to the process algebra and the set of attribute functions. The eb 3 syntax is presented in Figure 1 and the eb 3 trace semantics Sem T [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] are given in Figure 2 as a set of rules named T 1 to T 11 . Both figures are commented below.

Process expressions. We write x, y, x 1 , x 2 , . . . for variables and v, w, v 1 , v 2 , . . . for data expressions over user-defined domains, such as integers, Booleans and more complex domains that we do not give formally, for conciseness. Expressions are built over variables, constants, and standard operations. We also use the overlined notation as a shorthand notation for lists, e.g., x denotes a list of variables x 1 , . . . , x n of arbitrary length. An eb 3 specification consists of a set of attribute function definitions A 1 , . . . , A n , and of a set of process definitions of the form "P (x) = E", where P is a process name and E is a process expression.

Let Act be a set of actions written ρ, ρ 1 , ρ 2 , . . . and Lab be a set of labels written α, α 1 , α 2 , . . . Each action ρ is either the internal action written λ, or a visible action of the form "α (v)", where α ∈ Lab. An action ρ is the simplest process expression, whose semantics are given by rule T 1 . The symbol √ (which is not part of the user syntax) denotes successful execution. The trace T (implicit in the presentation) of an eb 3 specification at a given moment consists of the sequence of visible actions executed since the start of the system. (Note therefore that λ does not appear in the trace.) At system start, the trace is empty. If T denotes the current trace and action ρ can be executed, then T.ρ denotes the trace just after executing ρ.

(T1) ρ ρ -→ √ (T7) E1 ρ -→ E ′ 1 E2 ρ -→ E ′ 2 E1 |[∆]| E2 ρ -→ E ′ 1 |[∆]| E ′ 2 in (ρ, ∆) (T2) E1 ρ -→ E ′ 1 E1.E2 ρ -→ E ′ 1 .E2 (T8) E1 ρ -→ E ′ 1 E1 |[∆]| E2 ρ -→ E ′ 1 |[∆]| E2 ¬in (ρ, ∆) (T3) E2 ρ -→ E ′ 2 √ .E2 ρ -→ E ′ 2 (T9) √ |[∆]| √ λ -→ √ (T4) E1 ρ -→ E ′ 1 E1 | E2 ρ -→ E ′ 1 (T10) E0 ρ -→ E ′ 0 C ⇒ E0 ρ -→ E ′ 0 C (T5) E0 * λ -→ √ (T11) E[x := v] ρ -→ E ′ P (v) ρ -→ E ′ P (x) = E (T6) E0 ρ -→ E ′ 0 E0 * ρ -→ E ′ 0 .E0 *
eb 3 processes can be combined with classical process algebra operators such as the sequence "E 1 .E 2 " (T 2 , T 3 ), the choice "E 1 | E 2 " (T 4 ) and the Kleene closure "E 0 * " (T 5 , T 6 ). Rules (T 7 to T 9 ) define parallel composition "E 1 |[∆]| E 2 " of E 1 , E 2 with synchronization on ∆ ⊆ Lab. The condition "in (ρ, ∆)" is true iff the label of ρ belongs to ∆. The symmetric rules for choice and parallel composition have been omitted for brevity. Expressions "E 1 ||| E 2 " and "

E 1 || E 2 " are equivalent respectively to "E 1 |[∅]| E 2 " and "E 1 |[Lab]| E 2 ".
The guarded expression process "C ⇒ E 0 " (T 10 ) can execute E 0 if the Boolean condition C holds, which is denoted by the side condition " C ". Since C may contain calls to attribute functions, its evaluation depends on the trace obtained up to the moment when the condition is evaluated. Note that the evaluation of the guard C and the execution of the first action ρ in E 0 are simultaneous, i.e., no action is allowed in concurrent processes in the meantime. We call this property the guard-action atomicity. This property is essential for consistency as, by side effects, the occurrence of actions in concurrent processes could implicitly change the value of C before the guarded action has been executed.

Quantification is permitted for choice and parallel

composition. If V is a set of expressions {v 1 , . . . , v n }, "|x : V : E 0 " and "|[∆]|x : V : E 0 " stand respectively for "E 0 [x := v 1 ] | . . . | E 0 [x := v n ]" and "E 0 [x := v 1 ] |[∆]| . . . |[∆]| E 0 [x := v n ]",
where "E[x := v]" denotes the replacement of all occurrences of x by v in E. For instance, "||x : {1, 2, 3} : a (x)" stands for "a (1) || a (2) || a (3)". At last, named processes can be instantiated as usual (T 11 ). Given an eb 3 process expression E, we write vars (E) for the set of variables occurring free in E.

Attribute functions. Attribute function definitions are denoted by the symbol A in the grammar of Figure 1. Attribute functions are defined recursively on the current trace T representing the history of actions executed, with the aid of functions last (T) which denotes the last action of the trace, and front (T) which denotes the trace without its last action. The symbol ⊥ represents the undefined value. In particular, both last (T) and front (T) match ⊥ when the trace is empty. The symbol (wildcard) matches all actions not matched by any of the preceding action patterns α 1 (x 1 ), . . . , α q (x q ). Each v i (i ∈ 0..n) is an expression of the same type as f 's return type built over the variables y ∪ x i .

For defining formal semantics for attribute functions, the rule system of Figure 2 has to be expanded with trace and memory contexts for each process, representing the sequence of actions executed since the process was initiated, and the value of attribute functions for the current trace and any value for the rest of their arguments, stored into process memory M. Due to space limitations, we do not present the formal semantics here, but show how attribute functions are evaluated on a concrete example. The formal trace-memory semantics for attribute functions can be found in the companion paper [START_REF] Vekris | Efficient Operational Semantics for eb 3 for Verification of Temporal Properties[END_REF].

Example. We give an example of how the trace-memory semantics work for a simplified library management system, whose specification (processes and attribute functions) in eb 3 is given in Figure 3. Process main is the parallel interleaving between m instances of process book and p instances of process member . Process book stands for a book acquisition followed by its eventual discard. The attribute function "borrower (T, bId )" looks for actions of the form "Lend (mId , bId )" or "Return (bId )" in the trace and returns the current borrower of book bId or ⊥ if the book is not lent. In process book, action "Discard (bId)" is thus guarded to guarantee that book bId cannot be discarded if it is currently lent. How the use of attribute functions enhances expressiveness in the eb 3 specification of Figure 3 is discussed in [START_REF] Vekris | Efficient Operational Semantics for eb 3 for Verification of Temporal Properties[END_REF].

We illustrate how the eb 3 specification describing the library management system is evaluated. The idea lies in the observation that attribute functions can be turned into state variables (the memory M) carrying the effect of the system trace on their corresponding values. This avoids keeping the (ever-growing) trace leading to a finite state model. If f (T,

x 1 : T 1 , . . . , x l : T l ) is an attribute function, we construct |T 1 | × . . . × |T l | state variables, where |T i | (i ∈ 1..l) stands for T i 's cardinality.
As an example, we set m = p = NbLoans = 2, i.e. we consider two books b if mId = borrower (T, bId ) then nbLoans (front (T), mId) -1 else nbLoans (front (T), mId) end if | : nbLoans (front (T), mId) end match Fig. 3. eb 3 specification of a library management system

(borrower [b 1 ], borrower [b 2 ], nbLoans[m 1 ], nbLoans[m 2 ]
). The first two cells keep the two values of the attribute function borrower (T, •) for a given trace T, and the last two keep the values of nbLoans (T, •). After every step, the new value of each cell can be calculated from the previous memory and the action that has just been executed. The memory is initially set to (⊥, ⊥, ⊥, ⊥). After the trace "Acquire (b 1 ).Acquire (b 2 ).Register (m 1 ).Register (m 2 )" the memory contains (⊥, ⊥, 0, 0). If action "Lend (b 1 , m 1 )" is then executed, the new memory is (m 1 , ⊥, 1, 0). For instance, the new value m 1 for borrower [b 1 ] is obtained from the rule "Lend (bId , mId ) : mId " in the definition of the attribute function borrower (see Fig. 3), and the new value 1 for nbLoans[m 1 ] by the rule "Lend (bId , mId ) : nbLoans (front (T), mId ) + 1" of the attribute function nbLoans, where the value of nbLoans (front (T), m 1 ) corresponds to the value of nbLoans[m 1 ] in the previous memory state (value 0).

The Language LNT

LNT aims at providing the best features of imperative and functional programming languages and value-passing process algebras. It has a user friendly syntax and formal operational semantics defined in terms of labeled transition systems (LTSs). LNT is supported by the LNT.OPEN tool of CADP, which allows the on-the-fly exploration of the LTS corresponding to an LNT specification.

B ::= stop | null | G (O1, . . . , On) where E | B1; B2 | if E then B1 else B2 end if | var x : T in B end var | x := E | | loop L in B end loop | break L | select B1 [] . . . [] Bn end select | par G1, . . . ,
We present the fragment of LNT that serves as the target of our translation. Its syntax is given in Figure 4. LNT terms denoted by B are built from actions, choice (select), conditional (if ), sequential composition (;), breakable loop (loop and break) and parallel composition (par). Communication is carried out by rendezvous on gates, written G, G 1 , . . . , G n , and may be guarded using Boolean conditions on the received values (where clause). LNT allows multiway rendezvous with bidirectional (send/receive) value exchange on the same gate occurrence, each offer O being either a send offer (!) or a receive offer (?), independently of the other offers. Expressions E are built from variables, type constructors, function applications and constants. Labels L identify loops, which can be escaped using "break L" from inside the loop body. Processes are parameterized by gates and data variables. LNT semantics are formally defined in SOS style in [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator -Version 5[END_REF].

4 Translation from EB 3 to LNT Principles. Our translation of eb 3 relies on the trace-memory semantics. Thus, we explicitly model in LNT a memory, which stores the state variables corresponding to attribute functions (we call these variables attribute variables) and is modified each time an action is executed.

Assuming n attribute functions f 1 , . . . , f n , we model the memory as a process M placed in parallel with the rest of the system (a common approach for modeling global variables in process algebras), which manages for each attribute function f i an attribute variable (also named f i ) that encodes the function. To read the values of these attribute variables (i.e., to evaluate the attribute functions), processes need to communicate with the memory M , and every action must have an immediate effect on the memory (so as to reflect the immediate effect on the execution trace). To achieve this, the memory process synchronizes with the rest of the system on every possible action of the system (including λ, to which we associate an LNT gate also written λ in abstract syntax for convenience), and updates its attribute variables accordingly. The list of attribute variables f = (f 1 , . . . , f n ) is added as a supplementary offer on each eb 3 action α (v), so that attribute variables can be directly accessed to evaluate the guard associated to the action, wherever needed, while guaranteeing the guard-action atomicity. Therefore, every action α (v) will be encoded in LNT as α (!v, ?f ), and synchronized with an action of the form α (?x, !f ) in the memory process M , thus taking benefit of bidirectional value exchange during the rendezvous.

Translation of attribute functions. To formalize the translation, we assume Lab = {α 1 , . . . , α q } (not including λ), each α j has formal parameters x j , {f 1 , . . . , f n } is the set of attribute functions, and each f i is uniquely defined by the set of formal parameters y i and the set of data expressions w 0 i , . . . , w q i , such that:

f i (T, y i ) = match last (T) with ⊥ : w 0 i | α 1 (x 1 ) : w 1 i | . . . | α q (x q ) : w q i
We also assume that the attribute functions are ordered, so that for all h ∈ 1..n, i ∈ 1..n, j ∈ 1..q, every function call of the form f h (T, . . .) occurring in w j i satisfies h < i and every call of the form f h (front (T), . . .) satisfies h ≥ i. Such an ordering can be constructed if the eb 3 specification does not contain circular dependencies between function calls, which would potentially lead to infinite attribute function evaluation. In particular, the definition of an attribute function f i cannot contain recursive calls of the form "f i (T, . . .)", but only recursive calls of the form "f i (front (T), . . .)". Note that this does not limit the expressiveness of eb 3 attribute functions, because every recursive computation on data expressions only (which keeps the trace unchanged) can be described using standard functions and not attribute functions.

Ordering attribute functions in this way allows the memory to be updated consistently, from f 1 to f n in turn. At every instant, already-updated values correspond to calls of the form f h (T, . . .) (the value of f h on the current trace), whereas calls of the form f h (front (T), . . .) are replaced by accesses to a copy f ′ of the memory f , which was made before starting the update. This encoding thus enables the trace parameter to be discharged from function calls, ensuring that while updating f i , accesses to f h with h < i necessarily correspond to calls with parameter T.

Process M is defined in Figure 5. It runs an infinite loop, which "listens" to all possible actions α j of the system. Each attribute variable f i is an array with l i dimensions, where l i is the arity of the attribute function f i minus 1 (because the trace parameter is now discharged). Each dimension of the array f i thus corresponds to one formal parameter in y i , so that f i [ord (v 1 )] . . . [ord (v li )] encodes the current value of f i (T, v 1 , . . . , v li ), where ord (v) is a predefined LNT function that denotes the ordinate of value v, i.e., a unique number between 1 and the cardinal of v's type. For each type T we assume the existence of functions first T that returns the first element of type T , last T that returns the last element of type T , and next T (x) that returns the successor of x in type T (following the total order induced by ord). Such functions are available in LNT for all finite types. Function mod transforms an expression E by syntactically replacing function calls by array accesses, while discharging the trace parameter as explained above.

Upon synchronisation on action α j (?x j , !f ) with the LNT process corresponding to eb 3 's main process (see translation of processes below), the values of all attribute variables f i (i ∈ 1..n) are updated using function upd j i .

process

) mod (E) . = E [ fi (T, vi) := fi[ord (vi)], fi (front (T), vi) := f ′ i [ord (vi)] | i ∈ 1.
.n ] Fig. 5. LNT code for the memory process implementing attribute functions Translation of processes. We define a translation function t from an eb 3 process expression to an LNT process. Most eb 3 constructs are process algebra constructs with a direct correspondence in LNT. The main difficulty arises in the translation of guarded process expressions of the form "C ⇒ E 0 " in a way that guarantees the guard-action atomicity. This led us to consider a second parameter for the translation function t, namely the condition C, whose evaluation is delayed until the first action occurring in the process expression E 0 . The definition of t (E, C) is given in Figure 6. An eb 3 specification E 0 will then be translated into "par α 1 , . . . , α q , λ in t (E 0 , true) || M [α 1 , . . . , α q , λ] end par" and every process definition of the form "P (x) = E" will be translated into the process "process P [α 1 , . . . , α q , λ : any] (x : type (x)) is t (E, true) end process", where {α 1 , . . . , α q } = Lab. The rules of Figure 6 can be commented as follows:

-Rule (1) translates the λ action. Note that λ cannot be translated to the empty LNT statement null, because execution of λ may depend on a guard C, whose evaluation requires the memory to be read, so as to get attribute variable values. This is done by the LNT communication action λ (?f ). The guard C is evaluated after replacing calls to attribute functions (all of which have the form f i (T, v i )) by the appropriate attribute variables, using function mod defined in Figure 5. Rule ( 2) is similar but handles visible actions.

t (λ, C) = λ (?f ) where mod (C) (1) t (α (v), C) = α (v, ?f ) where mod (C) (2) t (E1.E2, C) = t (E1, C); t (E2, true) (3) t (C ′ ⇒ E0, C) = t (E0, C andthen C ′ ) (4) t (E1 | E2, C) = select t (E1, C) [] t (E2, C) end select (5)
t (|x : V : E0, C) = var x := any V ; t (E0, C) end var (6)

t (E0 * , true) = loop LE 0 in select λ (?f ); break LE 0 [] t (E0, true) end select end loop (7) t (E1 |[∆]| E2, true) = par ∆ in t (E1, true) || t (E2, true) end par (8) t (|[∆]|x : V : E0, true) = par ∆ in E0[x := v1] || . . . || E0[x := vn] end par where V = {v1, . . . , vn} (9)
t (P (v), true) = P [α1, . . . , αq, λ] (v) [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] In all other cases: -Rule (9) translates eb 3 quantified parallel composition into LNT parallel composition by expanding the type V of the quantification variable, since LNT does not have a quantified parallel composition operator. -Rule (10) translates an eb 3 process call into the corresponding LNT process call, which requires gates to be passed as parameters. -Rules ( 7) to [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] only apply when the guard C is trivially true. In the other cases, we must apply rule [START_REF] Garavel | CADP 2010: A toolbox for the construction and analysis of distributed processes[END_REF], which generates code implementing the guard. If C does not use attribute functions, i.e., does not depend on the trace, then it can be evaluated immediately without communicating with the memory process (first case). Otherwise, the guard evaluation must be delayed until the first action of the process expression E 0 . When E 0 is either a Kleene closure, a parallel composition, or a process call, identifying its first action syntactically is not obvious. One solution would consist in expanding E 0 into a choice in which every branch has a fixed initial action3 , to which the guard would be added. We preferred an alternative solution that avoids the potential combinatorial explosion of code due to static expansion. A process pr C (defined in Fig. 7) is placed in parallel to t (E 0 , true) and both processes synchronize on all actions. Process pr C imposes on t (E 0 , true) the constraint that the first executed action must satisfy the condition C (then branch).

t (E0, C) = 8 > > > > > > < > > > > > > : if mod (C)
For subsequent actions, the condition is relaxed (else branch).

The following example illustrates and justifies the use of process pr C as a means to solve the guard-action atomicity problem. Consider the eb 3 system "C ⇒ Lend (b 1 , m 1 ) ||| Return (b 2 )", where C denotes the Boolean condition "borrower (T, b 1 ) = ⊥ ∧ nbLoans (T, m 1 ) < NbLoans" and Lab = {Lend, Return}. The LNT code corresponding to this system is the following:

par Lend, Return, λ in par Lend, Return, λ in par Lend (b 1 , m 1 , ?f ) || Return (b 2 , ?f ) end par || pr C [Lend , Return, λ] (b 1 , m 1 ) end par || M [Lend , Return, λ] end par
The first action executed by this system may be either Lend or Return. We consider the case where Lend is executed first. According to the LNT semantics, it results from the multiway synchronization of the following three actions:

-"Lend (b 1 , m 1 , ?f )" in the above expression, -"Lend (?b, ?m, ?f ) where borrower [ord(b 1 )] = ⊥ ∧ nbLoans[ord(m 1 )] <

NbLoans" in process pr C (at this moment, start is true, see Fig. 7), and -"Lend (?b, ?m, !f )" in process M (see Fig. 5). Thus, in pr C at synchronization time, f is an up-to-date copy of the memory stored in M , b = b 1 , and m = m 1 . The only condition for the synchronization to occur is the guard mod (C), whose value is computed using the up-to-date copy f of the memory. In case mod (C) evaluates to true, no other action (susceptible to modifying f ) can occur between the evaluation of mod (C) and the occurrence of Lend as both happen synchronously, thus achieving the guard-action atomicity. Once Lend has occurred, Return can occur without any condition, as the value of start has now become false.

t (E, true) ρ (x,f ) ----→ t (E ′ , true) ∧ (∀f i ∈ f ) (∀v) f i (T, v) = f i [ord (v)].
The proof strategy for Theorem 1 relies on the existence of a bisimulation between each eb 3 specification and its corresponding LNT translation. It works by providing a match between the reduction rules of eb 3 [START_REF] Vekris | Efficient Operational Semantics for eb 3 for Verification of Temporal Properties[END_REF] and the corresponding LNT rules [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator -Version 5[END_REF].

We developed an automatic translator tool from eb 3 specifications to LNT, named eb 3 2lnt, implemented using the Ocaml Lex/Yacc compiler construction technology. It consists of about 900 lines of OCaml code. We applied eb 3 2lnt on a benchmark of eb 3 specifications, which includes variations of the library management system (examined in its simplest version in Section 2) and a bank account management system.

We noticed that, for each eb 3 specification, the code size of the equivalent LNT specification is twice as big. Part of this expansion is caused by the fact that LNT is more structured than eb 3 : LNT requires more keywords and gates have to be declared and passed as parameters to each process call. By looking at the rules of Figure 6, we can see that the other causes of expansion are rule [START_REF] Chossart | Évaluation d'outils de vérification pour les spécifications de systèmes d'information[END_REF], which duplicates the condition C, and rule [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF], which duplicates the body E 0 of the quantified parallel composition operator "|[∆]|x : V : E 0 " as many times as there are elements in the set V . Both expansions are linear in the size of the source eb 3 code. However, in the case of a nested parallel composition "

|[∆ 1 ]|x 1 : V 1 : . . . |[∆ n ]|x n : V n : E 0 "
, the expansion factor is as high as the product of the number of elements in the respective sets V 1 , . . . , V n , which may be large. If E 0 is a big process expression, the expansion can be limited by encapsulating E 0 in a parameterized process "P E0 (x 1 , . . . , x n )" and replacing duplicated occurrences of E 0 by appropriate instances of P E0 .

Case Study

We illustrate below the application of the eb 3 2lnt translator in conjunction with CADP for analyzing an extended version of the IS library management system, whose description in eb 3 can be found in Annex C of [START_REF] Gervais | Combinaison de spécifications formelles pour la modélisation des systèmes d'information[END_REF]. With respect to the simplified version presented in Section 2, the IS enables e.g., members to renew their loans and to reserve books, and their reservations to be cancelled or transferred to other members on demand. The desired behaviour of this IS was characterized in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] as a set of 15 requirements expressed informally as follows:

R1. A book can always be acquired by the library when it is not currently acquired. R2. A book cannot be acquired by the library if it is already acquired.

R3. An acquired book can be discarded only if it is neither borrowed nor reserved. R4. A person must be a member of the library in order to borrow a book. R5. A book can be reserved only if it has been borrowed or already reserved by some member. R6. A book cannot be reserved by the member who is borrowing it. R7. A book cannot be reserved by a member who is reserving it. R8. A book cannot be lent to a member if it is reserved. R9. A member cannot renew a loan or give the book to another member if the book is reserved. R10. A member is allowed to take a reserved book only if he owns the oldest reservation. R11. A book can be taken only if it is not borrowed. R12. A member who has reserved a book can cancel the reservation at anytime before he takes it. R13. A member can relinquish library membership only when all his loans have been returned and all his reservations have either been used or cancelled. R14. Ultimately, there is always a procedure that enables a member to leave the library. R15. A member cannot borrow more than the loan limit defined at the system level for all users.

We expressed all the above requirements using the property specification language MCL [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF]. MCL is an extension of the alternation-free modal µ-calculus [START_REF] Emerson | Efficient Model Checking in Fragments of the Propositional Mu-Calculus[END_REF] with action predicates enabling value extraction, modalities containing extended regular expressions on transition sequences, quantified variables and parameterized fixed point operators, programming language constructs, and fairness operators encoding generalized Büchi automata. These features make possible a concise and intuitive description of safety, liveness, and fairness properties involving data, without sacrificing the efficiency of on-the-fly model checking, which has a linear-time complexity for the dataless MCL formulas [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF].

We show below the MCL formulation of two requirements from the list above, which denote typical safety and liveness properties. Requirement R2 is expressed in MCL as follows:

[ true * .{ACQUIRE ?B : string}.(not {DISCARD !B}) * .{ACQUIRE !B} ] false This formula uses the standard safety pattern "[β] false", which forbids the existence of transition sequences matching the regular formula β. Here the undesirable sequences are those containing two Acquire operations for the same book B without a Discard operation for B in the meantime. The regular formula true * matches a subsequence of (zero or more) transitions labeled by arbitrary actions. Note the use of the construct "?B : string", which matches any string and extracts its value in the variable B used later in the formula. Therefore, the above formula captures all occurrences of books carried by Acquire operations in the model. Requirement R12 is formulated in MCL as follows:

[ true * .{RESERVE ?M : string ?B : string}.

(not ({TAKE !M !B} or {TRANSFER !M !B})) * ] (not ({TAKE !M !B} or {TRANSFER !M !B})) * . {CANCEL !M !B} true
This formula denotes a liveness property of the form "[β 1 ] β 2 true", which states that every transition sequence matching the regular formula β 1 (in this case, book B has been reserved by member M and subsequently neither taken nor transferred) ends in a state from which there exists a transition sequence matching the regular formula β 2 this case, the reservation can be cancelled before being taken or transferred). Using eb 3 2lnt, we translated the eb 3 specification of the library management system to LNT. The resulting specification was checked against all the 15 requirements, formulated in MCL, using the EVALUATOR 4.0 model checker of CADP. The experiments were performed on an Intel(R) Core(TM) i7 CPU 880 at 3.07GHz. Table 1 shows the results for several configurations of the IS, obtained by instantiating the number of books (m) and members (p) in the IS. All requirements were shown to be valid on the IS specification. The second and third line of the table indicate the number of states and transitions of the LTS corresponding to the LNT specification. The fourth line gives the time needed to generate the LTS and the other lines give the verification time for each requirement. Note that the number of states generated increases with the size of m and p as EVALUATOR 4.0 applies explicit techniques for state space generation.

Conclusion

We proposed an approach for equipping the eb 3 method with formal verification capabilities by reusing already available model checking technology. Our approach relies upon a new translation from eb 3 to LNT, which provides a direct connection to all the state-of-the-art verification features of the CADP toolbox. The translation, based on alternative memory semantics of eb 3 [START_REF] Vekris | Efficient Operational Semantics for eb 3 for Verification of Temporal Properties[END_REF] instead of the original trace semantics [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF], was automated by the eb 3 2lnt translator and validated on several examples of typical ISs. So far, we experimented only the model checking of MCL data-based temporal properties on eb 3 specifications. However, CADP also provides extensive support for equivalence checking and compositional LTS construction, which can be of interest to IS designers.

As future work, we plan to provide a formal proof of the translation from eb 3 to LNT, which could serve as reference for translating eb 3 to other process algebras as well. We also plan to study abstraction techniques for verifying properties regardless of the number of entity instances that participate in the IS, following the approaches for parameterized model checking [START_REF] Abdulla | Handling Global Conditions in Parameterized System Verification[END_REF]. In particular, we will observe how the insertion of new functionalities into an IS affects this issue, and we will formalize this in the context of eb 3 specifications.

EB 3 :

 3 := A1; . . . ; An; S1; . . . ; Sm A ::= f (T : T , y : T ) : T = match last (T) with ⊥ : v0 | α1 (x1) : v1 | . . . | αq (xq) : vq [| : vq+1] S ::

Fig. 2 .

 2 Fig. 2. eb 3 trace semantics Sem T

  1 and b 2 , and two members m 1 and m 2 . The memory has four cells: M = BID = {b1, . . . , bm}, MID = {m1, . . . , mp} book (bId : BID) = Acquire (bId ) . (borrower (T, bId) = ⊥) ⇒ Discard (bId ) loan (mId : MID, bId : BID) = (borrower (T, bId ) = ⊥) ∧ (nbLoans (T, mId) < NbLoans ) ⇒ Lend (bId , mId ) . Return (bId ) member (mId : MID) = Register (mId) . (|||bId : BID : loan (mId, bId ) * ) . Unregister (mId) main = (|||bId : BID : book (bId ) * ) ||| (|||mId : MID : member (mId) * ) nbLoans (T : T , mId : MID) : Nat ⊥ = borrower (T : T , bId : BID) : MID ⊥ = match last (T) with match last (T) with ⊥ : ⊥ ⊥ : ⊥ | Lend (bId , mId) : | Lend (bId, mId) : mId nbLoans (front (T), mId) + 1 | Return (bId ) : ⊥ | Register (mId) : 0 | : borrower (front (T), bId ) | Unregister (mId) : ⊥ end match | Return (bId ) :

Fig. 4 .

 4 Fig. 4. LNT syntax (limited to the fragment used in this paper)

Fig. 6 .

 6 Fig. 6. Translation from eb 3 process to LNT process

Fig. 7 .

 7 Fig. 7. Process pr C

  M [α1, . . . , αq, λ : any] is var f , f ′ : type (f ), y1 : type (y1), . . . , yn : type (yn), x1 : type (x1), . . . , xq : type (xq) in

	upd 0 1 ; . . . ; upd 0 n ;
	loop
	f ′ := f (* f ′ i [ord (v)] will encode fi (front (T), v) during memory update *)
	select
	α1 (?x1, !f ); upd 1 1 ; . . . ; upd 1 n
	[] . . . []
	αq (?xq, !f ); upd q 1 ; . . . ; upd q n
	[] λ (!f )
	end select
	end loop
	end var
	end process upd j i . = enum (yi, fi[ord (yi)] := mod (w j i )) enum ([ ], B) . = B enum (x :: y, B) . = x := first

T ; loop Lx in enum (y, B) if x = lastT then x := next T (x) else break Lx end if end loop where T = type (x) v[ord (y)] . = v[ord (y1)] . . . [ord (y l )], ?y = (?y1, . . . , ?y l ), where y = (y1, . . . , y l

  then t (E0, true) else stop end if if C does not use attribute functions

	par α1, . . . , αq, λ in t (E0, true)	(11)
	|| pr C [α1, . . . , αq, λ] (vars (C))
	end par	otherwise

  process pr C [α1, . . . , αq, λ : any] (vars (C) : type (vars (C))) is var start : bool, x1 : type (x1), . . . , xq : type (xq) in

	start := true;
	loop L in select
	if start then
	start := false;
	select
	α1 (?x1, ?f ) where mod (C)
	[] . . . []
	αq (?xq, ?f ) where mod (C)
	[]
	λ (?f ) where mod (C)
	end select
	else
	select
	α1 (?x1, ?f )
	[] . . . []
	αq (?xq, ?f )
	[]
	λ (?f )
	end select
	end if
	[] break L end select end loop
	end var
	end process

Table 1 .

 1 Model checking results for the library management system

	(m, p) (3,2)	(3,3)	(3,4)	(4,3)
	states 1,002	182,266	8,269,754 27,204,016
	trans. 5,732 1,782,348 105,481,364 330,988,232
	time	1.9s	14.4s	31'39s	140'22s
	R1	0.3s	1.8s	5'19s	20'13s
	R2	0.2s	2.9s	9'26s	36'7s
	R3	0.2s	9.4s	97'46s	26'47s
	R4	0.2s	1.7s	5'15s	18'40s
	R5	0.2s	2.2s	6'46s	21'52s
	R6	0.2s	4.1s	38'30s	10'19s
	R7	0.2s	7.4s	65'22s	24'33s
	R8	0.2s	2.2s	6'52s	22'27s
	R9	0.2s	2.3s	6'38s	22'29s
	R10	0.3s	13.3s	43'59s	62'07s
	R11	0.3s	2.5s	6'36s	22'14s
	R12		4.0s	10'47s	45'09s
	R13	0.4s	4.3s	11'46s	1'07s
	R14	0.3s	3.6s	10'41s	37'33s
	R15	0.2s	2.8s	7'53s	28'56s

Such a form, commonly called head normal form[START_REF] Bergstra | Handbook of Process Algebra[END_REF], is used principally in the context of the process algebra ACP[START_REF] Bergstra | Algebra of Communicating Processes with Abstraction[END_REF] to analyse the behaviour of recursive processes.

⋆ Partially supported by selkis ANR Project. The LACL group is grateful to CON-VECS for its warm welcome to INRIA Grenoble in 2012 and wishes to thank all its members for useful advice and discussions.