Lara Briñón Arranz

Alexandre Seuret

Carlos Canudas De Wit

Elastic Formation Control Based on Affine Transformations

This paper deals with the control of a fleet of nonlinear systems representing AUVs (autonomous underwater vehicles). The purpose is here to design a control law to stabilize the fleet to time-varying formations which are not only circular. A novel framework is proposed to express a general control law for a large class of formations. This is produced by applying a sequence of affine transformations such as translations, rotations and scalings. The paper also includes a cooperative control to distribute the agents along the formation which takes into account the communication constraints. The system was implemented in computer simulation, accessible through Web 1 .

I. INTRODUCTION

Cooperative control problems and multi-agent systems have received much attention in recent years. The field includes consensus algorithms for multi-agent systems [START_REF] Olfati-Saber | Consensus and cooperation in networked multi-agent systems[END_REF], [START_REF] Olfati-Saber | Consensus problems in networks of agents whit switching topology and time-delays[END_REF], flocking [START_REF] Olfati-Saber | Flocking for multi-agent dynamic systems: Algoand theory[END_REF], distributed sensor networks [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], [START_REF] Ögren | Cooperative control of mobile sensor networks: Adaptive gradient climbing in a distributed environment[END_REF], [START_REF] Zhang | Cooperative filters and control for cooperative exploration[END_REF], trajectory tracking and path following [START_REF] Kaminer | Trajectory tracking for autonomous vehicles: An integrated approach to guidance and control[END_REF], [START_REF] Frew | Coordinated standoff tracking of moving targets using lyapunov guidance vector fields[END_REF] and autonomous systems as underwater and unmanned air vehicles (AUVs and UAVs) [START_REF] Fiorelli | Adaptive sampling using feedback control of an autonomous underwater glider fleet[END_REF], [START_REF] Raffard | Distributed optimization for cooperative agents: Application to formation flight[END_REF]. Formation control and motion coordination have been extensively studied, see [START_REF] Martínez | Motion coordination with distributed information[END_REF], [START_REF] Ögren | A control lyapunov function approach to multiagent coordination[END_REF], among many others. Control laws have been provided to make a fleet of agents (vehicles) obtain circular and parallel formations [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], [START_REF] Sepulchre | Stabilization of planar collective motion with limited communication[END_REF]. Many extensions based on these works have been developed: three-dimensional formation control [START_REF] Hernandez | Three-dimensional motion coordination in a time-invariant flowfield[END_REF], planar circular formation control in a flow-field [START_REF] Paley | Stabilization of collective motion in a time-invariant flowfield[END_REF], translation [START_REF] Briñón | Translation control of a fleet circular formation of auvs under finite communication range[END_REF] and scaling [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF] of circular formations, and stabilization of a fleet to other closed forms [START_REF]General framework using affine transformations to formation control design[END_REF], [START_REF] Paley | Stabilization of symmetric formations to motion around convex loops[END_REF].

The objective of this paper is to design a general control law for a class of non-linear multi-agent systems to reach many class of formations including non-circular and timevarying formations. Based on [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], new results have been already proposed in [START_REF] Briñón | Translation control of a fleet circular formation of auvs under finite communication range[END_REF] and [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF] to deal with time-varying formations resulting from translating and contracting a circular formation. Nevertheless, generalization of these ideas to the called here elastic formation is pertinent to some applications where the agents should perform collaborative tasks requiring the formation to move towards an a priori unknown direction and to adapt to some particular form. For instance, in source seeking applications, the formation should displace in the source gradient direction and contract its size to adapt to the level curves of the source plume, [START_REF] Moore | Source seeking via collaborative measurements by a circular formation of agents[END_REF].

Translation, scaling and rotation are the three fundamental transformations of a formation [START_REF] Leonard | Virtual leaders, artifitial potentials and coordinated control of goups[END_REF]. These three Lara Briñón Arranz is with INRIA Rhône-Alpes, NeCS Team, Grenoble, France lara.brinon-arranz@inrialpes.fr Alexandre Seuret and Carlos Canudas de Wit are with the Department of Automatic Control, GIPSA-Lab, CNRS, NeCS Team, Grenoble, France {alexandre.seuret, carlos.canudas-de-wit} @gipsa-lab.grenoble-inp.fr main affine transformations, usually used in the fields of geometric and robotic control, are pertinent to express many class of closed curves in a matrix representation. A closed curve can be expressed as a sequence of transformations applied to the unit circle. In [START_REF]General framework using affine transformations to formation control design[END_REF], a general framework based on affine transformations is presented. This idea allows to control the agents to different trajectories which results from the application of these three affine transformations. The contribution of this paper is to stabilize the agents to the same elastic formation, not only to the same velocity reference, independently of initial conditions. A time-varying closed curve defined by a sequence of affine transformations is considered as an elastic formation. Our approach considers that this closed curve is know for all the agents (i.e. the sequence of transformations is a given reference).

In the context of the source seeking for underwater vehicles, it is relevant to constrain the agents in an appropriate shape to avoid unnecessary energy waste. Moreover, ensuring that the agents are uniformly distributed along the formation might be more adequate to produce efficient search motions, [START_REF] Moore | Source seeking via collaborative measurements by a circular formation of agents[END_REF]. Therefore, an additional component of the control law is also added to distribute of the agents along the elastic formation. This is achieved by taking into account the communication graph between the agents. The collaborative control law stands for the case of rangedependent graph.

The following section presents the problem formulation introducing the affine transformation and the model of the agents. Section III exposes the main contribution of the article which deals with the control law to stabilize the agents to an elastic formation and a cooperative control law to distribute the agents along the formation. Section V presents some particular closed formations and the simulation results.

II. PROBLEM FORMULATION AND PRELIMINARIES

A. Model of agents and Problem Formulation

Consider the standard agent model commonly used in the literature to model AUVs restricted kinematics [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], [START_REF] Sepulchre | Stabilization of planar collective motion with limited communication[END_REF], [START_REF] Paley | Stabilization of symmetric formations to motion around convex loops[END_REF]. It corresponds to a kinematic unicycle fitting with model properties subject to a simple non-holonomic constraint, adequate for the underwater vehicles. Consider a set of N agents, in which each agent k = 1, ..., N has the following constrained dynamics:

ẋk =v k cos θ k (1a) ẏk =v k sin θ k (1b) θk =u k (1c)
where (x k , y k ) T is the position vector of agent k, θ k is the heading angle and v k , u k are the control inputs.

Whit appropriate limits on the control inputs, this model can provide a reasonable approximation for many air and underwater vehicles.

The objective is to stabilize the fleet of agents into a richer class of formations, i.e. non-circular and time-varying formations. In [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], a complex notation was introduced to formulate in an simple manner the circular formation control law using the previous kinematic model with unit velocity v k = 1 ∀k. Here, the vectorial notation (1) is now employed and a simple formulation of the control law is obtained.

Moreover, an additional objective is to distribute the agents along the formation in a cooperative way, taking into account the communication constraints.

B. Preliminaries on Affine Transformations

A circular formation in the plane can be defined by three basic parameters, the center of the circle, its radius and the angular velocity of the agents along the circle. In order to modify these parameters, the affine transformations are introduced.

The three main transformations are the translation, the rotation and the scaling. To express these affine transformations the homogeneous coordinates are defined, [START_REF] Foley | Introduction to Computer Graphics[END_REF]. The homogeneous coordinates of a vector z ∈ R 2 can simply be defined as the new vector z h = (z x , z y , 1) T . Let the vectors e 1 = (1, 0, 0) T , e 2 = (0, 1, 0) T , e 3 = (0, 0, 1) T be a canonic base of the space R 2 expressed in homogeneous coordinates. In the sequel, the basic affine transformations and some of their properties are presented. c) Rotation: A rotation through an angle α counterclockwise around the origin can be written in a matrix form as previously z ′ = R α z h where

R α =   cos α -sin α 0 sin α cos α 0 0 0 1   ω0 ω0 ω0 ω0 ω0 ω0 ω0 cd(t) cd(t, ω0) Rd(t) Rd(rk) α R α(t) α Rα S Rd(rk) TRANSLATION SCALING ROTATION T cd(t) T cd(t,ω0) S Rd(t) S Rd(rk)
Fig. 1. Affine transformations applied to the circular formation Its inverse exists and satisfies R -1 α = R T α . The angle α can be time-varying. A rotation applied to a formation can change its orientation with respect to the frame origin or, in the case of a circular formation, it affects the angular velocity of the agents around the circle as shown in Fig. 1.

The objective is to find a general framework to stabilize the fleet of agents to an elastic formation using these affine transformations. An elastic formation is defined as a closed curve which results of applying a sequence of affine transformations to the unit circle (i.e. a circle centered at the origin with unit radius). This elastic formation can be time-varying if at least one element of the transformation matrices is time-varying. In the sequel, a sequence of affine transformations, which are generated by a combination of the previous ones, is defined as follows:

