In order to model ferromagnetic material in quasistatic PEEC method, a coupling with a volume integral equation is proposed. This coupling enables to take advantage of the strong points of each method. The modeling of complex conductor geometry is achieved thanks to PEEC method and magnetic materials are taken into account thanks to a volume integral equation. The coupling is carried out by introducing an impedance matrix (computed with PEEC method in the vacuum) within an integral magnetostatic equation solved by moment method..

I. INTRODUCTION

The PEEC method (Partial Element Equivalent Circuit) is mainly used for the modeling of complex interconnections and can be applied to a large range of devices where the air region is dominant [START_REF] Ruehli | Equivalent circuit models for three dimensional multiconductor systems[END_REF] (printed circuits, bus bars…). However, the classical PEEC method does not enable the 3D modeling of ferromagnetic materials widely present in devices (ferromagnetic shielding, disruptive magnetic masses, and cores of inductance). The magnetostatic moments method is well-known and derives from a volume integral equation solved by a point matching approach. It is particularly well adapted to model lightly very simple magnetic materials volume. Like the PEEC method, it does not require the meshing of the air region; on the other hand, it is limited to modeling of magnetostatic effects. Both methods are complementary. A strong coupling of them can be accomplished by modeling non conductive magnetic regions with a method of moments, while PEEC method allows the modeling the contributions of the inductors fed with alternative currents.

II. COUPLING PRINCIPLE

A. Magnetostatic moment method

Let us consider a non conductive magnetic material placed in an inductor field H0. The total magnetic field H is the sum of H0 and Hred,, the reaction of the material. A well-known integral volume equation links the local field to the magnetization of the whole material volume Vmat:

