IMSIA Olivier Cadot

Stochastic fluid structure interaction of a flat plate facing a uniform flow

Keywords: Stochastic, Symmetry breaking, Fluid structure interaction, Non Gaussian statistics

An experiment of a flat rectangular plate facing a uniform flow at Re=264000 shows the importance on the base pressure loading of the asymmetric static modes of the turbulent wake. The plate is free to rotate around its small symmetry axis. For plates with aspect ratio <6, the angular position exhibits strong random discontinuities between steady states of large non zero angles. The steady states have long time durations, more than one order of magnitude larger than the convective timescale. The discontinuities, comparable to violent and unexpected events are due to strong fluid forces associated with the drastic global change of the three dimensional wake, mainly the switching between static asymmetric modes.

Introduction

It is known that for three dimensional bodies, the first bifurcation in the flow solution as the Reynolds number is increased leads to steady symmetry breaking modes. This has been demonstrated for axisymmetric bodies [START_REF] Fabre | Bifurcations and symmetry breaking in the wake of axisymmetric bodies[END_REF][2] [START_REF] Bohorquez | Stability and dynamics of the laminar wake past a slenderblunt-based axisymmetric body[END_REF] and for bodies having rectangular blunt base [START_REF] Grandemange | Reflectional symmetry breaking of the separated flow over three-dimensional bluff bodies[END_REF] [START_REF] Marquet | Global wake instabilities of low aspect-ratio flat-plates[END_REF]. At low Reynolds number, these steady modes play an important role in problems of fluid structure interaction, such as for instance the dynamics of falling bodies [START_REF] Ern | Wake-induced oscillatory paths of bodies freely rising or falling in fluids[END_REF]. Recently, steady symmetry breaking modes have been evidenced at large Reynolds numbers, leading to random multistable dynamics. For bodies having a reflectional symmetry such as the Ahmed body, Grandemange et al. [START_REF] Grandemange | Turbulent wake past a three-dimensional blunt body. Part 1. Global modes and bi-stability[END_REF] have shown that the wake is bistable with a long time dynamics of random switching between two mirror symmetry breaking modes.

As shown in [START_REF] Marquet | Global wake instabilities of low aspect-ratio flat-plates[END_REF], simple rectangular plates are subjected to these steady symmetry breaking modes in the laminar regime and one may wonder how they can interfere in the case of fluid structure interaction at large Reynolds numbers. The purpose of this work is to study the consequence of such static symmetry breaking modes dynamics on a very simple fluid structure interaction experiment involving a three dimensional turbulent wake. It will be evidenced that the switching between these symmetry breaking modes leads to rare and violent events on the plate motion.

Experiment

The mechanical system is a simple plate that rotates freely around its small reflectional symmetry axis as depicted in Fig. 1. The plate is made of plexiglass, its thickness L is 6mm, the height H is 48mm. Aspect ratios =H/W ranging from 1 to 8 are investigated with plates of different widths W. The plates are pierced with a hole of 4.2mm in diameter at the position H/2. A rod (the axis of rotation), with a diameter of 4mm made of brass and lubricated with silicon oil is passed through the hole. The plate is then free to rotate around a fixed axis. Two teflon annuli avoid the plate to slide along the rod. We denote  the angle between the plate and the vertical unit vector, taken as positive in the clockwise direction. The plate angular velocity, expressed in rad.s -1 is  . Cross section view (a) and side view (b).

The dynamical system is placed in a hydrodynamics tunnel of cross section 15080mm. The test section is 800mm long and completely transparent. The fluid is water ( = 1000kg/m 3 ). The main flow velocity is set to U 0 =5.5m.s -1 , such that the Reynolds number defined as Re= U 0 H/=264000. There is no cavitation during the experiments unless during the visualisations for which the pressure has been reduced to produce enough bubbles to seed the wake. A Pegasus dual pulse 8 mJ Nd:YLF laser and a camera Photron APX RS with a resolution of 10241024 pixels are employed. The shutter of the camera is set to 60Hz and the repetition rate of the laser to 2kHz. As a result, bubble trajectories reveal the flow structure over a non dimensional duration of dt*=1/60•U 0 /H=1.91. For accurate measurements of the angle, we use a high speed and high precision optical Keyence micrometer (LS-7070M) constituted by a transmission unit (T in Fig. 1a) which emits light and a receiving unit (R in Fig. 1a) which detects the position of the shadow of the targeting object. The micrometer has an accuracy of ±3m and a sampling frequency of 2000Hz. In our case, it detects the horizontal position of the superior edge of the plate facing the flow as indicated by the  position in Fig. 1(b). The estimated accuracy for the angle measurements is =±0.01°.

Results and Discussion