G = I i J j K k S i R αj T c k (2)
where the subscripts denote the different transformations of the same type which are applied. For instance, the matrix G = S 1 S 2 R α T c is a combination of one translation, one rotation and two different scalings. Note that the matrix multiplication is not commutative. However, the general transformation G considered here, is a sequence of the three affine transformations and the order defined in (2) can be changed, for instance, to G = R α S 1 T c S 2 , which defines an other elastic formation.

As it is shown in the previous paragraph, the affine transformations are invertible, therefore the inverse matrix of the general transformation G -1 exists. Thanks to previous definitions, G and G -1 are differentiable, if their parameters are differentiable. Note that the operators derivative and invertible are not commutative, therefore

( d dt G) -1 = d dt (G -1 ) = Ġ-1 .
In this paper a general transformation is applied to the unit circle to provide different non-circular and time-varying formations. The final formation depends on the sequence used to define G. In other words, starting from a circle, a large class of formations can be obtained.

III. CONTROL DESIGN

In previous section, the basic affine transformations have been defined. The objective is now to design a control law such that the fleet of agents reach an elastic formation defined by any sequence of affine transformations applied to the unit circle.

A. Control Design: Change of Coordinates

Following the previous section, the problem becomes a formation control design based on the circular control law from [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF]. The desired elastic formation is defined by applying the matrix G to unit circle C 0 . The stabilization of system (1) to an elastic formation can be expressed as the stabilization of an adequate transformed system to the unit circle.

The position vector of the agent k in homogeneous coordinates is defined as r k = (x k , y k , 1) T . The main contribution of this paper is to introduce the coordinates transformation:

rk = G -1 r k (3)
where rk = (x k , ŷk , 1) T is the transformed position vector expressed in homogeneous coordinates. The main idea is first, to stabilize this new transformed system to a circle with unit radius R 0 = 1, centered at (0, 0) and with angular velocity ω 0 = 0. Then, to apply the circular control law from [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF]. Finally, to apply the inverse transformation to express the control law in the original framework.

In order to apply the circular formation control law, the new transformed system must have constant linear velocity equal to R 0 ω 0 . Therefore the dynamics of the transformed position vector are defined as:

ẋk =ω 0 cos ψ k (4a) ẏk =ω 0 sin ψ k (4b)
where ψ k represents the angular orientation of the transformed velocity vector ṙk such that:

ψ k = arctan e T 2 ṙk e T 1 ṙk + ǫπ = arctan e T 2 d dt (G -1 r k ) e T 1 d dt (G -1 r k ) + ǫπ where ǫ = 0 if e T 1 d
dt (G -1 r k ) > 0 and ǫ = 1 otherwise. The vector of the new control inputs for this transformed system is ψ = ( ψ1 , . . . , ψN ) T .

Applying the circular control law from [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF] expressed in the transformed framework, the system (4) converges to C 0 . Now we want to come back to the original framework to express the control inputs of the original system v k , u k with respect to the transformed control input ψk . Considering (1), it is easy to see that v k and θ k are given by:

v k = ṙk and tan θ k = ẏk ẋk
An expression of θk is obtained by computing the derivative of tan θ k as follows:

θk (1 + tan 2 θ k ) = d dt ẏk ẋk = ÿk ẋk -ẏk ẍk ẋ2 k
Using the homogeneous coordinates defined previously, the following equation holds:

θk = rT k R π 2 ṙk ṙk 2
The original system is related to the transformed system through the matrix G. The following equations are obtained from the change of coordinates (3):

r k = Gr k ṙk = Ġr k + G ṙk = GG -1 r k + ω 0 G(cos ψ k , sin ψ k , 0) T rk = Gr k + 2 Ġṙ k + G rk = = GG -1 r k + 2 Ġ Ġ-1 r k +2 ĠG -1 ṙk + GR π 2 ( Ġ-1 r k + G -1 ṙk ) ψk
Thanks to these relations, the original framework is expressed with respect to the transformed system and the circular control law for ψk .

B. Formation Control Law

Using the previous definitions of elastic formation and the general transformation matrix, a new control law is proposed in the following theorem:

Theorem 1 Let G be a twice differentiable matrix with bounded derivatives resulting of a sequence of affine transformations as [START_REF] Olfati-Saber | Consensus problems in networks of agents whit switching topology and time-delays[END_REF] and F = G • C 0 be the desired elastic formation. Let ω 0 = 0, κ > 0 be two control parameters such that the following condition is satisfied:

|ω 0 | = G -1 ĠG -1 r k (5)
Then the control law:

v k = ĠG -1 r k + ω 0 G(cos ψ k , sin ψ k , 0) T (6a) u k = 1 v 2 k GG -1 r k + 2 Ġ Ġ-1 r k + 2 ĠG -1 ṙk T R π 2 ṙk + ψk v 2 k Ġ-1 r k + G -1 ṙk T R T π 2 G T R π 2 ṙk (6b) with ψk =ω 0 1 + κω 0 (cos ψ k , sin ψ k , 0)G -1 r k (7a) ψ k (0) = arctan e T 2 d dt (G -1 r k )(0) e T 1 d dt (G -1 r k )(0) + ǫπ (7b)
makes all the agents defined by (1) converge to the elastic formation F . The direction of rotation is determined by the sign of ω 0 .

Proof: Using the relations between the original system and the transformed system detailed in the previous subsection, starting from [START_REF] Kaminer | Trajectory tracking for autonomous vehicles: An integrated approach to guidance and control[END_REF], the control inputs v k , u k are straightforwardly given by [START_REF] Zhang | Cooperative filters and control for cooperative exploration[END_REF]. The convergence of the transformed system to the circular formation is analyzed using the following Lyapunov function, based on the analysis of the circular control law proposed in [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF]:

S(r, ψ) = 1 2 N k=1 ṙk -ω 0 R π 2 rk 2 ≥ 0
where the matrix R π 2 represents a rotation by π 2 but erasing the homogeneous coordinate such that R π 2 (3, 3) = 0. Note that when S(r, ψ) = 0 the dynamics of the transformed system (4) satisfy ṙT k rk = 0 which is the kinematic relation for the rotation of the rigid body. Evaluating the derivative of S(r, ψ) along the solutions of the resulting closed-loop system (4) with the control law (7a) leads to:

Ṡ(r, ψ) = N k=1 ṙk -ω 0 R * rk T R π 2 ṙk ψk -ω 0 R π 2 ṙk = N k=1 ω 0 rT k ṙk (ω 0 -ψk ) = κ N k=1 ω 0 rT k ṙk 2 ≤ 0
Therefore S(r, ψ) is a suitable Lyapunov function for this transformed system. Thus, the solutions converge to the largest invariant set Λ, for which Ṡ = 0. Then, the transformed system (4) asymptotically reaches the circular formation centered at (0, 0) T and of unit radius with fixed angular velocity ω 0 . Thanks to the change of coordinates (3), the dynamic closed-loop equation corresponding to the transformed formation is time-invariant, hence LaSalle Principle can be applied. As stated above, this result is an adaptation of the circular control law in [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF] expressed in the new formulation. Note that this control law has singular points when v k = 0, such that:

v k = ĠG -1 r k + ω 0 G(cos ψ k , sin ψ k , 0) T = 0
This singular point occurs if there exists a time t c such that:

G -1 (t c ) Ġ(t c )G -1 (t c )r k (t c ) = |ω 0 | ∠G -1 (t c ) Ġ(t c )G -1 (t c )r k (t c ) = ψ k (t c )
where ∠ represents the argument of a vector. The equation ( 5) is a sufficient condition to avoid the singular points.

Remark 1 Note that the equation ( 5) is a condition imposed to the transformation matrix G to restrict the variation of its time-varying parameters with respect to the angular velocity ω 0 . In each particular case, it can be expressed in a simple manner and corresponds to an initialization protocol or a physical limitation. For instance, to avoid v k = 0 in the case of a time-varying translation T c , the velocity of the moving circle cannot be equal to the linear velocity of the agents in the circle. The condition [START_REF] Ögren | Cooperative control of mobile sensor networks: Adaptive gradient climbing in a distributed environment[END_REF] becomes R|ω 0 | > ċ where R is the radius of the circle and ċ the velocity of its center, see [START_REF] Briñón | Translation control of a fleet circular formation of auvs under finite communication range[END_REF].

Theorem 1 presents a general control law expressed in the new framework, to stabilize a group of agents to an elastic formation. The term elastic denote the capability of the formation to move and change its shape in order, for instance, to avoid an obstacle (see Fig. 2), to achieve the source seeking problem, to delimit a polluted region, or to avoid unnecessary energy waste. This elastic formation is defined by a sequence of affine transformations G applied to the unit circle. The matrix G is a given reference for all the agents. Note that each agent converges to the formation independently of the rest of the fleet. Following section presents a collaborative control to distribute the agents along the formation defined by G.