dV ) r r ) . ( 3 ( 4 1 Vmat 3 5      M r r M H H 0 (1)
where r is the vector linking the integration point to the point where the field is expressed, Vmat the ferromagnetic volume and M its magnetization. Usually, this integral is solved with a numerical technique. The easier way is to mesh the volume into n elements and to consider that the magnetization is uniform on each of them. Then, thanks to a point matching approach of the linear magnetic material's law at the center of each element, a linear matrix system is obtained. It remains to solve it, to obtain the magnetization of the whole volume Vmat. This method is usually called magnetostatic moment method. This formulation is known to suffer of some inaccuracies in some specific configurations [START_REF] Forsman | Influence of the Discrete Spaces an Integral Equation Formulations[END_REF]. However, the purpose of this paper is the coupling and very similar methodology can be applied to more sophisticated volume integral formulations.

Let's now assume that the inductor field is created by m unknown alternative currents I flowing in m conductors. In a very similar way to the previous one, we can get a linear system of equations. For instance, the equation associated to magnetic element k is:

j m i j V j 3 i n 1 i i _ Vmat 3 5 r dV I r 4 1 dV ) r r r ) . ( ( 4
1 1 j _ cond               r dl M r M M i i k (2)
where r is the relative permeability of the material. The second integral term correspond to the Biot and Savart's law integrated on each conductor volume Vcond_j. The global matrix system obtained has 6n equations (a vector complex equation per element) and 6n+2m unknowns (a vector complex magnetization per element plus m complex currents).

B. Inductive PEEC method

Let us consider m volume conductors fed with alternative sources placed in a surrounding air region without any magnetic materials. The well-known PEEC method is particularly reliable to solve this kind of problem. It is based on the determination of partial voltage generated on each conductor by electromagnetic sources. To compute these voltages volume integration on the conductor of the magnetic vector potential created by all the others conductor is provided. For instance, for the conductor k, the expression is [START_REF] Ruehli | Equivalent circuit models for three dimensional multiconductor systems[END_REF]:

k i V m 1 i V i i k 0 cond _ k dV ) dV r 1 s I ( s j 4 V k i         (3)
where  is the angular frequency and Si is the section of the ith conductor. This equation links partial voltages of conductors to currents flowing in them. If we write this equation for all conductors, we get a matrix system known as impedance matrix system. By combing these electromagnetic equations with the circuit ones representative of the conductors wiring and adding resistance source effect, it is possible to get a simplified system representative of the device which can be easily coupled with a standard circuit simulator. This inductive PEEC method has already shown is efficiency for the modeling of complex conductor geometries in comparison with FEM.

Let us now consider that linear ferromagnetic materials are present in the surrounding air region. Equation (3) has to be Numerical experimentations on the coupling between PEEC and volume integral method Tung Le Duc, Olivier Chadebec, Jean-Michel Guichon, Gérard Meunier, Yves Lembeye, Benoit Delinchant Grenoble Electrical Engineering Laboratory, Grenoble-INP / Université Joseph Fourier / CNRS ENSE 3 , BP46, 38402 Grenoble, France modified by taking into account the influence of the field created by the material. In fact, like in the first approach, we have to integrate the magnetic vector potential on the volume conductor k. A new voltage has to be added to the previous one, not generated by the current but by the magnetization [START_REF] Antonini | PEEC Modeling of Linear Magnetic Materials[END_REF].

k V i n 1 i V 3 k 0 mat _ k dV . ) dV r ( s j 4 V k i k i u r M          (4)
Finally, equations (3), ( 4) and (5) are brought together in a global square (6n+2m)×(6n+2m) matrix system:

                    V 0 I M L L BS MoM standard M (5)
where MoM is the standard moments matrix (first two rearranged term of equation ( 2), BS is the Biot and Savart integral term (last term of ( 2)), LM is the influence of magnetization on conductors in PEEC approach (equation ( 4)) and Lstandard the classical inductive and resistive PEEC matrix. By taking into account circuit equations, it is possible to reduce (5) to get a lighter system and to solve it to get magnetizations and currents in conductors.

III. NUMERICAL EXAMPLES

We consider two numerical examples (Fig. 1.). For both, three numerical methods are compared. The first one is the scalar magnetic potential FEM coupled with circuit equations. In this modeling, a special care is given to the mesh around both conductors to ensure accurate results. The second one is a coupling between PEEC to model inductances and FEM to take into account the ferromagnetic material. This approach has already shown its good accuracy with a reduced number of elements in comparison with standard FEM [START_REF] Tran | FEM-PEEC coupled method for modeling solid conductors in the presence of ferromagnetic material[END_REF]. The last one is the considered coupling.

In the first example, two conductors are considered with a ferromagnetic bar (r =1000, linear) placed between them (Fig. 1, left).The first conductor is fed by a voltage source (1V, 1 kHz). The second one is in short circuit mode. To compare different approaches, we focus on the computed current in the second conductor with different meshes for the three approaches (see table I). Whereas the convergence is quickly reached with the MEF/PEEC method, the problem needs a very fine mesh to be accurately solved with FEM. We can see a small difference between both computed values. It can be explained by a small difference in the modelling method used to represent conductors Results provided by our coupling are very encouraging, the convergence being reached with a very few number of elements (around 200). Of course, the obtained matrix is fully dense, but the computation time is divided per one hundred in comparison with FEM and ten with PEEC/FEM. Moreover, no specific mesh refinement has been needed. The second test case is an inductance of microphone converter. It is composed of a complex-shaped conductor and of two ferrite parts (Fig. 1., right). In our study, the conductor is fed by a voltage source (1V, 10 kHz) and the ferrite is considered as linear with a permeability of 1000. Values of currents are still compared. Results seem to be not so good for the coupling MoM / PEEC especially if we have a look to the imaginary part of the current. This inaccuracy is mainly due to the small distance between conductors and the magnetic material, leading to important variation of magnetization in the neighborhood of currents. This configuration benefits FEM in comparison with our coupling. A good improvement would certainly be to couple PEEC with a more sophisticated implementation of the volume integral equation.

IV. CONCLUSION

In this paper, we have presented a coupling between PEEC and an integral volume equation. Our approach can be very fast and accurate and enables the introduction of linear magnetic material in PEEC methodology. It is particularly capable for the modeling of complex shapes conductors and relatively simple magnetic material geometry.

Fig. 1 .

 1 Fig.1. Geometry of both tested numerical cases.

TABLE I .

 I Currents values obtained (A)

		MEF
	Nb of elements	230.000	600.000	1.000.000
	Current values	-36.25+6,00i	-32.47+7,94i	-32.61+7.87i
		MEF/PEEC
	Nb of elements	60.000	150.000
	Current values	-32.60+8,38i	-32.50+8.34
		MoM/PEEC
	Nb of elements	32	126	392
	Current values	35.97+8,95i	-32.94+8.34i	-32.70+8.32i

TABLE II

 II

		. Currents values obtained (A)
	FEM	FEM/PEEC	MoM/PEEC
	100.000 elements	30.000 elements	2000 elements
	14,36 -1,97i	14,39 -1,85i	14,43 -1,68i


P Enciu

F Wurtz

L Gerbaud

B Delinchant

AD for Optimization in Electromagnetism Applied to Semi-Analytical Models Combining Composed Functions

Keywords: Automatic Differentiation, Gradient Constrained Optimization, Software Environment for Optimization, Semi-analytical models

This paper deals with Automatic Differentiation, for the device sizing in electromagnetism by using gradient constrained optimization. CADES framework (Component Architecture for the Design of Engineering Systems), previously described, is presented here with extended features.

Design/Methodology/Approach

The paper is subject to further usage for optimization of Automatic Differentiation (also named Algorithmic Differentiation) which is a powerful technique that computes derivatives of functions described as computer programs in a programming language like C/C++, FORTRAN.

Findings

Indeed, analytical modeling is well suited regarding optimization procedure, but the modeling of complex devices needs sometimes numerical formulations. This paper then reviews the "External Functions" and the so called "External Function of Function" modeling concepts implemented in CADES which aim to manage the interactions of analytical and numerical modeling inside of gradient based optimization procedure. Finally, the paper shows that Automatic Differentiation has no limit for the input program complexity, or gradients accuracy, in the context of constrained optimization of an electromagnetic actuator.

Originality/value

Automatic Differentiated is employed for a large and complex numerical code computing multidimensional integrals of functions. Thus, the paper intends to prove the Automatic Differentiation capabilities in the context of electromagnetic device sizing by means of gradient optimization. The code complexity as also as the implications of Automatic Differentiation usage may stand as a good reference for the researchers in this field area.

I. INTRODUCTION

In electromagnetism, the device sizing has often to be carried out by using optimization procedures. The models are very constrained, with numerous parameters, so, the gradient based optimization algorithms are considered e.g. the Sequential Quadratic Programming (SQP) [START_REF] Gloud | A second derivative SQP method: local convergence[END_REF]. Such algorithms need accurately valued gradients.

Basically, the designer may use explicit analytical formulas to describe sizing mathematical models. In large-scale computational models, the objective functions may not be available in analytical form, but given by a computer program or by routines implementing numerical algorithms. These algorithms can implement numerical methods like integration of functions, solvers of non-linear implicit systems of equations, etc… The analytical parts of models interacting with the numerical modules, yields a semi-analytical model. A real difficulty may happen to calculate those partial derivatives of the constrained output variables with respect to optimizable inputs when they are linked by a numerical algorithm or computer program. For example, computing the exact derivatives of an objective function computed by a computer program with thousands of code lines simulating the electromagnetic field in a 3D given geometry may be the origin of serious problems.

Several large scale differentiation techniques may be used to accomplish the differentiation task.

The traditional way in electromagnetism to compute derivatives is the Finite Differences method such as:

(1) This method seems simple, however a suitably chosen step is far to be simple, playing a crucial role for derivatives accuracy. Some studies [START_REF] Delinchant | Reducing Sensitivity Analysis Time-Cost of the Compound Model[END_REF] show that if the derivatives are not accurately valued, the efficiency of gradient based algorithms decreases considerably.

The symbolic differentiation can be used (Mathematica [START_REF] Wolfram | The Mathematica Book[END_REF], Macsyma [START_REF] Petti | Introduction to Macsyma[END_REF], Maple [START_REF] Kofler | Maple: An Introduction and Reference[END_REF] ). Whereas accurate, this approach is limited by the fact that the representation of the differentiated expression grows fast with the number of input variables. Furthermore, this approach is limited to symbolic expressions and cannot differentiate algorithms.

Contrary to the previously presented methods, the Automatic Differentiation (AD) [START_REF] Griewank | Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation[END_REF]Bucker and Hovland, 2000) is accurate up to machine precision, minimal in terms of human computation effort, efficient in terms of running time and applicable for large algorithms. The purpose of this work is to use AD in the context of electromagnetic devices sizing like in [START_REF] Fischer | Using Automatic Code Differentiation for Optimization[END_REF], which is a study of automatic differentiation application for optimization of electrical devices where only explicit defined mathematical equations are treated. The present paper deals with the further application of AD, especially to differentiate algorithms. Firstly, a brief presentation of the existing AD techniques will be made.

Secondly, a special architecture implemented in a software for optimization, called CADES [START_REF] Delinchant | An optimizer using the software component paradigm for the optimization of engineering systems[END_REF], is presented. It combines both analytical and numerical parts of a sizing model. Finally, a gradient constrained optimization application of a semi-analytical electromagnetic model is presented.

II. INTRODUCTION TO AUTOMATIC DIFFERENTIATION

The Automatic Differentiation (AD), is a term applied to a collection of techniques for automatically producing derivative codes of functions implemented in a high-level computer language, such C/C++ or FORTRAN. AD analyses the program functions and the operators and systematically applies the differentiation rules, notably the chain rule, to value error free derivatives.

An automatic differentiator could be a pre-compiler that analyzes the source code and generates a new program that computes both output and derivative values for any user defined set of inputs. Such a technique namely Automatic Differentiation by Source-to-Source (see Fig. 1) is implemented in packages such TAPENADE [START_REF] Hascoet | TAPENADE 2.1 user's guide[END_REF], ADIC [START_REF] Bischof | ADIC: An Extensible Automatic Differentiation Tool for ANSI-C[END_REF], ADIFOR [START_REF] Bischof | ADIFOR 2.0: Automatic Differentiation of FORTRAN 77 Programs[END_REF] An automatic differentiator could instrument the routines of an initial code in order to be differentiated. Such tools demand some minor modifications of the initial source. Generally these tools implement this strategy by using the operator overloading capacities of certain high-level programming languages such C++, FORTRAN 90. The overloaded operators and operands of each arithmetic operation and elementary function are recorded on a "tape" (Fig. 2). Tapes are subsequently interpreted to provide the required derivatives. The most straightforward AD technique is perhaps based on operator overloading. Such representative tools are CppAD (CppAD 2008), FADBAD/TADIFF [START_REF] Bendtsen | FADBAD, a Flexible C++ Package for Automatic Differentiation[END_REF], ADOL-C [START_REF] Walter | working paper, ADOL-C: A Package for the Automatic Differentiation of Algorithms Written in C/C++[END_REF]

… P 0 x ) x ( F 0 P' 0 x ) x ( F 0 ) x ( x F 0   x  AD pre-compiler
int i; if(x[1]>2) a = x[1] + x[2]; else a = x[1]*x[2]
;

for(i = 1; i<=2; i++) a = a * x[i]; y[1] = a/x[2]; y[2] = sin(x[2]); end function f; X[1] y[1] y[2] X[2]
f temporary variable : a a. The trace building is slow [START_REF] Gay | Semiautomatic Differentiation for Efficient Gradient Computations[END_REF], but once it is constructed, it may be reused further with different sets of inputs. In ADOL-C this may be done by calling special functions, e.g., fov_forward, Fig. 4.b (for First Order Vectorial differentiation in forward mode) that succeeds only if all logical operations of the initial code yield the same result (e.g.: the tape in This discussion shows that the principles underlying AD are not complicated for the computation of first order derivatives, but they can also be easily generalized to the computation of univariate Taylor series or Hessians and multivariate high-order derivatives.

[1]<<=x0[1]; x[2]<<=x0[2];//independents if(x[1]>2) a = x[1] + x[2]; else a = x[1]*x[2]; for(i = 1; i<=2; i++) a = a * x[i]; y[1] = a/x[2]; y[2] = sin(x[2]); y[1]<<=y0[1]; y[2]<<=y0[2];//
1 [ x ] 2 [ x *  * \ sin ] 2 [ x ] 1 [ x a   ] 2 [ x ] 1 [ x ]) 2 [ x ], 1 [ x ( a         a * ] 1 [ x a  a * ] 1 [ x ] 1 [ x * a ) a ], 1 [ x ( * a        a * ] 2 [ x a  a * ] 2 [ x ] 2 [ x * a ) a ], 2 [ x ( * a        ] 2 [ x / a ] 1 [ y  ] 2 [ x * ]) 2 [ x * ] 2 [ x ( \ a a * ] 2 [ x \ 1 ]) 2 [ x , a ( \ ] 1 [ y         ]) 2 [ x sin( ] 2 [ y  ] 2 [ x * ]) 2 [ x cos( ]) 2 [ x sin( ] 2 [ y      ) 0 , 1 ( ] 1 [ x   ) 1 , 0 ( ] 2 [ x   3 ] 1 [ x ] 1 [ 0 x   2 ] 2 [ x ] 2 [ 0 x   0 : tape a.

III. ARCHITECTURE STRATEGY FOR SEMI-ANALYTICAL MODELS

In paper [START_REF] Delinchant | An optimizer using the software component paradigm for the optimization of engineering systems[END_REF], the authors describe CADES framework (Component Architecture for Design of Engineering Systems), a software environment designed to size and optimize engineering devices and systems. Its design pattern (Fig. 5) that formalizes the entire design process is made of: a mathematical model description in the language sml (for System Modelling Language) [START_REF] Delinchant | An optimizer using the software component paradigm for the optimization of engineering systems[END_REF],, a model analysis by Generators that create software Calculation Components (models) and the use of these components in services (e.g. optimisation, calculation…).

The sml language syntax is based on the analytical model description made of algebraic equations and explicitly defined functions. However, this simple description may be limited in electromagnetics. Models using numerical methods, or kind of various numerical algorithms can be seen as a further model completion. The paper names them semi-analytical models.

This section focuses on the features of numerically computed external functions and external functions of functions that interact with the analytical model. The description of analytical models is carried out in the sml language, with the following instructions:

 scalar constants and variables of double precision (R0, rho, L, S, etc…).

 basic arithmetic operators (+, -, *, /);  basic mathematical functions (trigonometric, logarithmic, etc… functions );

 user defined internal functions (like R(x));

Model components which are required to carry out the model computation, are automatically produced with respect to a set of rules according to ICAr norm [START_REF] Delinchant | An optimizer using the software component paradigm for the optimization of engineering systems[END_REF].

From the previous example, the resistance dependence on temperature can be defined with a numerical algorithm that interpolates some measurement values. As shown in Fig. 6, an external function is a function numerically computed outside the analytical model (e.g. in C or Java language). Note that for further optimization with gradient optimization algorithms like SQP, the jacobian of such an external numerical code is needed and several approaches might be used as shown in Fig. 6.

B. Semi-analytical modeling using the external functions of functions.

Another semi-analytical form lays on external functions of functions (extension of the previous formalism). On the example of Fig. 5, suppose that the conductor surface changes like in Fig. 7.a. The external numerical code computes the integral functional in (2).

(2) Such a function of functions is translated into sml language as (3):

(3)

Note that this syntax approach is formalized and the concerned elements are :

 integral -the name of the function of functions; this function is implementing a numerical algorithm. (4)

or "derive()" (like in (5)):

(5) permit to calculate this function values and partial derivatives respectively at different points (e.g.: in (4) and ( 5) at the integration bounds, 0 and "L") required by the numerical routine (here "integral"). Thus, a connection is established back (here from "integral") with the analytical model (here "invS", arrow 2 in Fig. 8.a)

and thus the function of functions strategy is based on the call back functions formalism.

 "_"is used, in the sml language, to notify the variable argument position among other arguments of argument function (in Fig. 9 the second argument of

"invS").   L 0 ) L , 0 _), , a ( invS ( egral int dx ) x , a ( invS

C. The integral differentiation reference

The numerical integration algorithms used in this paper are Cuhre (for n>1 dimensions) and Sympson (for n=1 dimensions), both implemented in Cuba library [START_REF] Hahn | Cuba: a library for multidimensional numerical integration[END_REF]. This subsection aims to define exact formulations for the partial derivatives of such integrals in order to achieve a strong reference.

Let consider the general k-dimension integral in (8), where represents the integral result, being a functional depending on the integration bounds and on the nonintegrable parameters, :

Translated into sml language as:

Here, the paper focuses on computing the partial derivatives of the integral with respect to its bounds and to the non-integrable parameters, like in ( 9) and ( 10).

(9) (10)

Resuming the Cuhre algorithm, it consists in several integrand valuations at discrete points between the lower and the upper bounds. Thanks to functions of functions formalism, the value of the integrand is:

On the other hand, the integrand in ( 10), at the lower bound, is:

A special attention was carried out for the case when the bounds are functions of nonintegrable parameters. A new formulation of the relation in ( 10) yields in this case, to:

IV. THE DESIGN OF AN ELECTROMAGNTIC DEVICE

Here, an electromagnetic actuator applied for a deformable mirror for astronomy adaptive optic [START_REF] Delinchant | Two-levels modelling for the optimization of electromagnetic actuators[END_REF][START_REF] Cugat | Deformable magnetic mirror for adaptive optics: technological aspects[END_REF] is proposed for being sized by gradient constrained optimization. Its model is semi-analytical with numerical integrals, using the Cuba library. Two approaches are considered for differentiation.

First, the analytical part of the sizing model is symbolically differentiated, using the differentiation engine implemented in CADES. The numerical integration algorithm is differentiated by hand (see subsection C above). This approach is considered the reference for the optimization final solutions.

Second, the entire semi-analytical model is differentiated using an AD tool (i.e. ADOL-C).

The same SQP optimization algorithm (i.e. VF13 [START_REF] Gloud | A second derivative SQP method: local convergence[END_REF]) is used for optimization.

So, the approaches differ only for differentiation.

A. Micro-actuator for deformable mirror

Here, a deformable mirror reflector actuated by a matrix of several identical microactuators is considered. Each actuator, separately controlled, is supposed to avoid image deformations. This device represents a specific application for adaptive optic [START_REF] Cugat | Deformable magnetic mirror for adaptive optics: technological aspects[END_REF]. The semi-analytical modeling of each electromagnetic micro-actuator is based on integral formulations for the force acting on the magnet in the electromagnetic field produced by the coil. For the coil shape (see Fig. 10), the Biot-Savard law calculates the magnetic field. We are particularly interested by the field component in the z-axis:

(11)
where represents a functional related to coil shape.

The force acting on the magnet, produced by the field in ( 11) is calculated by applying the equivalent surface charges method [START_REF] De Medeiros | Comparison of Global Force Calculations on Permanent Magnets[END_REF], like electrostatic devices, as in ( 12):

(12)
Only the z-component of this force will be used in the modeling approach.

Note the influence of the coil field on the magnet is completely ignored. So the magnet magnetization is considered homogenous and constant, making this formulation deficient in terms of accuracy.

B. The optimization goal

The aim of the optimization of the electromagnetic device in Fig. 10, is to reach a fixed actuating force at air Gap=0.5mm of 30mN, in order to limit the mirror deformability, with a minimal magnet volume. The variation range of geometrical parameters is restricted to the device validity domain. Without such safety measures, the optimization may go out of scope.

The initial values, as also the specifications, are reported in the table below.

C. Automatic Differentiation strategy of the integration algorithm

The integration algorithmsthe Cuhre and Sympson routines of the Cuba integration library, are instrumented with ADOL-C tool package, in order to be differentiated in the sense of calculating the partial derivatives in ( 9) and (10). The major changes made to the initial algorithm for differentiation, are listed below:

 Convert to C++. Certain header files (originally written in C) were converted to a form acceptable by C++.

 Changes to derivative type. All the variable types was changed from (float/double) to ADOL-C derivative type, adouble.

 Declaring the independent variables. The variables defining the integration bounds ( ) were declared as active independent variables.

 Taping the active section. The integration algorithm was called between the special functions "trace_on()" and "trace_off()".

 Declaring the dependent variables. The variables defining the integration result were defined as active dependent variables.

Regarding the complexity of the integration algorithm used in this paper [START_REF] Hahn | Cuba: a library for multidimensional numerical integration[END_REF],

we tend to consider it enough to demonstrate the actual capacities of AD. Many imbricated loops, conditional branches, integrands called thousands of times since the desired convergence is achieved, represent a short review that could measure this algorithm complexity.

D. Optimization results

In this subsection, a comparative study is done between the two differentiation strategies applied for the integrals in ( 11) and ( 12) that define the constrained force acting on the magnet. This formulation consists in calculating a two dimension integral of an integrand function valuating another one dimension integral. In order to check the robustness of the Automatic Differentiation capabilities, successive optimizations were applied for the same structure with the same specifications varying the coil radius in the range 0…0.9 mm. Outside this range, no solution was found for the both differentiation approaches since the validity domain of the device is no longer respected. In Fig. 13 are reported the optimization results by differentiating the integrals in ( 12) and ( 13) using AD and the reference approach. There are no major errors between the optimization solutions.

a.

b. In the paper, it is shown that a minimal human computational effort is required when differentiating a numerical code. More, no user knowledge is required for the algorithm in cause. The gradient accuracy obtained with AD is validated within the optimization of an electromagnetic actuator. In comparison with a reference approach, the values of the derivatives computed in double precision by AD agree to at least four digits. Such accuracy is acceptable for an SQP optimization algorithm since the solution as also as the iterations number is quite identical.

However, the running of the derivative code implemented with ADOL-C tends to be slower than the reference approach case.

A special architecture is proposed in this paper to handle the interaction between the analytical part describing a sizing model and the numerical codes within a software environment designed for sizing. Situations when such functions of functions are useful might be when the external function is supposed to compute an integral, or an implicit solver [START_REF] Enciu | Automatic Differentiation for Sensitivity Calculation in Electromagnetism: Application to Algorithms[END_REF], minimizations/maximizations of functions…

Fig. 1 .

 1 Fig. 1. Source-to-source AD technique.

Fig. 2 .

 2 Fig. 2. Tape storage AD techniqueAlmost all the AD tools existing in the literature implement two modes of differentiation, i.e. the forward mode and the reverse mode. In the following sub-sections, only the forward mode is explained using ADOL-C.

  dependents trace_off();//end tape buffer end function f; b.

Fig. 3 .

 3 Fig. 3. Example code for AD. a.: Initial Code b.: The instrumented code with ADOL-C The tape is the computer representation of the calling graph (see Fig. 4.a.). Since the tape construction is made at run time, it contains no branch and all loops are unrolled. The forward mode of differentiation means that both function and derivatives valuation are made in the same direction (from bottom to the top of the function graph).

]

Fig. 4 .

 4 Fig. 4. The AD tape. a.: The tape containing the overloaded operators for the forward mode. b.: Procedure used to reuse the tape in order to value derivatives

  Fig. 4.a changes if). Otherwise, the retaping is imposed by recalling the routine

Fig. 5 .

 5 Fig. 5. The chain generation of an analytical model.

  Cuhre.jar "; //import external code invS(a,x) = 1/(1+a*x*cos(x)*cos(x));//inverse of section fct R0 = rho*integral(invS(a,_),0,L);//fct. of fct. usage R(x) = = R0*(1+A*x+B*pow(x,2)); //Res. vs. temperature U = R(T)*I; //Ohm law;

Fig. 7 .

 7 Fig. 7. The external functions of functions. a.: Conductor shape; application to integral. b.: Semianalytical model calling external function of functions.



  Fig. 8.a). In the integral case, this function represents the integrand.

Fig. 8 .

 8 Fig. 8. Argument function: a.: strategy b.: architecture This special argument function is represented by an instance of a class implementing the interface of Fig. 8.b. The methods such "compute()"(like in (4)):

Fig. 9 .

 9 Fig. 9. Variables mapping in the integral case

  Fig. 10. Deformable mirror system and micro-actuator.

Fig. 11 .

 11 Fig. 11. Partial derivatives and errors obtained in the both considered approachesFor a set of model parameters arbitrary chosen in Fig.11, it is obvious that AD yields the same partial derivatives, as the considered reference approach. The maximum relative error for plotted partial derivatives in Fig.11, is 0.18%. Such error is acceptable for a gradient based optimization algorithm, its global convergence being not affected.In Fig.12, the initial and the final configuration obtained for the studied device are indicated. The objective value is obtained with a precision of . The optimization

Fig. 13 .

 13 Fig. 13. Optimization results for the robustness test: a.: The variation of volumic force and objective function when varying the magnet radius. b.: The error obtained for the objective function (magnet voulume) within the both differentiation approaches.

trace_on(0);//starting tape buffer x

	function f(adouble x[],double x0[]):
	return double y0[]
	begin function f:
	adouble a, y[2];
	int i;

TABLE I

 I

		THE OPTIMIZATION SPECIFICATIONS
	Parameter	Description	Unit	Value	Type
	Coil_W	Coil Width	mm	1	fixed
	Coil_H	Coil High	mm	1	fixed
	Coil_R	Coil Radius	mm	1	fixed
	J	Current Density	A/mm	100	fixed
	Mz	Magnetization	T	1	fixed
	Gap	Air gap	mm	0.5	fixed
	Mag_R	Magnet Radius	mm	0.5	Constrained [0.001,1]
	Mag_W	Magnet Width	mm	0.5	Constrained [0.1, 3]
	Mag_FF	Magnet Form Factor	-	0.25	Constrained [0.01, 1]
	prec	Integration accuracy	-	1e-5	fixed
	Mag_force The force on magnet	mN	30	fixed


Gwen Salaun

Jeff Kramer
email: j.kramer@imperial.ac.uk

Frederic Lang
email: frederic.lang@inria.fr

Jeff Magee
email: j.magee@imperial.ac.uk

Gwen Salaün

Frédéric Lang

Translating FSP into LOTOS and Networks of Automata

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Process calculi (or process algebras) are abstract description languages to specify concurrent systems. The process algebra community has been working on this topic for 25 years and many different calculi have been proposed. At the same time, several toolboxes have been implemented to support the design and verification of systems specified with process calculi. However, although they are based on the same kernel of operators, most of them are incompatible in practice. In addition, there is no connection between calculi and very few bridges between existing verification tools. Our goal is to reduce the gap between the different formalisms, and to propose some bridges between existing tools to make their joint use possible.

We focus here on the process calculi Fsp and Lotos. Fsp [START_REF] Magee | Concurrency: State Models & Java Programs[END_REF] is a widely-used and expressive process calculus conceived to make the writing of specifications easier and concise. Fsp is supported by Ltsa, a user-friendly tool which allows to compile Fsp specifications into finite state machines known as LTSs (Labelled Transition Systems), to visualise and animate LTSs through graphical interfaces, and to verify LTL properties. On the other hand, Lotos is an ISO standard [START_REF] Iso | Lotos: a Formal Description Technique based on the Temporal Ordering of Observational Behaviour[END_REF],

which has been applied successfully to many application domains. Lotos is more structured than Fsp, and then adequate to specify complex systems possibly involving data types. Lotos is equipped with Cadp [START_REF] Garavel | An Overview of Cadp 2001[END_REF], a verification toolbox for asynchronous concurrent systems. Cadp allows to deal with very large state spaces, and implements various verification techniques such as model checking, compositional verification, equivalence checking, distributed model checking, etc.

To sum up, the simplicity of Fsp makes it very accessible to everyone, whereas Lotos requires a better level of expertise. In addition, Cadp is a rich and efficient verification toolbox which can complement basic analysis possible with Ltsa. We propose to translate Fsp specifications into Lotos to enable Fsp users to access the verification means available in the Cadp toolbox. Since some Fsp constructs for composite processes are difficult to encode into Lotos (for instance synchronisations between complex labels or priorities), they have been encoded into the Exp format which is another input format of Cadp. Exp allows the description of networks of automata using parallel composition, but also supports renaming, hiding and priorities.

Our goal is not to replace Ltsa, since Ltsa is convenient to debug and visualise graphically simple examples, but to extend it with supplementary verification techniques such as those mentioned before. Furthermore, we choose a highlevel translation between process calculi, as most as possible, instead of low-level connections with Cadp (through the Open/Caesar application programming interface [START_REF] Garavel | Open/Caesar: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] for instance) because (i) we preferred to keep the expressiveness of the specification and then make the translation of most behavioural operators easier, (ii) high-level models are necessary to use some verification techniques available in Cadp, such as compositional verification, (iii) verification of the generated Lotos code can benefit from the numerous optimisations implemented in the Caesar.adt and Caesar [START_REF] Garavel | Compilation of Lotos Abstract Data Types[END_REF][START_REF] Garavel | Compilation and Verification of Lotos Specifications[END_REF][START_REF] Garavel | State Space Reduction for Process Algebra Specifications[END_REF] compilers of Lotos available in Cadp, which would be too expensive to re-implement at the Fsp level.

