This paper presents a methodology for modelling and verification of high-assurance distributed protocols. In the paper we describe two main technical contributions needed for the development method: communication modelling patterns and a refinement strategy. The applicability of the proposed method is demonstrated by developing a new distributed resource allocation protocol. We also discuss the necessity of integrating other tools such as stochastic model checkers for enabling verification of wider range of protocol properties.

I. INTRODUCTION

Developing distributed systems is an intricate process, which requires rigorous methods due to concurrent nature of the distributed systems. Formal methods -mathematical model driven techniques -provide a systematic approach for developing complex systems. They offer an approach to specify systems precisely via mathematically defined syntax and semantics as well as formally validate them by using semi-automatic or automatic verification tools. In particular formal notations such as Event-B [START_REF]The B-book: Assigning Programs to Meanings[END_REF] are thought to be well suited for development and verification of various protocols. The stepwise and proof driven development provided by such methods is attractive to developers and can significantly reduce the modelling and verification effort.

The overall aim of our research is to reduce complexity of applying formal methods for developing high-assurance distributed protocols. The proposed development methodology is based on a stepwise refinement and mathematical proof -two techniques which we believe can reduce modelling effort and provide a higher system assurance degree. Nonetheless, the effectiveness of these techniques significantly correlates with developers experience and an adequate tool support. Thus, to overcome these issues our research focuses on developing a method for automatically constructing model refinement chains from high-level distributed protocol specifications and integrating a better tool support for animation and verification of the model. In this paper we discuss the current main elements developed to facilitate this approach: communication modelling patterns and a generic refinement strategy. The paper also presents how these patterns can be applied by developing a new distributed resource allocation protocol. We also discuss the endured verification challenges and results from using additional verification techniques.

Related work. There have been several studies which aimed to develop a general way of modelling and verification of distributed protocols. But, not many methods were based on the refinement, we discuss ones that utilized the step wise development. In Iliasov et al. [START_REF] Iliasov | Formal derivation of a distributed program in Event-B[END_REF] authors presented a modelling technique based to bridge the gap between Event-B formal model and the software protocol implementation. Their approach proposes to introduce an environment into the model and to further decompose communication events to separately model sending and receiving a message. The paper [START_REF] Siala | An Event-B Development Process for the Distributed BIP Framework[END_REF] proposed an integrated method based on Event-B and BIP [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF] modelling languages for development of distributed systems. Their approach helps for a developer to interactively refine an abstract centralised system model with an assistance of domain languages and available plug-ins, and generate BIP model code. In the work by Hawblitzel et al. [START_REF] Hawblitzel | IronFleet: proving practical distributed systems correct[END_REF] authors developed a methodology to model and verify a non-trivial distributed systems (including implementations). Their method relies on proving refinement relation between different layers (e.g. design level and implementation) with a well known techniques such as TLA+ and state-of-the-art SMT solvers. A refinement based method for developing distributed protocols Paulius Stankaitis * , Alexei Iliasov * , Yamine Aït-Ameur † , Tsutomu Kobayashi ‡ , Fuyuki Ishikawa ‡ and Alexander Romanovsky *

In Section II we introduce the problem of a distributed resource allocation and propose a two stage distributed protocol for solving it. The following section describes our proposed development methodology in more detail including the background information on the Event-B specification language, ProB model checker [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF] and PRISM model checker [START_REF] Hinton | Prism: A tool for automatic verification of probabilistic systems[END_REF]. Section IV describes developed modelling patterns and refinement strategy to facilitate our development approach. In Section V we discuss how modelling patterns, refinement strategy and external tools were used to prove the distributed resource allocation protocol. The last section contains a conclusion and overviews the future work.

II. OVERVIEW OF THE PROTOCOL

The objective of the protocol is to enable safe distributed atomic reservation of a collection of resources. For instance any two distinct agents A 0 and A 1 may require any resource collections r 0 and r 1 , where r 0 , r 1 ⊆ R. The protocol must guarantee that each agent gets all or nothing -partial request satisfaction is not permitted -and ensure that every agent request will be eventually satisfied as long as certain degenerated situations are avoided. A resource itself has an attributed memory, where requests can be stored together with a read pointer rp(r k ), and a promise pointer pp(r k ) -the largest promised index in the r k request pool. In our system setting a resource is only allowed to exchange messages with agents and agents only with resources. Even though, we do not consider degenerate or malicious situations (messages cannot be altered or lost) requests can arrive at resources in any order. Permitting situations where requests can arrive in any order can cause situations where different requests are blocking each other and cause the system to deadlock.

In order to prevent a system deadlock and ensure progress we offer a two stage solution. The principal mechanism of solution we offer is distributed lane -a virtual data structure, which is only present at a conceptual level. To be more specific, a distributed lane is a uniform (single index) horizontal slice through request pools where a request pool is a resources request memory (vertical structure). A unique distributed lane can only belong to a single agent. An example of virtual distributed lane data structure is shown in Fig. 1. To lock (form a lane) resources, an agent has to go through a number of steps. The agents distributed protocol side can be split into two stages.

Stage 1

In this stage an agent attempts to negotiate a distributed lane by first sending request messages to resources of interest (objective). Once a resource receives a request message it replies with the current promised pointer value. An agent must wait to receive all reply messages before the decision is made. If all received promised pointer indexes are the same, an agent will create a distributed lane by sending write message. Otherwise, an agent will attempt to negotiate a distributed lane again by sending a special request message, which contains a desired value -lines 7-10 in Algorithm 1. The negotiation process continues until a lane is negotiated. Because of a probabilistic renegotiation nature we demonstrate in Section V that an agent will eventually negotiate a distributed lane. release(A n ) → r k 27: end Stage 2 This stage begins when an agent negotiates its distributed lane and was mainly introduced when subtle unsafe scenarios were discovered by animating the initial model. After sending write messages, an agent must wait until it receives all pready messages. Once all messages have been received, an agent will try to lock resources by sending lock messages. If between sending pready and receiving lock messages a resource has not received other lock sooner, that resource will send a response(ready) message. Once an agent receives all response messages it will make another decision. If all an agent received all response(ready) messages, that agent can proceed an consume resources. If at least one of the messages was response(ready) that agent will send release messages to resources, which sent response(ready) and will repeat the process by again waiting for pready all messages.

ALGORITHM 1 Agent communication algorithm

The resource in this protocol only replies to the agents messages, therefore its communication can be described with switch-case pseudocode (see Algorithm 2). Updating resource read pointers is perhaps the most interesting element in this algorithm part. In contrary to the promised pointer, the read pointer rpt(r) is always set to the minimum value of the request pool. This is necessary as an agent might negotiate a distributed lane with lower index than others, but its write messages are delayed (or even lost) so the protocol would halt. Allowing agents with higher distributed lane indexes, but sooner write message arriving to consume resources introduces fault-tolerance into the protocol. Important to note that a resource removes distributed lanes once a release message has been received so the read pointer value would change.

ALGORITHM 2 Resource communication algorithm

1: switch received message do 2: case request(A n ) 3: reply(ppt k , r k ) → A n 4: ppt(r k ) ′ = ppt(r k ) + 1 5: case srequest(A n , n) 6: reply(max(ppt k , n) + 1, r k ) → A n 7: ppt(r k ) ′ = max(ppt k , n) + 1 8: case write(A n , n) 9: if free(r k ) ∧ n = min(req pool(r k )) then 10: pready(r k ) → A n 11: rpt(r k ) ′ = n 12: case lock(A n ) 13: if free(r k ) then 14: response(ready, r k ) → A n 15: lock(r k , A n ) 16: else response(deny, r k ) → A n 17: case release(A n ) 18: req pool(r k ) = req pool(r k ) -req(A n ) 19: if A m • dist lane(A m ) = min(req pool(r k )) then 20: unlock(r k ) 21: pready(r k ) → A m 22: rpt(r k ) ′ = min(req pool(r k ))

III. INTEGRATED METHODOLOGY

This section overviews the proposed stepwise refinement and proof based development methodology of distributed protocols. We also discuss how this methodology was used to model and verify the distributed resource allocation protocol. Indeed, the stepwise refinement modelling approach would allow to manage a high distributed protocol modelling complexity by model abstraction and decomposition. The stepwise model development approach can also significantly reduce the mathematical proving effort which we regard as essential for ensuring safety of high-assurance systems. In our research we work towards an automatic refinement chain generation from high-level distributed protocol specification. In this paper we present key elements of the method: generic communication modelling patterns and the refinement strategy for modelling various distributed protocols. Our methodology also proposes to integrate other available tools for animating and model checking the distributed protocol model.

The cornerstone of the proposed methodology is a well known modelling framework -Event-B/Rodin. The Event-B method is a proof-based modelling language which facilitates a gradual system design through the stepwise refinement. The developer incrementally adds more detail in the proceeding refinement steps by including new information or proving properties. Properties are manually inserted as invariants and must be preserved by all state transitions (invariant preservation rule). The method we propose would automatically generate a distributed protocol model refinement chain from a high-level specification notation. For that we developed Event-B communication modelling patterns and a refinement strategy presented in the following section with an example. The generated Event-B model would then have multiple uses due to a number of useful plug-ins developed for the Rodin Platform including ProB animator and model checker.