We will consider two aspect ratios only, =6.85 and =3.43. The corresponding angle time series in Fig. 2 and spectra in Fig. 3 are very different. For the large aspect ratio, the plate response is very similar to a simple linear system excited with a random white noise ) (t

 : ) ( 2 0 t            
.

(1) The response power spectrum of the dynamical system (1) reads :

2 2 2 2 0 2 2 ) ( ) ( ) ( ~         , (2)
which superimposes satisfactorily to the experimental measurements in Fig. 3.

In the case of the lower aspect ratio, the angle undergoes much larger deviations, keeping same signs for very long time durations (more than hundreds natural timescale). The only characteristic frequency in the spectrum in Fig. 3 marks the beginning of a power law decrease at about f*=2.10 -2 with an exponent close to -3 over more than one decade. The exponent is related to the random occurrence of events of large deviations. These events are better quantified with the probability density function of the angle displayed in Fig. 4 (top). While the statistics is Gaussian for =6.85 as expected for a linear response of the random white noise forcing, it spreads extended tails for =3.43 showing extreme events of very large angle deviations. However, the extreme events of angular velocities are similar for both dynamics in Fig. 4 (bottom). The striking difference relies in the excess of event of zero angular velocity for the  = 3.43 plate. It is due to the presence of plateaus in Fig. 2, equivalent to static states, having random lifetimes.

Violent events are generally associated with large fluctuations compared to the typical one, it is then interesting to plot both statistics against their variable reduced by the standard deviation. As can be seen in Fig. 5, for the angle and the angular velocity, it is much more probable to observe a violent event, both in angle deviations and large velocities with the lowest aspect ratio plate. Flow visualizations and PIV measurements (not shown here) reveal the complex wake dynamics responsible for the stochastic behavior of the case  = 3.43. The wake is often clearly asymmetric, as shown in Fig. 6, with a large and intense circular recirculation close to the base either located on the bottom hand side (Fig. 6, left) or on the top hand side (Fig. 6, right). It has to be remember from above, that these static states (I.e. the angle keeps constant value) can have extremely long lifetimes compared to the natural timescale of the flow H/U 0 . The torque balance can be guessed from the pictures. While the intense recirculation in the wake associated with a low pressure (higher concentration of bubbles) creates a torque, the pressure distribution upstream the inclined plate produces a torque with an opposite sign.

Fig. 6 Flow visualization using bubbles technique showing some extreme events of angle for the plate free to rotate and having an aspect ratio  = 3.43.

The key ingredient for the stochastic fluid structure mechanism is actually based on the fact that when the plate is fixed, the stable wake is always reversed compared to that of the same inclination of the free plate. The fixed inclination then produce a global positive hydrodynamics stiffness with an equilibrium at =0. Thus,when the plate is free to rotate, the wake asymmetry produces a torque that inclines the plate in an unstable situation producing a wake reversal.

Conclusion

The stochastic dynamics is related to the existence of static symmetry breaking modes in the turbulent wakes of three-dimensional bluff bodies. In the case of the free to rotate flat plate, these static modes are able to create a violent an unintuitive dynamics. A model similar to (1) but with a stochastic forcing based on the probability of presence of the symmetry breaking modes with the angle now needs to be investigated.

Fig. 1

 1 Fig.1 Water tunnel facility and flat plate set up. Cross section view (a) and side view (b).

Fig. 2

 2 Fig.2 Angle time series for plates of aspect ratio  = 6.85 (blue) and  = 3.43 (black, artificially shifted by 15° for clarity).

Fig. 3

 3 Fig.3 Power spectrum of the angle for plates of aspect ratio  = 6.85 (blue) and  = 3.43 (black). The black line is the linear model (2) with  * =0.5 and f 0 * =0.13.

Fig. 4

 4 Fig.4 Probability density function of the angle (top), and angular velocity (bottom) for plates of aspect ratio  = 6.85 (blue) and  = 3.43 (black)

Fig. 5

 5 Fig.5 Probability density function of the reduced angle (top), and reduced angular velocity (bottom) for plates of aspect ratio  = 6.85 (blue) and  = 3.43 (black)

Proceedings of 3 rd International Conference on Violent Flows (VF-2016) 9-11, March 2016, Osaka, Japan


Matthias Güdemann

Pascal Poizat

Gwen Salaün

Lina Ye

VerChor: A Framework for the Design and Verification of Choreographies

Choreographies are contracts specifying from a global point of view the legal interactions that must take place among a set of services. Such a contract may serve as a reference in the development of concurrent distributed system, whether it is achieved following a top-down or a bottom-up approach. In this article, we present VerChor, a generic, modular, and extensible framework for supporting the development based on choreographies. It relies on a choreography intermediate format (CIF) into which several existing choreography description languages can be transformed. VerChor builds around a set of formal properties whose verification is central to choreography-based development.

To support this development process, we propose a connection between CIF and the CADP verification toolbox, which enables the full automation of the aforementioned properties. Finally, we illustrate a practical use of the VerChor framework through its integration with the Eclipse BPMN 2.0 designer.

I. INTRODUCTION

A PPLICATIONS are now often constructed out of the reuse and assembly of distributed and collaborating peers, e.g., software components, Web services, or Software as a Service in cloud environments. In order to facilitate the integration of these independently developed components, that may reside in different organizations, the peers participating in a composition should adhere to a global contract. Such a contract, called choreography, specifies from a global point of view the interactions that must take place among a set of peers. It is a reference for the further development steps, e.g., service selection, discovery, composition generation and evolution.

the composition of the peers has exactly the same behavior than what was prescribed in the requirements, i.e., the choreography. That is, that the reused peers are conform [START_REF] Bravetti | Contract Compliance and Choreography Conformance in the Presence of Message Queues[END_REF] to the choreography. Choreographies also support top-down development (Fig. 2). Choreographies are first used to obtain local, peer-level, requirements, also called (behavioral) skeletons. Again, one has to be sure that the composition of these peer requirements is conform to the specification, before going on and implementing the peers. The property checking whether a choreography can be realized or not by a set of peers is called realizability [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF]- [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF]. The design of the peer requirements could be achieved explicitly by a human as for the choreography. Still, it is much more interesting, following the generative programming paradigm, to retrieve the peer requirements automatically from the choreography specification, in which the peer requirements are implicitly defined. This can be achieved using projection operations [START_REF] Qiu | Towards the Theoretical Foundation of Choreography[END_REF], [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF], and thus yields a specific notion of realizability targeted at automated choreography-based development: a choreography is realizable if the set of peers that are obtained from it using projection conforms to the choreography itself. If so, a developer may implement the peer requirements by adding business code to them, following the same kind of process than, e.g., when complementing Java RMI skeletons generated from purely functional interfaces. The developer may also use the peer requirements to perform implementation by reuse, using behavioral discovery approaches [START_REF] Grigori | Behavioral Matchmaking for Service Retrieval[END_REF], or even by adapting services that would not perfectly match the needs [START_REF] Mateescu | Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques[END_REF]. If the choreography is not realizable, the designer has to change the choreography, unless corrective solutions are proposed.

Figure 3 presents a simple example of a conversation protocol [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF], one of the notations existing for describing choreographies, where each transition is labeled with a message exchanged between two peers, one sender and one receiver.

This protocol involves three peers: a client (cl), a Web application (appli), and a database (db). The client first submits a storage request to the application (req), then the application interacts with a database to store the information (store), and the database sends back an acknowledgment (ack). On the right hand side of Figure 3, we give the projection obtained from this choreography, where interactions are replaced with message receptions (question marks) and message emissions (exclamation marks). Even with this introductory example, it is difficult to say whether this choreography is realizable. This conversation protocol is actually realizable with synchronous communication but not realizable if peers interact via FIFO buffers (asynchronous communication), because the peer client can send in sequence several req messages whereas in the original contract, these messages can be sent only at a certain moment in time (but for the first one, after an ack interaction).

Motivations. The existing techniques for formally verifying choreographies suffer several drawbacks. First, they are language-specific, i.e., they focus on a single choreography modelling language, e.g., UML collaboration diagrams [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF], [START_REF] Bultan | Specification of Realizable Service Conversations using Collaboration Diagrams[END_REF], conversation protocols [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF], Singularity channels [START_REF] Stengel | Analyzing Singularity Channel Contracts[END_REF] or BPMN 2.0 choreographies [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF]. As a consequence, the other existing languages cannot take profit of these analysis techniques, which limits their applicability and impact. Second, most existing works, e.g., [START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF], [START_REF] Kazhamiakin | Analysis of Realizability Conditions for Web Service Choreographies[END_REF]- [START_REF] Gössler | Realizability of Choreographies for Services Interacting Asynchronously[END_REF], propose techniques for checking the realizability property only. Other formal properties and composition issues also need to be verified for choreographies but are hardly tackled in the literature. For instance, if a choreography is not realizable, it is of prime importance from a user perspective to provide automated solutions for resolving these issues, that is enforcing realizability by correcting the possible message sequences. Third, most existing choreography analysis techniques oversimplify verification by assuming a synchronous communication model. This is sufficient in some cases, but the asynchronous communication semantics, used in most distributed systems, raises important theoretical issues such as state space explosion due to communication buffers. These issues are not dealt with by purely synchronous approaches. It should be noted that the use of data being exchanged between peers may also result in state space explosion. Still, this has been recently addressed using symbolic models [START_REF] Nguyen | A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies[END_REF]. Last but not least, but for some exceptions [START_REF] Nguyen | A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies[END_REF]- [START_REF] Fu | WSAT: A Tool for Formal Analysis of Web Services[END_REF], limited effort has been spent to develop available formal verification tools for supporting the choreography-based design of communicating software. [START_REF] Decker | An Introduction to Service Choreographies[END_REF], there are two interaction models for choreography: interconnected interface models, where conversations are defined at (each) peer level and interactions are defined by connecting these conversations, and interaction models, where interactions between peers are the basic building blocks. The former nicely suits lowlevel languages such as WS-BPEL where an orchestration would be defined for each peer and communications would correspond to connections between peer models. However, from a designer perspective, and following the separation of concerns principle, interaction models better suit the needs of choreography specification due to their global perspective. Hence, we focus on interaction-based languages in this article.

Models. As classified by

Approach. In this paper, we present VerChor, a formal and tool-supported framework available at [START_REF]VerChor Framework[END_REF], that supports both bottom-up and top-down development. It also considers both synchronous and asynchronous communication models. As far as verification is concerned, in this article we focus on the compliance between the choreography and its distributed version consisting of interacting peers. This check includes not only the conformance and realizability properties, but also synchronizability [START_REF] Basu | Deciding Choreography Realizability[END_REF], which addresses conditions under which synchronous and asynchronous peer compositions are equivalent. The benefit of synchronizability is that if a choreography is synchronizable, conformance (hence realizability) can be checked for synchronous communication and yields for asynchronous communication too. Beyond these checks, if the choreography is not realizable, we propose a transparent and non-intrusive solution, which enforces the distributed system to respect the choreography requirements. This is achieved by synthesizing automatically distributed controllers that interact together for resolving message ordering issues. However, realizability enforcement is not possible for all choreographies. Therefore, before applying our solution based on controller generation, we need to check whether the repairability property is satisfied or not. This check can be achieved on the choreography itself and does not require an analysis of the distributed version of the system.

Figure 4 presents the models being used in a top-down development process, and the order in which properties and synthesis techniques are achieved. This applies also to bottomup development where peer skeletons are not obtained by projection but are available as an input of the process.

In order to accept the choreography specification languages commonly used by designers as input, we define a choreography intermediate format (CIF) and propose automated connections from existing choreography languages (such as conversation protocols or BPMN 2.0 choreographies) to this intermediate format. As far as the back-end connection is concerned, we have developed a translation from our interme- Fig. 5. Framework Overview diate format to the LOTOS NT (LNT) process algebra [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF], which is one of the CADP input specification languages [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. CADP is a verification toolbox providing a large variety of automated analysis techniques. This connection to LNT/CADP enabled us to develop a fully operational verification library for automating the key choreography synthesis and analysis tasks using behavioral model operations such as products, alphabet hiding, and equivalence checking.

All the steps of our approach, described in Figure 5, are fully automated by model transformations we have implemented, verification scripts we generate, and verification tools we reused from the CADP toolbox.

Other back-end verification toolboxes can be connected to our intermediate format. This requires to develop other translations from the intermediate format to one of the input formal languages of the targeted toolbox. If, for instance, one is interested in using interactive theorem proving for choreographies, an encoding into Isabelle, Coq or PVS input formats could be developed. Translating our intermediate format to Petri net models is also a promising option for reusing existing analysis techniques developed for Petri nets, e.g., [START_REF] Martens | Analyzing Web Service Based Business Processes[END_REF]- [START_REF] Decker | Local Enforceability in Interaction Petri Nets[END_REF].

It is worth noting that, since we have developed a connection to the CADP toolbox through a translation to LNT, all verification tools available in CADP can also be used on the system under design (choreography and distributed implementation). A noticeable example is the Evaluator 4.0 on-the-fly model checker that can verify temporal properties specified in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF], an extension of alternation-free µcalculus with regular expressions, data-based constructs, and fairness operators.

Contributions. Our contributions are as follows:

• We propose a generic, extensible format for describing choreographies accepting several languages as input (e.g., conversation protocols and BPMN 2.0 choreographies). • We define a verification library, automating key choreography analysis tasks using model and equivalence checking, with a focus on asynchronous communication (via FIFO buffers). Beyond property checking, we also present controller synthesis techniques for enforcing realizability. • We present a set of freely available tools we have implemented that supports and automates the different parts of our approach that is (i) translating the choreography description languages accepted as input into the intermediate format, (ii) translating the intermediate format into the input language of the verification tools used for the analysis, and (iii) generating the necessary scripts for automating all the translation and verification steps.

Outline. Section II introduces the choreography languages connected so far to our intermediate format, with a particular emphasis on BPMN 2.0. The choreography intermediate format is itself presented in Section III. In Section IV, we present our verification library. Section V describes the tools we have implemented for supporting our approach. Finally, Section VI reviews related work and Section VII concludes the article.

II. CHOREOGRAPHY DESCRIPTION LANGUAGES

We have considered the following three groups of interaction-based choreography description languages for designing the intermediate format presented in Section III:

• WSCI and WS-CDL rely on a standard exchange format (XML) which simplifies model Transformation. However, these languages are not systematically equipped with formal semantics and the absence of graphical front-end makes writing painful. • BPMN 2.0 choreographies [START_REF]Business Process Model and Notation (BPMN) -Version 2.0, OMG[END_REF] or UML collaboration diagrams [START_REF] Bultan | Specification of Realizable Service Conversations using Collaboration Diagrams[END_REF] are user-friendly graphical notations, convenient for end-users, but they often either lack of formal semantics or exhibit various (divergent) ones.

• Chor [START_REF] Qiu | Towards the Theoretical Foundation of Choreography[END_REF] and conversation protocols [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF] are formal description languages equipped with a formal semantics and analysis techniques. Yet, they are difficult for non-experts. In this section, we introduce conversation protocols and BPMN 2.0 choreographies, because these are the currently available front-ends in the VerChor framework. Yet all the languages mentioned above can be transformed to our intermediate format. We have a particular interest in BPMN 2.0 choreographies, because it became an OMG standard notation in 2011, an ISO standard in 2013 [START_REF]International Standard 19510, Information Technology -Business Process Model and Notation[END_REF], and it is now commonly used for modelling choreographies.

A. Conversation Protocols

A conversation protocol [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF] is a Labeled Transition System (LTS) specifying the desired set of interactions from a global point of view. Each transition specifies an interaction between two peers P sender , P receiver on a specific message m. A conversation protocol makes explicit the execution order of interactions. Sequence, choice, and loops are modelled using a sequence of transitions, several transitions going out from the same state, and a cycle in the LTS, respectively.

Definition 1 (Conversation Protocol): A conversation protocol CP for a set of peers P = {P 1 , . . . , P n } is an LTS (S CP , s 0 CP , L CP , T CP ) where S CP is a finite set of states; s 0 CP ∈ S CP is the initial state; L CP is a set of labels where a label l ∈ L CP is a tuple m Pi,Pj such that P i , P j ∈ P are the sending and receiving peers, respectively, P i = P j , and m is a message on which those peers interact; finally, T CP ⊆ S CP × L CP × S CP is the transition relation.

A transition t ∈ T CP is usually denoted as s m P i ,P j ----→ s ′ where s and s ′ are source and target states and m Pi,Pj is the transition label. An introductory example of conversation protocol is given in Figure 3.

A conversation protocol is a low-level formal model, which can be computed from other existing specification formalisms such as UML collaboration diagrams [START_REF] Bultan | Specification of Realizable Service Conversations using Collaboration Diagrams[END_REF], Singularity channels [START_REF] Stengel | Analyzing Singularity Channel Contracts[END_REF], or BPMN [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF]. It is worth noting that conversation protocols can serve as formal semantic model for the Choreography Intermediate Format (CIF) we present in Section III. However, it is much easier to transform a choreography description language to CIF than going directly to such a lowlevel model. Indeed, CIF consists of high-level operators that assure a straightforward translation for all afore-mentioned languages, whereas a transformation to conversation protocols requires the flattening of all operators (e.g., expanding a parallel composition to all the possible corresponding interleavings), which is quite difficult, see [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF] for a transformation from BPMN choreographies to conversation protocols.

We use LTSs for specifying the peer behavioral model, which defines the order in which the peer messages are executed. A label consists of a message name and a direction (emission ! or reception ?).

Definition 2 (Peer): A peer is an LTS P = (S, s 0 , Σ, T ) where S is a finite set of states, s 0 ∈ S is the initial state, Σ = Σ ! ∪ Σ ? is a finite alphabet partitioned into a set of send and receive messages, and T ⊆ S × Σ × S is the transition relation. We write m! for a message m ∈ Σ ! and m? for m ∈ Σ ? .

Each peer is obtained by projection from a CP by keeping only messages where that peer appears, and replacing interactions by emissions or receptions.

Definition 3 (Projection): Peer LTSs P i = (S i , s 0 i , Σ i , T i ) are obtained by replacing in CP = (S CP , s 0 CP , L CP , T CP ) each label m Pj ,P k ∈ L CP with m! if j = i, with m? if k = i, and with τ (internal action) otherwise; and finally removing the τ -transitions by minimizing the LTS modulo weak trace equivalence [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF], which yields a τ -free and deterministic LTS.

B. BPMN 2.0 Choreographies

BPMN 2.0 [START_REF]Business Process Model and Notation (BPMN) -Version 2.0, OMG[END_REF] (BPMN in the rest of this article) introduces Choreography Diagrams to support conversations with choreography tasks as first class entities. The basic building block of BPMN Choreography Diagrams is a one-way or two-way interaction between peers. This is modelled using a choreography task (Figure 6), where interactions involve two peers, A and B, represented by participant bands. A is the initiating peer, i.e., the one that decides when the interaction takes place, it is represented by a white band as opposed to a gray filled band for B. Together with the choreography tasks, there exist message flows relating the interaction with an initiating message (represented by a white envelope) and, possibly, a return message (represented by a black envelope). This yields one-way interactions (Figure 6,(a,c,d,e)) or two-way interactions (Figure 6, (b)). In the rest of this article, for simplification purposes, we assume that message and task names are always identical.

A choreography task may have an internal marker to denote whether, and how the related interaction (one or two message exchanges) is repeated. In a standard loop (Figure 6, (c)), the interaction is performed several times. In multi-instance parallel loops, the interactions are performed by several instances of the choreography task. This can be done in parallel (Figure 6, (d)) or in sequence (Figure 6, (e)). If the exchange is not repeated, no marker is used (Figure 6, (a, b)).

BPMN enables one to describe control flows using sequence flows for performing two tasks in sequence or gateways for more complex behaviors. In our work we take into account the main gateways found in BPMN (Figure 7), that is: exclusive gateways (decision, alternative paths), inclusive gateways (all combinations, from one to all), parallel gateways (creation of parallel flows), and event-based gateways (choice based on events, i.e., message reception or timeout). We require that gateways are either diverging / splitting (multiple outgoing sequence flows and at most one incoming sequence flow) or converging / joining (multiple incoming sequence flows and at most one outgoing sequence flow). Diagrams that would not adhere to this requirement can be transformed by adding new gateways [START_REF]Business Process Model and Notation (BPMN) -Version 2.0, OMG[END_REF], e.g., a gateway being both converging and diverging can be transformed as the sequence of a converging one and a diverging one.

III. CHOREOGRAPHY INTERMEDIATE FORMAT

In this section, we present the choreography intermediate format (CIF) we propose for automated verification of choreography description languages. Such an intermediate language presents several advantages. First, several input languages can be connected to it, and this allows designers to use their favorite choreography description language. Second, it makes it possible to use jointly several formal verification tools and techniques as back-end, provided that a connection to those tools exists. Third, it can also serve as an expressive standalone specification language for choreographies. Last but not least, the language can be easily extended with new choreography

A. A State Machine Meta-model

The CIF meta-model is based on a state machine representation of choreographies, where states model either interactions or choreography operators such as exclusive choice, start of parallel activities, or merging of execution flows. Sequence, i.e., the ordering between states, is modeled using arcs, each arc connecting a source and a target state. Such a meta-model is very close to the meta-models of workflowbased notations, which are the main family of domain specific modeling languages for business processes, choreographies, and orchestrations, with e.g., the WS-BPEL language and the BPMN notation. Indeed, workflows are directed graphs with nodes that correspond not only to gateways, but also to interactions, as demonstrated for example in the BPMN metamodel with ChoreographyTask (the class for interactions), which is a subclass of FlowNode, the class representing nodes in the workflow (these nodes being related by arcs of type SequenceFlow).

A first advantage of such a state machine meta-model is therefore to make it easier to transform workflow-based choreography languages into it, as demonstrated in Figure 9, still without hindering the transformation from other state and transition models such as the conversation protocols presented in Section II. A state machine meta-model also makes it easily possible to represent unbalanced workflows and complex loops (where the flow of execution gets back at some point earlier in the behavior) using arcs between states. Last but not least, the state machine pattern significantly facilitates a further encoding into any formal model of choreographies. This is the case for instance with LNT where some CIF constructs are translated in a straightforward way to the target language (see Section III-C for details), although other constructs deserve more attention. We give in Figure 8 the CIF meta-model describing more precisely the structure of our intermediate format, expressed as a class diagram. One of the main classes for the state machine representation is the State abstract class which provides an abstract method to access its list of successor states. The InitialState class represents the unique initial state of a choreography. It implements the getSuccessors operation, but has only a single successor state. The FinalState class represents a terminal state of the choreography and will therefore always have an empty list of successors. The Interaction class is used to model a basic choreography interaction through a Message exchanged between a sender and a receiver peer.

The Selection abstract class provides means to split the flow of a choreography into multiple possible continuations. Any instance of a class which extends it will always provide multiple successors through the getSuccessors operation. The most basic variants are Choice and DominatedChoice, where exactly one of the successor states continues. Choice is found in most choreography languages: one branch is executed among a number of possible executions. DominatedChoice is used in some languages (e.g., Chor [START_REF] Qiu | Towards the Theoretical Foundation of Choreography[END_REF]) for specifying explicitly the peer that makes the choice in case of ambiguity. The parallel execution of all continuations after a selection is represented by the AllSelect class. The parallel execution of a subset of the continuations can be specified using the SubsetSelect class. In this last case, all possible combinations should be possible in the corresponding behavior (e.g., if there are two branches involved we can execute only one of them or the two in parallel) as well as a default branch if such case is specified.

The dual of the Selection class is the abstract Join class, which is realized either by SimpleJoin which has only one incoming active flow, AllJoin for full parallel active flows and SubsetJoin for a subset of all incoming flows. Each join waits for the corresponding number of incoming active flows and synchronizes accordingly. Inconsistencies in a choreography, such as possible mismatches of selection and join operators, can be detected by structural analysis. It does not make sense for instance to match a single choice (Choice) with an all join (AllJoin), as only a single incoming flow is active and should be expected at the corresponding join point.

Figure 9 shows the CIF representation of the choreography in Figure 7, left, with an added initial state. One can easily identify the participants, represented with objects of class Peer. The exchanged messages are represented by objects of class Message, where each message has an associated sender and receiver. The interactions are represented by objects of class Interaction, with an association to the message which is exchanged, while the parallel gateway is represented by the object of class AllSelect. The sequence in the choreography is represented by the succeededBy association between objects.

One could wonder why we have not chosen other languages as intermediate format such as BPMN, conversation protocols, or the LNT process algebra that we use in the sequel as an intermediate step for generating the behavioral models (LTSs) of peers and choreographies. CIF is close to BPMN in the sense that it consists of high-level operators, but CIF may contain more operators than BPMN, the dominated choice for instance. The main issue with conversation protocols and LNT is that transforming the choreography description languages we consider here (e.g., BPMN) to such languages is quite complex for some constructs (see see Section III-C for details on the encoding from CIF to LNT). One of our main motivations was to make the front-end transformations as simple as possible, which is the case with CIF.

B. Front-end Connections

For illustration purposes, we focus on the subset of BPMN 2.0 choreographies introduced in Section II and show how to transform it into CIF, as illustrated in Figure 9. BPMN ChoreographyTask is transformed into CIF Interaction. If the task is related to a message via a BPMN MessageFlow (as in Fig. 6), we generate a CIF Message from it. Else, we use the ChoreographyTask name (as in Fig. 9). BPMN two-way interactions are first transformed into a sequence of two one-way interactions. BPMN gateways are transformed into corresponding CIF class instances, i.e., exclusive and event-based splits are transformed into Choice instances, parallel and inclusive splits into AllSelect and SubsetSelect constructs, respectively, exclusive and event-based joins into SimpleJoin, inclusive joins are encoded into SubsetJoin, and parallel joins into AllJoin. The sequencing between choreography nodes, achieved with SequenceFlow instances in BPMN, is transformed in CIF using the succeededBy association.

Similarly, the translation of the choreography description languages mentioned at the beginning of Section II is straightforward except for UML collaboration diagrams. Their encoding is slightly more complicated than for the others due to the use of synchronization points between concurrent threads that cannot be encoded using join operators. Therefore, the simplest solution is first to translate UML collaboration diagrams into a lower level formalism, such as conversation protocols or LTSs as done in [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF], and then connect this low-level format to our intermediate format. This connection is straightforward for conversation protocols, where sequences and loops are implicitly encoded using arcs in the state machine, and nondeterministic branches are translated to Choice states.

The semantics of our intermediate format is formalized by encoding into LNT (see Section III-C), LNT itself having a formal operational semantics defined in terms of LTSs.

Even if the semantics of the input choreography languages are not always formally defined (e.g., conversation protocols are equipped with a formal semantics, while the semantics of BPMN is informally defined [START_REF]International Standard 19510, Information Technology -Business Process Model and Notation[END_REF]), we paid a lot of attention when building our framework to preserve their semantics during the successive translations necessary for making their formal verification possible. We will comment on that with more details in Section V.

C. Back-end Connections

Several back-end connections can be proposed from our intermediate format. Possible candidates are for instance input languages of theorem proving tools (such as Coq, Isabelle, or PVS) and Petri net formalisms. In this article, we focus on input languages for model checking tools, because these verification techniques turn out to be adequate for the properties of interest here (see Section IV). In particular, we propose a connection to the LNT process algebra, which is one of the CADP input specification languages [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. Now we briefly describe the principles for translating CIF to LNT. More details are available in Appendix, in particular for unbalanced choreographies. The reader can also refer to Section V for technical details of the tool support. For each CIF state, we generate an LNT process as follows:

• Initial/Final state: for the initial state n, suppose n m, i.e., m is the next state of n. The process for n calls the process for m. For a final state, its process does nothing but terminates by using the empty statement (null).

• Interaction: each interaction is encoded as an LNT action.

• Selection: we focus here on three types of selection.

1) all select state n: suppose that n has k outgoing branches, i.e., n m i , i ∈ {1, ..., k}. The LNT process models the parallel execution of all outgoing branches using the LNT parallel operator (par). Each branch m i , i ∈ {1, ..., k} is translated by a call to the LNT process encoding the node m i . In addition, if there exists a corresponding all join state mp, we need to generate an additional parallel branch to realize the synchronization point among the different branches. To do so, for this join, we create a synchronization action sync at the beginning of the additional branch and at the end of all other branches. In this way, the additional branch synchronizes with all other branches on sync before calling the process for the next node after mp.

2) subset select state n: suppose n m i , i ∈ {1, ..., k}. Any combination of the branches m i can be executed. For each subset {m i1 , ..., m in }, 1 ≤ n ≤ k, ∀j ∈ {1, ..., n}, i j ∈ {1, ..., k}, we obtain all combinations of this subset by using the LNT parallel operator between m ij , j ∈ {1, ..., n}. Then the LNT choice operator (select) is used between all combinations of all subsets. If there exists a corresponding subset join state, we generate an additional branch for synchronization purpose as above.