The translation from Fsp to Lotos/Exp is completely automated in a translator tool we implemented (about 25,000 lines of code). This tool was validated on many examples (more than 10,000 lines of Fsp) to ensure that the translation is reliable. As regards semantics, our translation preserves a branching equivalence relation [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF] which is stronger than observational equivalence.

The remainder of this paper is organised as follows. Section 2 gives short introductions to Fsp, Lotos, and Exp. Section 3 presents some preliminary definitions that are used in the remainder of the paper. Sections 4 and 5 describe respectively the translation of Fsp sequential processes into Lotos and of Fsp composite processes into Exp. In Section 6, we present our tool and its validation. Section 7 illustrates how Ltsa and Cadp can be used jointly on a simple system. Section 8 ends with some concluding remarks. More details about this work are given in an Inria technical report [START_REF] Lang | Translating Fsp into Lotos and Networks of Automata[END_REF].

FSP, LOTOS, and EXP

We start with a short description of Fsp (Finite State Processes, see [START_REF] Magee | Concurrency: State Models & Java Programs[END_REF] for a more complete presentation of the language). Fsp can define (i) constants, ranges, and sets, (ii) basic (i.e., sequential) and composite processes, (iii) safety and progress properties (not handled in this work). In the grammar of Fsp basic processes below, an upper case identifier P refers to a process identifier, X (or x) is a variable, act is a string label, and V is an expression involving arithmetic, comparison, and logical operators with variables. We discard in this paper local process definitions as well as the visibility operateur "@", dual of the hiding operator, although the full expressiveness of Fsp is taken into account in the translator we implemented (see Section 6).