C. Cooperative Control: Symmetric Balanced Patterns

This section is dedicated to the problem of homogenizing the distribution of the agents along the formation. In the unit circle C 0 , the agents are uniformly distributed when the angular difference between adjacent vehicles is 2π/N . The distribution of the agents along an elastic formation F depends on the transformation matrix G applied to C 0 .

All-to-all communication topology and some cases of limited communication have been studied in [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], [START_REF] Sepulchre | Stabilization of planar collective motion with limited communication[END_REF] for the circular formation problem. The translation or contraction control laws including this consideration are straightforward obtained, as shown in [START_REF] Briñón | Translation control of a fleet circular formation of auvs under finite communication range[END_REF], [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF]. The solution proposed in these previous works deals with the addition of a potential function depending on the heading angles of which the minimum corresponds to a symmetric pattern. For instance, the symmetric pattern in which all of the particles are uniformly spaced around the circle is called a splay formation. This potential function contains information of the communication links between the agents. The communication topology for the group of agents is represented by means of a communication graph G. L denotes the Laplacian matrix of G, see [START_REF] Biggs | Algebraic Graph Theory[END_REF].

This paragraph presents the notation included in the corollary. The new Laplacian matrix considered is L = L ⊗ I 2 where ⊗ is the classical Kronecker product and I N ∈ R N ×N is the identity matrix and the matrix B m = (cos mψ 1 , sin mψ 1 , ..., cos mψ N , sin mψ N ) T contains all the orientation angles of the transformed system. Considering this notation and applying the previous mentioned works to our new formulation, the following corollary holds:

Corollary 1 Let G be a twice differentiable matrix with bounded derivatives resulting of a sequence of affine transformations as [START_REF] Olfati-Saber | Consensus problems in networks of agents whit switching topology and time-delays[END_REF] and F = G • C 0 be the desired elastic formation. Let ω 0 = 0, κ > 0 and K > 0 be three control parameters and the condition (5) be satisfied. Let G be the communication graph and L be the corresponding Laplacian matrix. Then the previous control law [START_REF] Zhang | Cooperative filters and control for cooperative exploration[END_REF] with:

ψk = ω 0 1 + κω 0 (cos ψ k , sin ψ k , 0)G -1 r k -∂U ∂ψ k U (ψ) = -K N ⌊N/2⌋ m=1 1 2m 2 B T m LB m (8)
where ⌊N/2⌋ is the largest integer less than or equal to N/2 and the initial conditions ψ(0) satisfy (7b), makes all the agents defined by (1) converge to the formation F . The direction of rotation is determined by the sign of ω 0 . Moreover, the splay pattern is an extremum point of the potential U (ψ). If the communication graph is complete (allto-all communication) the splay pattern is asymptotically stable and the uniform distribution of the angles ψ k along C 0 is achieved. Therefore the agents are distributed in the formation F , taking into account the transformation G.

Proof: The stability is analyzed by the composed Lyapunov function V (r, ψ) = κS(r, ψ) + U (ψ) of which the derivative is expressed as V (r, ψ) = κ Ṡ(r, ψ)+∇U (ψ). Based on the previous works [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], [START_REF] Sepulchre | Stabilization of planar collective motion with limited communication[END_REF], the potential function U (ψ) is invariant to rigid rotations. Therefore, using [START_REF] Frew | Coordinated standoff tracking of moving targets using lyapunov guidance vector fields[END_REF], the derivative of the Lyapunov function satisfies V (r, ψ) =

- N k=1 κω 0 rT k ṙk -∂U ∂ψ k 2 ≤ 0.
Thanks to LaSalle Principle, the system converges asymptotically to the elastic formation and the agents are distributed along F taking into account the transformation matrix G.

Remark 2 An extension of this result can be proposed for the case of limited communication preserving the same formulation and considering the connectivity properties for the Laplacian matrix which correspond to several communication graphs. See [START_REF] Olfati-Saber | Consensus problems in networks of agents whit switching topology and time-delays[END_REF], [START_REF] Sepulchre | Stabilization of planar collective motion with limited communication[END_REF], [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF], [START_REF] Biggs | Algebraic Graph Theory[END_REF].

The cooperative control law ( 8) is an extension of the previous formation control law to stabilize elastic formations. The splay pattern is an extremum of the potential function U (ψ) which is added to the transformed control variable ψk . In the case of limited communication range, a communication area ρ is introduced. This means each agent can only receive information from its close neighbors, i.e if the distance between two agents k and j is smaller than ρ, these agents are able to communicate, see [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF]. In this case, the function U (ψ) can be also considered as a repulsion potential which is able to avoid the collisions between the agents.

IV. SIMULATION RESULTS AND PARTICULAR CASES

The previous section shows the general control law to stabilize the agents modeled by (1) to a formation defined by the transformation G. The objective of this generalization is to express the previous formation control laws presented in the literature with the new formulation and to propose a solution to control new class of formations. In order to validate this result, some particular cases are presented in this section. First of all, we show that the works on circular formation [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF], [START_REF] Sepulchre | Stabilization of planar collective motion with limited communication[END_REF], [START_REF] Briñón | Translation control of a fleet circular formation of auvs under finite communication range[END_REF], [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF] can be expressed through this formulation. Next, some new formations are proposed. Some exemples are described in Table I.

A. Circular Formation

The more simple case when G = I 3 is analyzed. The control law becomes: This control law makes all the agents defined by (1) converge to the circular formation C 0 . This result is equivalent to the circular control law from [START_REF] Leonard | Collective motion, networks and ocean sampling[END_REF].

v k =|ω 0 | u k = ψk = ω 0 1 + κṙ T k r k
In order to stabilize a circular formation with a desired radius R > 0 and centered at c = (c x , c y ) the general transformation G is a sequence of a translation and a uniform scaling (s x = s y = R), such that G = T c S R . In this case the control law is expressed as:

v k =R|ω 0 | u k = ψk = ω 0 1 + κṙ T k (r k -c h )
where c h is the position vector of the center in homogeneous coordinates.

B. Combined Motion of a circle

The new formulation shown in this article makes possible the combination of several transformations. This is the case of the combined motion problem in which the circular formation with time-varying radius tracks a time-varying center. Consider the transformation G(t) = T c(t) S R(t) which represents a combined motion (translation and scaling) of the circular formation where the center of the desired formation c(t) : R → R 2 and its radius R(t) : R → R + are twice differentiable functions with bounded first and second time-derivatives. Applying Theorem 1, the agents converge to a circular formation with time-varying radius and moving center. This result is the combination of the two previous works [START_REF] Briñón | Translation control of a fleet circular formation of auvs under finite communication range[END_REF], [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF] expressed in the new framework.

Figure 2 shows the simulation of five agents governed by the control law ( 6) with [START_REF] Frew | Coordinated standoff tracking of moving targets using lyapunov guidance vector fields[END_REF] where G(t) = T c(t) S R(t) . The control law parameters are ω 0 = 1, κ = 1 and K = 1/10. The time-varying radius reference is R(t) = 5 + 2 cos 2π 500 t and c(t) = ( 1 10 t, 3 sin 2π 300 t) T is the tracked time-varying center. The agents converge to the moving formation for any random initial conditions (position and heading of the agent) represented in the figure by the blue void agents. This is an example of one possible application of the combined motion control law and a first step to achieve the final objective: to develop a collaborative control to generate both references in a distributed way. Moreover, the communication radius considered here is ρ = 10 which satisfies the geometrical condition ρ > 2R max sin π N where R max is the up-bound of the radius reference. Therefore the agents are distributed along the time-varying circular formation, see [START_REF]Contraction control of a fleet circular formation of auvs under limited communication range[END_REF].

C. Elliptic formation

The general formulation presented in this article is pertinent also to stabilize the fleet to non-circular formations as an ellipse. In this case the transformation is a time-invariant non-uniform scaling G = S where s x = s y .

Figure 3 shows a simulation of five agents with the controller designed in Theorem 1 and all-to-all communication. The control law parameters are ω 0 = 1, κ = 1 and K = 1/10. The agents are stabilized to the elliptic formation defined by the non-uniform scaling s x = 5, s y = 1. Moreover the agents are distributed along the formation considering the transformation of the splay pattern which is stable in the original unit circle.

V. CONCLUSIONS

We have developed a general control law to stabilize a fleet of agents to an elastic formation, for instance timevarying or non-circular formation, which is defined by a sequence of affine transformations (translation, rotation and scaling) applied to the unit circle. Some particular cases and simulations have been presented to show the convergence of this control law and some possible applications. Moreover, this paper proposes a cooperative control algorithm to distribute the agents along the elastic formation. This potential function is designed by taking into account the communication graph between agents.