3) choice state n: suppose n m i , i ∈ {1, ..., k}. The process models the choice execution of all outgoing branches m i using the LNT choice operator. Each branch calls the LNT process encoding the corresponding node.

• Join: We have three types of join state. A join state has only one outgoing branch. 1) all join (subset join, resp.) state n: suppose n m. The process for n first synchronizes with all corresponding incoming active branches on the synchronization action sync before calling the process for m, i.e., it corresponds to the additional parallel branch produced by translating the selection (all/subset select) state.

2) simple join state n: suppose n m, then the process for n calls the process for m. Recall that there is no synchronization point for this state. Once a CIF instance C has been translated to LNT, one can obtain the corresponding LTS using classical enumerative exploration techniques, e.g., the LNT compilers of CADP. The LTS generated from this LNT specification corresponds to all possible enactments of C.

D. Extensibility

Although CIF covers a large and important part of the possible modelling artifacts for choreographies, there exist possible extensions to the format. An interesting extension to CIF is adding data to message contents [START_REF] Nguyen | A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies[END_REF]. For example, it could be possible to have gateways where the choice among several flows depends on data exchanged in earlier messages. The currently implemented analysis abstracts from the data and can therefore be regarded as an over-approximation. For some of the formal properties of choreographies described in Section IV, data-dependent choices could be helpful. In particular in the case of realizability, where the distributed system obtained after projection is analyzed, data dependency could provide additional means to coordinate choices between distributed peers, which is not possible without data exchange. Data parameters are supported in the LNT formal language, which we use to encode CIF. However, the inclusion of data parameters may increase drastically the size of the LTS model obtained from the LNT encoding, limiting the usefulness of the approach. On the other hand, regarding the properties presented in Section IV, the results of the current encoding without data-dependent choices, can be analyzed a-posteriori to identify false-negatives. For example, it could be verified afterwards that data-dependent choices restore a property like realizability. In such a case our approach would support the choreography designer by highlighting the potential problems.