P B ::=P (X 1 =V 1 , . . . , X k =V k ) = B process definition +{A e1 , . . . , A en } alphabet extension /{A ′ r1 /A r1 , . . . , A ′ rn /A rn } \{A h1 , . . . , A hn } relabel + hide B::=stop | end | error | P (V 1 , . . . , V n ) terminations + process call | if V then B 1 else B 2 if-then-else structure | when V 1 S 1 → B 1 | . . . | when V n S n → B n choice | P 1 (V 11 , . . . , V 1k ); . . . ;P n (V n1 , . . . , V nl );B sequential composition S::=A 1 → . . . → A k sequence of labels A::=L 1 . . . L n label L::=act action | V | x : V expression | {A 1 , . . . , A n } | x : {A 1 , . . . , A n } set of labels | [V 1 ..V 2 ] | x : [V 1 ..V 2 ]
range Fsp has an expressive syntax to represent labels A, A 1 , etc. Each label is thus the concatenation of lower-case identifiers act, expressions V , and integers within a range "[V 1 ..V 2 ]" where V 1 and V 2 are integer expressions. A variable x may be associated to some labels, which allows to reuse them later in the behaviour. A basic process definition consists of a process name P , a set of parameters X 1 , . . . , X k with default values V 1 , . . . , V k , and a sequential behaviour B. This behaviour can be either relabeled, "A ′ ri /A ri " meaning that each label in A ri renames into labels A ′ ri (a single label may rename into several labels, thus yielding several transitions), or hidden to the environment, which corresponds to relabeling into the special action τ . Fsp uses label prefix matching while applying hiding and relabeling operators. The alphabet of a process consists of the set of labels (possibly renamed) occurring in B and the supplementary labels in "{A e1 , . . . , A en }". The stop, end, and error behaviours correspond to deadlock, successfull termination, and erroneous termination. Process call and if-then-else have a standard semantics. The "|" operator denotes a choice in which every branch "S i → B i " whose condition V i evaluates to true may execute nondeterministically; S i corresponds to a sequence of labels. Finally, a sequential composition is made up of a list of process calls requiring that all these processes terminate. Fsp composite processes are defined as follows:

P C ::=||P (X 1 =V 1 , . . . , X k =V k ) = C process definition ≫ {A p1 , . . . , A pn } \{A h1 , . . . , A hn } priority + hide | ||P (X 1 =V 1 , . . . , X k =V k ) = C
process definition ≪ {A p1 , . . . , A pn } \{A h1 , . . . , A hn } priority + hide C:

:=SL P (V 1 , . . . , V n ) /{A ′ r1 /A r1 , . . . , A ′ rn /A rn } process call + relabel | SL (C 1 || . . . ||C n ) /{A ′ r1 /A r1 , . . . , A ′ rn /A rn } parallel compo. + relabel | if V then C 1 else C 2
if-then-else structure SL::={A 1 , . . . , A m }::{A 1 , . . . , A n }:

sharing / labeling A composite process definition consists of a name "||P " (the symbol "||" indicating that P belongs to the class of composite processes), a set of parameters X 1 , . . . , X k with default values V 1 , . . . , V k , and a composite behaviour C. Priorities can be assigned to labels in C, "≫" (respectively "≪") meaning that labels in "{A p1 , . . . , A pn }" have lower (respectively higher) priority than all other labels occurring in C. A composite behaviour may be either a call to a basic process, a parallel composition of composite behaviours synchronising on the intersection of their alphabets, or a deterministic choice between composite processes. Relabeling and hiding are also possible using a syntax similar to basic processes. At last, Fsp contains two original operators named process labeling ":" and process sharing "::" which are always used subsequently (first sharing then labeling, see the grammar above). Process labeling "{A 1 , . . . , A n }:C" generates an interleaving of as many instances of C as there are labels in "{A 1 , . . . , A n }". All the labels of each instance are prefixed by the label of "{A 1 , . . . , A n }" associated to this instance. Process sharing "{A 1 , . . . , A m }::C" replaces each label l occurring in C by a choice between labels "{A 1 l, . . . , A m l}". As an illustration, the resulting automata for "||C1 = {a,b}:P" and "||C2 = {a,b}::P" are given below with "P = comm.END".

Example 1. The following specification describes a semaphore. The process ACCESS simulates a client which accesses the critical section protected by the process SEMAPHORE. The system, called SEMADEMO, is made up of the semaphore in charge of three resources a, b, c, and of the process which wants to access them. Lotos (Language Of Temporal Ordering Specification) is a specification language standardised by ISO [START_REF] Iso | Lotos: a Formal Description Technique based on the Temporal Ordering of Observational Behaviour[END_REF]. It combines definitions of abstract data types and algebraic processes. The full syntax of a process is the following:

process P [G 1 , ..., G m ] (X 1 :S 1 , ..., X n :S n ) : f unc := B where block 1 , ..., block p endproc A process defines a list of formal gates G i∈{1,...,m} and of parameters X j∈{1,...,n} of sort S j . Each block k∈{1,...,p} denotes a data type or process definition. The functionality f unc of a process is exit if it ends by an exit behaviour, or noexit otherwise. The process behaviour B is formalised in the following grammar. We present only operators that are required for our translation:

B ::= exit termination | G O 1 . . . O n [V ] ;B | i;B action prefix | [V ]->B guarded behaviour | B 1 []B 2 choice | B 1 >>B 2 sequential composition | hide G 1 , . . . , G n in B hiding | P [G 1 , . . . , G n ](V 1 , . . . , V m ) process call | choice X : T [] B choice on values O ::= !V | ?X : T emission / reception V ::= X | f (V 1 , . . . , V n ) value expression
Gate identifiers G may be complemented with a set of parameters called offers. An offer has either the form "!V " which corresponds to the emission of a value V , or the form "?X : T " which means the reception of a value of sort T in a variable X. A single action can contain several offers, and these offers can be complemented by a guard which constrains the received values. For instance, "COMM?X:Int[X==1]" means that 1 is the only value that can be received in X. The guarded behaviour "[V ]->B" means that B is executed only if the boolean expression V evaluates to true. The sequential composition "B 1 >>B 2 " executes first B 1 until it reaches an exit, then B 2 is executed. Hiding masks gates within a behaviour, thus producing an hidden event written i. Cyclic behaviours may be defined using tail-recursive process calls. The choice on values "choice X : T [] B" generates a choice between behaviours B V1 , . . . , B Vn where V 1 , . . . , V n are all the values of sort T , and variable X is instantiated with value

V 1 in B V1 , with value V 2 in B V2 , etc.
The main differences between Fsp and Lotos resides in the treatment of labels. On the one hand, Lotos labels are structured in the form of a static (i.e., determined at compile time) gate, possibly followed by dynamic (i.e., computed at run-time) offers. Label hiding and label synchronisation are determined uniquely by the gate. On the other hand, no such distinction between gate and offers exists in Fsp, where hiding and synchronization depend on full labels, computed at run-time by concatenation of sub-labels and replacement of variables. This difference constitutes the main difficulty of the translation.

Fortunately, Cadp also provides a tool for communicating automata, called Exp.Open [START_REF] Lang | Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods[END_REF], whose input language (Exp) features more flexible label handling mechanisms than Lotos. Exp allows to describe parallel compositions of finite state machines using several parallel composition operators, synchronisation vectors, as well as renaming, hiding, cutting, and priority operators. We present the part of the Exp language that is used in this paper. L 1 , L ′ 1 , . . . represent labels, which are merely character strings.

B ::= total rename L 1 → L ′ 1 , . . . , L n → L ′ n in B end rename rename | total hide L 1 , . . . , L n in B end hide hide | total cut L 1 , . . . , L n in B end cut cut | total prio all but L 1 , . . . , L n > L ′ 1 , . . . , L ′ k in B end prio priority (1) | total prio L 1 , . . . , L n > all but L ′ 1 , . . . , L ′ k in B end prio priority (2) | B 1 |||B 2 interleaving | label par L 1 , . . . , L m in B 1 || . . . ||B n end par par. compo. | label par V 1 , . . . , V m in B 1 || . . . ||B n end par vect. compo. V ::= (L 1 | ) * . . . * (L n | ) → L vector
Rename and hide respectively define a set of labels to be renamed, and a set of labels to be hidden in behaviour B. The cut operator is used to cut the transitions that carry some given labels in a transition system. Priority expresses that a set of labels have a higher priority than another set of labels. "all but L 1 , . . . , L n " represents all labels except L 1 , . . . , L n . We introduce three forms of parallel composition: "B 1 |||B 2 " means that B 1 and B 2 run in parallel without synchronising, "label par L 1 , . . . , L m in B 1 || . . . ||B n " means that B 1 , . . . , B n run in parallel and synchronise all together on labels L 1 , . . . , L m , and "label par V 1 , . . . , V m in B 1 || . . . ||B n " means that they synchronise following the constraints expressed by the synchronisation vectors V 1 , . . . , V m . Precisely, a vector "l 1 * . . . * l n → l" produces a transition labeled l if all B i such that "l i = " execute all together a transition labeled l i . Exp.Open provides alternative semantics for the hide, rename, cut, prio, and par operators, the precise semantics used in this paper being determined by the total (which means that a label matches if it matches a regular expression entirely) and label (which means that processes synchronise on full labels, and not only on the gate part of the label) keywords. Finally, we mention Svl [START_REF] Garavel | Svl: A Scripting Language for Compositional Verification[END_REF] (Script Verification Language), which allows a high-level and concise description of the calls to the different Cadp tools.