At this time, it is assumed that all agents have perfect knowledge of the transformation matrix G and its first and second derivatives. Further developments would consider a cooperative algorithm which will relax this assumption, and the elastic formation will be defined in a collaborative way.

Moreover, an other future research goal is to include the effect of different disturbances as currents on the formation control algorithm.

  a) Translation: The translation T of a point z by a vector c corresponds to the following operation T (z) = z + c. This can be expressed in a matrix multiplication of the form z ′ = T c z h where is expressed in homogeneous coordinates. Its inverse exists and satisfies T -1 c = T -c . Note that c can be timevarying. This translation is pertinent to move the center of the formation, see Fig. 1.b) Scaling: A non-uniform scaling expressed in homogeneous coordinates is a transformation such that z ′ = Sz h where x > 0, s y > 0. Its inverse matrix contains the inverse of its elements. The parameters of the scaling can be timevarying. Some examples of scalings can even lead to ellipses or other closed curves as shown in Fig.1.

  Circular formation (c,R) G = TcS Translation of circular formation G = T c(t) S Contraction of circular formation G = TcS R(t) Combined motion G = T c(t) S R(t) Elliptic formation G = S a,b Rotating elliptic formation G = RαS a,b

Fig. 2 .

 2 Fig.2. Simulation of five agents governed by the control law[START_REF] Zhang | Cooperative filters and control for cooperative exploration[END_REF] whereG(t) = S R(t) T c(t) .The circular formation with time-varying radius tracks the time-varying center reference in order to avoid the obstacles (black blocks).

Fig. 3 .

 3 Fig. 3. Simulation of five agents stabilized in an elliptic formation. The red line represents the trajectory of one agent (elliptic formation). The figure shows two snapshots. The blue agents represent the initial conditions. The ones represent the final state t = 400s.

This work was supported by EU STREP project FeedNetBack FP7-ICT-2007-2.[START_REF] Olfati-Saber | Consensus and cooperation in networked multi-agent systems[END_REF] Simulations are accessible in the CONNECT project web at http://www.lag.ensieg.inpg.fr/connect/.


Realistic Implementation of Message Sequence Charts

Keywords: High-level Message Sequence Charts, Communicating Finite State Machines, code generation, Promela, Sofat

This work revisits the problem of program synthesis from specifications described by High-level Message Sequence Charts. We first show that in the general case, synthesis by a simple projection on each component of the system allows more behaviors in the implementation than in the specification. We then show that differences arise from loss of ordering among messages, and show that behaviors can be preserved by addition of communication controllers, that intercept messages to add stamping information before resending them, and deliver messages to processes in the order described by the specification.

Introduction

Message Sequence Charts (MSCs for short)) [13] is a formal language based on composition of finite communication sequences. MSCs are made of two layers of specification. At the lowest level, basic MSCs describe the behavior of a finite set of processes that can communicate via asynchronous messages. At the higher level, basic MSCs are composed using High-level MSCs (HMSCs for short), a finite automaton labeled by basic MSCs. The language is then very simple and needs only to learn few concepts to be able to model behaviors of distributed systems. It has met considerable interest, both from an academic and industrial point of view. Indeed, this model has raised new theoretical problems (verification, synthesis, ...) but also renewed the interest for existing problems and solutions in other concurrency models such as traces [START_REF] Muscholl | Deciding properties for message sequence charts[END_REF]. From an industrial point of view, MSCs or their UML variant (sequence diagrams) have also been used to model requirements in distributed systems [START_REF] Baker | Automatic generation of conformance tests from message sequence charts[END_REF], and have proved to be efficient modeling tools to discover errors at early stages of system design. HMSCs are very expressive. The usual verification techniques that usually apply to finite state machines (model checking of temporal logic formulae, intersecting two specifications) are in general undecidable for HMSCs. Fortunately, several syntactic classes of HMSCs with more decidable problems have been characterized [START_REF] Alur | Model checking of message sequence charts[END_REF][START_REF] Ben-Abdallah | Syntactic detection of process divergence and non-local choice in message sequence charts[END_REF][START_REF] Genest | Infinite-state high-level mscs : Model-checking and realizability[END_REF]. The restriction to these classes should however remain a reasonable limitation of the expressive power of HMSCs that does not impact the usability of the model. Restricting to bounded HMSCs [START_REF] Alur | Model checking of message sequence charts[END_REF], for instance, reduces the expressive power of HMSCs to that of finite automata, which is in general too restrictive for the kind of asynchronous applications that are usually modeled with scenarios. The other difficulty is that in general, HMSCs are not implementable. It means that system designers can not synthesize a distributed program from HMSCs, and hence can not reuse all the modeling and verification work performed on HMSCs to guarantee correctness of the synthesized implementation.

Again, designers can rely on syntactic subclasses of HMSCs that can be implemented. However, proposed classes until now are not general enough. The reconstructible HMSCs of [11] impose restrictions on the way loops and choices are used, and the solution in [START_REF] Genest | Infinite-state high-level mscs : Model-checking and realizability[END_REF] imposes conditions on the set of active processes in a basic MSC. Other implementation techniques implement exactly the language of a bounded HMSC, but with deadlocks [START_REF] Mukund | Synthesizing distributed finitestate systems from mscs[END_REF], or avoid deadlocks but need several initial states in the synthesized machines [START_REF] Baudru | Synthesis of safe message-passing systems[END_REF]. In our opinion, deadlocks should not be allowed in an implementation of an HMSC : it amounts to deciding at runtime that an ongoing execution is not valid, as it does not belong to the specification. In this work, we consider that a realistic implementation of HMSCs should not allow deadlocks, at least in distributed systems that do not allow compensation and backtracking. We furthermore consider that a distributed system implements an HMSC if the prefix closure of the behaviors of the original specification and of the synthesized machines are identical.

This paper proposes an implementation mechanism for local message sequence charts, that is HMSC specifications that do not require distributed consensus to be implementable. The proposed technique is to project an HMSC on each process participating to the specification. It is well known that this solution produces programs with more behaviors than in the specification [11]. We then compose these projections with local controllers, that intercept mes-INRIA sages between processes and tag them with sufficient information to avoid the additional behaviors that appear in the sole projection. The main result of this work is that the projection of the behavior of the controlled system on events of the original processes is equivalent (up to a renaming) to the behavior of the original HMSC.

This paper is organized as follows. Section 2 defines the formal models that will be used in the next sections. Section 3 characterizes an interesting syntactic class of HMSCs called local HMSCs. Section 4 defines the projection operation, that generates communicating finite state machines from an HMSC, and shows that an HMSC and its projection are not equivalent in general. Section 5 proposes a solution based on local control and message tagging to implement properly an HMSC. Finally, section 6 presents a small prototype before conclusion.

Definitions