In developing the distributed resource allocation protocol we extensively used the ProB model checker and its animator for an early development stage validation. The ProB model checker together with built-in constraint solver enables an iterative model exploration for possible correctness violations or deadlocks. These tools allowed to discover subtle deadlock scenarios and hence modify protocol specifications before mathematically proving the model. Once the model developer has sufficient confidence about the model correctness, it must be proved by defining safety invariants and proving them. The paper contains one of the correctness proofs completed for distributed resource allocation protocol. However, not all properties are easy to define, in particular, for a distributed protocol verification.

In our example the distributed resource allocation protocol had a stochastic nature. Probabilistic or liveness properties are hard to formalise and prove in the Event-B method. Therefore, it was decided to prove progress of the protocol by redeveloping part of the model in the PRISM model checker. The PRISM model checker is a well established symbolic model checking tool, which allows to model and analyse probabilistic systems. Several types of stochastic input models are supported but predominately discrete-time Markov chains (DTMC), continuous-time Markov chains (CTMC) and Markov decision processes (DTMC) are used. The tool has also functionality for result visualisation which was used to observe protocols performance as the number of agents and resources were increased. In general, we believe that our methodology should include probabilistic reasoning, as some properties cannot be easily formalised by invariants.

Other uses of the generated distributed protocol Event-B model are still being discussed but a software code generation or documentation are of interest. In the following section, we present Event-B communication modelling patterns and the refinement strategy. Then we demonstrate few examples how these patterns were used for developing distributed resource allocation protocol.

IV. MODELLING PATTERNS AND REFINEMENT PLAN

This section mainly describes the developed modelling patterns and their application for modelling the resource allocation protocol. But first, we define a modelling strategy, or in other words refinement plan, which generally could be used as a modelling strategy for any distributed protocol.

A. Refinement strategy

The model development approach we propose is a rather standard and starts with the abstract model which formally specifies the objective of the protocol. In fact distributed aspects of the system are ignored at this model level and the abstract model considers a centralised configuration. The abstract resource allocation protocol model was captured by two machines -m 0 and m 1. The former model essentially summarises the high-level objective of the protocol which is agents safely capturing and releasing collection of resources (objectives). This abstract model contains individual events for capturing and releasing objectives. The next refinement step introduces resources into the model and decomposes two previously introduced events according to the loop pattern defined in the Subsection IV-C.

The following group of refinement steps introduce more details about the model by primarily modelling communication aspects. For protocol modelling we propose to use backward unfolding style where the next refinement step introduces preceding protocol step. The abstract models were firstly refined with stage 2 segment of the protocol. In the refinement, m 2, we introduced lock, response and release messages and associated events into the model. In this step we also demonstrated that the protocol stage 2 ensures safe distributed resource reservation by proving an invariant. The invariant states that no two agents will be both at resource consuming stage if both requested intersecting collections of resources. The following refinement, m 3, is the bridge between protocol stages stage 1 and stage 2 and introduces two new messages write and pready into the model. In the final refinement step -m 4 -we model stage 1 of the distributed protocol which is responsible for creating distributed lanes. Remaining messages request, reply, srequest and associated events are introduced together with the distributed lane data structure. In this refinement we prove that distributed lanes are correctly formed -the proof is explained in Section V.

The refinement plan could be further extended if distributed protocol developer considers its software implementation. In Iliasov et al. [START_REF] Iliasov | Formal derivation of a distributed program in Event-B[END_REF] -authors presented a modelling technique to bridge the gap between Event-B formal model and the software protocol implementation. Their approach proposes to introduce an environment into the model and to further decompose communication events to separately model sending and receiving a message. In the following subsections we present how this refinement strategy is modelled with communication patterns and few examples from the resource allocation protocol model.

B. Message context patterns

The Event-B model is made of two key componentsmachines and contexts which respectively describe dynamic and static parts of the system. The context contains modeller declared constants and associated axioms which can be made visible in machines. In our generic modelling approach we can distinguish two groups of contexts. The first group of contexts (context abstract) axiomatically define all objects present in the model -carrier set OBJ. For example, objects in the resource allocation protocol are agents and resources, in other protocols they are often called, for example, processes or cohorts. An object is often required to go through a number of protocol steps to achieve its goal. In the context abstract we also define an enumerated set OBJ STATUS which would define all program counter values an object can have. The second group of contexts are communication related and are used to define various messages types. Each message type (e.g. request) in the protocol is defined in a separate context file. In fact latter contexts can be generalised as a pattern and instantiated for the specific message type. To define the context pattern let's first define a generic message set -MSG. In this context we introduce three constant functions for: message source, message destination and (optionally) a message value. Depending on the message type, the source of the message in the distributed resource allocation protocol can be both an agent and a resource. Therefore, in our message pattern we can abstract all communicating objects including agents and resources to a general source -SRC.

Likewise for the message destination constant function form we give a general destination type -DST. In the distributed protocol can messages carry a value (e.g. reply contains promised pointer) so the last generic type we define is VAL and associated constant function (msgv) necessary for extracting value from the message. All constant message functions are surjective (։) functions meaning they are total in domain and range. Lastly, each message type contexts contains an axiom which states that there always exists a suitable message between any agent and resource.

∀s, d, v • s ∈ SRC ∧ d ∈ DST ∧ v ∈ VAL ⇒ (∃m • msgs(m) = s ∧ msgd(m) = d ∧ msgv(m) = v)

C. Communication event patterns

In order to generalise a distributed protocol modelling process we derived communication event and variable patterns which are presented below. The first step in introducing a new message into a machine is extending that machine with a message associated context (e.g. context request). The following step is creating a three letter variable msg of type inv 1 to represent that messages channel. However, as messages are added and removed from the channel msg we require a second generic local variable of type inv 2 to locally store what messages have been sent. inv 1 msg ⊆ MSG global message channel inv 2 msgo ∈ OBJ → P(MSG) sent msg messages After introducing message variables, one needs to create events in the model which send that message. From modelling various distributed protocols we identified two message sending event patterns. The most widely encountered communication situation is responding to received message -reply event type. We define a reply event pattern (object reply MSG) where the main principle of this event is to take a message from one channel and create a response message in the different channel. In this pattern we use constant message functions defined in the context files to select the source and destination of the new message. The reply event pattern has two event parameters -messages ms 1 and ms 2 where messages types must be defined according to the protocol. The first guard (grd 1 ) of this event states that a message ms 1 must have been sent, or in other words, already an element of that channel. Guards grd 1..4 select an appropriate reply message ms 2 by using constant functions defined in the message contexts. They state that a new messages destination is the source of received message and that the source of the new message is a destination of received message. The actions of this event create a new message by adding it to the channel variable, remove responded message and save sent receipt locally. Additional guards would be added according to the distributed protocol specifications. Another type of message sending event we can define is an initiating message sending (object initiating MSG). The principle of this event is create a new message once the program counter of an object changes to the specific status. This event pattern only has one event parameter ms 1 message which must be not sent yet (grd 1 ). The second guard states that the program counter (pctn) of the source message must be at some STATUS defined in the abstract context. The actions of the event add a new message to the message channel msg 1 and save message receipt locally.

object

D. Loop modelling pattern

In a distributed protocol an object is often required to send multiple messages or repeat the process numerous times. For such scenarios we created a two event loop pattern which would often be combined with message sending patterns to model burst message sending. The first event in this pattern is the loop body event (object STATUS b) and body events have b name extensions. The STATUS and object in the event name would be also modified to correspond to a specific event. The loop is triggered, firstly, if agents program counter status is at certain value. The remaining guards are used to selected an appropriate message or further constrain the event. In case of the sending multiple reply messages, guard select guards, would be instantiated with predicates grd 1..4 from object reply MSG pattern. Even though, the concrete (final) refinement step contained 23 events and a similar number of variables, only 3 events did not fit any pattern or were special cases.

A. Abstract distributed resource allocation protocol model

The distributed resource allocation protocol development approach follows a standard Event-B modelling approach where the abstract model summarises the protocol with a centralised view of the system. In short the objective of the distributed protocol is to enable safe resource locking which we abstract as agents capturing and releasing collections of resources -objectives. The abstract model was split in two machines where the first machine simply models agents capturing and releasing objectives. In the extension of the initial abstract model we introduced resources into the model and decomposing two previously introduced events agent capture and agent release. In this refinement step agents attempt to capture multiple resources in order to fulfil an objective where objective is a collection of resources. We started modelling by introducing new variables for storing captured resources capt and storing agents objective objt. Resources which belong to the objective can be extracted by applying an objective to the constant function objr which was defined in the abstract context. For the iterative capturing and releasing events we applied the loop pattern as depicted below in the model excerpt. The loop body event agent consume b is enabled if agents program counter is at the CONSUME state. Furthermore, the resource must be within agent's objective (grd 2 ) and not captured by any agent (grd 3 ). The action of this event (act) simply stores a new resource rs to that agent in the capt variable. The loop completion event agent consume c would be triggered as soon as the objective has been fulfilled and program counter would be updated to new state - RELEASE. Similarly in this refinement we transform agent release event according to the pattern presented. To show correctness of the extended model we prove an invariant, which states that no agents can have the same resource captured still this system is not deadlock free.

B. Protocol communication modelling with patterns

The abstract model is refined according to the proposed development method by introducing communication aspects of the protocol. The method also suggest to use a backward protocol unfolding modelling style. Therefore, the abstract model was refined by introducing stage 2 of the protocol first which is responsible for locking resources once a distributed lane has been negotiated. The following paragraphs explain how communication pattern were used to add lock message into the model.