Preliminary Definitions

Environment

When translating an Fsp specification into Lotos/Exp, we need to propagate along the abstract syntax tree of the Fsp specification, information collected during the tree traversal. This information is called an environment and is made of the following objects:

-E is a partial function associating expressions to variables, represented as a set of couples of the form "x → v". Environment E will be used during the translation to store variables defined in Fsp labels but also process parameters and constant definitions. E is initialised with constant definitions which are global to all processes. -S is a set of labels used with the "::" Fsp operator, to be shared between the parallel processes.

-L is a label coming from the ":" Fsp operator, to be distributed as prefix over the parallel processes. -R is a relabeling relation represented as a set of elements of the form "l → {l 1 , . . . , l k }", which associates sets of new labels to old labels. -H is a set of labels to be hidden.

-X is a mapping from variables to sets of labels, represented as a set of elements of the form "x → s", where s is either a range "(v 1 , v 2 )" or a set of labels "{l 1 , . . . , l k }".

An environment is a tuple " E, M, X " where M is a list of tuples " S, L, R, H ". We now define some functions used thereafter to formalise the translation. Function dom applies to R such that: dom({l 1 → s 1 , . . . , l k → s k }) = {l 1 , . . . , l k } where s i∈{1,...,k} are sets of labels. The dispatching function → d associates every element of one source set to all the elements of a target set:

{l 1 , . . . , l k } → d {l ′ 1 , . . . , l ′ k } = {l 1 → {l ′ 1 , . . . , l ′ k }, . . . , l k → {l ′ 1 , . . . , l ′ k }} Function ⊗ concatenates elements of two sets: {l 1 , . . . , l k } ⊗ {m 1 , . . . , m p } = {l 1 m 1 , . . . , l 1 m p , . . . , l k m 1 , . . . , l k m p }
Function pm is a prefix matching test, which takes as input a label l and a set of labels, and returns true if one of the labels in the list is a prefix for l: pm(l, {l 1 , . . . , l n }) = (∃i ∈ {1, . . . , n})(∃l ′ ) l = l i l ′ Function newlab takes as input a label l and returns the set of labels after relabeling by R:

newlab(l, {l 1 → s 1 , . . . , l k → s k }) = {l ′ i l ′ |(∃i ∈ {1, . . . , k}) l = l i l ′ ∧ l ′ i ∈ s i }

Expressions

Function f 2l e translates Fsp expressions (which are of type integer or string) into Lotos expressions substituting the values of variables wrt. environment E:

f 2l e (x, E) = E(x) f 2l e (f (V 1 , . . . , V n ), E) = f (f 2l e (V 1 , E), . . . , f 2l e (V n , E))
Function vars extracts the variables appearing in an expression:

vars(x) = {x} vars(f (V 1 , . . . , V n )) = vars(V 1 ) ∪ . . . ∪ vars(V n )
Function type computes the type of an expression, that is either Int or String. This function is standard, and therefore not defined here.

Translation of a Label

The translation of an Fsp label is not easy because Fsp labels involve different notions that have no direct counterpart in Lotos, namely sets, ranges, complex expressions, and variable definitions. Moreover, hiding or renaming of a label can only be made after flattening this high-level notation, as computed by Ltsa while generating transition systems from Fsp specifications. Consequently, we define two functions, f latten and f latten x , to translate an Fsp label into a set of Lotos labels. Function f latten expands all the variables appearing in the label, whereas f latten x translates as often as possible into Lotos variables the variables defined in the Fsp label. In the following, function f latten is used instead of the less space-consuming f latten x one when hiding or renaming has to be applied on the label.

We start with the definition of the f latten function which is called with an environment E associating one value to every variable appearing in Fsp, and returns a set of couples (label, environment). In case a variable is assigned several values (as defined in an Fsp range or set), f latten generates as many labels and environments as there are values associated to the variable. At this abstract level, all the label portions are stored in a list using the cons and nil operator. A variable is defined only once in an Fsp specification, so union between variable environments can be used instead of an overloading operation.

f latten(L 1 . . . L n , E) = {(cons(l 1 , l 11 ), E 11 ∪ E 1 ), . . . , (cons(l 1 , l 1m ), E 1m ∪ E 1 ), . . . , (cons(l k , l k1 ), E k1 ∪ E k ), . . . , (cons(l k , l kl ), E kl ∪ E k )} where {(l 1 , E 1 ), . . . , (l k , E k )} = f latten l (L 1 , E), {(l 11 , E 11 ), . . . , (l 1m , E 1m )} = f latten(L 2 . . . L n , E 1 )
, and

{(l k1 , E k1 ), . . . , (l kl , E kl )} = f latten(L 2 . . . L n , E k ).
The terminal case is defined on an empty list ε as: f latten(ε, E) = {(nil, E)} Function f latten l flattens a portion of label. In case of an expression indexed by a variable, environment E is extended with the variable x and its value v obtained after evaluation by f 2l e .

f latten l (act,

E) = {(act, E)} f latten l (V, E) = {(v, E)} f latten l (x :V, E) = {(v, {x → v} ∪ E)} where v = f 2l e (V, E).
In case of sets of labels, all the labels are expanded, and environments updated if necessary.

f latten l ({A 1 , . . . , A n }, E) = {(l 11 , E 11 ), . . . , (l 1k , E 1k ), . . . , (l n1 , E n1 ), . . . , (l nm , E nm )} f latten l (x:{A

1 , . . . , A n }, E) = {(l 11 , {x → l 11 } ∪ E 11 ), . . . , (l 1k , {x → l 1k } ∪ E 1k ), . . . , (l n1 , {x → l n1 } ∪ E n1 ), . . . , (l nm , {x → l nm } ∪ E nm )} where {(l 11 , E 11 ), . . . , (l 1k , E 1k )} = f latten(A 1 , E), and
{(l n1 , E n1 ), . . . , (l nm , E nm )} = f latten(A n , E). In case of ranges, all the integer expressions are computed from the range.

f latten l ([V 1 ..V 2 ], E) = {(v 1 , E), . . . , (v r , E)} f latten l (x:[V 1 ..V 2 ], E) = {(v 1 , {x → v 1 } ∪ E), . . . , (v r , {x → v r } ∪ E)} where v 1 = f 2l e (V 1 , E), r = (f 2l e (V 2 , E) -f 2l e (V 1 , E)) + 1, and (∀i ∈ {1, . . . , r -1}) v i+1 = v i + 1.
Example 2. The Fsp label "lab[x:1..2]" is translated using f latten as two abstract Lotos labels (see Section 7 for the concrete notation): "cons(lab, cons(1, nil))" and "cons(lab, cons(2, nil))".

Function f latten x generates Lotos labels keeping variables when the label is not concerned by relabeling or hiding. Function f latten x returns a set of tuples "(l, E, X)" where l is a label, E is a variable environment, and X binds variables which are kept while translating to a range of integer values, or a set of labels.

f latten x (L 1 . . . L n , E, X) = {(cons(l 1 , l 11 ), E 11 ∪ E 1 , X 11 ∪ X 1 ), . . . , (cons(l 1 , l 1m ), E 1m ∪ E 1 , X 1m ∪ X 1 ), . . . , (cons(l k , l k1 ), E k1 ∪ E k , X k1 ∪ X k ), . . . , (cons(l k , l kl ), E kl ∪ E k , X kl ∪ X k )} f latten x (ε, E, X) = {(nil, E, X)} where {(l 1 , E 1 , X 1 ), . . . , (l k , E k , X k )} = f latten xl (L 1 , E, X), {(l 11 , E 11 , X 11 ), . . . , (l 1m , E 1m , X 1m )} = f latten x (L 2 . . . L n , E 1 , X 1 ), {(l k1 , E k1 , X k1 ), . . . , (l kl , E kl , X kl )} = f latten x (L 2 . . . L n , E k , X k
), Function f latten xl translates a portion of an Fsp label into a portion of a Lotos label. All the variables appearing in the Fsp label are kept taking advantage of the expressiveness of Lotos offers. Thus, an Fsp set or range is translated as the variable at hand, and the set or range is stored in X that will be used during the translation of the full label to generate a guard constraining the value of the variable. If a variable is part of an expression to be translated, a new variable (y below) is kept in place of this expression.

f latten xl (act, E, X) = {(act, E, ∅)} f latten xl (V, E, X) = {(y, {y → y} ∪ E, {y → (v, v)})} if ∃z ∈ vars(V ) ∧ z ∈ X {(v, E, ∅)} otherwise f latten xl (x:V, E, X) = {(y, {x → v, y → y} ∪ E, {y → (v, v)})} if ∃z ∈ vars(V ) ∧ z ∈ X {(v, {x → v} ∪ E, ∅)} otherwise where v = f 2l e (V, E).
When translating sets and ranges, several labels with environments E and X are generated. In case a variable x appears as index of the set (resp. range), x is kept as a variable in E and the environment X is extended with all the possible values that can be computed for x from the set (resp. range).

f latten xl ({A 1 , . . . , A n }, E, X) = {(l 11 , E 11 , X 11 ), . . . , (l 1k , E 1k , X 1k ), . . . , (l n1 , E n1 , X n1 ), . . . , (l nm , E nm , X nm )} f latten xl (x:{A 1 , . . . , A n }, E, X) = {(x, {x → x} ∪ E, {x → {l 11 , . . . , l 1k , . . . , l n1 , . . . , l nm }})} where {(l 11 , E 11 , X 11 ), . . . , (l 1k , E 1k , X 1k )} = f latten x (A 1 , E, X), and

{(l n1 , E n1 , X n1 ), . . . , (l nm , E nm , X nm )} = f latten x (A n , E, X). f latten xl ([V 1 ..V 2 ], E, X) = {(y, {y → y} ∪ E, {y → (v 1 , v r )})} if ∃z ∈ (vars(V 1 ) ∪ vars(V 2 )) ∧ z ∈ X {(v 1 , E, ∅), . . . , (v r , E, ∅)} otherwise f latten xl (x:[V 1 ..V 2 ], E, X) = {(x, {x → x} ∪ E, {x → (v 1 , v r )})} where v 1 = f 2l e (V 1 , E), r = (f 2l e (V 2 , E) -f 2l e (V 1 , E)) + 1, and (∀i ∈ {1, . . . , r -1}) v i+1 = v i + 1.
Example 3. The Fsp label "lab[x:1..2]" is translated using f latten x in Lotos as "cons(lab, cons(x, nil))" with a guard "(x ≥ 1) ∧ (x ≤ 2)" which restricts the values of x. Both pieces of specification generate exactly the same labels.

