Rocco De Nicola
email: rocco.denicola@imtlucca.it

Tan Duong
email: tan.duong@gssi.it

Michele Loreti
email: michele.loreti@unicam.it

ABEL -A Domain Specific Framework for Programming with Attribute-Based Communication

Keywords: attribute-based communication, process calculi, distributed programming, Erlang

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

Introduction

Attribute-based communication, originally proposed in [START_REF] De Nicola | A formal approach to autonomic systems programming: The SCEL language[END_REF] is a novel paradigm that allows the dynamic selection of communication groups while taking into account run-time properties and status of interacting entities. At its core, the paradigm relies on a pair of communication primitives. The command send(v)@π is used to send a tuple of values v to all components satisfying the predicate π.

The command receive(x)@π is used to receive a tuple of values on x with contents satisfying the predicate π . The interaction predicates are also parametrised with local attributes and when their values change, the interaction groups do implicitly change, allowing opportunistic interactions.

This paradigm was formalized in the AbC kernel calculus [START_REF] Alrahman | On the power of attribute-based communication[END_REF][START_REF] Alrahman | A behavioural theory for interactions in collective-adaptive systems[END_REF] to study the impact of attribute-based communication in the realm of CAS [START_REF] Anderson | Adaptive collective systems: herding black sheep[END_REF]. In AbC , components are equipped with a set of attributes describing their features, which can change at runtime. Component interactions is driven by conditions over their states to enable anonymity, adaptivity and open-endedness. The expressive power of AbC in terms of representing different communication paradigms, such as point-to-point, group based, channel-based, and broadcast-based models has been demonstrated in [START_REF] Alrahman | A behavioural theory for interactions in collective-adaptive systems[END_REF]. AbC communication model follows broadcast in the style of [START_REF] Prasad | A calculus of broadcasting systems[END_REF]; output action can take place even without the presence of any receivers while input action instead waits to synchronize with available messages.

The original semantics of AbC has been formulated in a way that when a component sends a message, that message is delivered to all components in the system in a single move and each individual receiver decides whether to use the message or to discard it. This semantics implies a restriction on the ordering of message delivery because only one component can send its message at a time. That is, message delivery in AbC is performed according to a total order [START_REF] Baldoni | Total order communications: A practical analysis[END_REF]. Some proposals have already been put forward to efficiently implement message exchange for AbC . It has been implemented in Java [START_REF] Alrahman | Programming of cas systems by relying on attribute-based communication[END_REF], Google Go [START_REF] Alrahman | Goat: Attribute-based interaction in google go[END_REF] and Erlang [START_REF] De Nicola | AErlang: empowering Erlang with attribute-based communication[END_REF]. However, these implementations are either not in full agreement with the original semantics or do miss detailed performance evaluations. This may give rise to doubts about efficiency and correctness and thus prevent the adoption of attribute-based communication.

Indeed, there are a number of challenges to face when providing an implementation fully respecting the exact semantics of AbC . The first is posed by the fact that its message passing model requires guaranteeing a total order on message delivery. While various protocols for total order broadcast have been proposed in the literature, see, e.g., [START_REF] Birman | Lightweight causal and atomic group multicast[END_REF][START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], the anonymity and open-endedness features of AbC makes then unsuitable in this context because components cannot contribute to establishing an order. A closely related work in building total order for AbC has recently been presented in [START_REF] Alrahman | A distributed coordination infrastructure for attribute-based interaction[END_REF] where a sequencer-based protocol is formalized and proved correct on different topologies of networks. However, there is still the possibility for the proposed protocol to give rise to unexpected behaviours due to the complex behaviour of AbC components. Moreover, since AbC components contain parallel processes operating independently on a shared, dynamic changing attribute environment, to simulate the right interleaving semantics among processes, any implementation should carefully coordinate processes, otherwise situations may arise where processes interfere without exhibiting the wanted behaviour.

In this paper, we continue the search for efficient implementations of AbC and present ABEL -a programming framework for systems whose elements interact according to the AbC style. Our framework provides an execution environment for AbC specifications, that supports AbC programming abstractions for writing and running programs, and, at the same time, fully preserves the original semantics of AbC . More concretely:

1. We provide a set of attribute-based programming constructs, implemented as an Erlang library that allows easily defining component programs. 2. We implement coordination mechanisms for intra-and inter-components interactions in Erlang, each dealing with one of the parallel operators of AbC and together guaranteeing the original semantics. 3. We demonstrate with experiments that better performances can be achieved if the "strong" AbC requirement on the total order of message delivery is relaxed.

We show that by starting from a given AbC specification, it is straightforward to derive a corresponding Erlang program containing API calls. We also show that the close correspondence between AbC and ABEL enables us to reason about the execution code by using verification tools developed for AbC [START_REF] De Nicola | Verifying properties of systems relying on attribute-based communication[END_REF]. Moreover, by experimenting with a number of case studies, we show that it is possible to preserve AbC semantics while guaranteeing good performance and that by, slightly relaxing the ordering requirements, better ones can be obtained.

The rest of the paper is organized as follows. In Section 2 we briefly review the AbC calculus, and provide examples illustrating its programming paradigm. In Section 3, we present the API support for AbC . In Section 4, we describe the coordination mechanisms used to handle intra-and inter-components interactions. Section 5 reports our experiments on case studies, taking into account different message ordering strategies. Section 6 concludes the paper by discussing the difference between our work and previous proposals, together with some conclusions and hints to future works.

Programming with AbC

The AbC calculus provides concrete primitives that permit the construction of formally verifiable models of CASs according to the attribute-based communication paradigm. A system is rendered as a collection of interacting components. A component C is either a process P associated with an attribute environment Γ and an interface I, or the parallel composition of two components.

(Components)

C ::= Γ :

I P | C1 C2
The environment Γ is a partial mapping from attribute names to values, representing the component state. The interface I ⊆ Dom(Γ ) contains a set of names, exposed for interaction purpose. The process P can be either an inactive process 0, a prefixing process α.P , an update process U , an awareness process Π P , a choice process P 1 + P 2 , a parallel process P 1 |P 2 , or a process call K (with a unique definition K P ).

(Processes)

P ::= 0 | ( Ẽ)@Π.U | Π(x).U | Π P | P1 + P2 | P1|P2 | K (Update) U ::= [a := E]U | P (Expressions) E ::= v | x | a | this.a | f ( Ẽ) (Predicates) Π ::= tt | p( Ẽ) | Π1 ∧ Π2 | ¬Π
AbC prefixing actions exploit run-time attributes and predicates over them to determine the internal behaviour of components and the communication partners.

( Ẽ)@Π is an output action that evaluates expressions Ẽ under the local environment and sends the result to those components whose attributes satisfy predicate Π; Π(x) is an input action that binds to the variables x the message received from any component whose attributes and the communicated values satisfy the receiving predicate Π; [a := E] is an update operation that assigns to attribute a the evaluation of expression E under the local environment; Π blocks the following process until Π is satisfied under the local environment.

Attribute updates and awareness predicates are local to components and their executions are atomic with the associated communication action.

An expression E may be a constant value v, a variable x, an attribute name a, or a reference this.a to attribute a in the local environment. Predicate Π can be either tt, or can be built using comparison operators between two expressions and logical connectives ∧, ¬, . . .. Both expressions and predicates can take more complex forms, of which we deliberately omit the precise syntax; we just refer to them as n-ary operators on subexpressions, i.e., f ( Ẽ) and p( Ẽ).