To begin with, the machine m 2 is extended with the message type context context message lock which defines constant functions of the message. Then, we create variables lck (inv 1 ) and lcke (inv 2 ) which will represent a communication message channel and a memory where sent lock message receipts are locally stored. In this protocol it was more convenient to locally save where message have been sent rather than messages itself.

inv 1 lck ⊆ LCK lock message channel inv 2 lcke ∈ AGT → P(RES) locally stored messages
To model lock message sending we apply a loop together with initiating message modelling patterns to create two new events agent lock b and agent lock c. In the protocol lock message is of the reply type, however, since preceding protocol messages are modelled in the next refinement lock message is an initiating message at this stage but in the next refinement is modified to a reply type. The actions of the loop body event send a new lck message firstly if the program counter of an agent is at LOCK phase. Secondly, the new message must not have been sent already grd 1,2 and destination of the message (resoure) is within agent's objective grd 3 . The loop completion event, agent lock c, detects the end of the loop and updates the program counter. For the lock message sending event -an agent must detect when all messages have been sent or in other words the objective has been fulfilled (grd 1 ). The action of this event simply updates the program counter to the next state. Formally specifying a system is not sufficient to guarantee a high safety and correctness confidence degree. In the proposed methodology we regard mathematical proofs as essential for ensuring high system assurance. Therefore, our development method relies on adding and proving properties (invariants) in the Event-B model. The literature review and our experience in developing various distributed protocols however show that formalising sufficient properties in many cases might be too challenging, thus, a wider validation tool support is crucial.

Three different verification techniques were used in developing the resource allocation protocol. From the beginning it was decided to use ProB model checker, which is available as a Rodin Platform plug-in, to validate early protocol designs before formalising and proving properties. To use ProB model checker we had to develop additional message contexts, since ProB built-in constraint solver could not compute bounded sets according to the defined axioms. On the other hand, ProB tool accepts Event-B model as an input, so it was not necessary to manually translate the model. In result, the model checker helped to discover subtle protocol deadlock scenarios which could be replayed on the built-in model animator. The model checker allowed to discover and significantly modify the protocol in early design stages without formalising and proving complicated properties. The state explosion was still a big issue even for checking protocol with few agents and resources would take several hours. The following subsections discuss one of the main completed proofs and the use of probabilistic model checker tool for proving protocol stage 1 termination.

A. Correctness of forming distributed lanes

In order to ensure a safe and deadlock free distributed resource reservation we developed a solution based on notion of distributed lane. In the final model refinement step, we had to prove that the system is deadlock free. To prove that distributed system never deadlocks one could write an invariant which asks to prove that there is always at least one event enabled. However, this results in a very complicated proof so instead we reformulated the problem into a simpler one but for that the final model had to be extended with additional only proof related variables.

The cross blocking deadlock occurs when request messages of multiple agents which are interested in common resources are delayed. Indeed, this scenario is not possible for a simple non-distributed queue model since unique request has only a single slot in the queue. By unifying agents requests indexes over distributed resources, distributed lane solution essentially creates a virtual localised queues. In other words, agents which requested common resources and negotiated a distributed lane, can be virtually collapsed into a single non-compact queue like data structure. Thus, one only needs to prove that distributed lanes are correctly formed.

inv pro ∀r, n 1 , n 2 • r ∈ R ∧ n 1 , n 2 ∈ dom(his wr (r)) ∧ ∧ n 1 < n 2 ⇒ his wr (r)(n1) < his wr (r)(n2)
Due to limited space we only state that a distributed lane will be correctly formed if resource always replies with unique value ppt(r k ) value. For the proof we created a new history variable which stores chronological values of the promise pointer. Every time a promise pointer is updated in the model the history variable stores that value and increments its write value. The invariant now can be expressed (inv pro) on the history variable which states that for any resource the recorded promised pointer values increases as history variable write pointer increases. In the model two proofs obligations (ignoring well-defined verification conditions) were generated and proved interactively.

B. Argument for renegotiation termination

The progress of the protocol relies on agents ability to negotiate a distribute lane. As negotiating a distributed lane is a probabilistic process in our protocol we need to demonstrate that a desired state will be eventually reached. The probabilistic reasoning in Event-B is extremely complicated and therefore the decision was made to demonstrate negotiation termination outside the Rodin platform. For that purpose we use a well-known symbolic probabilistic model checker -PRISM. In PRISM modelling framework the model is constructed of individual modules which contain local variables and commands. In generic model we used the functionality of modules to captures resources and agents with an individual module. The modularisation allowed us to capture agents concurrency and model extreme scenarios where some agents could be much faster in sending messages than others.

To model the distributed lane renegotiation we developed a generic stage 1 phase model which would be instantiated to model specific scenarios -defined by a number of agents and resources, and also what resources agent would like to capture. The generic model itself could be partitioned into three major parts: global variable declaration, resource modules and agent modules. The two types of global variables in generic model are both associated with agents. One variable is used to store an promised pointer index the agent receives from the resource as well as to store a special request value which is sent if distributed lane is not negotiated. The second variable, agents state variable, was introduced to disable an agent once a distributed lane was negotiated and in turn affect the transition probabilities. Each resource has an attributed resource module which contains local variable and a command. The local variable we need for resource modules is the promised pointer variable (ppt). The module also only requires a single command to represent request and reply message exchanges. Lastly, each agent also has an associated agent module which models part of the agents algorithm, where all reply messages have been received and now a decisions must be made whether to renegotiate or create a distributed lane. Having designed the generic model we developed a simple program which would create random instantiated PRISM models and simulate them until either all distributed lanes were negotiated or a time-out was reached. The experiment was repeated for a number of scenarios and results were plotted for analysis. A number of steps taken to terminate was plotted against the number of resources and agents in that scenario.

VII. CONCLUSIONS AND FUTURE WORK

In this work we described a refinement and proof based methodology for developing high assurance distributed protocols. To facilitate the method we rely on a firmly established formal modelling framework which provides a refinement based development and a number of useful tools. Communication modelling patterns and a generic refinement strategy presented in this paper are essential towards our main research objective of automatically generating refinement chains from high-level protocol descriptions. These technical contributions were mainly defined by developing a variety of distributed protocols including the distributed resource allocation protocol presented here.

In the paper we also discuss the verification challenges of the distributed protocol. Available plug-ins, particularly, the ProB model checker and its Rodin animation plug-in was extremely useful in discovering subtle deadlock scenarios. Still, due to complex protocol behavior a state-space problem was clear as a single exhaustive model checking run would take hours (even for small scenarios). Still, an alternative option to complete proofs at early development phase was not an appealing choice. As some of early deadlock scenarios discovered were intricate and unlikely captured by an invariant or else proving strong invariant would have been even more time consuming. Demonstrating the termination of the distributed lane negotiation was also decided to be completed outside the Event-B environment as existing probability theory support such as [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF] would likely have not been sufficient. Even the discussed proof was not completed systematically and it was necessary to further abstract the problem and add additional variables into the model. The main focus of the future work is development of a high-level protocol specification language which would be translated into a Event-B refinement chain.

Fig. 1 :

 1 Fig.1: An example virtual distributed lane data structure with 5 agents and 4 resources. Each dl n only belongs to a single agent. Multiple distributed lanes can have the same index, but they cannot overlap (e.g. dl 1 and dl 2 ).

20 :

 20 forall r k ∈ received response(responses[A n ] ⊳ready) 13 24: else consume resources 25: while sent releases[A n ] = objective[A n ] do 26:

STATUS 1 ,

 1 STATUS 2 . . . STATUSn possible object status AXIOMS partition(OBJ STATUS, {STATUS 1 }, . . . {STATUSn})

  ∈ MSG ։ SRC message source axm2 msgd ∈ MSG ։ DST message destination axm3 msgv ∈ MSG ։ VAL message value axm4

object STATUS b any ob when grd 1

 1 pctn(ob) = STATUS grd 2..n select guards guards for selecting message then act 1 send message act 2 remove message * end Another event in this pattern is a loop completion event and events have c name extension. As name suggests this event detects when the iterative process has been completed. The loop completed guard would be typically predicated on locally saved message receipt variable msgo. The action of this event simply updates objects program counter to the next value. object STATUS c any ob when grd 1 pctn(ob) = STATUS program counter status grd 2 loop completed guard loop is completed then act 1 pctn(ob) := NEXT STATUS end V. DISTRIBUTED PROTOCOL DEVELOPMENT In this section we present only few examples on how the presented communication and loop modelling patterns were used in developing the distributed resource allocation protocol.

  agent consume b any rs, ag event parameters : agent and resource when grd 1 ag ∈ dom(capt) grd 2 rs ∈ objr(objt(ag)) resource within the objective grd 3 rs ∈ union(ran(capt)) not yet consumed resource grd 4 pct0(ag) := CONSUME then act 1 capt(ag) := capt(ag) ∪ {rs} capture new resource end

agent consume c any ag when grd 1

 1 capt(ag) = objr(objt(ag)) completed its objective grd 2 pct0(ag) = CONSUME then act 1 pct0(ag) := RELEASE update program counter end

agent lock b any lc when grd 1

 1 lc ∈ LCK \ lck grd 2 lckd(lc) ∈ lcke(lcks(lc)) messages not sent yet grd 3 lckd(lc) ∈ objr(objt(lcks(lc))) within the objective grd 4 pct2(lcks(lc)) = LOCK then act 1 lck := lck ∪ {lc} send new message act 2 lcke(lcks(lc)) := lcke(lcks(lc)) ∪ lckd(lc) end