Hiding or Renaming

Function horr tests if a set of flattened labels is concerned by hiding or renaming, and is used while translating sequences of labels to decide if variables may be kept (use of f latten x ) or not (use of f latten) in the Lotos code. The list of tuples " S, L, R, H " is applied starting by the first tuple since this list is built adding in head, and tuples have to be applied starting by the most recent one.

horr({l 1 , . . . , l k }, [ S 1 , L 1 , R 1 , H 1 , . . . , S n , L n , R n , H n ]) = i∈{1,...,q},j∈{1,...,k} ( pm(s i ml j , H 1 ) ∨ pm(s i ml j , dom(R 1 )) ∨ horr({s i ml j }, [ S 2 , L 2 , R 2 , H 2 , . . . , S n , L n , R n , H n ]
) ) where S 1 = {s 1 , . . . , s q }, and L 1 = m.

Translating FSP Sequential Processes into LOTOS

This section presents function f 2l p which translates a sequence of labels, and function f 2l b which generates Lotos code for Fsp sequential processes.

Sequence of Labels

The translation of a sequence depends if labels have to be modified (renamed or hidden) during the translation: if it is the case, they are flattened using the f latten function; otherwise variables are kept and function f latten x is used. We also recall that an Fsp label may correspond to several labels in Lotos. Therefore, the translation of a label may generate a choice in Lotos with as many branches as labels computed by f latten or f latten x .

Hiding or relabeling required. More formally, it means that horr({l 1 , . . . , l h }, M ) = true where {(l 1 , E 1 ), . . . ,

(l h , E h )} = f latten(A 1 , E). f 2l p (A 1 → . . . → A k → B, E, M, X ) = f 2l l (apply(l 1 , M )) seq(l 1 , M ) f 2l p (A 2 → . . . → A k → B, E 1 ∪ E, M, X ) [] . . . [] f 2l l (apply(l h , M )) seq(l h , M ) f 2l p (A 2 → . . . → A k → B, E h ∪ E, M, X ) f 2l p (B, E, M, X ) = f 2l b (B, E, M, X )
The last rule applies when the sequence of labels is empty. Function f 2l b dedicated to the translation of sequential processes is defined in the sequel. Function apply computes a set of labels resulting of the application in sequence of the list of tuples on a label. Note that relabeling may replace a single label by several ones, and that prefixing, relabeling and hiding are successively applied.

apply(l, [ S 1 , L 1 , R 1 , H 1 , . . . , S n , L n , R n , H n ]) = apply(l ′′ 1 , [ S 2 , L 2 , R 2 , H 2 , . . . , S n , L n , R n , H n ]) ∪ . . . ∪ apply(l ′′ k , [ S 2 , L 2 , R 2 , H 2 , . . . , S n , L n , R n , H n ]) where S 1 = {s 1 , . . . , s q }, L 1 = m, {l 1 , . . . , l p } = {s 1 ml, . . . , s q ml}, {l ′ 1 , . . . , l ′ r } = apply R (l 1 , R 1 ) ∪ apply R (l p , R 1 ), and {l ′′ 1 , . . . , l ′′ k } = apply H (l ′ 1 , R 1 ) ∪ apply H (l ′ r , R 1 ).
Functions apply R and apply H are resp. in charge of renaming and hiding.

apply R (l, R) = newlab(l, R) if pm(l, dom(R)) l otherwise apply H (l, H) = i if pm(l, H) l otherwise. Function f 2l l generates a Lotos choice from a set of labels.

f 2l l ({l 1 , . . . , l n }) = l 1 if n = 1 l 1 ;exit [] . . . []
l n ;exit otherwise Function seq chooses the Lotos sequential composition "≫" as sequence operator when this operator is preceded by a behaviour (a choice among several labels), and the Lotos action prefix ";" when preceded by a single label.

seq(l, M ) = ≫ if |apply(l, M )| > 1 ; otherwise
No hiding or relabeling required. In this case, there is horr({l 1 , . . . , l m }, M ) = f alse where {(l 1 , E 1 ), . . . ,

(l m , E m )} = f latten(A 1 , E). f 2l p (A 1 → . . . → A k → B, E, M, X ) = f 2l l (apply(l 1 , M ), X 1 ∪ X) seq(l 1 , M, X 1 ∪ X) f 2l p (A 2 → . . . → A k → B, E 1 ∪ E, M, X 1 ∪ X ) [] . . . [] f 2l l (apply(l h , M ), X h ∪ X) seq(l h , M, X h ∪ X) f 2l p (A 2 → . . . → A k → B, E h ∪ E, M, X h ∪ X ) f 2l p (B, E, M, X ) = f 2l b (B, E, M, X ) where {(l 1 , E 1 , X 1 ), . . . , (l h , E h , X h )} = f latten x (A 1 , E, X).
Extra variables in X generated while flattening labels using f latten x (see for instance the second rule of f latten xl , page 9) are not considered below because they make the notation concise but are not used in the following of the behaviour.

f 2l l ({l 1 , . . . , l n }, X) = l 1 if n = 1 l 1 [G];exit(x 1 , . . . , x p ) [] . . . [] l n [G];exit(x 1 , . . . , x p ) otherwise where X = {x 1 → D 1 , . . . , x p → D p }, and G = f 2l t (x 1 → D 1 ) ∧ . . . ∧ f 2l t (x p → D p
). Function f 2l t generates guards from tuples of X. These guards are used to constrain the values of variables introduced in the translation of labels.

f 2l t (x → (v 1 , v 2 )) = (x ≥ v 1 ) ∧ (x ≤ v 2 ) f 2l t (x → {l 1 , . . . , l k }) = (x = l 1 ) ∨ . . . ∨ (x = l k )
Finally, function seq makes the variable passing explicit when the Lotos sequential composition "≫" is chosen as sequence operator. This is mandatory compared to the expanded translation of labels since variables are preserved here and can be used in the rest of the behaviour.

seq(l, M, X) = ≫ accept x 1 : T 1 , . . . , x p : T p in if |apply(l, M )| > 1 ;
otherwise where X = {x 1 → D 1 , . . . , x p → D p }, and T 1 = type(x 1 ), . . . , T p = type(x p ).

Sequential Processes

Fsp sequential processes are translated into Lotos processes. Fsp allows the definition of local processes which are translated as local processes into Lotos as well. We only present the translation of a process without local definitions, although this structuring is taken into account into the tool we have implemented (see Section 6). Now, we define the translation from Fsp to Lotos as a function f 2l b . Function f unc computing the process functionality is defined in [START_REF] Lang | Translating Fsp into Lotos and Networks of Automata[END_REF]. Note also that only two concrete Lotos gates are generated by our translation: EVENT which prefixes all the regular Fsp labels, and EVENT ERROR which is used to encode the Fsp error termination.

f 2l b (P (X 1 =V 1 , . . . , X k =V k ) = B + {A e1 , . . . , A en } /{A ′ r1 /A r1 , . . . , A ′ rn /A rn } \{A h1 , . . . , A hn }, E, M, X ) = process P [EVENT,EVENT ERROR] (X 1 : T 1 , . . . , X k : T k ) : f unc(B) := f 2l b (B, E 0 , [ ∅, ∅, R 0 , H 0 , M ], X ) endproc where T 1 = type(V 1 ), . . . , T k = type(V k ), E 0 = {X 1 → V 1 , . . . , X k → V k }∪E, {(l r11 , E r11 ), . . . , (l r1k , E r1k )} = f latten(A r1 , E), {(l ′ r11 , E ′ r11 ), . . . , (l ′ r1k , E ′ r1k )} = f latten(A ′ r1 , E), {(l rn1 , E rn1 ), . . . , (l rnk , E rnk )} = f latten(A rn , E), {(l ′ rn1 , E ′ rn1 ), . . . , (l ′ rnk , E ′ rnk )} = f latten(A ′ rn , E), R 0 = {{l r11 , . . . , l r1k } → d {l ′ r11 , . . . , l ′ r1k }, . . . , {l rn1 , . . . , l rnk } → d {l ′ rn1 , . . . , l ′ rnk }}, {(l h11 , E h11 ), . . . , (l h1k , E h1k )} = f latten(A h1 , E), {(l hn1 , E hn1 ), . . . , (l hnk , E hnk )} = f latten(A hn , E)
, and H 0 = {l h11 , . . . , l h1k , . . . , l hn1 , . . . , l hnk }. Usual terminations (stop and end) have direct equivalent in Lotos. The error termination is translated using a P ERROR process whose behaviour is an endless loop on an EVENT ERROR label.

f 2l b (stop, E, M, X ) = stop f 2l b (end, E, M, X ) = exit f 2l b (error, E, M, X ) = P

ERROR [EVENT ERROR]

A process call is translated as is with as parameter its list of arguments.

f 2l b (P (V 1 , . . . , V n ), E, M, X ) = P [EVENT,EVENT ERROR] (f 2l e (V 1 , E), . . . , f 2l e (V n , E))
The if structure is encoded as a Lotos choice with two branches respectively encoding the then and else part of the Fsp behaviour.

f 2l b (if V then B 1 else B 2 , E, M, X ) = [f 2l e (V, E)]-> f 2l b (B 1 , E, M, X ) [] [¬f 2l e (V, E)]-> f 2l b (B 2 , E, M, X ) The Fsp choice is translated into a Lotos choice with guards. f 2l b (when V 1 S 1 → B 1 | . . . |when V n S n → B n , E, M, X ) = [f 2l e (V 1 , E)]-> f 2l p (S 1 → B 1 , E, M, X ) [] . . . [] [f 2l e (V n , E)]-> f 2l p (S n → B n , E, M, X )
Last, a sequential composition is translated similarly in Lotos. f 2l b (P 1 (V 11 , . . . , V 1k ); . . . ;P n (V n1 , . . . , V nl );B, E, M, X ) = P 1 [EVENT,EVENT ERROR](f 2l e (V 11 , E), . . . , f 2l e (V 1k , E)) ≫ . . . ≫ P n [EVENT,...](f 2l e (V n1 , E), . . . , f 2l e (V nl , E)) ≫ f 2l b (B, E, M, X ) No variables are passed along the Lotos sequential composition because processes involved in the composition are independent of each other: each process has to terminate correctly before starting the next one. In addition, Lotos local processes are generated for each process called in the sequential composition. This is needed to apply the environment (and possible renaming or hiding) to the definitions of referred processes. As an example, process P 1 is translated as follows, where P1 is the process definition of P 1 :