The original semantics of AbC has been formulated in a way that when a component sends a message, this is delivered in a single move to all components in the system. Atomically, each individual receiver decides whether to keep the message or to discard it. This semantics imposes a restriction on the ordering of message delivery because only one component at a time can send a message. That is, message delivery in the original AbC is performed according to a total order [START_REF] Baldoni | Total order communications: A practical analysis[END_REF].

Even if this approach is useful to describe in an abstract way the AbC one-tomany interactions, it may be considered too strong when large scaled distributed systems are considered. To relax the total ordering formulation of the original AbC semantics, we have extended AbC syntax to explicitly model the infrastructure responsible of message dispatching already used in [START_REF] Alrahman | A distributed coordination infrastructure for attribute-based interaction[END_REF].

To this goal we introduce the new category of servers. AbC systems are now built by using servers of the form {•} ι,ω that are responsible for managing a set of components. Each server is equipped with an input queue ι and an output queue ω. The former is the queue of messages, coming from the environment, that the server must deliver to the managed components. The latter is the queue of messages that have been generated locally and that the server must forward to other components. Each message m is a triple of the form (Γ, π, ṽ) where Γ is the environment of the sending component, π is the target predicate used to select the receivers, and ṽ is the tuple of sent values. In what follows we will use q to denote a queue of messages, and [] to denote the empty queue. Moreover, we will use m :: q (resp. q :: m) to represent an extended queue obtained by adding message m at the beginning (resp. at the end) of q.

The syntax of AbC servers is the following:

(Servers) S ::= {M } ι,ω (Managed Elements) M ::= C | S S
A server thus equips its managed element (which in turn can be either single AbC component or recursively other servers) with input and output queues. Servers communicate with one another by adding and withdrawing messages from their queues, thereby relaxing the original synchronous semantics.

The operational semantics of AbC systems is defined via the transition relation -→⊆ Sys × Lab × Sys, where Lab is the set of transition labels λ defined by the following syntax:

λ ::= Γ Π(ṽ) | Γ Π(ṽ) | τ
The transition label Γ Π(ṽ) represents an output of ṽ executed by a component with environment Γ that is sent to receivers satisfying Π. Input actions are represented by label Γ Π(ṽ) that represents the capability of a system to receive message ṽ sent by a component with environment Γ to receivers satisfying Π. Finally, τ represents internal/silent actions.

We have fully formalized the new semantics that relies on the two queues of the servers. Due to lack of space, in Table 1 we only report some the rules of the operational semantics that we consider more relevant.

S1 Γ Π(ṽ) -----→ S 1 S2 Γ Π(ṽ) -----→ S 2 S1 S2 Γ Π(ṽ) -----→ S 1 S 2 Sync S1 Γ Π(ṽ) -----→ S 1 S2 Γ Π(ṽ) -----→ S 2 S1 S2 Γ Π(ṽ) -----→ S 1 S 2 ComL S1 Γ Π(ṽ) -----→ S 1 S2 Γ Π(ṽ) -----→ S 2 S1 S2 Γ Π(ṽ) -----→ S 1 S 2 ComR m = (Γ, ṽ, Π) M1 Γ Π(ṽ) -----→ M2 {M1} m::ι,ω τ -→ {M2} ι,ω SerDIn M1 Γ Π(ṽ)M 2 -------→ {M1} ι,ω τ -→ {M2} ι,ω::(Γ,ṽ,Π) SerDOut {M1} ι,ω Γ Π(ṽ) -----→ {M2} ι::(Γ,ṽ,Π),ω SerIn {M1} ι,(Γ,ṽ,Π)::ω Γ Π(ṽ) -----→ {M2} ι,ω
SerOut Table 1. Operational Semantics: Relevant Rules

The rules for parallel composition ( ) are the expected ones: Sync states that S 1 and S 2 , when in parallel, can both receive the same message; ComL and ComR state that messages sent by S 1 (resp. S 2 ) are received by S 2 (resp. S 1 ) and the result of the synchronisation is an output label to allow other components in parallel to receive the same message.

The rules describing behaviour of a server are SerDIn, SerDOut, SerIn and SerOut. The first two rules model the interaction of the server with the enclosed element, while the last two describe the interaction of the server with the enclosing environment. Rule SerDIn states that the first message is consumed from the input queue when the managed element M 1 receives it. Rule SerDOut states that a message is added at the end of the output queue whenever the managed element M 1 executes an output action. A message is added at the end of the input queue whenever a new message is received from the enclosing environment (rule SerIn). Conversely, a server sends a message by removing it from the front of output queue (rule SerOut).

AbC at work

In order to illustrate AbC primitives and assess our implementation we now provide a couple of simple case studies that we will later use also for assessing performances of our implementations.

Stable matching. We consider a variant of the well-known stable matching problem (SMP) [START_REF] Gale | College admissions and the stability of marriage[END_REF] that can be naturally expressed in terms of partners' attributes [START_REF] De Nicola | Verifying properties of systems relying on attribute-based communication[END_REF]. Solving an SMP problem amounts to finding a stable matching between two equally-sized sets of elements, after each element has specified an ordering of preferences over all members of the opposite set. The original algorithm [START_REF] Gale | College admissions and the stability of marriage[END_REF] goes through a sequence of proposals initiated by members of one group, say M, according to their preference lists. Members of the other group, say W, after receiving a proposal, do choose the best candidate between their current partner and the one making advances. The algorithm guarantees the existence of a unique set of pairs, which is stable, i.e. there is no pair of unmatched elements, that prefer each other to their current partners. An AbC specification for this algorithm can be found in [START_REF] Alrahman | Programming of cas systems by relying on attribute-based communication[END_REF].

Our variant allows participating agents to express their interests in potential partners by relying on partner's attributes rather than on their identities. In this scenario, M components start by proposing to those W components that satisfy their highest requirements, i.e., a predicate that specifies all wanted attributes. If an M agent cannot find any partner for a given demand, it retries after weakening the predicate by dropping one of the wanted attributes. W components are reactive to proposals and perform "select and swap" partners as before. However, since a proposal may target multiple partners, the protocol needs extra acknowledgement messages between agents of two types to select the partner. And, an agent of type M relaxes a predicate Π only if all potential partners, addressed by Π, rejected it.

In AbC the two types of components M and W are modelled as follows:

M i Γ mi : {id,a1,a2,...} P M and W j Γ wj : {id,b1,b2,...} P W where the interfaces expose the names of attributes that represent the features of the components and P M and P W their actual behaviour.

Below, we specify part of the system concerned components of type M , whose behaviour combines 4 processes

P M Q | P | A | R
An agent m that is looking for partners satisfying predicate Π 4 has first to learn about the number of potential partners, say c, satisfying this predicate. This is taken care by process Q that first broadcasts a query message and then collects interested replies (not detailed here). For each attempt, m keeps track of the set bl of partners which have rejected it. As long as there are available partners (c > |bl|), process P sends a 'propose' message containing the agent's characteristics (denoted by the sequence msg) to predicate Π, excluding those in bl.

P partner = 0 ∧ c > |bl| ∧ send = 1
('propose', this.id, msg)@(Π ∧ id / ∈ this.bl).[send := 0]P + . . .

Other branches of P have a similar structure and will be used for proposing with other requirements. Process A, reported below, handles multiple 'yes' messages which may arrive in parallel. The continuation H chooses the sender (bound to y) of the first message to match, confirms to y that it has been selected and updates new partner. A 'toolate' message is sent to senders of subsequent 'yes' messages:

A (x = 'yes')(x, y).(H | A)
H ( partner = 0 ('conf irm')@(id = y).[partner := y]0 + partner > 0 ('toolate')@(id = y).0

The sent proposal may also be rejected. Process R collects messages of this type. The arrivals of 'no' and 'split' requests cause the addition of the senders to the set bl and enabling send. A 'split' message which originates from some matched partner resets the current partner and opens the possibility for process P to become active and retry.

R (x = 'split')(x, y).[bl := bl ∪ {y}, send := 1, partner := 0]R + (x = 'no')(x, y).[bl := bl ∪ {y}, send := 1]R 4
As an example, consider a user interested in finding a server that has some specific resources. A possible communication predicate would be Π = (cores = this.pcores∧ mem = this.pmem) where cores and mem are two attributes of servers, and pcores and pmem are two attributes of users.

Graph colouring. We now consider a distributed graph colouring problem where vertices exchange messages with their neighbours to collaborate on deciding a colour (in our case a positive number) for each of them in such a way that adjacent vertices do not get the same colour. The following AbC specification is adapted from [START_REF] Alrahman | Programming the interactions of collective adaptive systems by relying on attribute-based communication[END_REF]. A graph is modelled naturally as a set of components V i Γ i : {id,nbr} P V , one for each vertex, with attribute id representing a unique identifier, and nbr representing a set of neighbours ids. Vertices operate in rounds and in each round they use a predicate (this.id ∈ nbr) to send messages to neighbours. Vertices concurrently execute the four processes F, T, D, A until they get assigned a 'definitive' colour.

Every non assigned vertex selects the first available colour which has not been used by his neighbours, that is min{i / ∈ this.used}. A try message of the form ('try', c, r) is sent to inform others that the sending vertex wants to attain colour c at round r.

F

('try', min{i / ∈ this.used}, this.r)@(this.id ∈ nbr).

[colour := min{i / ∈ used}, counter := counter + 1]0

Each vertex counts the number of 'try' messages (including its own) using the attribute counter. Process T collects 'try' messages from neighbours where it records colours proposed from neighbours with greater ids in a set constraints to avoid conflict. Other branches of T (not shown here) deal with 'try' messages from neighbours operating in one round ahead, i.e., (this.r < z) for which the relevant information are kept in attributes counter1, constraints1.

T (x = 'try' ∧ this.id < id ∧ this.r = z)(x, y, z).

[counter := counter + 1, constraints := constraints ∪ {y}]T + (x = 'try' ∧ this.id > id ∧ this.r = z)(x, y, z).

[counter := counter + 1]T + . . .

After collecting all 'try' messages, i.e., (counter = |nbr| + 1), each vertex checks whether the colour it proposed among neighbours is valid, encoded in process A below. If this is the case 5 , the vertex sends a 'done' message of the form ('done', c, r) to indicate that c has been taken at round r, setting assigned to true and terminates. If the proposed colour leads to conflict, the vertex starts a new round by sending a new 'try' message. At this point, the vertex has learnt about neighbours and thus tries to take the best decision by selecting a new colour excluding also constraints, i.e., min{i / ∈ this.used ∪ this.constraints}. During this new round, r + 1, the vertex does not count messages from those vertices who might have sent a 'try' message (collected by process T above via counter1) and from 'done' neighbours (collected by process D presented next).

A (counter = |nbr| + 1) ∧ colour / ∈ constraints ∪ used
('done', this.colour, this.r)@(this.id ∈ nbr).[assigned := tt]0

+ (counter = |nbr| + 1) ∧ colour ∈ constraints ∪ used
('try', min{i / ∈ this.used ∪ this.constraints}, this.r + 1)@(this.id ∈ nbr).

[r := r + 1, counter := done + counter1 + 1, constraints := constraints1, . . .]A

Each vertex collects 'done' messages to update the set of used colours, and counts 'done' neighbours in done. In addition, if the messages come from the previous round, i.e., (this.r > z), the vertex treats them as 'try' messages in the current round, and thus increments the counter.

D (x = 'done' ∧ this.r = z)(x, y, z).

[done := done + 1, used := used ∪ {y}]D + (x = 'done' ∧ this.r > z)(x, y, z).

[done := done + 1, used := used ∪ {y}, counter := counter + 1]D

3 Programming support for AbC

Our framework aims at providing a direct mapping from AbC specifications to executable programs in Erlang, allowing experimentations with attribute-based communication with little of efforts. An ABEL program is based on a sequence of behaviour definitions for processes, and top-level commands for starting all components. The running program is a set of concurrently executing components. In the above commands, environment Env is represented as a map whose keys are atoms denoting attribute names. Interface I is a tuple of atoms denoting public attributes, to which other components may want to use their values. In particular, when sending a message, any component attaches also the portion of the environment Env' corresponding to Env but limited by the interface.

Creating components

Behaviour Definition

The syntax for behaviour definition is given in Fig. 1. Elements wrapped by are optional. A definition BDef is a function that has as first parameter a component address C. The body of a definition is a sequence of commands, which also require C as their first parameters.

Action Act gives the descriptions for AbC input and output actions. There we use m to denote message, u to denote update and g, s, r to denote awareness, sending and receiving predicates respectively. We now briefly explain the different commands.

Prefix -takes as a parameter a pair containing a prefixing action Act and a continuation BRef . The command executes Act and continues with BRef . If Act is an output description, the command evaluates m into ṽ, the sending predicate s into s and broadcast the triple (Env , s , ṽ) to all components and possibly performs an attribute update u, whenever guard g (if specified) is satisfied. If Act is an input description; the command returns a message and optionally performs an attribute update u, whenever guard g (if specified) is satisfied and the sender's attributes and the communicated message satisfy the receiving predicate r. Choice -takes as parameter a list of pairs, each providing a description of the prefixing action Act and a continuation in form of BRef . This command executes one of the actions and continues with the behaviour associated to that action. Parallel -This command dynamically creates parallel processes, each of which executes a behaviour indicated by a reference in the parameter list. Process Call -executes the behaviour Beh.

The basic elements m, g, r, s, u are represented as follows.

Message. A message m to be sent is represented as a tuple. A message element can be a function parameterized with the sender environment, i.e., f un(S) → . . . end, for making it possible to refer to attribute values in S.

Predicates. An awareness predicate g is a unary function parameterized with the environment of the executing component, i.e., f un(E) → . . . end. A sending predicate s is a binary function parameterized with the sender and receiver environments in that order, i.e., f un(S, R) → . . . end. A receiving predicate r is a ternary function parameterized with the environments of the receiver and the sender, and a communicated message in that order, i.e., f un(R, S, M ) → . . . end.

Attribute Update. An update is represented as a list of pairs; in each pair, the first element is an attribute name and the second is an expression to be used for the update. The expression can be a function parameterized with the local environment (to use also attribute values), and with the communicated message, when in case the update is associated with a receive action.

As an example of using the presented API for deriving execution code from AbC specifications, Fig. 2 presents the definitions in ABEL for processes F and D in the graph coloring scenario (Example 2). Bold-faces are used to highlight the structural correspondence between the ABEL code and the AbC one. The rest of the code is used to specify predicates, messages and updates, which can be addressed by automatic translation. Indeed, we have developed the translator from AbC to ABEL and made it available with the ABEL implementation.

Coordinating components

In this section, we consider two alternative implementations for coordinating AbC components. The first implementation is obtained by using an infrastructure similar to the one proposed in [START_REF] Alrahman | A distributed coordination infrastructure for attribute-based interaction[END_REF]; minor modifications have been introduced to make the total ordering protocol more robust. The second one is obtained from the former by relaxing some requirements on ordering preservation. For both implementations we have a corresponding formal semantics. The first one exactly captures the original total ordering AbC semantics first presented in [START_REF] Alrahman | On the power of attribute-based communication[END_REF] while the second one is that briefly explained in Sect. 2.

An AbC system in ABEL consists of a set of components and an infrastructure with a set of nodes that collaborate on mediating message exchanges. Components join the system via a globally named registration node which assigns them to a node of the infrastructure. Fig. 4 shows an example of a tree-structure where each node (black) is responsible for a group of components (white). The model assumes that a node only communicates with those connected to it; likewise a component only communicates with the node they are assigned to. In what follows, we describe the implementations with respect to the behaviour of components and infrastructure nodes. Coordinating processes An AbC component is an autonomous entity with multiple processes operating on a shared environment. The behaviour of a component is that of its processes. We have that (i) If more than one process offers an output action, then only one of them will be allowed (ii) If more than one process can actually input a message, again only one of them will succeed. (iii) A component discards a message only if all of its processes discard that message. (iv) Processes and environment influence each other, e.g., a change in the environment caused by one process may enable or disable other processes.

This semantics suggests us considering the attribute environment as a reactive process, rather than a static store. Fig. 3 pictures the internal structure of an AbC component. Processes P represent AbC processes that communicate with a coordinator C by message passing via the API presented in Sect. [START_REF] Alrahman | On the power of attribute-based communication[END_REF]. Each process submits one action at a time, and continues only after receiving an acknowledgment message. The coordinator keeps track of component environment and decides the actual actions to be executed. The execution of an action may require updating the environment if the action has an associated update request. Actions that cannot be executed because of guards are stored and retried when the environment is updated.

To model interleaving, a coordinator dynamically keeps track of the number of processes, of the set of submitted actions, and uses an input queue for storing messages forwarded from infrastructure. Events that are handled by a coordinator includes commands from processes, messages forwarded from the infrastructure and other implicit information. We briefly explain the operations performed for each event as below.

Parallel events The coordinator creates new processes, and updates the total number of processes. Sending events When the guard (if specified) is satisfied, the message is forwarded to the infrastructure and the sending process is acknowledged, otherwise, the sending action is added to the set of submitted ones. Receiving events The action is added to the set of submitted actions.

Choice events The coordinator handles them like normal sending and receiving events, the acknowledgement message to the choice process is a continuation behaviour. Delivery events These events are internally generated when the input queue is not empty and the number of submitted actions is equal to the number of processes. Predicates of input actions are checked against messages extracted from the queue, one by one until there is a match or the queue is empty. In case of matching, the message is delivered to the receiving process. Retry events These events are internally triggered when the environment changes.

Output actions and choices among output actions in the submitted set are retried.

Coordination Strategies As mentioned above we have implemented two different strategies for message exchange that may lead to different ordering of message delivery, we call them synchronous and asynchronous.

Synchronous. Encapsulated in the infrastructure presented in [START_REF] Alrahman | A distributed coordination infrastructure for attribute-based interaction[END_REF] there is a sequencer-based protocol that guarantees a total order of message delivery for AbC components. The infrastructure, apart from broadcasting messages for components, plays the role of a sequencer that allocates unique ids for components messages. When a component is willing to send a message, it requests a fresh id for the message. A component can deliver a message labeled with an id only if it has delivered all messages with id < id. This means that messages are delivered in the order of consecutive messages' ids, which is total.

This protocol is used to coordinate ABEL components by relying on a treebased infrastructure as follows. Every component coordinator keeps a counter c, initially set to 1.

To handle sending events, the coordinator, after checking the guard, requests a fresh id if his previous one has already been used. The output action can take place only if the fresh id matches the counter, otherwise it is postponed. If the action is executed, c is incremented by 1.

To handle delivery events, the coordinator sends a message extracted from the input queue if its id is equals to c, and increases the counter. If the message is not consumed by any input action, the procedure repeats until the queue is empty or there is no message with the expected id.

To handle retry events, the coordinator may send an empty message if there is an unused fresh id which is equal to the local counter and if all components processes can not send a message.

When a non-root tree node receives an id request, it forwards the request to its parent. The root replies its counter value for each request and increments the counter. This fresh id is forwarded along the same path of the original request, but in a reverse order. Eventually, the node which initiated the request receives the fresh id and sends it to the requesting component. When a tree node receives a data message, it forwards the messages to the other connected nodes and to connected AbC components, except the sender. In addition, to guarantee that the number of messages exchanged is bound, each node has an input queue for storing incoming data messages and only forwards a message if its id equals to the node's counter.

Asynchronous. In this implementation, components can send the actual messages simultaneously via the infrastructure without asking and checking for fresh ids. We rely on the tree structure as for the synchronous case but we do not take advantage of it and could have used another structure. A component delivers messages from its input queue in any order to its processes, while trying to filter out as many 'uninteresting' messages as possible. In this case, tree nodes forward messages as soon as they receive them and the root has no special role; which makes the implementation simpler.

Experiments

In this section, we report on the performance evaluation of our Erlang prototype 6 of ABEL by considering the two case studies, stable marriage and graph colouring, whose AbC specifications have been sketched in Sect. 2. These AbC specifications were model checked by following the approach presented in [START_REF] De Nicola | Verifying properties of systems relying on attribute-based communication[END_REF].In particular, we have verified the termination and soundness properties for the graph colouring problem, and the completeness, symmetry of matchings and orchestration properties for stable matching problem. The explicit-state model checker [START_REF] Beek | A state/event-based modelchecking approach for the analysis of abstract system properties[END_REF] helped us to verify early designs of these case studies and to come up with correct specifications. From the verified specifications we have then derived the ABEL programs introduced in Sect. 3.

For our experiments, we used a workstation with a dual Intel Xeon processor E5-2687W (16 cores in total) and 128 GB of memory. The OS version is Linux 4.9.95-gentoo and the Erlang/OTP version is 21.2. In addition, the coordination infrastructure is the tree-based one with a varying number of nodes and the the previously outlined communication strategies. The tree-based infrastructure was chosen as the default topology after considering the result in [START_REF] Alrahman | A distributed coordination infrastructure for attribute-based interaction[END_REF] showing that it guarantees better performance over others.

Stable Marriage with Attribute

The input to this case study is randomly generated assuming some predefined probabilities of attributes and preferences. First, we define their ranges, then we associate a probability to each value in the range so that the sum of the probabilities is 1. In this way, an attribute (or preference) can take a concrete value v with a probability p(v). In the experiment, we consider 2 attributes and 2 preferences with ranges of 2 values. We select 10 different combinations of probabilities, consider problem sizes of 100 and 200 pairs of elements, and generate 100 instances for each problem size.

We ran the ABEL program to solve problem instances and took the average of the execution times. We have also checked the completeness and stability conditions on the outcomes of the program. Table 2 presents the numbers under two different ordering strategies. These numbers are the average over 500 runs with a tree of 7 nodes. The result shows that the interaction protocol for this case study performs faster when using asynchronous messaging.

Graph Colouring

We conducted some experiments with several DIMACS graphs collected from various public sources: flat300 28 0.col (300 vertices and 21695 edges), dsjc500.1.col (500 vertices and 12458 edges), will199GPIA.col (701 vertices and 7065 edges) and dsjc1000.1.col (1000 vertices and 49629 edges). The datasets chosen provides an increasing number of vertices which are considered as AbC components.

The following metrics are considered: the running time in seconds, the total number of messages exchanged between components and the infrastructure and the total size of messages in MB. When measuring, vertices do not wait for each other to report the completion of their colouring: as soon as a vertex decides on a colour, it reports that colour, the number of messages exchanged (and message size) to an external process. Tables 3 and4 show the results of graph colouring with total ordering and relaxed ordering, respectively. S is the number of nodes used by the tree structure. The other columns show the numbers for colour, round, messages and the total size in that order. The execution times are computed as the average of 50 runs, the other numbers report the average over the results of different number of nodes. Overall, the ABEL code can perform colouring for experiment graphs without any conflicts, and resulted in small speedups when increasing the number of nodes. This is however more obvious with the larger graph. On the other hand, its performance varies on different graphs. This might have to do with their specific topologies. In general, in graphs with more edges, components are more likely to face colour conflicts among neighbours and thus to require more interactions. This leads to an increased number of rounds and message exchanges.

It can be seen from the results that both ordering strategies return similar outcomes for the same input graphs. Although, in most cases, relaxed ordering guarantees slightly better performance.

Concluding Remarks and Related Works

We have presented ABEL, an implementation of AbC in Erlang that builds on an API that mimics AbC constructs. Our purpose is to develop and experiment with systems featuring complex interactions according to the AbC paradigm. The API is integrated seamlessly with underneath coordination mechanisms that together simulate the original synchronous semantics of AbC and a less demanding one. Because of the direct correspondence between the two formal semantics and our actual implementations, we can perform formal verification of ABEL programs by considering their AbC abstractions. Indeed, from AbC specifications we can obtain verifiable models that can be provided as input to model checkers.

There have been other attempts at providing implementations of AbC . AErlang [START_REF] De Nicola | AErlang: empowering Erlang with attribute-based communication[END_REF] extends Erlang processes to allow attribute-based communication beside the point-to-point one. However, the programming style is based on the host language and it might not be immediate to derive AErlang programs from AbC specifications. Furthermore, the lack of a corresponding formal semantics of AErlang calls for alternative directions, not based on translations, when it comes to reasoning on programs. Other AbC implementations such as [START_REF] Alrahman | Goat: Attribute-based interaction in google go[END_REF][START_REF] Alrahman | Programming of cas systems by relying on attribute-based communication[END_REF] exhibit a gap between AbC primitives and their programming constructs. More efforts are needed to derive AbC code and and automatic translations are not immediate. We refer the readers to [START_REF] De Nicola | AErlang: empowering Erlang with attribute-based communication[END_REF] for a more detailed account of related works on concurrent languages and communication models.

In near future, we want to establish a formal relationship between ABEL and AbC and prove the correctness of the API implementation, as well as the correctness of the developed translation. This would require studying the operational semantics of the inter-and intra-components coordinators, and formalizing the translation rules. We also plan to integrate the model checking part within our framework. Moreover, it might be useful to equip ABEL with other communication and synchronization abstractions; we have experienced that programming complex distributed systems using only AbC send and receive may be difficult.

  A component is set up in two steps: it is first created and then assigned an initial behaviour. To create a new component, an attribute environment Env and an interface I are provided to new component(Env,I ), which returns a unique address C. The command start beh(C, [BRef ]) starts the execution of a component C with an initial behaviour specified as a list of behaviour references, whose actual definitions have been previously declared. The term [elem] is used to indicate a list of type elem. C = new component(Env, I), start beh(C, [BRef ])

BDefFig. 1 .

 1 Fig. 1. ABEL API for process definitions.

  f(C) → M = {'try', fun(S) → min colour(att(used,S)) end, fun(S) → att(round,S) end}, P = fun(S,R) → sets:is element(att(id,S),att(nbr, R)) end, U = [{counter, fun(S) → att(counter,S) + 1 end}, {colour, fun(S) → min colour(att(used,S)) end}], Act = {M,P,U}, prefix(C,{Act,nil}). d(C) → P1 = fun(R,S,M) → size(M) == 3 andalso element(1,M) == 'done' andalso att(round,S) == element(3,M) end, U1 = [{done, fun(R,M) → att(done,R) + 1 end}, {used, fun(R,M) → sets:add element(element(2,M),att(used,R)) end}], Act1 = {P1, U1}, P2 = fun(R,S,M) → size(M) == 3 andalso element(1,M) == 'done' andalso att(round,S) > element(3,M) end, U2 = [{done, fun(R,M) → att(done,R) + 1 end}, {used, fun(R,M) → sets:add element(element(2,M),att(used,R)) end}, {counter,fun(R,M) → att(counter,R) + 1 end}], Act2 = {P2, U2}, DRef = fun() → d(C) end, choice(C,[{Act1,DRef},{Act2,DRef}]).

Fig. 2 .

 2 Fig. 2. Example code derived from the AbC processes F and D in Graph Colouring

Fig. 3 .

 3 Fig. 3. An AbC component in ABEL Fig. 4. A tree-based infrastructure

Table 2 .

 2 Results of stable matching

	Odering	Execution Times (in sec.) Size = 100 Size = 200
	Total Order	5.65	54.63
	No Order	3.39	35.56

Table 3 .

 3 Results of graph colouring using total order

	Graph	Execution Times (in sec.) #C #R S = 3 S = 7 S = 15 S = 31	#Msg (in milli.)	Size (in MB)
	flat300 28 0 4.57 4.22 4.19	4.4	46 44	1.5	7,141
	dsjc500.1	4.22 3.65 3.34	3.39	20 19	2.15	4,008
	will199GPIA 7.46 5.95 5.56	5.53	11 25	4.62	4,255
	dsjc1000.1.col 32.02 27.19 25.94 24.97 32 30	12.5	42,324

Table 4 .

 4 Results of graph colouring using relaxed order

	Graph	Execution Times (in sec.) #C #R S = 3 S = 7 S = 15 S = 31	#Msg (in milli.)	Size (in MB)
	flat300 28 0 3.76 4.69 4.44	4.53	46 45	1.5	7,095
	dsjc500.1	3.17 3.32 2.22	2.94	20 19	2.12	3,905
	will199GPIA 6.53 4.03 3.02	2.81	11 25	4.5	4,070
	dsjc1000.1.col 49.62 33.58 28.69 21.04 32 30	12.4	41,524

https://github.com/ArBITRALABEL


Marco Autili
email: marco.autili@univaq.it

Amleto Di Salle
email: amleto.disalle@univaq.it

Francesco Gallo
email: francesco.gallo@univaq.it

Claudio Pompilio
email: claudio.pompilio@univaq.it

Massimo Tivoli
email: massimo.tivoli@univaq.it

CHOReVOLUTION: Automating the Realization of Highly-Collaborative Distributed Applications

Keywords: service choreographies, distributed computing, automated synthesis

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

Introduction

The Future Internet [START_REF]European Commission: Digital Agenda for Europe -Future Internet Research and Experimentation (FIRE) initiative[END_REF] reflects the changing scale of the Internet and its trend toward the integration and cooperation of different domains supported by an expanding network infrastructure. It relies on large-scale computing environments that will increasingly be connected to a virtually infinite number of services.

This vision is embodied by reuse-based service-oriented systems, in which services play a central role as effective means to achieve interoperability among parties of a business process, and new systems can be built by reusing and composing existing services.

Service choreographies are a form of decentralized composition that model the external interaction of the participant services by specifying peer-to-peer message exchanges from a global perspective. When third-party (possibly blackbox) services are to be composed, obtaining the distributed coordination logic required to enforce the realizability of the specified choreography is a nontrivial and error prone task. Automatic support is then needed. The need for choreographies was recognized in the Business Process Modeling Notation 2.0 (BPMN2) [START_REF][END_REF], which introduced Choreography Diagrams to offer choreography modeling constructs. Choreography diagrams specify the message exchanges among the choreography participants from a global point of view.

The CHOReVOLUTION H2020 EU project1 develops a platform for the generation and execution of scalable distributed applications that leverage the distributed collaboration of services and things by means of service choreographies. In particular, it realizes an Integrated Development and Runtime Environment (IDRE) that comprises a wizard-aided development environment, a system monitoring console, and a back-end for managing the deployment and execution of the system on the cloud.

The CHOReVOLUTION IDRE makes the realization of choreography-based smart applications easier by sparing developers from writing code that goes beyond the realization of the internal business logic. For "internal business logic" we mean the one related to the provisioning of the single system functionalities, as taken in isolation. That is, the distributed coordination logic, which is needed to realize the global collaboration prescribed by the choreography specification, is automatically synthesized by the IDRE. Thus, while coding, developers can avoid to care about coordination aspects. Furthermore, developers can also more easily reuse existing consumers/providers services. These aspects have been appreciated by the industrial partners in that the approach permits to develop distributed applications according to their daily development practices.

The IDRE is an open-source and free software, available under Apache license. It is available as a ready-to-use bundle by the OW2 consortium from https://l.ow2.org/idrevm, and all the documentation can be found at http: //www.chorevolution.eu/bin/view/Documentation/WebHome. The source code is also available at https://gitlab.ow2.org/chorevolution.

The remainder of the paper is organized as follows. Section 2 describes the development approach supported by CHOReVOLUTION. Section 3 describes the components constituting the CHOReVOLUTION IDRE. Section 4 highlights the use of the IDRE through a running example. Section 5 briefly evaluates the two CHOReVOLUTION use cases, and Section 6 concludes the paper.

CHOReVOLUTION approach

The CHOReVOLUTION synthesis process consists of a set of core code generation phases (see Figure 1) that takes as input a choreography specification together with a set of existing concrete services as possible candidates to play the choreography roles and automatically generates a set of additional software entities. When interposed among the services, these software entities "proxify" the participant services to externally coordinate and adapt their business-level interaction, as well as to bridge the gap of their middleware-level communication paradigms and enforce security constraints. Validation -This activity validates the correctness of the choreography specification against the constraints imposed by the BPMN2 standard specification. The goal is to check practical constraints concerning both choreography realizability and its enforceability (see [4, 13-15, 21-23, 26]). Selection -This activity is about querying the Service Inventory in order to select concrete services that can play the roles of the choreography participants. Once the right services have been selected, the related description models will be used to generate the Binding Components (BCs), Security Filters (SFs), Adapters (As), and Coordination Delegates (CDs).

BC Generation -BCs are generated when the middleware-level interaction paradigm of a selected service is different from SOAP [START_REF]W3C: SOAP Version 1.2[END_REF], which is used by the CDs as the middleware-level interaction paradigm [START_REF] Bouloukakis | Enabling Emergent Mobile Systems in the IoT: from Middlewarelayer Communication Interoperability to Associated QoS Analysis[END_REF].

SF Generation -SFs are generated for those (selected) services having security policies associated. SFs filter the services interactions according to the specified security requirements.

Adapter Generation -When needed, adapters allow to bridge the gap among the interfaces and interaction protocols of the selected services and the ones of the (respective) participant roles they have to play, as obtained via projection.

In other words, adapters solve possible interoperability issues due to operation names mismatches and I/O data mapping mismatches (see [START_REF] Autili | Model-driven adaptation of service choreographies[END_REF][START_REF] Autili | On the model-driven synthesis of adaptable choreographies[END_REF][START_REF] Salle | Towards adapting choreography-based service compositions through enterprise integration patterns[END_REF]). CD Generation -CDs are in charge of coordinating the interactions among the selected services so as to fulfill the global collaboration prescribed by the choreography specification, in a fully distributed way (see [5-8, 11, 12]). Choreography Architecture Generation -Considering the selected services and the generated BCs, SFs, As, and CDs, an architectural description is automatically generated, and a graphic representation of the choreographed system is provided, where all the system's architectural elements and their interdependencies are represented. Choreography Deployment Generation -The last activity of the development process concerns the generation of the Choreography Deployment Description (called ChorSpec) out of the Choreography Architecture model. The deployment description will be used for deploying and enacting the realized choreography. As depicted in Figure 2, the CHOReVOLUTION IDRE is layered into: (1) a front-end layer; (2) a back-end layer; and (3) a cloud layer. The red boxes in the figure contain the IDRE components developed within CHOReVOLU-TION from scratch. In particular, they are: the CHOReVOLUTION Studio, the CHOReVOLUTION Console, and the Synthesis Processor together with the artifacts it generates. As detailed below, the components outside the boxes are the ones developed within CHOReVOLUTION and built on top of existing opensource projects. For instance, the Identity Manager extends the Apache Syncope project [START_REF]Apache: Apache Syncope[END_REF]. It is worth noticing that the choice about the existing projects the IDRE relies on comes from the partners of the CHOReVOLUTION consortium. However, the IDRE is an extensible platform and, as such, in the future, it may also support other technologies such as: Kubernetes for deployment and enactment, IBM's AIM for identity management.

(1) The Front-end layer consists of the following:

(1.1) -The CHOReVOLUTION Studio is an Eclipse-based IDE that allows to (i) design a choreography exploiting BPMN2 Choreography Diagrams; (ii) define all the details required to instrument the interaction among the services involved in the choreography (e.g. service signatures, identity attributes and roles); (iii) drive the generation of BCs, SFs, As, and CDs exploiting the automated generation facilities offered by the back-end layer.

(1.2) -The CHOReVOLUTION Console is a web-based application that allows to (i) configure, administer and trigger actions on running services and choreographies; (ii) monitor the execution of a choreography with respect to relevant parameters, such as execution time of choreography tasks, number of messages exchanged for the execution of tasks, end-to-end deadlines, etc.

(2) The Back-end layer consists of the following: (2.1) -The Synthesis Processor implements the activities of the synthesis process described in Section 2. In particular, it takes as input the BPMN2 choreography diagram and the models of the participant services, and generates all the needed additional software entities that are required to concretely realize the choreography, i.e., CDs, As, SFs, and BCs. Finally, it generates a concrete description of the choreography (ChorSpec) that is passed to the Enactment Engine (via the Identity Manager) for deployment and enactment purposes.

(2.2) -The Enactment Engine (EE) is a REST API that extends the Apache Brooklyn project [START_REF]Apache: Apache Brooklyn[END_REF]. It automatically deploys the choreography based on the choreography deployment description by using the Cloud Layer. The EE also interacts with the Identity Manager to include into the deployment description the actual deployment and runtime details. Then, once a choreography is deployed and running, the EE listens for command requests from the Identity Manager for runtime choreography control. It is worth noticing that, although choreography monitoring and control is performed by centralized IDRE components (e.g., EE and IdM), the realization and running of the choreography still remain fully distributed into the various artifacts generated by the Synthesis Processor.

(2.3) -The Federation Server handles the runtime authentication and authorization for services that uses different security mechanism at the protocol level by storing various credentials on behalf of the caller.

(2.4) -The Identity Manager (IdM) is based on Apache Syncope project [START_REF]Apache: Apache Syncope[END_REF] and it is responsible for managing users and services. In particular, the IdM is able to query the services for supported application contexts and played roles; force a specific application context for a certain service (put in "maintenance" or disable/enable). The Service Inventory is a sub-component of the IdM. It acts as a central repository for the description models of the services and things that can be used during the synthesis process.

(3) The Cloud layer executes concrete service choreography instances on a cloud infrastructure and adapts their execution based on the actual application context. At execution time, for each choreography, in the CHOReVOLUTION cloud, there are (i) a set of choreography instances at different execution states; (ii) a set of virtual machines executing a custom-tailored mix of services and middleware components to serve different parts of the choreography. VMs are installed and configured with services according to selectable policies. Due to the fact that EE is based on Apache Brooklyn, the CHOReVOLUTION IDRE is not constrained to a specific Infrastructure as a Service (IaaS) platform (e.g., Open Stack [START_REF]OpenStack: Open Stack[END_REF], Amazon EC2 [START_REF] Amazon | Amazon Elastic Compute Cloud (Amazon EC2)[END_REF]).

The IDRE mainly targets three types of users described as follows. Service providers interact with the CHOReVOLUTION Studio to define the description models (i.e., interface and security models) of existing services and then publish them into the Service Inventory. The benefit they obtain is to foster and ease the reuse of their services by developers, hence increasing the opportunities to be involved in new businesses. Choreography developers interact with the CHOReVOLUTION Studio to (i) model a choreography by using the Choreography Modeler. (ii) Realize the modeled choreography through the automatic synthesis of BCs (for solving heterogeneity issues), CDs (for solving coordination issues), As (for solving interface mismatches), and SFs (to make the choreography secure). This is done by exploiting the Synthesis Processor. Choreography operators interact with the CHOReVOLUTION console to (i) deploy and enact the generated choreography-based application through a structured process that involves the back-end layer; (ii) monitor the status of the execution cloud environment; (iii) monitor the execution of the choreography instances and managing their lifecycle.

Running Example

This section describes a simple example, called Chor-eCOM, that is used as a guide-through to explain the CHOReVOLUTION IDRE. The simple case study falls within the e-commerce domain. It concerns the purchasing of one or more products of different nature.

In our example, the customer is connected to the Internet through a web client or a mobile app. The customer can select a list of items and, once the payment has been performed, the order can be processed, and the invoice can be sent back to her. Then, according to the delivery schedule, the items are packaged and sent to the customer, who will in turn receive shipping information.

Figure 3 shows the Chor-eCOM example choreography specification by means of a BPMN2 Choreography Diagram. A choreography diagram specifies the way the choreography participants exchange information (messages) from a global point of view. The main element of a choreography diagram is the choreography task (e.g., Order Products task on left of Figure 3). Graphically, BPMN2 diagrams uses rounded-corner boxes to denote choreography tasks. Each of them is labeled with the roles of the two participants involved in the task. The white box denotes the initiating participant that decides when the interaction takes place. A task is an atomic activity that represents an interaction by means of one or two (request and optionally response) message exchanges (orderRequest) between two participants (Order Processor and Scheduler).

The use case starts with the mobile application Customer sending her information together with the ordering data. From this information, Order Processor sends the message scheduleRequest to the Scheduler participant for scheduling the order. Then, it initiates two parallel flows in order to retrieve the information for delivering and paying the order (see the parallel branch represented as a rhombus marked with a "+", with two outgoing arrows, namely a Diverging Parallel Gateway, just after the choreography task Organize Schedule). In particular, the top-most branch retrieves payment and invoice information, while the bottom-most branch gathers delivery information. Finally, the two parallel flows are joined together in order to notify order information to the user by means of Notify Order Information choreography task.

We used the choreography specification in Figure 3 to realize a simple ecommerce choreography-based system where a number of publicly available ser-vices can be reused. They have been reused -as black-box third-party software -to instantiate the roles of the participants Scheduler, Payment System, Invoicer, and Carrier. The other participants (Order Processor and Shipper) had to be developed from scratch, and here our synthesis method comes into play. These participants represent the missing logic to be composed and coordinated with the logic offered by the reused services. Note that, the Customer participant represents the mobile app used by the user.

In the remainder of this section the Chor-eCOM example is used to show the realization of a choreography-based system by highlighting the roles played by the three types of users of the CHOReVOLUTION IDRE described in Section 3.

Service Provider -A service provider uses the IDRE in order to publish the description models of the services into the Service Inventory. The IDRE allows to deal with the heterogeneity of the services involved in a choreography. To this extent, it provides a uniform description for any service or thing, given by means of the Generic Interface Description Language (GIDL) [START_REF] Bouloukakis | Enabling Emergent Mobile Systems in the IoT: from Middlewarelayer Communication Interoperability to Associated QoS Analysis[END_REF] or the WSDL [START_REF]W3C: Web Services Description Language (WSDL) Version 2.0[END_REF] in case of SOAP services. GIDL supports interface description for any kind of possible services (e.g., REST services) and thing. As already said in Section 2, the published services are selected in order to play the participants roles of a choreography. Then, the next phases will use the services models to synthesize the additional software artefacts (i.e., BCs, SFs, CDs, As) of the choreography.

Referring to the Chor-eCOM example, the service provider has to create a Service/Thing project inside the CHOReVOLUTION Studio by using a GIDL description for the following services: Scheduler, Payment System, Invoicer, and Carrier. Due to lack of space, we do not provide the steps to create and publish services within the Service Inventory. At the end of this process, the Service Inventory contains the following published services (see Figure 4). Choreography Developer -A choreography developer exploits the CHOReV-OLUTION Studio to model a choreography and to realize it. For this purpose the developer has to create a CHOReVOLUTION Synthesis project. Then, he or she models the BPMN2 choreography diagram together with the XML messages by using the Eclipse BPMN2 choreography modeler [START_REF]Eclipse: Eclipse BPMN2 Modeler[END_REF]. As already discussed in Section 2, after the modeling phase, the choreography developer starts the synthesis process. The first two activities of the process (i.e., Validation and Choreography Projection) do not require any user interaction. Then, the choreography developer starts a wizard interface that through several steps realizes the other activities of the synthesis process. Selection The first step of the wizard requires the choreography developer to select, for each choreography participant, its corresponding service from the Service Inventory. Referring to the simple example choreography, the choreography developer has to select all the services published into the Service Inventory as described previously, see Figure 5.

BC Generation Figure 6 shows the step of the wizard used by the choreography developer to configure the Binding Components generator for those selected concrete services that do not use the SOAP [START_REF]W3C: SOAP Version 1.2[END_REF] protocol. Moreover, the choreography developer has to specify the interaction paradigm used by the client participant of the choreography, by choosing either REST or SOAP.

Considering the Chor-eCOM example, since all the services selected in the previous step are REST services, they are listed in the wizard together with their GIDL description. Moreover, the example provides the purchase information through a mobile application, so the choreography developer has to choose REST as the interaction paradigm of the client participant (Customer). The SF Generation step is skipped because the existing services do not have security constraints. Adapter Generation -Figure 7 shows the view of the wizard used by the choreography developer to solve interface mismatches. These mismatches can arise due to a possible gap between the selected services and the (respective) participant roles in the specified choreography. They concern operation names mismatches and I/O data mapping mismatches. The wizard shows all the choreography tasks that require the choreography developer to specify the adaptation logic, they are grouped by their initiating participant, see the left-most column in Figure 7. By clicking on the button labeled with "..." a new window is opened, as shown in Figure 8. By interacting with this new dialog window, the choreography developer specifies the mapping between the choreography task messages, reported on the left-most column, and the service operations messages, reported on the rightmost column. The elements identified with the red shapes are mandatory to be mapped, whereas those in orange are optional. First, the choreography developer has to map the choreography task with a service operation, and then the related Input and Output messages are auto-mapped. Furthermore, the items forming the message(s) associated to the choreography task under study have to be mapped with the related items forming the specific service message.

CD Generation -It concerns the generation of the Coordination Delegates. The choreography developer has to specify the Correlations Tasks, i.e., a correla-Fig. 9. CD generation activity Fig. 10. Choreography Architecture tion between two choreography tasks. The first task involves a client participant as the initiating participant and a service as the receiving participant. The second task of the correlation involves the same service as the initiating participant and the same client as the receiving participant. In other words, a Correlation Task serves to specify that, in the specified choreography, there are two different tasks that are correlated. Note that these tasks are not necessarily consecutive in the defined choreography flow. This means that the two interactions represented by the two correlated tasks, between the considered client and service, will be indeed realized by a single request-response operation (synchronous interaction) on the service side. The first task corresponds to the invocation by the client of the service' operation and the second task corresponds to the reply by the service to the invocation previously performed by the client.

Considering the Chor-eCOM example, the mobile application starts the choreography by sending the ordering information and then it gets back all the information related to the order. Thus, the choreography developer has to specify a correlation between the task Order Products and the task Notify Order Information (see Figure 9). Choreography Architecture Generation Considering the selected services and the generated BCs, SFs, ADs, and CDs, an architectural description is automatically generated. A graphical representation (reported in Figure 10) of the choreographed system shows the architectural description related to the Chor-eCOM example. As described in the previous steps, each selected service is a REST service (R purple label) associated with a Binding Component (BC black label) and an adapter (A dark blue label). The green and red boxes correspond to the generated CDs. The blue box represents the mobile application. Choreography Deployment Description Generation The last activity of the synthesis process concerns the generation of the Choreography Deployment Description (aka ChorSpec) out of the choreography architectural description. The After the upload of the choreography specification, the choreography is available in the CHOReVOLUTION console (see Figure 11). Choreography Operator -At the end of the synthesis phase, the choreography is in the CREATED status on the CHOReVOLUTION Console (see Figure 6.46). At this point, the Operator can use the "gear" icon to deploy the choreography into the Cloud by passing the ChorSpec to the Enactment Engine. After few minutes the status changes to STARTED.

Once correctly enacted, the choreography operator can check the health of the virtual machines running the choreography by clicking on the magnifying glass icon. The choreography details page reports monitoring data collected from each virtual machine, and these data can be used by the choreography operator to take action to adapt the virtual machine pool to the expected load, see Figure 12. The SMT use case has been implemented in cooperation with Softeco, the industrial partner from the Genoa city (Italy). The main scope of the SMT use case is to realize a Collaborative Travel Agent System (CTAS) through the cooperation of several content and service providers, organizations and authorities publicly available in Genoa. The SMT use case involves a mobile application as an "Electronic Touristic Guide" that exploits CTAS in order to provide both smart mobility and touristic information.

The Urban Traffic Coordination (UTC) use case has been implemented in cooperation with RISE Viktoria, the industrial partner from the Götheborg city (Sweden). As described in detail in [START_REF] Chen | Choreographing services for smart cities: Smart traffic demonstration[END_REF], the main scope of the UTC use case is to realize a Cooperative intelligent transport systems (C-ITS) that allows vehicles and transport infrastructure to interconnect, share information and use it to coordinate their actions. The C-ITS provides traffic coordination services exploited through a mobile app for assisting drivers in an eco-friendly and comfortable driving experience.

We evaluated the CHOReVOLUTION IDRE by conducting an experiment for each use case. The goal of the two experiments was to measure the time saving for realizing, maintaining and evolving the two use cases with the CHOReVO-LUTION approach when compared to the development approaches the partners daily use. The considered development phases are: implementation, maintenance and evolution. The implementation phase consists of the development of a choreography-based system from scratch. The maintenance phase concerns the implementation of updates through service substitution. The evolution phase concerns the development effort required to tackle business goal changes through the modification of the choreography specification. According to the considered phases, the experiment aims to test the following hypotheses. The CHOReV-OLUTION approach allows developers to implement (Hypothesis 1), maintain (Hypothesis 2), and evolve (Hypothesis 3) a choreography-based system more quickly.

The time saving is measured in terms of person-hour (ph). In particular, regarding the SMT use case, we employed the following experimental units:

SMT Experimental unit 1 (SMT-EU1): CHOReVOLUTION approach -full usage of the CHOReVOLUTION IDRE except for the development of the mobile application, which is out of the scope.

SMT Experimental unit 2 (SMT-EU2): General-purpose enterpriseoriented technology -full usage of the technologies daily adopted by the Softeco partner, i.e., Microsoft .Net, C#, and Visual Studio.

SMT Experimental unit 3 (SMT-EU3): Domain-specific system integration platform -full usage of the proprietary platform developed by the Softeco partner, i.e., emixer [START_REF] Emixer | EMixer[END_REF]. It is a content and system integrator that is specific for the travel and mobility information domain.

With respect to the UTC use case, we defined two experimental units. The UTC-EU1 is the same as the SMT-EU1. The second one is defined as follows UTC Experimental unit 2 (UTC-EU2): General-purpose enterpriseoriented technology -full usage of the development technology daily adopted by the RISE partner, i.e., NodeJS and ExpressJS, and Microsoft Visual Studio.

The technologies of SMT-EU2, UTC-EU2, and SMT-EU3 were selected considering that the industrial partners were already skilled with them.

Table 1 summarizes the results of the experiment on the two use cases by distinguishing the implementation, maintenance, and evolution phases. In particular, the EU2 and EU3 highlight in bold the ph saved by using our approach. The industrial partners experienced a significant time decrease with respect to the their daily development approaches.

Conclusions

This paper has presented the CHOReVOLUTION IDRE, an integrated platform for developing, deploying, executing and monitoring choreography-based distributed applications. A simple explanatory example, has been used to show the CHOReVOLUTION IDRE at work. We evaluated the IDRE against two industrial use cases. During the evaluation, the industrial partners experienced a significant time decrease with respect to their daily development approaches. The results of the experiments indicate that CHOReVOLUTION has a great potential in developing choreography-based applications and the two use cases got a full benefit from it. More pilots and development cases will allow to consolidate the technical maturity of the product and pose the basis for a commercial validation.

Fig. 1 .

 1 Fig. 1. CHOReVOLUTION development process

Fig. 2 .

 2 Fig. 2. CHOReVOLUTION IDRE overview

Fig. 3 .

 3 Fig. 3. Chor-eCOM choreography diagram

Fig. 4 .

 4 Fig. 4. Service Inventory

Fig. 5 .

 5 Fig. 5. Selection activity

Fig. 6 .

 6 Fig. 6. BC generation activity

Fig. 7 .

 7 Fig. 7. Adapter generation activity

Fig. 8 .

 8 Fig. 8. Adapter Mapping

Fig. 11 .

 11 Fig. 11. Uploaded choreography

Fig. 12 .

 12 Fig. 12. Monitoring a choreography

Table 1 .

 1 Overall calculation of time savings

			SMT use case
	EUs	Implementation	Maintenance	Evolution	Time saving
	1	7	0,7	1	-
	2	113 106 saved	10 9,3 saved	27 26 saved	141,3
	3	58,5 51,5 saved	8,5 7,8 saved	14 13 saved	72,3
			UTC use case
	1	11	0,7	1,5	-
	2	152 141 saved	12,5 11,8 saved	26,5 25 saved	177,8

http://www.chorevolution.eu

Acknowledgments

Supported by: (i) EU H2020 Programme under grant no. 644178 (CHOReVO-LUTION -Automated Synthesis of Dynamic and Secured Choreographies for the Future Internet), (ii) the Ministry of Economy and Finance, Cipe resolution n. 135/2012 (INCIPICT), and (iii) the GAUSS national PRIN project (Contract no. 2015KWREMX).