agent lock c any ag when grd 1

 1 lcke(ag) = objr(objt(ag)) all lock messages sent grd 2 pct2(ag) = LOCK then act 1 pct2(ag) := CONFIRMC update program counter end VI. DISTRIBUTED PROTOCOL VERIFICATION

  Sending message from A n to r k . 3: end 4: wait until received replies[A n ] = objective[A n ] 5: if |replies[A n ]| = 1 All replied indexes are not the same. The end of stage 1 of the protocol. 14: wait until received pready[A n ] = objective[A n ] 15: while sent lock[A n ] = objective[A n ] do wait until received response[A n ] = objective[A n ] 19: if deny ∈ responses[A n ] then Exists a deny message.

	1: while sent requests[A n ] = objective[A n ] do
	2: request(A n ) → r k 6: then while |replies[A n ]| = 1 do
	7:	m = max(replies(A n )) + 1
	8:	while sent srequests[A n ] = objective[A n ] do
	9:		srequest(A n , m) → r k
	10:	end
	11: while sent write[A n ] = objective[A n ] do
	12:	write(A n , m) → r k
	13: end 16:	lock(A n ) → r k
	17: end
	18:

  when grd 1 ms 1 ∈ msg 1 received message grd 2 ms 2 ∈ MSG 2 \ msg 2 create a new message grd 3 msg 2 d(ms 2 ) = msg 1 s(ms 1 ) grd 4 msg 2 s(ms 2 ) = msg 1 d(ms 1 )then act 1 msg 2 := msg 2 ∪ {ms 2 } send new message act 2 msg 1 := msg 1 \ {ms 1 } remove message act 3 msgo 2 (msg 2 s(ms 2 )) := msgo 2 (msg 2 s(ms 2 )) \ {ms 2 }

	object reply MSG
	any
	ms 1 , ms 2
	end

  initiating MSG any ms 1 when grd 1 ms 1 ∈ MSG 1 \ msg 1 create a new message grd 2 pctn(msg 1 s(ms 1 )) = STATUS program counter at then specific value act 1 msg 1 := msg 1 ∪ {ms 1 } send new message act 2 msgo 1 (msg 1 s(ms 1 )) := msgo 1 (msg 1 s(ms 1 )) \ {ms 1 }

	end

Acknowledgements. This work is supported by an iCASE studentship (EPSRC and Siemens Rail Automation).


Joanna Kowal

Mercedes Tkach

Clotilde Théry
email: clotilde.thery@curie.fr

Biogenesis and secretion of exosomes

Keywords: extracellular vesicles, exosomes, microparticles, microvesicles, RAB, SNARE, ESCRT, lipids, tetraspanins dendritic cell, ESCRT: endosomal sorting complex required for transport, EV: extracellular vesicle, ILV: intraluminal vesicle, LBPA: lysobisphosphatidic acid, MHC: Major Histocompatibility Complex, MVB: multivesicular body, PLP: proteolipid protein, PLD2: phospholipase D2, PM: plasma membrane, SNARE

Although observed for several decades, the release of membrane-enclosed vesicles by cells into their surrounding environment has been the subject of increasing interest in the past few years, which led to the creation, in 2012, of a scientific society dedicated to the subject: the International Society for Extracellular Vesicles. Convincing evidence that vesicles allow exchange of complex information fuelled this rise in interest. But it has also become clear that different types of secreted vesicles co-exist, with different intracellular origins and modes of formation, and thus probably different compositions and functions.

Exosomes are one sub-type of secreted vesicles. They form inside eukaryotic cells in multivesicular compartments, and are secreted when these compartments fuse with the plasma membrane. Interestingly, different families of molecules have been shown to allow intracellular formation of exosomes and their subsequent secretion, which suggests that even among exosomes different sub-types exist.

Highlights:

ESCRT proteins, lipids and tetraspanins can independently generate intraluminal vesicles Different RAB proteins can target multivesicular compartments to the plasma membrane Vesicles with different densities, and probably different origins, are co-secreted

Introduction: the discovery of exosomes

The release of membrane-enclosed vesicles from tumor cells and platelets [START_REF] Crawford | The presence of contractile proteins in platelet microparticles isolated from human and animal platelet-free plasma[END_REF][START_REF] Dvorak | Tumor shedding and coagulation[END_REF], possibly explaining observations of extracellular vesicles (EVs) within tissues [START_REF] Anderson | Vesicles associated with calcification in the matrix of epiphyseal cartilage[END_REF] or body fluids [START_REF] Crawford | The presence of contractile proteins in platelet microparticles isolated from human and animal platelet-free plasma[END_REF][START_REF] Stegmayr | Promotive effect on human sperm progressive motility by prostasomes[END_REF] was described more than 40 years ago. Originally, these EVs were thought to bud directly from the plasma membrane (PM). In the 1980's, however, two groups studying reticulocyte maturation described a more complex mode of EV secretion. They showed that small vesicles were formed by inward budding inside an intracellular endosome, leading to the formation of a multivesicular body (MVB), which could then fuse with the PM and release outside its internal vesicles [START_REF] Pan | Electron microscopic evidence for externalization of the transferrin receptor in vesicular form in sheep reticulocytes[END_REF][START_REF] Harding | Receptor-mediated endocytosis of transferrin and recycling of the transferrin receptor in rat reticulocytes[END_REF] (Figure 1). In 1987, the word "exosomes" was proposed for these EVs of endosomal origin [START_REF] Johnstone | Vesicle formation during reticulocyte maturation. Association of plasma membrane activities with released vesicles (exosomes)[END_REF] (Box 1). The existence of this unusual EV secretion pathway was confirmed afterwards in, among others, antigen-presenting cells [START_REF] Raposo | cell responses, suggesting a signaling, rather than "garbage", role for exosomes[END_REF][START_REF] Zitvogel | Eradication of established murine tumors using a novel cell-free vaccine: dendritic cell-derived exosomes[END_REF], epithelial cells [START_REF] Van Niel | Intestinal epithelial cells secrete exosome-like vesicles[END_REF] and tumour cells [START_REF] Wolfers | Tumor-derived exosomes are a source of shared tumor rejection antigens for CTL cross-priming[END_REF]. Further description of mRNA and miRNA in exosomes [START_REF] Valadi | Exosomemediated transfer of mRNAs and microRNAs is a novel mechanism of genetic exchange between cells[END_REF] sparked a strong interest in these vesicles. Since mRNA had also been shown in PM-derived microvesicles [START_REF] Ratajczak | Embryonic stem cell-derived microvesicles reprogram hematopoietic progenitors: evidence for horizontal transfer of mRNA and protein delivery[END_REF], it is currently believed that cells use EVs as a mean of extracellular communication and exchange of proteins, lipids and nucleic acids [14]. Whether exosomes and other EVs display different or identical functions is, however, still unclear. Answering this question will become possible from a detailed knowledge of the cell biology of these vesicles, which should provide targets to specifically affect their production in vivo. This review will summarize the recent advances on the molecular machineries of exosome formation and secretion, but interested readers can refer to our more detailed review also discussing the other types of EVs [15].

Exosome composition

Initial proteomic studies revealed that exosomes contain a specific subset of proteins from endosomes, the PM and the cytosol [16], but very few from other intracellular organelles (nucleus, mitochondria, Golgi). This confirmed that exosomes represent a specific subcellular compartment, since they do not contain a random set of proteins, as would be the case for cell debris. These observations were validated in numerous other studies of the protein composition of exosomes, and recently of other EVs, which have been made accessible through the creation of two specific databases compiling published data: Vesiclepedia [START_REF]vesicular components, including proteins, mRNAs, miRNAs, and lipids. Here, both prokaryotic and eukaryotic EVs are included[END_REF] and EVpedia [START_REF] Kim | EVpedia: an integrated database of high-throughput data for systemic analyses of extracellular vesicles[END_REF]. Of note, although exosomes should be enriched in endosomal components, as compared to PM-derived EVs, the two types of EVs display a large overlap in composition, and it is not possible today to name universal (i.e. valid for any cell type) protein markers specific for exosomes versus PM-derived vesicles.

Interestingly, although investigations of the lipid composition of exosomes were not as frequent as proteomic analyses, all studies showed differences with whole cell membranes [START_REF] Brouwers | Distinct lipid compositions of two types of human prostasomes[END_REF][START_REF] Laulagnier | Mast cell-and dendritic cell-derived exosomes display a specific lipid composition and an unusual membrane organization[END_REF][START_REF] Llorente | Molecular lipidomics of exosomes released by PC-3 prostate cancer cells[END_REF][START_REF] Trajkovic | Ceramide triggers budding of exosome vesicles into multivesicular endosomes[END_REF][START_REF] Wubbolts | Proteomic and biochemical analyses of human B cell-derived exosomes. Potential implications for their function and multivesicular body formation[END_REF][START_REF] Laulagnier | PLD2 is enriched on exosomes and its activity is correlated to the release of exosomes[END_REF]. Exosomes are enriched in cholesterol, sphingomyelin, ceramide and phosphatidylserine, but not in lysobisphosphatidic acid (LBPA), a lipid described in MVBs' intraluminal vesicles (ILVs) [START_REF] Matsuo | Role of LBPA and Alix in multivesicular liposome formation and endosome organization[END_REF]. Some of these lipids (e.g. sphingomyelin and cholesterol) and some exosomal proteins (e.g. GPI-anchored proteins and flotillins) are also enriched in detergent-resistant subdomains of the PM called lipid rafts [START_REF] Ikonen | Roles of lipid rafts in membrane transport[END_REF]. Indeed, a direct link between endocytosis of lipid rafts and eventual secretion into exosomes has recently been shown in mesenchymal stem cells [START_REF] Tan | Therapeutic MSC exosomes are derived from lipid raft microdomains in the plasma membrane[END_REF].