process

P 1 [EVENT,EVENT ERROR] (X 1 : T 1 , . . . , X k : T k ) : f unc( P1 ) := f 2l b ( P1 , E 0 , M, X ) endproc where T 1 = type(V 1 ), . . . , T k = type(V k ), E 0 = {X 1 → V 1 , . . . , X k → V k }∪E.

Translating FSP Composite Processes into EXP

Encoding Fsp composite processes into Lotos is tedious for several reasons:

-Lotos hiding and synchronisation constructs operate on gates, whereas Fsp constructs operate on full labels (which are gates + offers in Lotos). -Lotos has no renaming operator. The only way to rename a gate in Lotos is to instantiate a process with an actual gate different from the formal one. Such a renaming is not always satisfactory, because it only permits injective renaming (different gates cannot be renamed into the same gate), whereas non-injective renaming is allowed in Fsp. -Lotos does not have a priority operator. The only way to express it is by refactoring the specification to only allow labels with high priority to be executed when necessary.

Consequently, we chose to translate Fsp composite processes into the Exp format instead of Lotos. Translation of an Fsp composite process into Exp is made up of three steps. First, all the Fsp sequential processes are translated into Lotos using function f 2l b presented in Section 4. This translation takes into account the possible parameters coming with the process call. Then, Svl [START_REF] Garavel | Svl: A Scripting Language for Compositional Verification[END_REF] scripts are automatically derived to generate a Bcg file (which is a computer representation for state/transition models) for each sequential process translated into Lotos. These Bcg descriptions of processes are used in the last step, namely the translation of Fsp composite processes into Exp. Function f 2l c translates composite processes into Exp specifications. The abstract notation "l. * " matches labels with l as prefix, and is used to take the prefix matching into account while hiding labels. The environment is only used during the translation of composite processes to store values of process parameters. This is due to the top-down approach our translation is based on, and to the fact that all the Fsp operators are directly expressed in Exp.

f 2l c ( ||P (X 1 =V 1 , . . . , X k =V k ) =
C ≫ {A p1 , . . . , A pn } \{A h1 , . . . , A hn }, E, M, X ) = total hide l h11 , l h11 . * , . . . , l h1k , l h1k . * , . . . , l hn1 , l hn1 . * , . . . , l hnk , l hnk . * in total prio all but l p11 , . . . , l p1k , . . . , l pn1 , . . . , l pnk > l p11 , . . . , l p1k , . . . , l pn1 , . . . , l pnk in

f 2l c (C, E 0 , M, X ) end prio end hide f 2l c ( ||P (X 1 =V 1 , . . . , X k =V k ) =
C ≪ {A p1 , . . . , A pn } \{A h1 , . . . , A hn }, E, M, X ) = total hide l h11 , l h11 . * , . . . , l h1k , l h1k . * , . . . , l hn1 , l hn1 . * , . . . , l hnk , l hnk . * in total prio l p11 , . . . , l p1k , . . . , l pn1 , . . . , l pnk > all but l p11 , . . . , l p1k , . . . , l pn1 , . . . , l pnk in f 2l c (C, E 0 , M, X ) end prio end hide where

T 1 = type(V 1 ), . . . , T k = type(V k ), E 0 = {X 1 → V 1 , . . . , X k → V k }∪E, {(l h11 , E h11 ), . . . , (l h1k , E h1k )} = f latten(A h1 , E), {(l hn1 , E hn1 ), . . . , (l hnk , E hnk )} = f latten(A hn , E), {(l p11 , E p11 ), . . . , (l p1k , E p1k )} = f latten(A p1 , E)
, and {(l pn1 , E pn1 ), . . . , (l pnk , E pnk )} = f latten(A pn , E). As regards the translation of a process call into Exp, process P is duplicated in as many interleaved processes P as there are labels in the labeling set with all the labels of process P prefixed by one label of this set, respectively m 1 , m 2 , etc. The "label par" statement is used below for renaming purposes, since the rename statement existing in Exp does not allow to rename a single label into several labels (thus producing several transitions from a single one). Therefore, we use synchronisation vectors (usually used for synchronisation purposes) to rename labels (vectors r ), and to prefix all the labels of the process by the labels defined in S (vectors p ). Function alpha computing the alphabet of a process is defined in [START_REF] Lang | Translating Fsp into Lotos and Networks of Automata[END_REF].

f 2l c (SL P (V 1 , . . . , V n ) /{A ′ r1 /A r1 , . . . , A ′ rn /A rn }, E, M, X ) = label par vectors r (R 0 , alpha(SL P (V 1 , . . . , V n ), E, M, X )) in label par vectors p ({s 1 , . . . , s k }, {m 1 } ⊗ alpha(P (V 1 , . . . , V n ), E, M, X )) in f 2l pr (P (V 1 , . . . , V n ), E, M, X ) end par ||| . . . ||| label par vectors p ({s 1 , . . . , s k }, {m p } ⊗ alpha(P (V 1 , . . . , V n ), E, M, X )) in f 2l pr (P (V 1 , . . . , V n ), E, M, X ) end par end par where {s 1 , . . . , s k } = f latten sh (SL, E), {m 1 , . . . , m p } = f latten lb (SL, E), {(l 11 , E 11 ), . . . , (l 1k , E 1k )} = f latten(A r1 , E), {(l ′ 11 , E ′ 11 ), . . . , (l ′ 1k , E ′ 1k )} = f latten(A ′ r1 , E), {(l n1 , E n1 ), . . . , (l nk , E nk )} = f latten(A rn , E), {(l ′ n1 , E ′ n1 ), . . . , (l ′ nk , E ′ nk )} = f latten(A ′
rn , E), and R 0 = {{l 11 , . . . , l 1k } → d {l ′ 11 , . . . , l ′ 1k }, . . . , {l n1 , . . . , l nk } → d {l ′ n1 , . . . , l ′ nk }}. Functions f latten sh and f latten lb flatten the sets of labels used as prefixes:

f latten sh ({A 1 , . . . , A m }::{A 1 , . . . , A n }:, E) = f latten({A 1 , . . . , A m }, E) f latten lb ({A 1 , . . . , A m }::{A 1 , . . . , A n }:, E) = f latten({A 1 , . . . , A n }, E)
Auxiliary functions f 2l pr , vectors r , and vectors p are now defined. Function f 2l pr refers to the Bcg file generated previously from the Lotos code if it is a sequential process, or calls the f 2l c function if it is a composite process. We present a simplified version of f 2l pr since a same process can be referred several times with different parameters. In our translator tool, we indexed such processes with numbers to distinguish their different instances.

f 2l pr (P (V 1 , . . . , V n ), E, M, X ) = "P.bcg" if is sequential(P ) f 2l c (P ( X1 =V 1 , . . . , Xn =V n )= P , E, M, X ) otherwise
where Xi∈{1,...,n} refers to formal parameter identifiers, and V i∈{1,...,n} refer to actual values for them.

Function vector r generates vectors with as left part a single element corresponding to the label to rename, and as right part its new name. Labels which are not concerned by relabeling preserve their original name.

vectors r (R, {l 1 , . . . , l p }) = l 1 -> l 1 , vectors r (R, {l 2 , . . . , l p }) if newlab(l 1 , R) = ∅ l 1 -> n 1 , . . . ,l 1 -> n q , vectors r (R, {l 2 , . . . , l p }) otherwise where {n 1 , . . . , n q } = newlab(l 1 , R). Function vector p generates vectors with as left part the label to extend, and derives from it a new label with a prefix taken into a set of prefixes. All the combinations are computed for the set of labels and prefixes in input. Function cat corresponds to the concatenation of lists.

vectors p ({s 1 , . . . , s k }, {l 1 , . . . , l p }) = l 1 -> cat(s 1 , l 1 ), . . . ,l 1 -> cat(s k , l 1 ), vectors p ({s 1 , . . . , s k }, {l 2 , . . . , l p }) Similarly to the translation of a process call, for a parallel composition, interleaving of processes is derived, as well as renaming and prefixing using respectively vectors r and vectors p functions. Synchronisation sets are made explicit. Below, the composite process C 1 synchronise with the rest of the involved processes on labels I 1 , . . . , I q .