IV. VERIFICATION LIBRARY

We present in this section key properties which are of utmost importance when designing choreography-based communicating systems. Following the process described in Figure 4, we proceed as follows. From a choreography model, projection is used to retrieve one model for each peer in the choreography. The synchronous and asynchronous compositions are computed from these behavioral models. Synchronizability checking is then achieved by checking the equivalence between these synchronous and asynchronous compositions. If the choreography is synchronizable, realizability checking is run, by checking the equivalence between the synchronous composition of the peers and the choreography model. If realizability yields, then the choreography design is fine. If either synchronizability or realizability is not achieved, we run the repairability check on the choreography model. If this fails too, the choreography design is incorrect and it must be modified using counter-examples produced in the different verification steps. If the choreography is repairable, then we generate distributed controllers to make the peers behave exactly as prescribed in the choreography. All these tasks are fully automated thanks to the encoding of CIF into the LNT process algebra, and the use of the CADP toolbox for model generation and verification.

The notion of realizability (conformance, resp.) we present in this paper is quite strong yet often used in the literature, see, e.g., [START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF]- [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF]. It ensures that the distributed system exactly reproduces the same sequences of messages as those defined in the choreography. This means that whatever composition is used (synchronous or asynchronous), the visible behaviour must remain exactly the same. This is what the synchronizability property checks. Weaker realizability notions could be considered such as those presented in [START_REF] Kazhamiakin | Analysis of Realizability Conditions for Web Service Choreographies[END_REF].