These analyses of exosome composition unravelled the presence of molecules or families of molecules, which could be involved in their formation inside MVBs, or in their release outside the cell. We will thus now discuss the current knowledge of exosome biogenesis and in particular their formation as ILVs in MVBs and their secretion requiring the transport and fusion of MVBs with the PM.

Exosome biogenesis: formation of ILVs in endosomal compartments

MVBs, which appear along the endocytic pathway, are characterized by the presence of vesicles in their lumen (i.e. ILVs) formed by inward budding from the limiting membrane [START_REF] Klumperman | The complex ultrastructure of the endolysosomal system[END_REF] (Figure 1). The molecular mechanisms of ILV formation have been extensively studied, especially in yeast [START_REF] Henne | Molecular mechanisms of the membrane sculpting ESCRT pathway[END_REF], but we will describe here only the studies analysing these molecules in the context of exosome release, as summarized in Table 1.

a) ESCRT-machinery

Description of the Endosomal Sorting Complex Required for Transport (ESCRT) machinery involved in the formation of ILVs began in the early 2000's [START_REF] Katzmann | Ubiquitin-dependent sorting into the multivesicular body pathway requires the function of a conserved endosomal protein sorting complex, ESCRT-I[END_REF], and has been widely reviewed lately in the literature [START_REF] Henne | Molecular mechanisms of the membrane sculpting ESCRT pathway[END_REF][START_REF] Hanson | Multivesicular body morphogenesis[END_REF] Four independent studies have shown a requirement for the ESCRT-0 member HRS in exosome secretion, demonstrated by a decrease in exosome secretion upon HRS inhibition in various cell types: HeLa cells [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF], mouse DCs (but only after incubation with a antigen) [START_REF] Tamai | Exosome secretion of dendritic cells is regulated by Hrs, an ESCRT-0 protein[END_REF], HEK293 [START_REF] Gross | Active Wnt proteins are secreted on exosomes[END_REF] and head and neck squamous cell carcinoma [START_REF] Hoshino | Exosome Secretion Is Enhanced by Invadopodia and Drives Invasive Behavior[END_REF]. In addition, in our shRNA-based screen performed in HeLa cells expressing the Major Histocompatibility Complex (MHC) class II machinery of antigen presentation (HeLa-CIITA), depletion of the STAM1 ESCRT-0 component also reduced exosome secretion [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF].

Depletion of TSG101, an ESCRT-I component, also lead to reduced exosome secretion in the tumour cells HeLa-CIITA [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF], MCF-7 [START_REF] Baietti | Syndecan-syntenin-ALIX regulates the biogenesis of exosomes[END_REF], and in immortalized RPE1 epithelial cells [37], but not in the oli-neu oligodendroglial cells, where another ESCRT-independent mechanism was described (see below) [START_REF] Trajkovic | Ceramide triggers budding of exosome vesicles into multivesicular endosomes[END_REF].

Members of the ESCRT-II and ESCRT-III complexes are consistently found in proteomic analyses of various exosomes (see Vesiclepedia and EVpedia). In our shRNA screen, we did not observe a clear influence of ESCRT-II proteins on exosome secretion by HeLa-CIITA cells, and technical issues prevented conclusions on ESCRT-III components [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF]. In the MCF-7 cell line, however, depletion by RNAi of each isoform of CHMP4, separately or simultaneously, decreased exosome secretion [START_REF] Baietti | Syndecan-syntenin-ALIX regulates the biogenesis of exosomes[END_REF].

The ESCRT-III-associated protein ALIX was recently shown to promote intraluminal budding of vesicles in endosomes and hence exosome biogenesis, upon interaction with syntenin, the cytoplasmic adaptor of heparan sulphate proteoglycan receptors [START_REF] Baietti | Syndecan-syntenin-ALIX regulates the biogenesis of exosomes[END_REF]. In HeLa-CIITA cells, depletion of ALIX caused an increase of MHC class II molecules in the cells and consequently in the released vesicles, without a clear effect on the amount of exosomes secreted, while in primary DCs silencing of ALIX decreased secretion of CD63, CD81 and MHC class II positive vesicles in half of the donors [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF]. In a muscle cell line, ALIX depletion promoted an increased release of PM-derived EVs containing HSC70 but decreased secretion of CD63 (a tetraspanin enriched in late MVBs, hence in exosomes) [START_REF] Romancino | Identification and characterization of the nano-sized vesicles released by muscle cells[END_REF].

VPS4 is involved at the final steps of ILV formation -i.e. scission of a membrane and/or dissociation of the ESCRT-III complex [START_REF] Hanson | Multivesicular body morphogenesis[END_REF]. Data concerning its impact on exosome biogenesis seem contradictory: in our hands, shRNA inhibition of VPS4B in HeLa-CIITA cells increased exosome secretion [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF], while a decrease in exosome secretion was observed in MCF-7 upon simultaneous silencing of VPS4A and VPS4B, with no significant effect of single inhibition of each isoform [START_REF] Baietti | Syndecan-syntenin-ALIX regulates the biogenesis of exosomes[END_REF]. A dominant-negative form of VPS4 (which blocks the function of both isoforms) has also been shown to inhibit exosome secretion in RPE1 cells [37], but not in oli-neu cells which secrete exosomes in a ESCRT-independent manner [START_REF] Trajkovic | Ceramide triggers budding of exosome vesicles into multivesicular endosomes[END_REF]. Either compensation of VPS4B by increased activity of VPS4A, or alternative functions of VPS4B in HeLa cells, possibly linked to their constitutive expression of papillomavirus proteins (which have recently been shown to reduce exosome secretion [START_REF] Honegger | Silencing of human papillomavirus (HPV) E6/E7 oncogene expression affects both the contents and the amounts of extracellular microvesicles released from HPV-positive cancer cells[END_REF]) could explain the observed increase of exosome secretion in our study [START_REF] Colombo | Analysis of ESCRT functions in exosome biogenesis, composition and secretion highlights the heterogeneity of extracellular vesicles[END_REF].

Although many studies use ESCRT inhibition as a tool to inhibit secretion of exosomes, one should be aware that these proteins are involved in other cellular mechanisms, especially cytokinesis [START_REF] Henne | Molecular mechanisms of the membrane sculpting ESCRT pathway[END_REF][START_REF] Bissig | ALIX and the multivesicular endosome: ALIX in Wonderland[END_REF], and that their silencing should be examined with care since this may alter cellular functions other than the formation of MVB. In addition, ESCRT members (e.g. TSG101, ALIX, VPS4) have been shown to promote budding from the PM of enveloped viruses [START_REF] Bissig | ALIX and the multivesicular endosome: ALIX in Wonderland[END_REF][START_REF] Garrus | Tsg101 and the vacuolar protein sorting pathway are essential for HIV-1 budding[END_REF][START_REF] Pornillos | HIV Gag mimics the Tsg101recruiting activity of the human Hrs protein[END_REF],

or of microvesicles or exosome-like vesicles, especially in T lymphocytes [START_REF] Booth | Exosomes and HIV Gag bud from endosome-like domains of the T cell plasma membrane[END_REF][START_REF] Choudhuri | Polarized release of T-cell-receptor-enriched microvesicles at the immunological synapse[END_REF].

Hence ESCRT-dependence does not necessarily demonstrate MVB origin.

b) ESCRT-independent mechanisms

Recently, several articles suggested that ESCRT-independent mechanisms are also involved in ILV formation and exosome biogenesis: these mechanisms involve lipids, tetraspanins, or heat shock proteins. Of note, mammalian cells depleted for key ESCRT components still form MVBs [START_REF] Stuffers | Multivesicular endosome biogenesis in the absence of ESCRTs[END_REF].

Exosomes bearing the proteolipid protein (PLP) are normally secreted by oligodendroglial cells after ESCRT inhibition [START_REF] Trajkovic | Ceramide triggers budding of exosome vesicles into multivesicular endosomes[END_REF]. In these cells, inhibition of neutral sphingomyelinase, leading to impaired ceramide biogenesis, decreased exosome secretion. Ceramide was proposed to induce inward curvature of the limiting membrane of MVBs to form ILVs. Since this work, several labs have used neutral sphingomyelinase inhibition as a proof that their analysed EVs were indeed exosomes [START_REF] Dreux | Short-range exosomal transfer of viral RNA from infected cells to plasmacytoid dendritic cells triggers innate immunity[END_REF][START_REF] Kosaka | Secretory mechanisms and intercellular transfer of microRNAs in living cells[END_REF], although a potential effect of such treatments on release of PM-derived EVs, or on other cellular functions or secretions has never been actually ruled out. Caution should thus be taken in interpreting sphingomyelinase inhibition experiments.