MSCs is a partial-order based standard formalism. It is a visual notation, which clearly expresses interactions among concurrent processes. It consists essentially of a finite set of processes (also called instances) denoted I, that run in parallel and exchange messages in a one-to-one, asynchronous fashion. MSCs and their variants are widely used to capture use cases and requirements during the early design stages of distributed systems. They have been adopted within several software engineering methodologies and tools for concurrent, reactive and real-time systems. e.g. [1,2,[START_REF]Uml notation guide[END_REF][START_REF] Selic | Real-time object-oriented modelling[END_REF].

A basic MSC is a diagram that defines a simple communication scenario between instances. The life lines of instances are drawn vertically from top to bottom and define sequences of events. An event can be a message sending or reception, or a local action. Horizontal arrows represent asynchronous messages from one instance to another. Examples of bMSCs are shown in Figure 1.

Definition 1 (bMSCs)

A bMSC is a tuple M = (E, ≤, C, φ, t, m) where :

-E is a finite set of events.

-φ : E -→ I localizes events on the different instances. E can be split into a disjoint union p∈I E p , where E p = {e ∈ E | φ(e) = p} is the set of events occurring on instance p. E can also be considered as the disjoint union S R L in order to distinguish send events (e ∈ S), receive events (e ∈ R) or local actions (e ∈ L). -C is a finite set of message contents and action names.

-t : E -→ Σ gives a type to each event, with Σ = {p!q(a), p?q(a), a | p, q ∈ I, a ∈ C}. We have t(e) = p!q(a) if e ∈ E p ∩S is a send event of message a from p to q, t(e) = p?q(a) if e ∈ E p ∩R is a receive event of message a by p from q and t(e) = a if e ∈ E p ∩ L is a local action, named a located on p. -m : S -→ R is a bijection that matches send and receive events. If m(e) = f , then t(e) = p!q(a) and t(f ) = q?p(a) for some p, q ∈ I and a ∈ C. -≤ ⊆ E 2 is a partial order relation (the "causal order"). It is required that events of the same instance are totally ordered : ∀(e For a bMSC M , we will denote by min(M ) = {e ∈ E | ∀e ∈ E, e ≤ e ⇒ e = e}, the set of minimal events of M , and by min p (M ) the first event located on instance p ∈ I (if it exists). An instance is called minimal if it carries a minimal event. Similarly, we will denote by max(M ) = {e ∈ E | ∀e ∈ E, e ≤ e ⇒ e = e} the set of maximal events of M .

Standard notation of bMSCs also allows for the definition of a zone on an instance axis called co-region. It describes the absence of ordering along an instance axis. MSCs also allow behaviors with message overtaking, i.e. in which messages are not received in the order of their emission. Without loss of generality, we do not consider these aspects : co-regions can be simulated by adding a finite number of alternatives in an HMSC containing the interleaving of events within coregions, and message crossing can not occur within the targeted architecture. We then suppose that all bMSCs are FIFO, that is for two sending events e, e such that p = ϕ(e) = ϕ(e ), q = ϕ(m(e)) = ϕ(m(e )) we always have e ≤ p e ⇐⇒ m(e) ≤ q m(e ).

Definition 2 Let M = (E, ≤, C, φ, t, m) be a bMSC. A prefix of M is a tuple (E , ≤ , C , φ , t , m ) such that E is a subset of E closed by causal precedence (i.e. e ∈ E and f ≤ e implies f ∈ E ) and ≤ , C , φ , t , m are restrictions of ≤, C, φ, t, m to E . A suffix of M is a tuple (E , ≤ , C , φ , t , m ) such that E is closed by causal succession (i.e. e ∈ E and e ≤ f implies f ∈ E ) and ≤ , C , φ , t , m are restrictions of ≤, C, φ, t, m to E . A piece of M is the restriction of M to a set of events E = E \ X \ Y , such that the restriction of M to X is a prefix of M and the restriction of M to Y is a suffix of M .

Note that prefixes, suffixes and pieces are not always bMSCs, as the message mapping m is not necessarily a bijection from sending events to receiving events. In the rest of the paper, we will denote by P ref (M ) the set of all prefixes of a bMSC M .

INRIA

Definition 3 (Sequencing) The sequencing operator • for two bMSCs

M 1 = (E 1 , ≤ 1 , C 1 , φ 1 , t 1 , m 1 ) and M 2 = (E 2 , ≤ 2 , C 2 , φ 2 , t 2 , m 2
) consists in concatenation of the two bMSCs instance by instance. M 1 • M 2 = (E, ≤, C, φ, t, m), where :

-

E = ϕ 1 (E 1 ) ϕ 2 (E 2 )
where ϕ 1 and ϕ 2 are two isomorphisms with disjoint images. -∀e, e ∈ E, e ≤ e iff ϕ -1

1 (e) ≤ 1 ϕ -1 1 (e ) or ϕ -1 2 (e) ≤ 2 ϕ -1 2 (e ) or ∃(e 1 , e 2 ) ∈ E 1 × E 2 : φ 1 (e 1 ) = φ 2 (e 2 ) ∧ ϕ -1 1 (e) ≤ 1 e 1 ∧ e 2 ≤ 2 ϕ -1 2 (e ) -∀e ∈ E, φ(e) = φ 1 (ϕ -1 1 (e)) if e ∈ ϕ 1 (E 1 ) or φ(e) = φ 2 (ϕ -1 2 (e)) if e ∈ ϕ 2 (E 2 ) and m(e) = m 1 (ϕ -1 1 (e)) if e ∈ ϕ 1 (E 1 ) or m(e) = m 2 (ϕ -1 2 (e)) if e ∈ ϕ 2 (E 2 ).
An example of concatenation is shown in Figure 2. In the next sections, we will also need to concatenate prefixes and pieces of bMSCs. Prefix and piece concatenation is defined alike bMSC concatenation with an additional phase that rebuilds the message mappings. Let O 1 be a prefix of a bMSC, and O 2 be a piece of MSC. Then, the concatenation of O 1 and O 2 is denoted by

O 1 • O 2 = (E, ≤, C, φ, t, m)
, where E, ≤, C, φ, and t are defined as in definition 3 and m is a function that associates the n th sending event from p to q to the n th reception from p on q for every pair of processes p, q ∈ I. Note that this sequencing is not defined if for some p, q, n, the types of the n th sending and reception do not match, that is one event is of the form p!q(m) and the other one q?p(n) with n = m. In particular, we will denote by O • {a} the prefix obtained by concatenation of a single event a to a prefix O. HMSC diagrams are automata that compose basic MSCs or other HMSCs. The whole language contains iteration, choice, and parallel composition. In this paper, we restrict to HMSCs without parallel frames, and suppose without loss of generality that our HMSCs comprise only one hierarchical level, i.e. they are automata labeled by bMSCs.

Definition 4 (HMSCs)

A HMSC is a graph H = (I, N, →, M, n 0 ), where -I is a finite set of instances.

-N is a finite set of nodes and n 0 ∈ N is the initial node of H.

-M is a finite set of bMSCs which participating instances belong to I, and defined on disjoint sets of events. -→⊆ N × M × N is the transition relation.

Figure 1 shows a complete HMSC. In the rest of the paper, and without loss of generality, we will consider that all nodes, except possibly the initial node and the sink nodes are choice nodes, i.e. have several successors by the transition relation (by finite concatenation of bMSCs, an HMSC can be always transformed in such a canonical form). We also require HMSCs to be deterministic (this can be ensured by the standard determinization procedure of finite automata).

Definition 5 (HMSC behavior) As usual, for an HMSC H, we define as P aths(H) the set of paths of H starting from the initial node. We will say that a path is acyclic if and only if it does not contain twice the same transition. Note that our definition of the language of an HMSC H includes all prefixes of bMSCs generated by H. A correct implementation of an HMSC H is a distributed system which reproduces exactly (and nothing more) L(H).

Local HMSCs

A bMSC can have several minimal instances, called deciding instances. The set of deciding instances in a bMSC M is simply φ(M in(M )). They carry the first events that happen in M . Obviously, these events cannot be message receptions. So the deciding instances can choose to perform exactly the same scenario at a choice node. The other non-deciding instances have to conform to the chosen scenario. This raises a problem : if the outgoing transitions of a choice node are labeled by bMSCs with distinct deciding instances, then, without synchronization among them in the distributed implementation, one instance might decide to perform one scenario M 1 , and another instance an incompatible scenario M 2 . There are two solutions to avoid this bad situation : either impose synchronization of all processes before each choice with more than one deciding instance to elect the next scenario to perform, or restrict to HMSCs in which a single instance decides at each choice (the so-called local-choice HMSCs [START_REF] Ben-Abdallah | Syntactic detection of process divergence and non-local choice in message sequence charts[END_REF]). The first solution has the drawback that it adds synchronization and consensus mechanisms to the implementation, and hence modifies the specification. We will show later in the paper that working with local-choice HMSCs does not always guarantee that the implementation is correct.

Definition 6 (Local choice node) Let H = (I, N, →, M, n 0 ) be an HMSC, and let c ∈ N . Choice c is local if and only if for every pair of (non necessarily

distinct) paths ρ = c M1 -→ n 1 M2 -→ n 2 . . . n k and ρ = c M 1 -→ n 1 M 2 -→ n 2 . . . n k there is a single minimal instance in O ρ and in O ρ (i.e. φ(M in(O ρ )) = φ(M in(O ρ )) and |φ(M in(O ρ ))| = 1). H is called a local-choice HMSC if all its choices are local.
Intuitively, the local-choice property [START_REF] Ben-Abdallah | Syntactic detection of process divergence and non-local choice in message sequence charts[END_REF] guarantees that every choice is controlled by a unique instance.

Theorem 1 (Deciding locality) Let H be an HMSC. H is not local iff there exists a node c and a pair of acyclic paths ρ, ρ originating from c, such that O ρ and O ρ have more than one minimal instance.

INRIA

Proof : one direction is straightforward : if we can find a node c and two (acyclic) paths with more than one deciding instance, then obviously, c is not a local choice, and H is not local. Let us suppose now that for every node c, and for every pair of acyclic paths of H originating from c, we have only one deciding instance. Now, let us suppose that there exist a node c 1 and two paths ρ 1 , ρ 1 such that at least one (say ρ 1 ) of them is not acyclic. Then ρ 1 has a finite acyclic prefix w 1 . The set of minimal instances in O w1 and in O ρ1 is the same, as φ(min(M •M )) = φ(min(M )). Hence, c, ρ 1 , ρ 1 are witnesses for the non-locality of H iff c, w 1 , ρ 1 are also such witnesses.

Theorem 2 (Complexity of local choice) Deciding if an HMSC is localchoice is in co -N P .

Proof : the objective is to find a counter example, that is two paths originating from the same node with distinct deciding instances. One can choose in linear time in the size of H a node c and two finite acyclic paths ρ 1 , ρ 2 of H starting from c, that is sequences of MSCs of the form

M 1 . . . M k . One can compute a concatenation O = M 1 • • • • • M k in polynomial
time in the total size of the ordering relations. Note that to compute minimal events of a sequencing of two bMSCs, one does not have to compute the whole causal ordering ≤, and only has to ensure that maximal and minimal events on each instance in two concatenated MSCs are ordered in the resulting concatenation. Hence it is sufficient to recall a covering of the local ordering ≤ p on each process p ∈ I plus the message relation m. Then finding the minimal events (or equivalently the minimal instances) of O can also be performed in polynomial time in the number of events of O, as M in(M

) = E \ {f | ∃e, e ≤ p f ∨ f = m(e)}.
From theorem 1, an algorithm that checks locality of HMSCs is straightforward. It consists in a width first traversal of acyclic paths starting from each node of the HMSC. If at some time we find two paths with more than one minimal instance, then the choice from which these path starts is not local. Note that minimal instances need not be computed for the whole MSC labeling each path, and can be updated at the same time as paths. Indeed,

if ρ = ρ 1 .ρ 2 is a path of H, then φ(M in(M ρ )) = φ(M in(M ρ1 )) ∪ (φ(M in(M ρ2 )) \ φ(M ρ1 )).
It is then sufficient for each path to maintain the set of instances that appear along this path, and the set of minimal instances, without memorizing exactly the scenario played. As we consider only acyclic paths of the HMSC the following algorithm terminates.

The following algorithm was proposed in [11]. It builds a set of acyclic paths starting from each node of an HMSC. A non-local choice is detected if there is more than one deciding instance for a node c. The algorithm remembers a set of acyclic paths P , extends all of its members with new transitions when possible, and places a path ρ in M AP as soon as the set of transitions used in ρ contains a cycle.

Algorithm 1 LocalChoice(H)

for c node of

H do P = {(t, I, J) | t = (c, M, n) ∧ I = φ(min(M )) ∧ J = φ(M )} MAP = ∅ /*Maximal acyclic Paths*/ while P = ∅ do MAP = MAP ∪ {(w.t, I ) | w = t 1 ...t k ∧ t k = (n k-1 , M k , n k ), t = (n k , M, n) ∧ t ∈ w ∧ (w, I, J) ∈ P ∧ I = I ∪ (φ(min(M )) -J)} P = {(w.t, I , J ) | (w, I, J) ∈ P, w = n 1 ...n k ∧ t k = (n k-1 , M k , n k ), t = (n k , M, n) ∧ t ∈ w ∧ J = J ∪ φ(M ) ∧ I = I ∪ (φ(min(M )) -J)} end while DI = (w,I)∈M AP I /*Deciding Instances*/ if | DI | >1 then H contains a non-local choice c end if end for

The synthesis Problem

In this section, we introduce our implementation model, namely Communicating Finite State Machines (CFSM) [START_REF] Brand | On communicating finite state machines[END_REF]. A CFSM A is a network of finite state machines that communicate over unbounded, non-lossy, error-free and FIFO communication channels. We will write A = i∈I A i to denote that A is a network of machines describing the behaviors of a set of machines {A i } i∈I . A communication buffer B (i,j) is associated to each pair of instances (p, q) ∈ I 2 . Buffers will implement messages exchanges defined in the original HMSC. Now that HMSCs (a global specification) and communicating finite state machines (a set of local reactive machines, without global control) are defined, we can describe the synthesis problem as follows : given an HMSC H over a set of instances I, build a set of communicating state machines A 1 , . . . A |I| which behaves exactly as L(H).

An obvious solution is to project the original HMSC on each instance. Unfortunately, this solution does not work for all HMSCs. Consider for instance a non local HMSC that contains a choice c, such that c M1 → n 1 and c M2 -→ n 2 , and M 1 and M 2 have two distinct deciding instances p and q. Then, the projection of H on its instances produces automata that can behave exactly as in H up to choice c, and then p decides to execute scenario M 1 while q decides to execute scenario M 2 . Clearly, this execution was not defined in H. Hence, the projection of an HMSC on its instances can define more behaviors than the original specification, but can also deadlock. In the rest of the paper, we will only consider local-choice HMSCs. However, we will show in this section that this is not sufficient to ensure correctness. We will also consider that two MSC labeling distinct transitions of a local HMSC start with distinct messages. This assumption will be used to differentiate distinct choices at runtime. It is not essential in our framework, as we may enforce instances to tag their messages with the transition of the HMSC currently executed by the instance. However, it greatly simplifies the notations and proofs.

INRIA

The principle of projection is to copy the original HMSC on each instance, and to remove all the events that do not belong to the considered instance. By construction, we keep the structure of the HMSC automaton. Each transition is a sequence (possibly empty) of events. This object can be considered as a finite state automaton by adding intermediary states in sequences of events. Empty transitions can be removed by the usual ε-closure procedure for finite state automata.

Definition 7 (Projection) Let us consider an HMSC H = (I, N, →, M, n 0 ). The set of events of a bMSC M is denoted by E M , and the set of events of M located on instance i by E M i . States can be coded by tuples Q = N × M × N × N, the first three components designating an HMSC transition and the last one designating the rank of the event on the considered instance in the bMSC labeling this transition. For an instance i ∈ I, we define the finite state automaton A i , result of the projection of H onto the instance i by

A i = (Q, → i , E i ∪ {ε}, n 0 ) with E i = M ∈M E M i . The set E M i is totally ordered. We denote its elements by e 1 , • • • , e |E M i | . With the convention that (n, M, n , 0) ≡ n and (n, M, n , |E M i |) ≡ n , → i is the smallest set such that ∀n, n ∈ N, ∀M ∈ M, if E M i = ∅, (n, ε, n ) ∈→ i , else 1≤k≤|E M i | ((n, M, n , k - 1), e k , (n, M, n , k)) ∈→ i .
Each run of this set of communicating machines defines a prefix, that can be built incrementally starting from the empty prefix, and appending one executed event after the other (i.e. it is built from a total ordering of all events occurring on the same process, plus a pairing of messages sending and receptions). From this definition, the language L(A) of a set of communicating machines is the set of all prefixes associated to runs of A. Let us consider the projections of H in Figure 1 on all its instances given in Figure 3. A correct behavior of H is shown in the left part of Figure 4, while a possible but incorrect behavior of the distributed interaction of the projected RR n°7597 machines is shown in the right part. We can see that message m 3 sent by machine A to machine D can be delayed and received after message m 4 from machine D, hence mixing two different basic MSCs. Machine C does not have enough information to decide to delay the reception of m 4 according to the HMSC semantics. This example proves that in general, even for local HMSCs, the synthesis by projection is not correct. It is however proved [11] that the set of behaviors of the synthesized specification contains the set of behaviors of the original specification. The machines synthesized by projection allow more behaviors than the original global specification because some global ordering among actions is lost during projection. A subclass of local HMSCs called reconstructible HM-SCs that avoids this problem has been proposed [11]. This reconstructibility condition says that local ordering among events from two consecutive choices originating from the same node can be deduced from the FIFO property and from the ordering among minimal events in each chosen MSC. However, reconstructibility is easily lost when two instances communicate indirectly through distinct sets of instances, as in the example of figure 1. Another solution proposed by [START_REF] Genest | Infinite-state high-level mscs : Model-checking and realizability[END_REF] restricts to a class of local HMSCs in which all processes take part in every branch. Both approaches are restrictive, as they constrain the way processes are used in each branch of an HMSC.

In the next section, we take a different approach, and show that adding information to messages is sufficient to obtain a correct synthesis in the general case of local HMSCs.

Implementing HMSCs with message Controllers

We propose a new implementation mechanism, that will allow for the implementation of any local HMSC H, without syntactic restriction. The architecture is as follows : for each process, we compute an automaton, as shown in previous section by projection of H on each of its instances. The projection is the same as previously, with the slight difference that the synthesized automaton communicates with his controller, and not directly with other processes. To differentiate, we will denote by K(A i ) the "controlled version" of A i , keeping in mind that A i and K(A i ) are isomorphic machines. Then, we add to each automaton K(A i ) a controller C i , that will receive all communications from K(A i ), and tag them INRIA with a stamp. Similarly, each controller will receive all tagged messages destinated to K(A i ), and decide with respect to its tag whether a message must be sent immediately to K(A i ) or delayed. Automata and their controller communicate via FIFO channels, which defines a total ordering on message receptions or sendings. In this section, we first define the distributed architecture and the tagging mechanism that will allow for preservation of the global specification. We then define control automata and their composition with synthesized automata. We then show that for local HMSCs the controlled local system obtained by projection behaves exactly as the global specification (up to some renaming and projection that hides the controllers).

Distributed architecture

We consider the n = |I| automata {K(A i )} 1≤i≤n obtained by projection of the original HMSC on the different instances. These automata K(A i ) are connected via a bidirectional FIFO channel (port P ) to their associated controller C i (port P i ). The controllers are themselves interconnected via a complete graph of bidirectional FIFO channels (for all i = j, port P j of controller C i is connected to the port P i of controller C j ). This is illustrated in Figure 5. This architecture is quite flexible : all the components run asynchronously and exchange messages, without any other assumption on the way they share resources, memory or processors.

Tagging mechanism

Definition 8 Let H be a local HMSC. We set an ordering on all nodes of H, and adopt a lexicographical ordering l on labels of Σ. A branch of H is a transition (c, M, n) of H, such that c is a choice node. We will denote by B H all branches of H. For a given choice node c, we will suppose that all branches stemming from c are pairwise distinguishable from their minimal actions, that is if (c, M, n) and (c, M , n ) are two branches, then t(min(M )) = t(min(M )). The ordering on nodes extends to branches : we will say that b

1 = (c 1 , M 1 , n 1 ) precedes b 2 = (c 2 , M 2 , n 2 ) and write b 1 b 2 iff        c 1 c 2 , or c 1 = c 2 and n 1 n 2 , or c 1 = c 2
and n 1 = n 2 and t(min(M 1 )) l t(min(M 2 ))

Definition 9 ( Choice clocks) A choice clock of an HMSC H is a vector of

N B H . Let ρ = n 0 M1 -→ n 1 M2 -→ n 2 . . . M k -→ n k be a path of H. The choice clocks labeling of O ρ is a mapping τ : E Oρ -→ N B H such that for every i ∈ 1..k, e ∈ M i , τ (e)[b] is the number of occurrences of branch b in n 0 M1 -→ n 1 M2 -→ n 2 . . . Mi -→ n i
The usual terminology and definitions on vectors apply to choice clocks. A vector V 2 is an immediate successor of a vector

V 1 of same size, denoted V 1 V 2 , if there is a single component b such that V 1 [b]+1 = V 2 [b], and V 1 [b ] = V 2 [b ] for all other entries b . Vectors V 1 and V 2 are equal if V 1 [b] = V 2 [b] for every entry, and V 2 is greater than V 1 iff V 1 [b] = V 2 [b] for some entries b, and V 1 [b] < V 2 [b] for all others.
For a given path ρ = n 0

M1 -→ n 1 M2 -→ n 2 . . . M k
-→ n k , we will call the choice events of O ρ the minimal events in every M i , i ∈ 1..k. It is rather straightforward to see that when an HMSC H is local, then for every path ρ of H, the set of choice events in O ρ is totally ordered. Note also that for a pair of events e, f in O ρ , τ (e) = τ (f ) if and only if e, f belong to the same MSC M i . From these facts, the following proposition is straightforward :

Proposition 1 Let H be a local HMSC, and ρ be a path of H. Let ≺ be the usual ordering on integer vectors. Then (τ (E Oρ ), ≺) is a totally ordered set. This proposition is important : it means that if one is able to maintain locally a consistent tagging of messages, then a local automaton that receives two messages can always decide which message should be received first.

Definition 10 (Concerned instances) Let b = (c, M, n) be a branch of an HMSC H. We will say that instance p ∈ I is concerned by branch b if and only if there exists an event of M on p (E M p = ∅). Let K ∈ N B H be a choice clock, and let p ∈ I be an instance of H. The vector of choices that concern p in K is the restriction of K to branches that concern p, and is denoted by [K] p .

For a given instance i, the controller C i associated with the projected automaton K(A i ) will receive the messages sent by K(A i ) and by the other controllers. We consider that messages exchanged between the automata and the controllers are triple (j, m, b) where j ∈ I is the destination automaton, m ∈ C is the message name, and b the branch in which the sending event has occurred. In other words, in our controlled architecture, an automaton executes p!C p (q, m, b) instead of p!q(m). The messages exchanged between controllers are tagged and represented by pairs (m, τ ) where m is a message name and τ ∈ N B H a choice vector. In addition, the controller C i maintains several local variables :

INRIA -τ i ∈ N B H ,
its local known choices vector. It is initialized to the null vector, and updated upon consumption of incoming messages. -nbevt, which counts the remaining number of communication events of the instance i to be treated in the current branch that is being processed. -Rec is a sequence of reception events. nbevt and Rec are initialized with constant values (that depend on the chosen branch) when dealing with the first event of a branch on process i. -currentb, which memorizes the branch of H that is currently executed by process i. In the rest of the paper, we will denote by π i (M ) the sequence of events obtained by projection of M on instance i ∈ I, and by π i,? (M ) the restriction of this sequence to receptions. The generic algorithm for a controller C i is composed of two rules, which are continuously active. Rule 1 applies to communications from K(A i ) to C i . First case corresponds to minimal events controlled by the projected automaton K(A i ). When dealing with the first event of the bMSC (branch b) to be processed, the only role of the controller is to compute the tag (increment of the corresponding component of τ i ) and to initialize the variables nbevt and Rec. The currently processed branch is stored in variable currentb. The other case deals with communications from K(A i ) that are not choices of K(A i ). These events are generated in correct order by construction of the projection.

The second rule applies for every port P j , j = i, and aims at controlling the order of the different receptions. This is the rationale of the controller. There are three cases. The first case occurs when a branch of H has already been started, that is a controller C i has received (i.e. consumed) a message indicating the choice performed by the deciding instance of this branch, and a valid message arrives. In this situation, all the components concerning K(A i ) of the current tag τ i and of the tag τ labeling the incoming message must be equal, and this incoming message must be the next expected message (i.e. the next reception in Rec) in currently executed branch. Then the message can be consumed by C i and forwarded to K(A i ). The fact that there is only one FIFO channel between the controller C i and the projected automaton K(A i ) ensures the correct order of receptions on this automaton. The second case is when the incoming message is the first communication signaling a new choice. The controller then checks if the received message defines the next branch of H that must be executed by K(A i ). This is done by verifying if the received tag is the next tag to be treated (considering only the components that concern

K(A i )), that is [τ i ] i [τ ] i .
In that case, the current tag can be updated. The current branch is retrieved by considering the component that differs between [τ ] i and [τ i ] i . Then the remaining number of events that should be executed within this branch (the number of events on the instance i in the bMSC of the current branch, minored by one) is set, as well as the expected sequence of receptions, before transmission of the message to K(A i ). The third case applies when none of the above situations hold, that is the incoming message on port P j can not yet be consumed, either because it is not the next reception expected (another reception on another port should occur before this one) or the incoming message signals that a new choice has been started, but more events must occur before consuming it. In such case, the controller does nothing, and waits for other messages on other ports.

Lemma 1 For all H, local choice HMSC, the choices events in any behavior of the synthesized communicating machines are totally ordered.

proof : We will prove this property by induction. Let us denote by P n the property : for all H, local choice MSC, the choices in any behavior of the synthesized communicating machines in a run containing n choices are totally ordered.

Let us first verify this property for n = 2. As H is local choice, then there is only one CFM that can perform an action (a message sending) from the initial configuration. The next choice can then only be played after the first one. Hence, the first two choices are ordered.

Let us suppose the property verified up to n, and prove that it also holds for

n + 1. Let us suppose a prefix O • O from L(||K(A i )|C i ) with n + 1 choices, such that O contains n choices. Then, O is of the form O = {c 1 } • O 1 . . . {c n } • O n ,
where each c i is a choice event, and such that {c 1 } • O 1 is a prefix of the first MSC M 1 played in this run. Then, O•O can be completed by piece P 1 such that O • O • P 1 contains a complete execution of the first MSC M 1 (so far, nothing forces M 1 to be completely executed). O • O • P 1 can be equivalently rewritten as

O•O 1,1 •. . . O 1,n •P 1 •{c 2 }•O 2 . . . {c n }•O n •O , where each O 1,i is the part of O i that belongs to M 1 and O i = O i \ O 1,i , as events in {c 2 } . . . {c n } • O n • O do not need
to wait for the execution of any event in P 1 to be fireable. Note that P 1 is ensured to be a legal continuation of O • O as no machine can start executing events with tag greater than 0 B H before executing its task in M 1 . Let us denote by P 2,n = {c 2 } . . . {c n }•O n •O the tagged piece starting at choice event c 2 , and by P 2,n the same piece, where all tags are decremented on component M 1 . P 2,n is a run with n choices of an HMSC H , which is a copy of H where the initial node is the node reached in H after M 1 . Hence, all choices in P 2,n are ordered, and so are choices in w . Hence, all choices in O • O are totally ordered.

As choice events are the only moment when a tag is updated, this lemma also means that the set of tags that can appear in an execution is the set of tags labeling choice events, and hence that the tags produced in any run that belongs both to L(H) and L(||K(A i )|C i ) are the same. We are now ready to prove the two inclusions. I) First let us show that Ru(U nc(L(||K(A i )|C i ))) ⊆ L(H) (rewritten for short as L 1 ⊆ L 2 ).

Suppose that there exists a prefix

O • {a} ∈ L 1 such that O ∈ L 2 , but O • {a} ∈ L 2 .
Suppose that a is a sending event from p to q, i.e. a = p!q(m) for some m. O brings the CFSM in a configuration C A and H in a configuration C H . The automaton K(A p ) is in a state from which a can be fired, that is all predecessors of a on p have been executed both in C A and C H . Hence, action a is also allowed from C H , as projection preserves sequences of events on each process. Contradiction. A similar case holds for atomic actions. Hence, a can only be a receive action, i.e. a is of the form a = p?q(m) for some q, m. Then, there exists a

prefix O ∈ L(||K(A i )|C i ) such that RU (U nc(O )) = O, and O is of the form O 1 • {a } • .O 2 ,
where O 1 is a prefix, and O 2 a piece of bMSC. Action a is of the form a = C p ?C q (m, τ, b), otherwise a can not be played after O. O 1 is of the form O 1 = P 1 .{b}.P 2 .{b }.P 3 where b = K(A q )!C q (m, p, b) and b = C q !C p (m, τ, b), with the same tag τ as in a .

After O, the automata are in a configuration where the FIFO queue from C p to K(A p ) has a message m as head. In configuration C H corresponding to O there is a message sent but not received from q to p. If a is not allowed in C H , then it is not because the message to be received was not sent, but rather because there exists some former events on process p to be executed (i.e. there is piece of bMSC O a such that a can be played from C H only after O a has been played. Let us get back to the communicating automaton K(A p ). K(A p ) has reached a state s in C A . As there exists a transition by a from K(A p ) and as we know that there exists also several events in O a that can be executed from the configuration C H , then state s is a choice, from which a and the minimal event of O a on instance p are possible. O a and a are hence consequences of different choices, and we have that τ (O a ) = τ (a). From lemma 1 we know that all choices in an execution of the communicating automata are ordered. As all choices are totally ordered, the tags associated to an execution of an HMSC and to an execution of communicating automata are the same. We then have τ (O a ) < τ (a). As O a and a are events of choices that concern p, the communication C q !C p (m, τ (a)) that must occur in O before a can not be played as the message received is tagged by a vector which is not the expected successor tag on C p . We then have a contradiction, and L 1 ⊆ L 2 . II) Let us now prove the reverse direction :

L 2 ⊆ L 1 . Let us suppose there exists O • {a} such that O • {a} ∈ L 2 , O ∈ L 1 but O • {a} ∈ L 1 .
If a is a sending of a message or an atomic action, then all preceding events on the same process have been executed in the CFM, and hence a can be fired, as atomic actions and sendings can be fired as soon as the considered process is in a state that enables it, without considering queues contents. Contradiction.

Then, a is a reception a = p?q(m), and the sending m -1 (a) from q to p has been executed in O, that is both in H and in the CFM. A message m from p to q is translated in a CFM execution as a sequence of actions :

s 1 = K(A q )!C q (m, p, b), r 1 = C q ?K(A q )(m, p, b), s 2 = C q !C p (m, τ, b), r 2 = C p ?C q (m, τ, b), s 3 = C p !K(A p )(m), r 3 = K(A p )?C p (m).
As O ∈ L 1 , we know that r 1 has been executed. Similarly, the automaton K(A p ) is in a sate from which r 3 can be fired, because all predecessors of a on process p have been executed by K(A p ). Then, r 3 can not be executed iff r 1 , s 2 , r 2 or s 3 has not been executed. Similarly, if all communications from K(A q ) to C q took place in RU -1 (U nc -1 (w)), then r 1 is either fired or fireable, and as a consequence s 2 can also be fired. Let us suppose that C p is blocked at r 2 . Then it means that the message to receive is not properly tagged, or that C p still have to perform some interactions from previous choices with K(A p ). This can only be receptions of messages from K(A p ), as otherwise, all events in O would not be executed on K(A p ). Hence, C p can always consume these messages before playing r 2 . Now, let us suppose that the tag of the message sent in s 3 is not the expected tag on C p . Then it means that C p should observe other tagged messages from a former choice ; The actions to be performed by C p can only be receptions, and all the message sendings that should have occurred indeed occurred, for the same reasons as before. Hence, all these events can be executed by C p before executing r 2 and then s 3 . Hence the reception can not be blocked in L 2 .

A prototype implementation

We have integrated our synthesis method to the SOFAT toolbox, a scenario manipulation environment [10]. SOFAT provides some procedures to decide INRIA whether an HMSC is bounded, local choice, etc. When possible, SOFAT also proposes to animate the HMSC and builds the corresponding chronograms.

The code generated by our synthesis algorithm is written in Promela, the input language of the SPIN model-checker [12]. In Promela, we can easily describe the distributed architecture and the behavior of each component using the notion of Promela process and guarded commands. Using SPIN, it is then possible to simulate the target code, and output the result of a simulation as a bMSC. Spin also allows to model-check some properties (up to some bound on the contents of channels). The text below shows the Promela code generated from the HMSC of Figure 1 and an example of scenario (in a bMSC layout) as produced by the SPIN simulator is shown in Figure 6. We have also modelchecked this code to prove that the order of receptions provided by our algorithm is correct on this example.

Conclusion

We have proposed a synthesis framework that produces an implementation for local choice HMSCs. This synthesis works with additional processes that tag messages and delay them to ensure correct ordering of message receptions. To keep the construction of CFSM simple, we have supposed FIFO semantics of communications, and we will hence suppose that the HMSCs that we implement do not contain message overtaking. However, the extension of our implementation to models that allow message overtaking should be easy. One fact worth mentioning again is that the controllers are purely asynchronous, which leaves a lot of freedom to choose a particular architecture. In a real implementation, one may suppose that a process and its controller are implemented on the same machine, but this is not mandatory. Controllers are designed to need as little information as possible to ensure that the processes they control are always executing a valid run of the specification : each process executes its task as defined in the projection of the specification, and controllers ensure coordination. In the future, we would like to study whether asynchronous controllers can in addition guarantee properties such as boundedness of some buffers, avoidance of a given configuration, etc.

INRIA

Figure 2 -

 2 Figure 2 -The bMSC obtained by concatenation of M 1 and M 2 in Fig. 1.

  A path ρ ∈ P aths(H) defines a sequence of M * and thus the corresponding bMSC formed by concatenation and denoted by O ρ . Let us denote by L(H) = ρ∈P aths(H) P ref (O ρ ), the set of behaviors of the HMSC H.

Figure 3 -

 3 Figure 3 -The instance automata projected from the HMSC of Fig. 1.

Figure 4 -

 4 Figure 4 -A correct behavior of the HMSC of Fig. 1, and a possible distortion due to the distributed interaction of the projected instances.

Figure 5 -

 5 Figure 5 -The distributed controlled architecture.

Figure 6 -

 6 Figure 6 -A bMSC produced by SPIN during simulation of the Promela generated code, implementing our synthesis method.

RR n°7597

http://www.inria.fr ISSN 0249-6399

Algorithm 2 Controller C i RULE 1 : when (j, m, b) available on port P i consume (j, m, b)

send (m, τ i ) on port P j else nbevt -send (m, τ i ) on port P j end if RULE 2 : when (m, τ ) available on port

.nbevt] send (j, m) on port P i end if end if

Proof of correctness

Definition 11 Let O = (E, ≤, t, φ, m) be a prefix in L(||K(A i )|Ci). The restriction of O to non-control events is a restriction of O to events located on K(A i )'s. We will denote by U nc(O) this restriction. The uncontroling of O = (E, ≤, t, φ, m) is a renaming function Ru() that replaces communications to and from the controller of a process by direct communications with the process concerned by the sent/received message, and builds the message mapping. Ru(O) = (E, ≤, t , φ, m ), where t (e) = p!q(m) if t(e) = p!C p (m, q, c), t (e) = p?q(m) if t(e) = p?C p (m, q), and t (e) = t(e) otherwise. Function m maps the i th sending from p to q with the i th reception on q from p for every pair of processes.

Note that for a prefix O in L(||K(A i )|Ci), the message mapping in U nc(O) is an empty relation.

Theorem 3 Let H be an HMSC, and let ||K(A i )|C i be its controlled synthesis. Then, Ru(U nc(L(||K(A i )|C i ))) = L(H).

Proof : We will prove this theorem by showing inclusion in the two directions. We will also need a technical lemma that shows that the tagging mechanism is the same in an HMSC and in its implementation.