A. Synchronizability

Synchronizability is used to check if all interaction sequences in the asynchronous system are also possible in the synchronous one, ensuring that the asynchronous version of the system does not exhibit additional behavior, which is not present in the synchronous composition. These compositions must be the same, otherwise they cannot be conform to the choreography since the asynchronous system diverges somehow by introducing new (unexpected) behaviors.

Definition 4 (Synchronizability): A set of peers {P 1 , . . . , P n } is synchronizable when the synchronous composition of these peers LT S s = (P 1 | . . . | P n ) is equivalent to their asynchronous composition LT S a = (P 1 , B 1 ) || . . . || (P n , B n ) (both compositions are defined in [START_REF] Basu | Deciding Choreography Realizability[END_REF]), that is, LT S s ≡ t LT S a , where ≡ t stands for weak trace equivalence as advocated in [START_REF] Basu | Deciding Choreography Realizability[END_REF] and compares synchronizations in the synchronous composition with emissions from peers to peer buffers in the asynchronous composition.

A recent decidability result [START_REF] Basu | Deciding Choreography Realizability[END_REF] proposes the following decision procedure for checking synchronizability: The set of peers is first generated by projecting the choreography specification to each peer, ignoring the messages that are not sent or received by that peer. Then, both the system consisting of peers interacting synchronously and the system consisting of peers interacting via 1-bounded FIFO buffers are computed. Finally, equivalence checking is used to decide whether the two systems are equivalent. If this is the case, the choreography is synchronizable, meaning that the behavior of the distributed implementation will remain the same whatever is Fig. 10. Example of a Non-Synchronizable Choreography the size chosen for bounding buffers. This decision procedure relies on bounded, hence finite, systems and thus avoids the generation and analysis of possibly infinite systems.

Definition 5 (Synchronizability Decision): A set of peers {P 1 , . . . , P n } is synchronizable iff LT S s ≡ t LT S 1 a . In other words: LT S s ≡ t LT S 1 a ⇔ LT S s ≡ t LT S a . When computing synchronizability, only send actions are considered in the asynchronous case. Ignoring receive actions makes sense for checking synchronizability because: (i) send actions are the actions that transfer messages to the network and are therefore observable, (ii) receive actions correspond to local consumptions by peers from their buffers and can therefore be considered to be local and private information.

We show in Figure 10, the peers obtained by projection from the choreography in Figure 3. This system is not synchronizable, because cl can send several requests (req) in sequence in the asynchronous system, whereas the three interactions req, store, and ack always occur one after the other in the synchronous system, as specified in the choreography.

B. Realizability

This property is used to check if the distributed version of the system behaves exactly as specified in the choreography. This is crucial in a top-down development process in order to ensure that the implementation obtained via projection respects the global specification. Strong notions of realizability can be checked using equivalence checking. Other notions of realizability [START_REF] Kazhamiakin | Analysis of Realizability Conditions for Web Service Choreographies[END_REF] can be verified similarly, using pre-order simulation or partial order techniques.

Realizability as presented in [START_REF] Basu | Deciding Choreography Realizability[END_REF] is checked as follows: one first checks that a set of peers obtained via projection from the choreography is synchronizable. If the synchronizability check returns false, the system is not realizable. Second, if synchronizability is satisfied, the peer composition is computed from the choreography specification: the synchronous version is enough because we know it is equivalent, by synchronizability, to the asynchronous system. We finally compare the choreography with the peer composition, and if they are equivalent, the choreography is realizable.