Another lipid enriched in exosome membranes is cholesterol [START_REF] Laulagnier | Mast cell-and dendritic cell-derived exosomes display a specific lipid composition and an unusual membrane organization[END_REF][START_REF] Llorente | Molecular lipidomics of exosomes released by PC-3 prostate cancer cells[END_REF][START_REF] Wubbolts | Proteomic and biochemical analyses of human B cell-derived exosomes. Potential implications for their function and multivesicular body formation[END_REF], an important component of MVBs [START_REF] Hornick | Isolation and characterization of multivesicular bodies from rat hepatocytes: an organelle distinct from secretory vesicles of the Golgi apparatus[END_REF]. In the same oligodendroglial cells, drugor genetic mutation-induced cholesterol accumulation in late MVBs was shown to increase the secretion of vesicles bearing Flotillin-2, ALIX, CD63 and cholesterol, in a Flotillin-2-dependent manner [START_REF] Strauss | Exosome secretion ameliorates lysosomal storage of cholesterol in Niemann-Pick type C disease[END_REF].

Finally phospholipase D2 (PLD2), which, unlike phospholipase D1 (PLD1), is enriched in exosomes [START_REF] Laulagnier | PLD2 is enriched on exosomes and its activity is correlated to the release of exosomes[END_REF], is involved in hydrolysis of phosphatidylcholine to phosphatidic acid (PA). PLD2, but not PLD1, was shown in two different cell types to be necessary for exosome biogenesis [START_REF] Laulagnier | PLD2 is enriched on exosomes and its activity is correlated to the release of exosomes[END_REF][START_REF] Ghossoub | Syntenin-ALIX exosome biogenesis and budding into multivesicular bodies are controlled by ARF6 and PLD2[END_REF]. The model proposed is that PA formation in the inner leaflet of MVB's limiting membrane would induce inward curvature and thus formation of ILVs, as described for ceramide [START_REF] Ghossoub | Syntenin-ALIX exosome biogenesis and budding into multivesicular bodies are controlled by ARF6 and PLD2[END_REF]. Thus, one would expect enrichment of PA in exosomes, which has not been addressed so far.

On the other hand, four-transmembrane domain proteins of the tetraspanin family have recently been proposed as instrumental in selecting cargoes for exosome secretion. In human melanoma cells, CD63 allows sorting of a melanosomal protein into ILVs, in a ceramide-and ESCRT-independent manner Finally, the chaperone HSC70 was previously shown to allow recruitment of the transferrin receptor (TFR) to exosomes [START_REF] Geminard | Degradation of AP2 during reticulocyte maturation enhances binding of hsc70 and Alix to a common site on TFR for sorting into exosomes[END_REF]. More recently, cytosolic proteins containing a KFERQ-motif were found to bind HSC70, which induced their selective transfer to ILVs [START_REF] Sahu | Microautophagy of cytosolic proteins by late endosomes[END_REF].

It is not known whether these multiple mechanisms of biogenesis of exosomes and ILVs can take place in a single MVB, or rather if they suggest that different MVBs populations can coexist within the cell. Indeed, evidence of the heterogeneity of MVBs within a single cell already exist: e.g. the non-ubiquitous distribution of cholesterol in all MVBs [START_REF] Mobius | Immunoelectron microscopic localization of cholesterol using biotinylated and non-cytolytic perfringolysin O[END_REF], the lack of enrichment of LBPA in exosomes, as opposed to its enrichment in ILVs [START_REF] Wubbolts | Proteomic and biochemical analyses of human B cell-derived exosomes. Potential implications for their function and multivesicular body formation[END_REF][START_REF] White | EGF stimulates annexin 1-dependent inward vesiculation in a multivesicular endosome subpopulation[END_REF], or the existence of two distinct MVB subsets within DCs, one being formed upon cognate interaction with T lymphocytes [START_REF] Buschow | MHC II in dendritic cells is targeted to lysosomes or T cell-induced exosomes via distinct multivesicular body pathways[END_REF].

Exosome secretion: transport and fusion of MVBs with the plasma membrane

Mechanisms that drive mobilization of secretory MVBs and fusion of their limiting membrane with the PM have started being unravelled in the past few years. The studies described below are summarized in table 2.

The RAB family of small GTPase proteins controls different steps of intracellular vesicular trafficking, such as vesicle budding, vesicle and organelle mobility through cytoskeleton interaction, and docking of vesicles to their target compartment, leading to membrane fusion [START_REF] Stenmark | Rab GTPases as coordinators of vesicle traffic[END_REF]. Since the first proteomic studies, endosome-associated members of this family were identified in exosomes [16]. RAB11 has been linked to the control of TFR and HSC70containing exosome release in K562 cells [START_REF] Savina | Rab11 promotes docking and fusion of multivesicular bodies in a calcium-dependent manner[END_REF]. Using different screening strategies, several RAB proteins emerged as new players in exosome secretion [START_REF] Hsu | Regulation of exosome secretion by Rab35 and its GTPase-activating proteins TBC1D10A-C[END_REF][START_REF] Zylbersztejn | of two medium-scale screening strategies to identify molecular machineries of exosome secretion, showing a role for Rab 67[END_REF]. Inhibition of RAB35 impaired PLP-bearing exosome secretion in oli-neu cells [START_REF] Hsu | Regulation of exosome secretion by Rab35 and its GTPase-activating proteins TBC1D10A-C[END_REF], and in primary oligodendrocytes [64]. In the human cell line RPE1 either RAB11 or RAB35 were required for the secretion of anthrax toxin-loaded exosomes to the extracellular medium [37]. In our shRNA-based screening of different RAB proteins in HeLa-CIITA cells, depletion of RAB5A, RAB9A, RAB2B, and more strikingly RAB27A and RAB27B, efficiently decreased exosome secretion, whereas depletion of RAB11A or RAB7 did not [START_REF] Zylbersztejn | of two medium-scale screening strategies to identify molecular machineries of exosome secretion, showing a role for Rab 67[END_REF]. By contrast, syntenin-and ALIX-containing exosome secretion by MCF-7 cells was shown to require RAB7 [START_REF] Baietti | Syndecan-syntenin-ALIX regulates the biogenesis of exosomes[END_REF]. The involvement of RAB27A in vesicle secretion was later confirmed in numerous tumour cell lines: murine melanoma [65] and mammary carcinoma [66], and human squamous cell carcinoma cells [START_REF] Hoshino | Exosome Secretion Is Enhanced by Invadopodia and Drives Invasive Behavior[END_REF]. These RAB proteins are thought to function in MVB docking to the PM, which is required for eventual fusion of the two membranes, to allow secretion of the vesicles present in this compartment.

It is important to stress that RAB27A controls not only exosome secretion, but also the secretion of a subset of soluble factors. For instance, inhibition of RAB27A decreased secretion of the soluble pro-metastatic factor matrix metalloproteinase 9 in 4T1 mammary carcinoma cells [66], as well as pro-angiogenic placental growth factor 2, platelet-derived growth factor A and osteopontin in the B16-F10 melanoma [65]. Thus, using RAB27A inhibition alone is not sufficient to demonstrate that a physiological effect is due to exosome secretion, and therefore the possible roles of other proteins involved in secretion must be evaluated. For RAB11 and RAB35, their potential roles in secretion of soluble proteins were not analysed in the articles reporting their effects in exosome secretion [START_REF] Savina | Rab11 promotes docking and fusion of multivesicular bodies in a calcium-dependent manner[END_REF][START_REF] Hsu | Regulation of exosome secretion by Rab35 and its GTPase-activating proteins TBC1D10A-C[END_REF] erythroleukemia cells [START_REF] Fader | TI-VAMP/VAMP7 and VAMP3/cellubrevin: two v-SNARE proteins involved in specific steps of the autophagy/multivesicular body pathways[END_REF], inhibition of VAMP7 in MDCK cells impaired lysosomal secretion but not the release of exosomes [72]. More recently, the R-SNARE protein YKT6 was found to be required for secretion of exosomes carrying the WNT3A morphogen in HEK293 cells [START_REF] Gross | Active Wnt proteins are secreted on exosomes[END_REF], and these results await confirmation in other models.

Again, the heterogeneity in the requirement for docking and fusion machineries could suggest the coexistence of different multivesicular compartments within the cell. RAB11 and RAB35 are described as associated with recycling and early sorting endosomes, whereas RAB27A and RAB27B are associated with the late endosomal and secretory compartments [START_REF] Stenmark | Rab GTPases as coordinators of vesicle traffic[END_REF]. Thus, we would like to propose that different RABs are involved in docking of ILVcontaining endosomes of different maturation stages along the endosomal pathway (Figure 1). These different MVBs could give the rise to different subpopulations of small EVs. This could explain RAB27A-independent secretion of a subpopulation of vesicles from tumour cells [73], or of anthrax toxincontaining exosomes from human epithelial cells [37].

Future challenges: separation of the different subtypes of exosomes

It recently became clear that all currently used protocols for exosome purification actually co-purify different subtypes of EVs. Demonstrations of this caveat were published recently, by three independent groups [73-75] and came from the careful analysis of the behaviour of exosomes upon floatation into a sucrose gradient. Although the density of exosomes in such gradients has been described for at least a decade as ranging between 1.11 and 1.19 g/ml, recent articles show that different types of EVs are present within this range of densities. Two reports showed that some EVs in the exosome pellet display similar equilibrium densities but different kinetics to reach this density, and thus are likely compositionally different [74,75]. We confirmed this observation, and also showed that the vesicles equilibrating at lower density fractions (1.11 g/ml) were less dependent on Rab27a for their secretion than those floating at 1.14 g/ml [73] consistent with the presence of at least two subpopulations of EVs within the purified exosome population. An urgent need in the field is to ameliorate already existing protocols, or to establish new methods that will allow separate analysis of the different subsets of EVs.