f 2l c (SL (C

} = f latten sh (SL, E), {m 1 , . . . , m p } = f latten lb (SL, E), {(l r11 , E r11 ), . . . , (l r1k , E r1k )} = f latten(A r1 , E), {(l ′ r11 , E ′ r11 ), . . . , (l ′ r1k , E ′ r1k )} = f latten(A ′ r1 , E), {(l rn1 , E rn1 ), . . . , (l rnk , E rnk )} = f latten(A rn , E), {(l ′ rn1 , E ′ rn1 ), . . . , (l ′ rnk , E ′ rnk )} = f latten(A ′ rn , E), and R 0 = {{l r11 , . . . , l r1k } → d {l ′ r11 , . . . , l ′ r1k }, . . . , {l rn1 , . . . , l rnk } → d {l ′ rn1 , . . . , l ′ rnk }}. The if construct is translated as for sequential processes. f 2l c (if V then C 1 else C 2 , E, M, X ) = f 2l c (C 1 , E, M, X ) if f 2l e (V, E) f 2l c (C 2 , E, M, X ) otherwise

Tool and Validation

Translator Tool. We developed an automatic translator from Fsp to Lotos using the Syntax and Lotos nt compiler construction technologies [START_REF] Garavel | Compiler Construction Using Lotos nt[END_REF]. The tool consists of about 5,000 lines of Syntax, 20,000 lines of Lotos nt, and 500 lines of C. This implementation was split into two main steps: (i) parsing the Fsp language and storing the result into an abstract syntax tree, (ii) translating the abstract syntax tree into semantically equivalent Lotos code. The parsing task was difficult since Syntax accepts only LALR(1) grammar as input. Therefore, the abstract Fsp grammar as formalised in [START_REF] Magee | Concurrency: State Models & Java Programs[END_REF] was refined to a concrete grammar free of ambiguities. We validated the translator on about 10,500 lines of Fsp specifications (approx. 2,400 Fsp processes) that we reused from [START_REF] Magee | Concurrency: State Models & Java Programs[END_REF] or wrote ourselves. In the latter case, we tried to systematically explore all the expressiveness that allows the Fsp notation to ensure robustness of our translation. These 10,500 lines of Fsp correspond after translation to about 72,000 lines of Lotos, 2,000 lines of Svl, and 8,000 lines of Exp. This large number of Lotos lines has two main explanations: (i) Lotos is more verbose than Fsp, for instance there are more keywords, or gates have to be made explicit; (ii) although we keep variables as often as possible, our translation of Fsp sequential processes may flatten labels whereas Fsp allows a concise notation for them.

Correctness of the Translation. It is essential to preserve the semantics of the source language after translation into the target one. Indeed, any verification performed with Cadp on the specification obtained after translation has to be valid for the initial specification. Our translation preserves semantics of both process calculi wrt. a branching equivalence relation [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF]. Branching equivalence is the strongest of the weak equivalences found in the literature. Unlike strong equivalence, branching equivalence does not require a strict matching of τ transitions. This is exactly what we need since sequential composition in Lotos induces τ transitions which do not appear in the semantics of Fsp. Semantics preservation modulo branching equivalence is important as it ensures that the properties restricted to visible actions (e.g., safety and fair liveness) verified on the Lotos specification are indeed properties of the Fsp specification. One drawback of branching equivalence might be that it does not preserve τ cycles. For instance, two systems can be branching equivalent even if one system contains a τ cycle which does not appear in the other. However, our translation ensures that all the τ cycles in the Fsp specification are preserved in the Lotos one, and no new cycle is introduced.

We checked on all the examples that we used for validation that branching equivalence is preserved by our translation. For each specification, this test is performed on LTSs generated by Ltsa and Cadp wrt. the semantics of their respective notations. It was verified automatically using Bisimulator [START_REF] Bergamini | Bisimulator: A Modular Tool for On-the-Fly Equivalence Checking[END_REF] for nontrivial examples. Bisimulator is a tool of the Cadp toolbox which allows to verify the most common notions of behavioural equivalences. The equivalence test cannot be applied directly because Fsp labels generated by Ltsa and Lotos labels generated by Cadp do not follow the same syntactic conventions. Additionally, the Fsp hidden event tau corresponds to i in Lotos, and the Lotos termination event exit has no counterpart in Fsp. However, Cadp allows to systematically transform an LTS with Fsp conventions into one with Lotos conventions, by renaming and cutting labels that match some predefined regular expressions.

Application

In this section, we focus on the specification of a semaphore. We present several refinements of this specification, and show how the use of Ltsa is complemented by the use of Cadp based on the translation from Fsp to Lotos/Exp. The starting point is the specification of the semaphore given in Fsp in Example 1. The resulting automaton is made up of 7 states and 9 transitions.

A first refinement is to extend the number of resources ("{a,b,c}" but also "{1,2,3}") being concerned by the mutual exclusion as well as the number of accesses. This result is obtained by this new specification: from which Ltsa generates an automaton with 13 states and 18 transitions. The next step aims at duplicating both semaphores so that each semaphore is in charge of a single resource. The resulting automaton contains 49 states and 126 transitions and becomes difficult to analyse visually, because all the transitions between resources "{a,b,c}" and "{1,2,3}" are interleaved. The last refinement defines the specification as a composition of two composite processes being dedicated to one resource. The automaton generated by Ltsa has the same number of states and transitions as the former system, but it is impossible to claim that both specifications (SEMADEMO2 and SEMADEMO3) are equivalent. At this level, we use the translation to check this equivalence with the Cadp toolbox. We show first some pieces of the code obtained by our translation. The Fsp process SEMAPHORE is translated as follows in Lotos: The concrete notation for Lotos labels is slightly different from the abstract notation we introduced in Section 3. Indeed, a label is systematically represented by the EVENT gate followed by an offer consisting of a list of items of types Int and String, using the following data type: -> Label endtype

If variables appear in one label, the Lotos choice construct is used to distinguish variables and regular string labels. For instance, the Fsp label "lab[x:1..2]" is translated in Lotos using the aforementioned concrete syntax as: Now we show a piece of Exp code generated for the C P process defined in the SEMADEMO3 system. Processes ACCESS and SEMAPHORE synchronise on the set of labels appearing at the beginning of the Exp description. This example shows how prefixing labels of ACCESS by B is done using synchronisation vectors, and how the exit label is cut within sequential processes. Processes SEMADEMO2 and SEMADEMO3 translated into Lotos/Exp have been checked strongly equivalent using the Bisimulator tool of the Cadp toolbox. We illustrated here the use of equivalence checking on Fsp designs, but other Cadp verification techniques can be used to complement Ltsa validation, such as distributed, compositional, or on-the-fly verification to tackle the state explosion problem, or efficient model checking techniques available in Evaluator [START_REF] Mateescu | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus[END_REF]. Last, the debugging stage using Cadp does not add any complexity for designers because labels used in counter-examples may be translated in Fsp format (see Section 6) using renaming facilities available in Cadp.

In this paper, our motivation was to reduce the gap between existing tool support for process calculi. We chose here the popular process calculus Fsp and the international standard Lotos. Fsp is based on an expressive and concise notation. Therefore, we proposed a translation from Fsp to Lotos (and Exp) to make the joint use of Ltsa and Cadp possible for Fsp users. The translation is completely automated by a tool we implemented. This translator will be integrated in a future release of the Cadp toolbox.

As regards related work, to the best of our knowledge, the only proposals focusing on high-level translations between process algebras have been made in the hardware area [START_REF] Salaün | Translating Hardware Process Algebras into Standard Process Algebras: Illustration with Chp and Lotos[END_REF][START_REF] Wang | Towards a Unifying Csp approach to Hierarchical Verification of Asynchronous Hardware[END_REF]. Their common goal is to allow verification of asynchronous circuits and architectures. Beyond that, the most related set of works are those advocating the encoding of process calculi (mainly Acp, Ccs, Csp and their dialects) into higher-order logics, inputs of theorem provers such as Hol, Pvs, Isabelle [START_REF] Nesi | Formalising a Value-Passing Calculus in Hol[END_REF][START_REF] Dutertre | Using a Pvs Embedding of Csp to Verify Authentication Protocols[END_REF][START_REF] Tej | A Corrected Failure-Divergence Model for Csp in Isabelle/Hol[END_REF][START_REF] Basten | Process Algebra in Pvs[END_REF] or into the B method [START_REF] Butler | Csp2B: A Practical Approach to Combining Csp and B[END_REF]. Motivations of these works are to take advantage of the formal verification means available for the target formalism. Theorem proving allows to fight the state explosion problem and to deal with infinite automata, but is not suitable to prove temporal properties. We preferred model checking because it makes verification steps easier thanks to a full automation and its adequacy to automata-based models.

A first future work is to apply our approach on complex systems, such as web service models described first in Bpel or Ws-Cdl, and then automatically translated into Fsp for analysis purposes [START_REF] Foster | Tool Support for Model-Based Engineering of Web Service Compositions[END_REF]. In this case, many interacting services can involve huge underlying state spaces which can be generated and minimised using the optimised means of Cadp. Moreover, equivalence checking available in Cadp can help in web services to ensure that an abstract specification of a problem and its solution described as a composition of services are equivalent [START_REF] Salaün | Describing and Reasoning on Web Services using Process Algebra[END_REF]. Another perspective is to take Fsp safety and progress properties into account, and to translate them into regular alternation-free mu-calculus formulas, input format of the on-the-fly model checker Evaluator [START_REF] Mateescu | Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus[END_REF].

  SEMAPHORE(N=0) = SEMA[N], SEMA[v:0..1] = ( up -> SEMA[v+1] | when (v>0) down -> SEMA[v-1] ). ACCESS = ( mutex.down -> critical -> mutex.up -> ACCESS ). ||SEMADEMO = ( {a,b,c}:ACCESS || {a,b,c}::mutex:SEMAPHORE(1) ).

  ||SEMADEMO1 = ( {a,b,c}:ACCESS || {a,b,c,[1..3]}::mutex:SEMAPHORE(1) || [1..3]:ACCESS ).

  ,c}:ACCESS || {a,b,c}::mutex:SEMAPHORE(1) || [1..3]::mutex:SEMAPHORE(1) || [1..3]:ACCESS ).

  ||C_P = ( {a,b,c}:ACCESS || {a,b,c}::mutex:SEMAPHORE(1) ). ||C_Q = ( [1..3]:ACCESS || [1..3]::mutex:SEMAPHORE(1) ). ||SEMADEMO3 = ( C_P || C_Q ).

  process SEMAPHORE [EVENT,EVENT_ERROR] (N:Int): noexit := SEMA [EVENT,EVENT_ERROR] (N) where process SEMA [EVENT,EVENT_ERROR] (N:Int): noexit := EVENT !CONS(UP,NIL); SEMA[EVENT,EVENT_ERROR](N+POS(1)) [] [V>POS(0)]-> EVENT !CONS(DOWN,NIL); SEMA[EVENT,EVENT_ERROR](N-POS(1)) endproc endproc

type

  Label is IntegerNumber, String sorts Label opns CONS (*! constructor *) : String, Label -> Label CONS (*! constructor *) : Int, Label -> Label NIL (*! constructor *) :

  choice X:Int [] EVENT !CONS (LAB, CONS (X, NIL)) [(X>=POS(1)) and (X<=POS(2))]

  label par "EVENT !CONS (A, CONS (MUTEX, CONS (DOWN, NIL)))", "EVENT !CONS (A, CONS (MUTEX, CONS (UP, NIL)))", "EVENT !CONS (B, CONS (MUTEX, CONS (DOWN, NIL)))", ... in label par "EVENT !CONS (MUTEX, CONS (DOWN, NIL))" -> "EVENT !CONS (B, CONS(MUTEX, CONS (DOWN, NIL)))", "EVENT !CONS (CRITICAL, NIL)" -> "EVENT !CONS (B, CONS (CRITICAL, NIL))" , "EVENT !CONS (MUTEX, CONS (UP, NIL))" -> "EVENT !CONS (B, CONS (MUTEX, CONS (UP, NIL)))" in total cut exit in "ACCESS.bcg" end cut end par || ... total cut exit in "SEMAPHORE.bcg" end cut ... end par

  1 || . . . ||C n ) /{A ′ r1 /A r1 , . . . , A ′ rn /A rn }, E, M, X ) = label par I 1 , . . . , I q in ( label par vectors r (R 0 , alpha(SL C 1 , E, M, X )) in label par vectors p ({s 1 , . . . , s k }, {m 1 } ⊗ alpha(C 1 , E, M, X )) in f 2l c (C 1 , E, M, X ) (SL (C 2 || . . . ||C n ) /{A ′ r1 /A r1 , . . . , A ′ rn /A rn }, E, M, X ) end par where {I 1 , . . . , I q } = alpha(SL C 1 /{A ′ r1 /A r1 , . . . , A ′ rn /A rn }, E, M, X ), ∩ alpha(SL (C 2 || . . . ||C n ) /{A ′ r1 /A r1 , .. . , A ′ rn /A rn }, E, M, X ), {s 1 , . . . , s k

	end par
	end par
	||| . . . |||
	label par vectors r (R 0 , alpha(SL C 1 , E, M, X )) in
	label par
	vectors p ({s 1 , . . . , s k }, {m p } ⊗ alpha(C 1 , E, M, X )) in
	f 2l c (C 1 , E, M, X )
	end par
	end par
	)
	|| f 2l c

⋆ ⋆ ⋆ G. Salaün currently works at Universidad de Málaga, Spain (salaun@lcc.uma.es).