Definition 6 (Realizability):

A conversation protocol C and the set of peers P i = (S i , s 0 i , Σ i , T i ) obtained by projection from this choreography (see, Def. 3) are realizable iff the set of peers is synchronizable (Def. 5) and the choreography is equivalent to the synchronous composition, that is, C ≡ t LT S s .

We recall that a conversation protocol is a low-level formal model, which can be computed from other existing choreography description languages, see Sections II-A and V.

Figure 11 gives an excerpt of a choreography originally presented in [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF], where a client (cl) pays a bank (bk), and in sequence, a booking system (bs) stores some information in a database (db) to keep track of a completed transaction. This choreography is synchronizable but not realizable: the resulting (synchronous and 1-bounded asynchronous) compositions are the same, but they are not equivalent to the choreography.

C. Conformance

In a bottom-up development process, peers are being reused and integrated into a new composition. The choreography serves as a contract that the implementation under construction must respect. From a verification point of view, it can be checked exactly as realizability, except that projection is not necessary. Conformance checking takes as input a choreography and a set of peers, whereas realizability checking only requires a choreography specification.

Definition 7 (Conformance): A conversation protocol C and a set of arbitrary peers P i = (S i , s 0 i , Σ i , T i ) are conformant iff the set of peers is synchronizable (Def. 5) and the choreography is equivalent to the synchronous composition, that is, C ≡ t LT S s .

D. Repairability

When a choreography is not realizable, an automated and non-intrusive solution for enforcing realizability is to generate distributed controllers that are in charge of correcting ordering issues to make the corresponding distributed implementation respect the choreography requirements. Repairable choreographies are those for which this controller synthesis solution But not all choreographies are repairable: A choreography is not repairable when at some point in its behavior there is a choice between interactions involving different sending peers [START_REF] Stengel | Analyzing Singularity Channel Contracts[END_REF]. In that case, realizability cannot be enforced because there is no way to impose the same choice on several distributed peers interacting using asynchronous communication. Therefore, it is important to check whether an unrealizable choreography respects this property before applying the controller generation solution.

Definition 8 (Repairability):

A conversation protocol C = (S, s 0 , L, T ) is repairable if ∄ s ∈ S such that s m P i ,P j ----→ s ′ , s m P k ,P l
-----→ s ′′ ∈ T and P i = P k . We can imagine finer notions of repairability, because there are situations where such a divergent choice actually corresponds to the start of interleaved behaviors (i.e., this is not a real choice but all possible interleavings of a same set of interactions), and in that case, the choreography is repairable.

Figure 12 presents a partial choreography involving two peers, client (cl) and booking system (bs), which communicate on two messages pay and alert. Here, there is a divergent choice because each peer can take a different decision than its partner, possibly resulting in a deadlock in the system if both peers choose to send, pay (cl) and alert (bs), respectively (grey state in the resulting asynchronous composition, Figure 12, right). Typically, such a situation is not repairable.

E. Control for Enforcing Realizability

If a choreography is not realizable yet repairable, we propose an approach to enforce that the distributed system respects the (synchronizability and) realizability of a choreography by generating distributed controllers [START_REF] Güdemann | Counterexample Guided Synthesis of Monitors for Realizability Enforcement[END_REF]. These controllers act locally by interacting with their peer and the rest of the system in order to make the peers respect the choreography requirements. A controller catches local peer emissions and relays them to other peers. Synchronization messages between controllers make them respect the choreography ordering constraints. Figure 13 gives an architectural view of how peers, buffers, and controllers interact altogether.

Definition 9 (Controller): A peer controller is an LTS C = (S, s 0 , Σ, T ) where S is a finite set of states, s 0 ∈ S is the initial state, Σ = Σ ! ∪ Σ ? ∪ Σ s is a finite alphabet partitioned into send, locally receive, and synchronization messages. T ⊆ S × Σ × S is the transition relation.

These controllers are obtained by first generating the set of distributed peers by projection from the choreography specification. Then, we check in sequence the system synchronizability and realizability using equivalence checking. If one of these properties is violated, we exploit the generated counterexample to augment the controllers with a new synchronization message. This process is iterated to obtain the controllers via automatic refinement until satisfying both synchronizability and realizability.

A communicating system is controlled if we can synthesize a set of controllers that are able to enforce the peers to realize the choreography specification.