In all studies published thus far, several fractions recovered after floatation of exosomes into a sucrose gradient are pooled together to study the presence of different exosome markers and to perform functional assays.

Further improvement could be now to analyse separately the vesicles recovered in 3-5 fractions of the expected exosome density. Immuno-capture of specific subsets of vesicles has been also performed, using CD63 as a marker of MVBderived vesicles [START_REF] Zylbersztejn | of two medium-scale screening strategies to identify molecular machineries of exosome secretion, showing a role for Rab 67[END_REF], or markers of the apical versus basolateral surface of polarized tumour cells [START_REF] Tauro | Two Distinct Populations of Exosomes Are Released from LIM1863 Colon Carcinoma Cell-derived Organoids[END_REF]. Although powerful, these approaches will benefit from the future identification of specific surface markers of each subtype of EVs.

Finally, polymer-based kits are now commercialized for vesicle isolation.

Although this method is less laborious and time-consuming, and apparently provides a higher rate of recovery, especially of extracellular RNAs [START_REF] Taylor | Exosome isolation for proteomic analyses and RNA profiling[END_REF], we suspect that even more heterogeneous types of particles present in conditioned medium or body fluids will be recovered with this method, especially lipoproteins, and cell debris, and optimisation is still called for.

Conclusions / closing remarks

A number of discoveries in recent years have increased the interest of cell biologists in exosomes: first the confirmation of this secretory pathway within immune cells [START_REF] Raposo | cell responses, suggesting a signaling, rather than "garbage", role for exosomes[END_REF], then their identification in body fluids [START_REF] Andre | Malignant effusions and immunogenic tumour-derived exosomes[END_REF] hence their existence in vivo, and finally, the discovery of their nucleic acid (RNA) content [START_REF] Valadi | Exosomemediated transfer of mRNAs and microRNAs is a novel mechanism of genetic exchange between cells[END_REF]. These breakthroughs led to a rise in the number of exosome-related studies in the literature, but also to a general rise in interest in all types of EVs. Interestingly, so far, no universal mechanism of either biogenesis or secretion of exosomes has emerged. It remains to be determined whether the differences in mechanisms described by different groups are due to cell-intrinsic specific mechanisms of exosome formation and secretion, or to differences in the nature of the vesicles analysed. Finally, a crucial question remains unsolved: the physiological relevance of exosome and/or PM-derived vesicle release in vivo.

The answers to these questions will only become possible when the outstanding cell biology issues have been solved, especially what drives the fate of MVBsfusion with the PM or with lysosomes, and how MVBs fuse with the PM.

Box 1: Nomenclature issue.

Here, we use the term "exosomes" as defined by Rose Johnstone in 1987 [START_REF] Johnstone | Vesicle formation during reticulocyte maturation. Association of plasma membrane activities with released vesicles (exosomes)[END_REF], and not the more general use for any vesicles released by cells [START_REF] Trams | Exfoliation of membrane ectoenzymes in the form of micro-vesicles[END_REF]. Currently, the use of the term "exosomes" for MVB-derived EVs is generally accepted in the field, although the variety of EVs secreted by cells and difficulties in proving the actual origin of EVs led to a less strict usage: either for any small EVs (of 50-100 nm diameter by transmission electron microscopy), or for EVs recovered after 100,000g ultracentrifugation. As proposed recently by S. Gould and G. Raposo [START_REF] Gould | As we wait: coping with an imperfect nomenclature for extracellular vesicles[END_REF], given the lack of perfect demonstration of EVs' endosomal origin, we can only suggest that researchers clearly specify their interpretation of whatever term they use for the EVs they analyse. In addition, the term "exosome" has been used since 1997 in a completely different field, not related to EVs: for a multienzyme ribonuclease complex involved in RNA processing [START_REF] Mitchell | The exosome: a conserved eukaryotic RNA processing complex containing multiple 3'-->5' exoribonucleases[END_REF]. Note that the first occurrence of the term in the literature was in 1970 for an "exosome model", proposing that DNA segments enter the cells of treated individuals and become firmly associated with their homologous chromosome segments, but are never integrated into the linear structure of the chromosome [START_REF] Fox | DNA-induced transformation in Drosophila: locusspecificity and the establishment of transformed stocks[END_REF]. « Exosome » is not used in this particular sense anymore. The fate of MVBs can be either fusion with lysosomes or fusion with the PM, which allows the release of their content to the extracellular milieu. Several RAB proteins (RAB11, RAB27 and RAB35) have been shown to be involved in the transport of MVBs to the PM and in exosome secretion. Here, we propose that these proteins can act on different MVBs. In addition, SNAREs are probably involved in fusion of these MVBs with the PM. Other types of secreted vesicles bud directly from the plasma membrane, and are often called microvesicles, or micro particles, two words also sometimes used generally for all types of EVs.

  . ESCRT consists of 4 complexes plus associated proteins: ESCRT-0 is responsible for cargo clustering in a ubiquitin-dependent manner, ESCRT-I and -II induce bud formation, ESCRT-III drives vesicle scission, and the accessory proteins (especially the VPS4 ATPase) allow dissociation and recycling of the ESCRT machinery. Members of the ESCRT family, TSG101 and ALIX (gene name: Pdcd6ip), were found in our first extensive proteomic analysis of mouse dendritic cell (DC)-derived exosomes, even before they were known to belong to this machinery [16]. Identification of ESCRT components in exosomes was further confirmed and extended by others (see EVpedia: www.evpedia.info; Vesiclepedia: www.microvesicles.org).

  [51]. Tetraspanins are enriched in ILVs of MVBs and in exosomes [52]. TSPAN8 expression could modify both the mRNA content and the protein composition of exosomes secreted by rat pancreatic adenocarcinoma cells [53]. Similarly, CD81 was recently shown to allow targeting of an array of its ligands into secreted exosomes [54].

  and thus further work is required to clarify this. After docking of two different intracellular compartments, soluble NSFattachment protein receptor (SNARE) complexes are instrumental in allowing fusion of the lipid bilayers [67]. The SNARE proteins SNAP-23, VAMP-7 and VAMP-8 are involved in Ca 2+ -regulated fusion of secretory lysosomes with the PM in different cell types [68-70]. However SNAREs do not necessarily mediate the fusion of MVBs with the PM during exosome secretion. While VAMP7 is essential for the release of acetylcholinesterase-containing EVs in K562

Figure 1 :

 1 Figure 1: intracellular machineries of exosome biogenesis and secretion Schematic representation of the origin and release of exosomes by eukaryotic cells. Exosomes are formed as ILVs by budding into early endosomes and MVBs. Several molecules are involved in the biogenesis of ILVs, such as the ESCRT machinery, the lipid ceramide and the tetraspanins. It is still unknown whether these mechanisms act simultaneously on the same MVB or on different MVBs.

  66. Bobrie A, Krumeich S, Reyal F, Recchi C, Moita LF, Seabra MC, Ostrowski M, Thery C: Rab27a supports exosome-dependent and -independent mechanisms that modify the tumor microenvironment and can promote tumor progression. Cancer Res 2012, 72:4920-4930. 72. Proux-Gillardeaux V, Raposo G, Irinopoulou T, Galli T: Expression of the Longin domain of TI-VAMP impairs lysosomal secretion and epithelial cell migration. Biol Cell 2007, 99:261-271. 73. Bobrie A, Colombo M, Krumeich S, Raposo G, Thery C: Diverse subpopulations of vesicles secreted by different intracellular mechanisms are present in exosome preparations obtained by differential ultracentrifugation. J Extracell Vesicles 2012, 1: 18397. ** One of three studies (with [74, 75]) showing the co-secretion of different subtypes of exosomes. Here, inhibition of Rab27a in a mouse tumor breast cell line leads to inhibition of secretion of vesicles bearing some classical exosome markers, while vesicles bearing another subset of exosome markers remained abundant. Flotation on sucrose gradient shows different floatation behaviours of these different markers. 74. Aalberts M, van Dissel-Emiliani FM, van Adrichem NP, van Wijnen M, Wauben MH, Stout TA, Stoorvogel W: Identification of distinct populations of prostasomes that differentially express prostate stem cell antigen, annexin A1, and GLIPR2 in humans. Biol Reprod 2012, 86:82. ** Like [73, 75], this study unravels the heterogenity of vesicles present in human seminal fluids. Here, floatation of the vesicles on sucrose gradient reveals the existence of vesicles of similar equilibrium densities, but reaching this equilibrium with different kinetics. 75. Palma J, Yaddanapudi SC, Pigati L, Havens MA, Jeong S, Weiner GA, Weimer KM, Stern B, Hastings ML, Duelli DM: MicroRNAs are exported from malignant cells in customized particles. Nucleic Acids Res 2012, 40:9125-9138.