Definition 10 (Controlled System): A set of peers P i = (S i , s 0 i , Σ i , T i ) obtained by projection from a conversation protocol C is controlled if there exists a set of controllers C i = (S i , s 0 i , Σ i , T i ) such that: • the controlled synchronous composition is equivalent to the controlled asynchronous composition (both compositions are defined in [START_REF] Güdemann | Counterexample Guided Synthesis of Monitors for Realizability Enforcement[END_REF]), i.e., ((P where local interactions (peers to controllers) and interactions between controllers are achieved synchronously, and remote interactions (controllers to peers) are achieved using handshake communication in the synchronous composition and via FIFO buffers (B i ) in the asynchronous composition. In that case, ≡ t also ignores local interactions from peers to controllers and synchronizations among controllers. Figure 14 shows the example introduced in Figure 11. While this choreography is not realizable, it is repairable because it does not involve any divergent choice. Non-realizability is caused by peer bs that can send store before peer cl sends pay, and this violates the message ordering as defined in the choreography. We show how controllers for peers cl and bs can solve this problem. Both controllers catch messages sent by their peers. The client controller can immediately forward the payment message to the bank peer. In contrast, the booking system controller is waiting for a message from the client controller (sync cl bs) indicating that it can proceed with the emission of the store message. This additional synchronization between both controllers enforces the peers to realize the choreography as shown in the resulting composition (Figure 14, bottom left) where we can see that store! always

V. TOOL SUPPORT AND EXPERIMENTS

A. Tool Support

In this section, we present the tool support [START_REF]VerChor Framework[END_REF] that enables the use of VerChor for a fully-automated choreography-based design approach. As presented in Figure 5, VerChor can be applied to a given choreography specification language provided that a model transformation from it to the choreography intermediate language (CIF) is defined. We have chosen to illustrate here the use of VerChor on the BPMN 2.0 standard. In that case the choreography designer can design BPMN choreographies with the Eclipse IDE using the Eclipse BPMN modeler plugin 1 . This plugin is based on an EMF meta-model that is compatible with the OMG BPMN 2.0 specification [START_REF]Business Process Model and Notation (BPMN) -Version 2.0, OMG[END_REF].

We use XML for the textual representation of the intermediate format. Accordingly, we have defined an XML schema (XSD) for it. This schema can be used to validate the (syntactic) correctness of XML intermediate format descriptions. Further, the XML schema can be used to automatically retrieve class implementations of the intermediate format concepts, together with parsers (retrieving object instances from an XML file) and printers (generating an XML file from object instances), e.g., in Java with the JAXB framework.

We have extended the Eclipse IDE, Figure 15, in order to seamlessly integrate our formal verification techniques within 1 http://www.eclipse.org/bpmn2-modeler/ the choreography design activity. This is achieved by using the Eclipse IDE external tool extension mechanism. Each tool supporting a formal activity in the choreography design can be called using the Eclipse IDE external tools menu. These tools operate on a given BPMN choreography specification, selected by the designer: 1) clean project removes all intermediate files that have been generated for the BPMN specification verification, 2) generate intermediate format generates the CIF representation of the BPMN specification (XML file), 3) generate verification models and scripts generates the LNT models and the verification scripts (written in the SVL language [START_REF] Garavel | SVL: A Scripting Language for Compositional Verification[END_REF]) from the CIF representation, 4) check synchronizability and realizability checks if the BPMN specification is synchronizable and realizable, 5) check repairability and generate controllers checks if the BPMN choreography is repairable, and, if so, generates a set of controllers.

We made the choice to let the designer decide in which order to apply the verifications that we propose. Still, one has to apply steps ( 2) and (3) first to have any of the subsequent verifications working. The model transformation from BPMN 2.0 into our intermediate format could have been defined using different techniques, e.g., using an XSLT transformation or dedicated model transformation description languages such as ATL. However, to promote modularity and reuse, we have defined it directly in Java. The EMF resource corresponding to the BPMN model within the Eclipse IDE (this is an object instance) is retrieved and analyzed to generate an object instance of the CIF Java meta-model obtained using JAXB (see above). This object instance may then easily be serialized into the CIF XML format using the JAXB-generated XML printers.

As for back-end verification techniques, we have connected our intermediate format to the CADP verification toolbox [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], used here for checking the properties presented in Section IV, with a translation library we implemented in Python. First, we use the PyXB Python library for parsing XML files written using our intermediate format, and for encoding them into a corresponding Python model, which implements classes presented in the meta-model given in Figure 8. Second, we have developed a translation from this Python model for choreographies to the LNT process algebra (Section III-C). CADP tools are convenient for verifying automatically all the properties presented in Section IV, because they enable the verification of choreographies using both model and equivalence checking. Verification of the properties is fully automated thanks to verification scripts generated by our Python translator. It is worth observing that the encoding into LNT also enables other kinds of formal analysis with CADP, such as deadlock search, simulation, or checking temporal properties written in MCL using the Evaluator model checker [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF].

An intermediate model in Python code was necessary, instead of translating directly XML to LNT, because we also use Python code for automating various tasks, such as the generation of verification scripts or the analysis of counterexample for distributed controller generation.

The successive encodings (source choreography language, CIF, LNT, and LTS models) on which we rely on in this article must preserve the semantics of the original choreography specification language. Since the final model is an LTS, this is feasible for languages such as conversation protocols or Chor, and it can be verified using trace (or strongest if necessary) equivalence [START_REF] Milner | Communication and Concurrency[END_REF]. In contrast, this is much more difficult for notations like WS-CDL or BPMN choreographies. Indeed, these notations do not come with a formal semantics. It is even worse because industrial tools often interpret differently existing standards. Business processes defined with BPMN and the resulting LTS models cannot be compared easily because the first one advocates high-level diagrammatic notation whereas LTSs give low-level flattened views of choreographies. Consequently, in order to validate semantics preservation, model transformations involved in the VerChor platform have been validated experimentally: the results obtained during our experiments were always consistent with the expected verification results. Other techniques such as co-simulation techniques or conformance testing could be considered for comparing both description levels.

B. Evaluation

Table I shows experimental results on some examples of our database, which contains about 400 choreographies, many of them are real-world examples found in the literature, e.g., [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF], [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF], [START_REF] Stengel | Analyzing Singularity Channel Contracts[END_REF], [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF], [START_REF] Basu | Deciding Choreography Realizability[END_REF], [START_REF]Business Process Model and Notation (BPMN) -Version 2.0, OMG[END_REF], [START_REF] Güdemann | Counterexample Guided Synthesis of Monitors for Realizability Enforcement[END_REF], [START_REF]Singularity Design Note 5 : Channel Contracts[END_REF], [START_REF] Wong | Verifying Business Process Compatibility[END_REF]. Experiments have been carried out on a Xeon W3550 (3.07GHz, 12GB RAM) running Linux. It is worth observing that the translation time (from the input languages to CIF and from CIF to LNT) is negligible even for the largest examples. For each experiment, the table gives the specification language used for describing the input choreography and the size of the choreography in terms of number of peers (P), interactions (Inter.), and selection operators (Sel.). Then, we give the size of the corresponding LTS and the size of the largest intermediate state space for generating the asynchronous version of the distributed system (number of states and transitions). In order to reduce the generation time for compiling the LTS for the asynchronous system, we use recent compositional aggregation techniques [START_REF] Crouzen | Smart Reduction[END_REF], which heuristically determine the best sequence of successive composition/reduction for minimizing the intermediate state spaces size. The times for generating all LTSs (C), i.e., synchronous and asynchronous versions of the distributed system, verifying synchronizability (S c ) and realizability (R), and checking whether the choreography is repairable or not (R p ), are given. We have not checked conformance directly when making these experiments because we followed a top-down design approach and used a choreography as input in our experiments. However, the equivalence checking that is central to conformance is used in realizability checking when it comes to compare the choreography model and the product of the peers that have been generated by projection. Finally, the last column details the results for checking synchronizability, realizability, and repairability. Repairability does not need to be checked when the choreography is both synchronizable and realizable.

First of all, when a choreography specification (written in CIF or BPMN for instance) involves parallel operators (AllSelect, SubSetSelect), they are expanded in all the possible interleaved behaviors when the corresponding LTS is generated. This can result in large LTSs (see example 7). We note that the overall time for generating LTSs for choreography and both distributed systems (synchronous and asynchronous) as well as for verifying properties S c and R is reasonable for medium-size choreographies, see for instance examples 2, 3, 4, 6 in Table I. In any case, even when it takes some time, this is not an issue since these checks are achieved at design-time. In most cases it is more costly to check realizable examples because it deserves an exhaustive exploration of all cases, whereas when the choreography is not realizable, the analysis stops as soon as a violation is found, which can appear early during equivalence computation. We observe that the main cause of explosion, particularly in the asynchronous distributed system and its corresponding computation time, is an increase in the parallelism degree that can arise from (i) the number of peers (e.g., 15 peers in example 7) or (ii) the number of (interactions in) parallel branches.

In Figure 16, the top part shows that for each topology (choreography with the same structure) the augmentation of peer number leads to an exponential grow in terms of state space size and generation time. Note that we give the largest intermediate number of transitions, which is always larger than the number of states, and represent it using logarithmic coordinates. Similarly, the bottom part of Figure 16 shows that for each case (choreography with the same number of peers and interactions) if we augment the number of parallel branches, size and time gradually increase but less quickly than for the number of peers.

If the choreography is not realizable but repairable, we generate local controllers which synchronize together in order to force the distributed system to respect the order of messages as specified in the global contract. For instance, example 5 presents several ordering issues if peers are generated using projection. In that case, our process requires 6 iterations to construct these controllers, meaning that 6 additional synchronization messages are necessary to make the system realizable. It takes about 20 minutes for this example to successively check synchronizability/realizability using equivalence checking and exploit the resulting counterexample to refine controllers, until completion of the process.

VI. RELATED WORK

The advent of choreography description languages for designing interaction-based systems has raised many issues, such as analysis and verification (projection, realizability, conformance, repair), discovery, code generation, and testing. In this state-of-the-art overview, we will focus on existing works for analyzing and verifying choreography specifications.

Realizability by construction. The results presented in [START_REF] Qiu | Towards the Theoretical Foundation of Choreography[END_REF], [START_REF] Carbone | Structured Communication-Centred Programming for Web Services[END_REF], [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF] formalize well-formedness rules to enforce the specification to be realizable. More precisely, in [START_REF] Carbone | Structured Communication-Centred Programming for Web Services[END_REF], [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], Carbone et al. identify three principles for global description under which they define a sound and complete end-point projection that is the generation of distributed processes from the choreography. Qiu et al. [START_REF] Qiu | Towards the Theoretical Foundation of Choreography[END_REF] propose a choreography language with new constructs (named dominated choice and dominated loop) ensuring realizability by design. During the projection of these new operators, communications are added to make peers respect the choreography specification. These solutions make the system design more complicated by obliging the designer to specify extra-constraints in the choreography, e.g., by associating dominant roles to certain peers. In [START_REF] Decker | Local Enforceability in Interaction Petri Nets[END_REF], Decker and Weske propose a Petri Net-based formalism to specify choreographies. They also define realizability and local enforceability and propose algorithms to check them. However, they consider synchronous communication, and have not investigated mappings from higher-level modeling languages (e.g., UML collaboration diagrams or BPMN).

Asynchronous communication. Several works focused on the realizability problem assuming asynchronous communication. Fu et al. [START_REF] Fu | Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services[END_REF] proposed three sufficient conditions (lossless join, synchronous compatible, autonomous) that guarantee a realizable conversation protocol. More recently, Basu and Bultan proposed to check choreography conformance and realizability verifying the synchronizability property [START_REF] Basu | Deciding Choreography Realizability[END_REF]. Synchronizability compares both the synchronous version of the system with the asynchronous one, and relies on existing finite state verification techniques. [START_REF]Decidability Results for Choreography Realization[END_REF] studies several notions of realizability and investigates decidability results for choreographies involving services interacting via buffers, which do not assume that messages arrive in the same order in which they have been sent. In [START_REF] Bravetti | Contract Compliance and Choreography Conformance in the Presence of Message Queues[END_REF], the authors tackle the choreography conformance issue from a theoretical point of view, and propose notions of contract refinement and choreography conformance for services that communicate through message queues. [START_REF] Gössler | Realizability of Choreographies for Services Interacting Asynchronously[END_REF] proposes techniques to check whether a set of peers interacting asynchronously can realize a choreography with finite buffers, and if so, for what buffer sizes.

Bultan and Fu [START_REF] Bultan | Specification of Realizable Service Conversations using Collaboration Diagrams[END_REF] defined sufficient conditions to check the realizability of choreographies specified with UML collaboration diagrams (CDs). In [START_REF] Salaün | Realizability of Choreographies Using Process Algebra Encodings[END_REF], Salaün and Bultan refine and extend this work with techniques to enforce realizability by adding additional synchronization messages among peers, and a tool-supported approach to automatically check the realizability of CDs for bounded asynchronous communication. The realizability problem for Message Sequence Charts (MSCs) has also been studied (e.g., [START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF], [START_REF] Alur | Inference of Message Sequence Charts[END_REF], [START_REF] Uchitel | Incremental Elaboration of Scenario-based Specifications and Behavior Models using Implied Scenarios[END_REF]). [START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF] for instance presents some decidability results on bounded MSC graphs, which are graphs obtained from MSCs using bounded buffers. These notations are limited because branching and cyclic behaviors are not well supported by CDs and MSCs (e.g., no choice operator and repetition limited to a message at a time in CDs). [START_REF] Balbiani | Algorithms and Complexity of Automata Synthesis by Asynchronous Orchestration With Applications to Web Services Composition[END_REF] analyzes the computational complexity of the composition problem, which aims at generating a composition of services interacting via bounded buffers that satisfies a given goal. Our synthesis techniques are quite different because peers are obtained via projection from a choreography specification and controllers non-intrusively monitor those peers to make them respect the choreography ordering constraints.

Realizability enforcement. Lanese et al. [START_REF] Lanese | Bridging the Gap between Interaction-and Process-Oriented Choreographies[END_REF], [START_REF] Lanese | Amending Choreographies[END_REF] present a transformation procedure for amending choreographies that does not respect common syntactic conditions for projection correctness. Their approach adds interactions on private operations that make the choreography respect the desired conditions, while preserving the observational semantics. To do so, they define three connectedness properties (sequence, choice, repeated operation) and show how to enforce each of them, preserving the set of weak traces of the choreography. The main difference compared to our work is that they change the peers' behaviors whereas our approach is non-intrusive and ordering issues are corrected via external controllers.

In [START_REF] Autili | A Model-Based Synthesis Process for Choreography Realizability Enforcement[END_REF], the authors present a model-based synthesis process for automatically enforcing choreography realizability. This approach relies on several model transformations for synthesizing the coordination delegates. The provided tool supports the generation of Java code for coordinating, e.g., SOAP-based Web services. This work assumes that actions inside the peers are controllable, which allows to implement an election process in case of divergent choices and pick a winner among the possible senders. Controllability is possible only if developers have preemptively anticipated it. Since this is not always the case, we prefer in our approach to assume that peer actions cannot be controlled. Another work [START_REF] Güdemann | Counterexample Guided Synthesis of Monitors for Realizability Enforcement[END_REF] proposes a similar approach for generating distributed controllers enforcing realizability for asynchronously communicating peers. This work tackles this issue from a formal point of view and introduces a sufficient condition for detecting faulty choreographies, that is, choreographies for which realizability cannot be enforced.

BPMN verification. Decker and Weske present, in [START_REF] Decker | Interaction-centric Modeling of Process Choreographies[END_REF], an extension of BPMN 1.0 (iBPMN) in the direction of interaction modeling. They also propose a formal semantics for iBPMN in terms of interaction Petri nets. Interaction Petri nets are an extension to classical place/transition nets presented in [START_REF] Decker | Interaction-centric Modeling of Process Choreographies[END_REF] for formalizing choreography semantics through labeling of transitions and thus simplifying the reuse of existing tools for conversation-based languages. At the end of this paper, the authors mention realizability as a novel challenge, but do not give any solution for this issue. Lohmann and Wolf [START_REF] Lohmann | Realizability Is Controllability[END_REF] show how realizability can be verified by using existing techniques for the controllability problem, which checks whether a service has compatible partner processes. They mention several models that can be used for modeling choreographies, such as iBPMN, but present their results on multi-peer automata called choreography automata. Their approach works for peers interacting via arbitrary bounded buffers and only consider finite conversations. In [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF], the authors have focused on the translation of a subset of BPMN into process algebra for automating the formal analysis of choreographies using model and equivalence checking.

All this related work focuses on specific languages and verification problems (mainly realizability). Our goal is to provide a generic framework, which considers several choreography description languages as input and provides verification primitives for checking some crucial properties in choreographybased design of distributed software, in a fully automated way.

Preliminary versions of this work have been published in [START_REF] Poizat | Checking the Realizability of BPMN 2.0 Choreographies[END_REF], [START_REF] Güdemann | VerChor: A Framework for Verifying Choreographies[END_REF] and are extended here as follows: we present the Choreography Intermediate Format (Section III), which allows external developers to plug their own languages and tools as front-end and back-end, respectively; we describe in detail the properties that can be analyzed using our framework (Section IV); we present the different components of our verification platform that automates all the checks presented in this article (Section V); we present an extended discussion comparing our approach with related work (Section VI) ; we introduce a new encoding into LNT, which takes unbalanced split/join operators into account (Section III-C, Appendix).

VII. CONCLUDING REMARKS

Designing software applications consisting of communicating entities has been greatly simplified with the advent of choreography description languages. Yet, these languages and development processes raise new issues that deserve to be worked out in order to become mainstream in this area. One central problem concerns the correspondence between the global choreography specification and the distributed version of the system composed of a set of peers interacting asynchronously. Beyond providing automated techniques for verifying model compliance, there is also a need for techniques that enforce peers to respect the requirements specified in the choreography. There has been quite some works on these issues, but most results are hardly reusable because they focus on specific notations and do not provide available tool support.

In this article, we have first proposed an intermediate format for describing choreographies. Several interaction-based notations already existing for choreographies (e.g., conversation protocols or BPMN) have been connected to this intermediate format. We have also presented a verification library, which presents a set of key properties that choreographies must respect for ensuring correctness of the system under development. We show how these properties can be automatically verified in practice using model and equivalence checking techniques, via an encoding into process algebra. We had a particular focus on asynchronous communication semantics, that is, peers involved in the distributed version of the system exchange messages via FIFO buffers. Our approach is fully supported by freely available tools that we have implemented [START_REF]VerChor Framework[END_REF]. This work can be seen as a first step for joining forces and mutual effort for developing verification techniques and tools for formally analyzing choreographies.

Fig. 2 .

 2 Fig. 2. Top-Down Development Process

Fig. 3 .

 3 Fig. 3. Example of Conversation Protocol

Fig. 4 .

 4 Fig. 4. Top-Down Development Process (Refined) in VerChor

Fig. 6 .

 6 Fig. 6. BPMN 2.0 Notation Primer -Choreography Tasks

Fig. 7 .

 7 Fig. 7. BPMN 2.0 Notation Primer -Control Flow and Gateways

Fig. 8 .

 8 Fig. 8. CIF Meta-Model

Fig. 9 .

 9 Fig.9. CIF Model for the Choreography in Fig.7, left (with an added initial state and message contents abstracted)

Fig. 11 .Fig. 12 .

 1112 Fig. 11. Example of a Synchronizable but Non-Realizable Choreography

Fig. 14 .

 14 Fig. 14. Example of Repairable Choreographies and Generated Controllers

Fig. 16 .

 16 Fig. 16. Experimental Measures: Increased Number of Peers (top) and Increased Number of Branches (bottom)