Table 1 . Published studies on exosome biogenesis

 1 (italics highlight tumour cell models)

	Protein Name	Cell type used in study	Markers used for exosome definition	Tools used for inhibition	Reference
			HeLa-CIITA	CD63, CD81, MHCII	shRNA	[32]
			Primary Dendritic cells	Ubiquitinated proteins, TSG101, VPS4B	shRNA	[33]
	ESCRT-0	HRS	HEK293 Head neck squamous cell carcinoma	EVI, WNT3A, CD81 MT1, TSG101	siRNA siRNA	[34] [35]
			(SCC25-H1047R)
		STAM1	HeLa-CIITA	CD63, CD81, MHCII	shRNA	[32]
			HeLa-CIITA	CD63, CD81, MHCII	shRNA	[32]
	ESCRT-I	TSG101	MCF-7 RPE1	Syntenin-1, CD63, syndecan-1 C-terminal fragment Flotillin-1	siRNA siRNA	[36] [37]
			Oli-neu	PLP	siRNA	[22]
	ESCRT-III	CHMP4	MCF-7	Syntenin-1, CD63, fragment syndecan-1 C-terminal	siRNA	[36]
			HeLa-CIITA	CD63, CD81, MHCII	shRNA	[32]
				Syntenin-1, CD63,
	Accessory proteins	ALIX VPS4	MCF-7 C2C12 RPE1 HeLa-CIITA	syndecan-1 C-terminal fragment ALIX, HSC70, beta enolase, Pan-actin, CD63 Flotillin-1 CD63, CD81, MHCII	siRNA siRNA Dominant negative mutant overexpressed shRNA	[36] [38] [37] [32]
				Syntenin-1, CD63,	Inhibition of
			MCF-7	syndecan-1 C-terminal	both isoforms by	[36]
				fragment	siRNA
			ESCRT-independent mechanism
					GW4869
			Oli-neu	PLP	(neutral sphingomyelinas	[22]
					e inhibitor)
	Ceramide		Syntenin-1, CD63,
			MCF-7	syndecan-1 C-terminal	siRNA	[36]
				fragment
			Huh-7.5.1c2	CD63, CD81	GW4869	[46]
			HEK293	CD63	GW4869, siRNA	[47]
	Flotillin-2	Oli-neu	Flotillin-2, ALIX, CD63, cholesterol	siRNA	[49]
					siRNA,
			MCF-7	ALIX, Syntenin-1, CD63	CAY10594	[50]
		PLD2			(PLD2 inhibitor)
			RBL-2H3	Fluorescent staining of membranes	Overexpression of active /	[24]

Table 2 . Published studies on exosome secretion.

 2

	(italics highlight tumour cell models)
			RAB family
	Name	Major intracellular localization	Cell type used in the study	Markers used for vesicle definition	Tools used inhibition for	Reference
	RAB2B	Endoplasmic reticulum and	HeLa-CIITA	CD63, MHC II, CD81	shRNA	[63]
		Golgi apparatus.
	RAB5A	Early endosomes	HeLa-CIITA	CD63, MHC II, CD81	shRNA	[63]
				CD63, Syntenin-1,
	RAB7	Late endosomes	MCF-7	Syndecan 1 C-	siRNA	[36]
				Terminal Fragment
	RAB9A	Late endosomes	HeLa-CIITA	CD63, MHC II, CD81	shRNA	[63]
	RAB11	Recycling and early sorting	K562	TFR, HSC70, Acetylcholinesteras e activity	Dominant negative overexpress mutant	[61]
		endosomes			ion
			RPE1	Flotillin-1, Anthrax Toxin Lethal Factor	siRNA	[37]
	RAB27A	Late endosomes and lysosome-related organelles	HeLa-CIITA 4T1, TS/A B16-F10, SK-Mel-28	CD63, MHC II, CD81 ALIX, HSC70, CD63, TSG101 ALIX, TSG101	shRNA shRNA shRNA	[63] [66] [65]
			SCC61, SCC25-H1047R	-	shRNA	[35]
		Late endosomes
	RAB27B	and lysosome-related	HeLa-CIITA	CD63, MHC II, CD81	shRNA	[63]
		organelles
					siRNA and
					dominant
			Oli-neu	PLP	negative mutant	[62]
	RAB35	Recycling			overexpress
		endosomes			ion
			RPE1	Flotillin-1	siRNA	[37]
			Primary
			oligodendrocyt	ALIX, PLP	siRNA	[64]
			es
			SNARE family
	VAMP7	Lysosomes and late endosomes	K562	Acetylcholinesteras e activity	Truncated VAMP7 overexpress	[71]
					ion
	YKT6	Early and recycling	HEK293	WNT3A, CD81	siRNA	[34]
		endosomes

*This

paper, like [18], reports the creation of a database compiling lipid, RNA, and protein data from different classes of eukaryotic EVs from the studies published over the past several years. The idea is to promote a continuous update of the database by the authors, before and after publication of their articles.

	37. Abrami L, Brandi L, Moayeri M, Brown MJ, Krantz BA, Leppla SH, van der Goot
	FG: Hijacking multivesicular bodies enables long-term and exosome-
	mediated long-distance action of anthrax toxin. Cell Rep 2013, 5:986-996.

**

This paper shows hijacking of the exosome machinery by anthrax toxin: the toxin is protected from degradation by targeting into the lumen of ILVs in endosomes, which allows a long-term delivery to the cytosol. ILVs containing anthrax toxin can also be released to the extracellular space as exosomes, where they can be incorporated by recipient cells allowing a long-range action of the toxin.

	51. van Niel G, Charrin S, Simoes S, Romao M, Rochin L, Saftig P, Marks MS,
	Rubinstein E, Raposo G: The tetraspanin CD63 regulates ESCRT-
	independent and -dependent endosomal sorting during melanogenesis.
	Dev Cell 2011, 21:708-721.

**

This paper shows for the first time a tetraspanin-dependent and ESCRT- independent mechanism of cargo sorting into ILVs. ESCRT complex is necessary for disposal of the remaining cargo by targeting to lysosomal degradation.

	52. Escola JM, Kleijmeer MJ, Stoorvogel W, Griffith JM, Yoshie O, Geuze HJ:
	Selective enrichment of tetraspan proteins on the internal vesicles of
	multivesicular endosomes and on exosomes secreted by human B-
	lymphocytes. J Biol Chem 1998, 273:20121-20127.
	53. Nazarenko I, Rana S, Baumann A, McAlear J, Hellwig A, Trendelenburg M,
	Lochnit G, Preissner KT, Zoller M: Cell surface tetraspanin Tspan8
	contributes to molecular pathways of exosome-induced endothelial cell
	activation. Cancer Res 2010, 70:1668-1678.
	54. Perez-Hernandez D, Gutierrez-Vazquez C, Jorge I, Lopez-Martin S, Ursa A,
	Sanchez-Madrid F, Vazquez J, Yanez-Mo M: The Intracellular Interactome
	of Tetraspanin-enriched Microdomains Reveals Their Function as Sorting
	Machineries toward Exosomes. J Biol Chem 2013, 288:11649-11661.

proteins.

The authors used a library of GTPase Activating Proteins in oli- neu cells, and thus identified TBC1D10 family and its target Rab35 as crucial for secretion of exosomes bearing PLP. 63

  . Ostrowski M, Carmo NB, Krumeich S, Fanget I, Raposo G, Savina A, Moita CF, Schauer K, Hume AN, Freitas RP, et al.: Rab27a and Rab27b control different steps of the exosome secretion pathway. Nat Cell Biol 2010, 12:19-30; sup pp 11-13.

**

Screening strategy as in [62], but using a library of shRNA specific for RAB proteins, in HeLa-CIITA cells. RAB27A and RAB27B were identified as crucial for secretion of CD63-and MHC class II-or CD81-containing exosomes. 64

  . Fruhbeis C, Frohlich D, Kuo WP, Amphornrat J, Thilemann S, Saab AS, Kirchhoff F, Mobius W, Goebbels S, Nave KA, et al.: Neurotransmittertriggered transfer of exosomes mediates oligodendrocyte-neuron communication. PLoS Biol 2013, 11:e1001604. 65. Peinado H, Aleckovic M, Lavotshkin S, Matei I, Costa-Silva B, Moreno-Bueno G, Hergueta-Redondo M, Williams C, Garcia-Santos G, Ghajar C, et al.: Melanoma exosomes educate bone marrow progenitor cells toward a prometastatic phenotype through MET. Nat Med 2012, 18:883-891.

* Like [66],

this article addresses the function of exosome secretion by tumors in vivo, and shows a prometastatic effect of melanoma exosomes acting as a mediators between tumor cells and bone marrow progenitors. Of note, the authors use Rab27a depletion to decrease exosome secretion, and like in [66], they show that not only exosome, but also soluble factors require Rab27a for efficient secretion.

* This paper reveals an ESCRT-dependent mechanism for ILV/exosome formation, involving the connection of transmembrane proteoglycan receptor syndecans with syntenin and through syntenin with ALIX.

* Using extensive mass spectrometry, this article shows a crucial function of the tetraspanin CD81 in sorting its interacting partners into exosomes.

* Study similar to [66] in a murine breast cancer cell model. A role of exosomes, together with secreted soluble factors, in recruiting protumoral neutrophils to the tumor is shown. Here also, Rab27a depletion inhibits secretion not only of exosomes, but also of some soluble factors.

** Study similar to [73, 74], analysing vesicles secreted by human breast cancer cells. The authors show that different miRNA are associated with distinct subpopulations of EVs, which achieve density equilibrium at different time points.

Acknowledgements:

We apologize to all colleagues whose work could not be extensively quoted in this short review. Exosome-related work performed in the Théry lab is supported by fundings from Institut National de la Santé et de la Recherche Médicale, Institut Curie (including fellowship to J. Kowal), Association pour la Recherche contre le Cancer (including fellowship to M. Tkach), Fondation de France, Agence Nationale de la Recherche ([ANR-10-IDEX-0001-02 PSL*] and [ANR-11-LABX-0043]). We thank Omar Vivar for critical reading and english editing of the manuscript.