Towards correct Evolution of Conversation Protocols

Abstract

Distributed software systems change dynamically due to the evolution of their environment and/or requirements, their internal designing policies, and/or their specification bugs which must be fixed. Hence, checking system changes must be run continuously. Such systems are usually composed of distributed software entities (called peers) interacting with each other through message exchanges, and this is to fulfil a common goal. The goal is often specified by a conversation protocol (CP), i.e. sequences of sent messages. If there exists a set of peers implementing CP, then CP is said to be realisable. In this paper, we propose a stepwise approach for checking whether an evolution, i.e. adding and/or removing messages and/or peers, can be applied to a CP that was realisable before updating it. We define a set of correct evolution patterns and we suggest an algebra of CP evolution. Our approach ensures that CP evolution preserves the realisability condition.

1. INTRODUCTION

Distributed software systems change dynamically due to the evolution of their running environment and/or requirements, their internal designing policies, and/or their possible specification bugs which must be fixed. Such systems are usually composed of distributed software entities (called peers) evolving concurrently in a distributed setting and interacting with each other throughout messages exchanges to fulfil a common goal.

In a top-down design of distributed software, the interaction among peers is usually modelled using collaboration diagrams, Message Sequence Chains (MSCs) or conversation protocols (CP) (Bultan 2006) . Let us focus on CPs, these describe interactions among peers by describing uniquely the allowed sequences of sent messages. Here, it is crucial to know if the set of interactions in a CP can be implemented. In other word, considering a CP, one must check whether there exists a set of peers where their composition generates the same sequences of send messages as specified by the CP. This issue characterises the realisability problem. In order to formally specify, verify, and fix issues which violate realisability, CP can be modelled using Labelled Transition Systems (LTSs) where communication follows either synchronous or asynchronous semantics. Using this model enables automated analysis of interaction properties, e.g., realisability checking. Although it is obvious to check realisability in the case of synchronous communication, this realisability problem remains undecidable in the most general setting (Brand and Zafiropulo 1983) due the possibly ever-increasing queuing mechanism and unbounded buffers in the case of asynchronous communication.

The recent work of (Basu et al. 2012) proposed a necessary and sufficient condition for verifying if a CP can be implemented by a set of peers communicating asynchronously throughout FIFO buffers with no restriction on their buffer sizes. This work solves the realisability issue for a subclass of asynchronously communicating peers, namely, the synchronisable systems, i.e., the system composed of interacting peers behaves equally by applying synchronous or asynchronous communication. A CP is realisable if there exists a set of peers implementing that CP, i.e., they send messages to each other in the same order as CP, and such that their composition is synchronisable. In (Basu et al. 2012) , the full checking of CP realisability applies the following steps: i) peer projection from CP; ii) checking synchronisability; and iii) checking equivalence between CP and its distributed system. Based on LTS model, we can verify CP realisability using existing techniques such as model checking for systems with reasonable sizes (Basu et al. 2012) (i.e., number of states, transitions and communicating peers) or theorem proving for scalable systems (Farah et al. 2016) .

Considering realisable CPs, we are interested in studying the evolution of those CPs. In fact, these specify cross-organisational interactions with no centralised control between peers which can be administrated and executed by geographically distributed and autonomous companies. In order to cope with new environment changes and enduser requirements, system interaction and the corresponding CP need to evolve continuously over time. However, changing CP might result in knockon effects on its realisability. Hence, verifying the correctness of CP evolution to ensure realisability preservation must also be run continuously. Regarding the literature, existing work such as (Rinderle et al. 2006b; Ryu et al. 2008; Roohi and Salau¨n 2011) give some solutions for system evolution. In (Rinderle et al. 2006b; Ryu et al. 2008) the authors propagate the choreography updates into communicating peers. (Roohi and Salau¨n 2011) focuses on system reconfiguration meaning that for a CP which has been updated into CP’, the authors check whether the traces that has been executed in CP can be performed again in CP’. This reconfiguration can be better applied for run-time system to ensure execution consistency. All these approaches do not consider realisability preservation.

There exist other research approaches which can be applied as a posteriori evolution checking. The approaches suggest solutions every time the realisability check fails. For example, existing work on enforcing CP realisability such as the one given in (Gu¨demann et al. 2012) and recently on CP repairability (Basu and Bultan 2016) can be used to ensure the realisability of an already updated CP. Our statement is different than existing work and it is as follows: an evolution is allowed if it does not violate the CP realisability. By doing so, we suggest a priori verification approach of CP evolution. Instead of running the full realisability checking as described previously and detailed in Section 2, our proposal consists in performing partial verification uniquely at the CP level in order to answer the question if there still exist a set of peers implementing the updated CP. In this work, we consider the evolution at the CP level and we study its realisability effect on the distributed peers. The main issue is considering that system specifications may change over time (e.g., service upgrade or degrade by adding and/or removing either messages exchanges or interacting peers), how can we ensure realisability preservation? to answer these questions, we proceed as follows: We first describe CP using LTS We rely on the realisability condition given in (Basu et al. 2012) We identify the set of behavioural properties which can hold by CP evolution yet they violate the realisability condition We suggest a set of evolution patterns and we show how the application of such patterns do not violate CP realisability We propose a language for correct CP evolution The remainder of this paper is structured as follows: Section 2 introduces the formal definitions and the background on which our proposal relies. Section 3 presents the behavioural properties to be checked before application of CP evolution. In Section 4, we suggest an algebra for CP evolution with no violation of realisability. We present in Section 5 a case study to illustrate our approach. Section 6 overviews related work. Lastly, we conclude our work and present some perspectives in Section 7.

2. DEFINITIONS

In this section, we present our behavioural model for peers and CP. We, then, define how distributed peers can be obtained by projection from a given CP. Lastly, we define synchronisable systems, and we present realisability condition considering asynchronous communication.

2.1. Peer Model

We use Labeled Transition Systems (LTSs) for modelling the CP and the peers included in that specification. This behavioural model defines the order of sent messages in CP. At the peers level, the LTS can be computed by projection from CP and they describe the order in which those peers execute their send and receive actions.

Definition 1 (Peer) A peer is an LTS P = (S; s0; ; T ) where S is a finite set of states, s0 2 S is the initial state, = ! [ ? [ f g is a finite alphabet partitioned into a set of send messages, receive messages, and the internal action, and T S S is a transition relation.

We write m! for a send message m 2 ! and m? for

a receive message m 2 ?. We use the symbol (tau in figures) for representing internal activities. A transition is represented as s !l s0 where l 2 . Example 1 The right side of Figure 1 shows an example of three peers LTSs. synchronous system (P1 j : : : j Pn) is the LTS (S; s0; ; T ) where: Definition 2 (Conversation Protocol : CP) A con- (interact) s m! s0 2 T if 9i; j 2 f1; : : : ; ng : m 2 !i \ j? versation protocol CP for a set of peers fP1; : : : ; Png where 9 si m!! s0i 2 Ti, and sj m!? s0j 2 Tj is an LTS CP =< SCP ; s0CP ; LCP ; TCP > where SCP such that 8k 2 f1; : : : ; ng; k 6= i ^ k 6= j ) s0k = is a finite set of states and s0CP 2 SCP is the initial sk state; LCP is a set of labels where a label l 2 LCP is denoted mPi;Pj such that Pi and Pj are the sending 2.3. Asynchronous Composition and receiving peers, respectively, Pi 6= Pj, and m is a message on which those peers interact; finally, TCP SCP LCP SCP is the transition relation.

We require that each message has a unique sender and receiver: 8(Pi; m; Pj); (Pi0; m0; Pj0) 2 LCP : m = m0 =) Pi = Pi0 ^ Pj = Pj0.

In the remainder of this paper, we denote a transition t 2 TCP as s mPi;P!j s0 where s and s0 are source and target states and mPi;Pj is the transition label.

Example 2 The left side of Figure 1 shows an example of CP LTS.

Definition 3 (Projection) Peer LTSs Pi =< Si; si0; i; Ti > are obtained by replacing in CP =< SCP ; s0CP ; LCP ; TCP > each label (Pj; m; Pk) 2 LCP with m! if j = i with m? if k = i and with (internal action) otherwise; and finally removing the -transitions by applying standard minimisation algorithms Hopcroft and Ullman (1979) .

Example 3 Notice that the peers on Figure 1 are obtained by projection from the CP shown on left side of the same Figure.

2.2. Synchronous Composition

The synchronous composition of a set of peers corresponds to the system in which the peer LTSs communicate using synchronous communication. In this context, a communication between two peers occurs if both agree on a synchronisation label, i.e., if one peer is in a state in which a message can be sent, then the other peer must be in a state in which that message can be received. One peer can evolve independently from the others through an internal action.

Definition 4 (Synchronous System) Given a set of peers fP1; : : : ; Png with Pi = (Si; si0; i; Ti), the T S S, and for s = (s1; : : : ; sn) 2 S and s0 = (s01; : : : ; s0n) 2 S In the asynchronous composition, the peers communicate with each other asynchronously through FIFO buffers. Each peer Pi is equipped with an unbounded message buffer Qi. A peer can either send a message m 2 ! to the tail of the receiver buffer Qj at any state where this send message is available, read a message m 2 ? from its buffer Qi if the message is available at the buffer head, or evolve independently through an internal action. Since reading from the buffer is not considered as an observable action, it is encoded as an internal action in the asynchronous system.

Definition 5 (Asynchronous Composition) Given a set of peers fP1; : : : ; Png with Pi = (Si; si0; i; Ti), and Qi being its associated buffer, the asynchronous composition ((P1; Q1) jj : : : jj (Pn; Qn)) is the labeled transition system LT Sa = (Sa; s0a; a; Ta) where: 1. Sa S1 Q1 : : : Sn f1; : : : ; ng; Qi ( i?) Qn where 8i 2 2. s0a 2 Sa such that s0a = (s01; ; : : : ; s0n; ) (where denotes an empty buffer) 3. a = [i i 4. Ta Sa a Sa, and for s = (s1; Q1; : : : ; sn; Qn) 2 Sa and s0 = (s01; Q01; : : : s0n; Q0n) 2 Sa (send) sf1; : : : ;m!n!g whesr0e i 6=2 j : Tma if29i; j!i \ j?2, (i) si m!! s0i 2 Ti, (ii) Q0j = Qjm, (iii) 8k 2 f1; : : : ; ng : k 6= j ) Q0k = Qk, and (iv) 8k 2 f1; : : : ; ng : k 6= i ) s0k = sk (consume) s ! s0 2 Ta if 9i 2 f1; : : : ; ng : m 2 i?, (i) si m!? s0i 2 Ti, (ii) mQ0i = Qi, (iii) 8k 2 f1; : : : ; ng : k 6= i ) Q0k = Qk, and (iv) 8k 2 f1; : : : ; ng : k 6= i ) s0k = sk (internal) s ! s0 2 Ta if 9i 2 f1; : : : ; ng, (i) si ! s0i 2 Ti, (ii) 8k 2 f1; : : : ; ng : Q0k = Qk, and (iii) 8k 2 f1; : : : ; ng : k 6= i ) s0k = sk We use LT Sak to define the bounded asynchronous composition, where each message buffer is bounded to size k. The definition of LT Sak can be obtained from Def. 5 such that the maximum number of send messages that can be stored in the buffers is limited to k. A system is synchronizable (Basu et al. 2012) when its behavior remains the same under both synchronous and asynchronous communication semantics. This is checked by bounding buffers to k = 1 and comparing interactions in the synchronous system with send messages in the asynchronous system.

Definition 6 (Synchronizability) Given a set of peers fP1; : : : ; Png, the synchronous system (P1 j : : : j Pn) = (Ss; ss0; Ls; Ts), and the 1-bounded asynchronous system ((P1; Q11) jj : : : jj (Pn; Q1n)) = (Sa; s0a; La; Ta), two states r 2 Ss and s 2 Sa are synchronizable if there exists a relation Sync such that Sync(r; s) and: for each r m! r0 2 Ts, there exists s m!! s0 2 Ta, such that Sync(r0; s0); for each s m!! s0 2 Ta, there exists r m! r0 2 Ts, such that Sync(r0; s0); for each s m!? s0 2 Ta, Sync(r; s0).

The set of peers is synchronizable if Sync(ss0; s0a). Example 4 The system described in Figure 1 is not synchronisable because peer 1 can send “a” and “c” in sequence in the asynchronous system, whereas “b” occurs before “c” in the synchronous system as specified in the CP.

In order to check CP realisability, there is a need to check well-formedness. Well-formedness states that whenever the i-th peer buffer Qi is nonempty, the system can eventually move to a state where Qi is empty. For every synchronizable set of peers, if the peers are deterministic, i.e., for every state, the possible send messages are unique, wellformedness is implied.

The approach presented in Basu et al. (2012) proposes a sufficient and necessary condition showing that the realizability of conversation protocols is decidable.

Definition 7 (Realizability) A conversation protocol CP is realizable if and only if (i) the peers computed by projection from this protocol are synchronizable, (ii) the 1-bounded system resulting from the peer composition is well-formed, and (iii) the synchronous version of the distributed system fP1; : : : ; Png is equivalent to CP.

In the remainder of this paper, we refer to a realisable CP as R(CP).

Both synchronizability and realizability properties can be checked automatically using equivalence checking as done in Basu et al. (2012) . This check requires the modification of the asynchronous system for hiding receptions (m? ), renaming emissions into interactions (m! m), and removing transitions using standard minimization techniques. The correctness of that approach is given in (Farah et al. 2016) .

3. BEHAVIOURAL PROPERTIES

In order to check the realisability of a CP that has been updated, we must ensure that the resulting LTS does not hold some branching and/or sequential structures which violate realisability condition. We define in the following some properties which enable us to check such structures.

3.1. Branches related Properties Property 1 (Non-Deterministic Choice (NDC))

Given a conversation protocol CP =< SCP ; s0CP ; LCP ; TCP >, a state sCP 2 SCP is called non-deterministic branching state if : 9fsCP mPi;P!j s0CP , sCP mPi;P!j s0C0 P g and TCP , s0CP 6= s0C0 P This choice is referred to as non-deterministic choice.

We define in the following divergent choice (this is also called non-local branching choice in the literature) and it is different than process divergence (Ben-Abdallah and Leue 1997) . Property 2 (Divergent-Choice) Given a conversation protocol CP =< SCP ; s0CP ; LCP ; TCP >, a state sCP 2 SCP is divergent branching state if : and 9fs mPi;P!j s0CP , sCP m0Pj;P!i s0C0 P g TCP , s0CP 6= s0C0 P , and m 6= m0 This choice is referred to as divergent choice.

3.2. Sequences related Properties

Given a CP, there is at least two partitions of peers where there exist no interaction between both partitions.

Property 3 (Independent Sequences (ISeq)) Given a conversation protocol CP =< SCP ; s0CP ; LCP ; TCP >, a transition sequence mPi;Pj m0Pk;Pq sCP ! : : : s0CP ! s0C0 P , where all transitions are in TCP , is called independent sequence if:

fPi; Pjg \ fPk; Pqg = ? The following property enables us to detect sequences in CP which lead to non-local emission choices made by two different peers in the distributed system. To avoid that situation, every peer that join the conversation at an intermediate state (i.e., different than the initial state) must be receiver the first time it shows up. Otherwise, if a peer would like to send a message m at an intermediate state, then this must be receiver in its last interaction before sending m.

Property 4 (Divergent Sequences (DSeq)) Given a CP, there exists a transition sequence s0CP mPi;P!j : : : s0CP m0Pk;P!q s0C0 P where all transitions are in TCP : for every sender peer Pt appearing before state s0CP , t 6= k, or there is at least a transition sCP mPk;P!t s0C00P 2 TCP such that: s0C00P : : : s0 receiver. – s0CP is reachable from sCP , and – there is no transition in sCP mPk;P!t m0Pk;Pq ! s0C0 P where Pk is

4. COMPOSITIONAL REALISABILITY

CP evolution stands for two possible tasks, namely, adding and/or removing either messages and/or interacting peers. We define here how CP realisability can be preserved by applying some evolution patterns presented in the following.

4.1. Evolution Patterns

We introduce in this paper two composition operators denoted as (+;sCP) for branching composition and ( ;sCP) for sequential composition. We also assume other operators not presented here for lack of space, namely, (k;sCP) for parallel composition, and ( ;sCP) for looping composition. The operator

(k;sCP) generates at a state sCP all the interleaved behaviour of a set of transitions such that every generated branch must satisfy sequence related properties. The operator ( ;sCP) enables us to add self-loop of the form s mPi;P!j s where i 6= j and such that sequence related properties must be preserved.

Definition 8 ( ;sCP) Given a CP =< SCP ; s0CP ; LCP ; TCP >, a CP 0 =< SCP0; s0CP0; LCP0; TCP0 > and a state sCP 2 SCP , the sequential composition ( ;sCP)(CP; CP 0) means that CP must be executed before CP 0 such that Properties 3 and 4 do not hold.

Definition 9 (+;sCP) Given a CP =< SCP ; s0CP ; LCP ; TCP >, a set fCPi0g, i = 1::n such that CPi0 =< SCPi0; s0CPi0; LCPi0; TCPi0 > and a state sCP 2 SCP , the branching composition (+;sCP)(CP; fCP10; : : : ; CPn0 g) means that there is a choice at sCP between the remaining behaviour of CP (i.e., starting from sCP ) and all CPi0 such that: Properties 1 and 2 do not hold at the state sCP , and 8CPi0; ( ;sCP)(CP; CPi0) holds Remark 1 The application of an operator (op;sCP)(CP; CP0) assumes that the initial state of CP0 is fused with the state sCP . 4.2. Algebra for CP Evolution: syntax and language We introduce in Listing 1 a CP algebra which we use for defining the evolution such that realisability is preserved. We refer to a state sf as final if there is no outgoing transition at that state. We denote by ECP a CP that evolutes over time while preserving realisability. The expression ECP+ stands for one or more ECP.

ECP ::= ECPb j ECP op ECPb+ ECPb ::= s (Pi;m;Pj!) s0 j ? op ::= (+;sf) j ( ;sf) j (k;sf) j ( ;sf)

Listing 1: CP Evolution Grammar

4.3. Realisable CP Evolution

Conjecture 1 ECPb is realisable.

Proof 1 This is obvious by default.

Conjecture 2 Given an ECP =< SECP ; s0ECP ; LECP ; TECP > and a ECPb such that R(ECP) and R(ECPb), sf 2 SECP , then R( ( ;sf )(ECP ; ECPb )) (1) Sketch 1 This follows from Definition 7 and Properties 3 and 4. .

Conjecture 3 Given an ECP =< SECP ; s0ECP ; LECP ; TECP > and a set of n 2 N ECPbi (i 2 [0::n 1]) such that R(ECP ) and R(ECPb ), sf 2 SECP , then

R( (+;sf )(ECP ; fECPb0 ; : : : ; ECPbn 1 g)) (2) Sketch 2 This follows from Definition 7 and Properties 1 and 2.

We denote by zE}C|P{ the set of all conversation

protocols resulting from any evolution and such that the realisability is preserved. zE}C|P{ can be obtained by inductive composition using the aforementioned operators and the grammar.

Definition 10 (Correct Evolution) Given a CP and n CPb where n 2 N , CPbi stands for the ith CPb such that i 2 [0::n 1], and R(CP ), then: zE}C|P{ = fECP j 8opj ; j 2 [0::n]; opj 2 OP;

ECP = op0 : : : opn(CP CPb0 : : : CPbn 1 ) g In the evolution context, an initial CP can be updated into an ECP if and only if ECP 2 zE}C|P{.

We generalise in the following the result given previously in this section.

Conjecture 4

R(CP ) R(CPb); op 2 OP R(op(CP;CPb)) 8ECP 2 zE}C|P{; R(ECP ) (3) Sketch 3 It follows from Conjectures 1, 2, and 3 and Definition 10.

5. CASE STUDY

5.1. Toy Example

This section shows some examples to better understand our proposal. We first give an illustration of CP evolution using a toy example where an initial CP and a possible evolution of that CP are shown on Figures 2 and 3, respectively. Notice that the added behaviour is presented with dashed transitions on Figure 3. Valid Evolution. In this example, the evolution is valid and can be applied since it is possible to generate ECP by application of the set of production rules from the evolution grammar (Listing 1) as follows. we try to rewrite ECP starting from the initial state of CP: CP = s0 CPb0 = s1 CPb1 = s1 CPb2 = s2 CPb3 = s3 m1P 1;P 2

! s1 m2P 2;P 1

! s2 m3P 2;P 3

! s3 m4P 2;P 3

! s4 m5P 3;P 1

! s4 Production Rules for toy ECP ECP =

( ;s3)( ( ;s2) (

(+;s1)(CP ; fCPb0 ; CPb1 g) ; CP b2)

CP b3) For illustration purposes we specify the use of an application in the cloud. This system involves four peers: a client (cl), a Web interface (int), a software application (appli), and a database (db). We show first a conversation protocol (Figure 4) describing the requirements that the designer expects from the composition-to-be. The conversation protocol starts with a login interaction (connect) between the client and the interface, followed by the access request (access) triggered by the client. This request can be repeated as far as necessary. Finally, the client decides to logout from the interface (logout) Invalid Evolution. We show on Figure 6 an updated version of the CP given on Figure 4 describing the new requirements that the designer expects from the composition-to-be. The conversation protocol starts with a login interaction (connect) between the client and the interface, followed by the setup of the application triggered by the interface (setup). Then, the client can access and use the application as far as necessary (access). Finally, the client decides to logout from the interface (logout) and the application stores some information (start/end time, used resources, etc.) into a database (log). Figure 7 shows the four peers obtained by projection. This set of peers seems to respect the behaviour specified in the conversation protocol, yet this is difficult to be sure using only visual analysis, even for such a simple example. In addition, as the CP involves looping behaviour, it is hard to know whether the resulting distributed system is bounded and finite, which would allow its formal analysis using existing verification techniques. Actually, this set of peers is not synchronisable (and therefore not realisable), because the trace of send messages “connect, access” is present in the 1-bounded asynchronous system, but is not present in the synchronous system. Synchronous communication enforces the sequence “connect, setup, access” as specified in the CP , whereas in the asynchronous system peer cl can send connect! and access! in sequence.

This kind of evolution resulting in non realisable CP can be avoided using our method with no need of CP projection. Starting from the initial state of CP that is shown on Figure 4 and using the grammar given in Listing 1, there is no way to generate the interaction sequence “connect, setup, access” because adding “access” interaction violates Property 4.

6. RELATED WORK

Studying the evolution of software systems is not a new topic in itself. For instance, as stated in (Roohi and Salau¨ n 2011) , dynamic reconfiguration (Medvidovic 1996) is dealt with in the context of distributed systems and software architectures, graph transformation, software adaptation, or metamodelling. However, these do not study systems where their interaction is described with conversation protocols. In this section we restrict our study to the related approaches focusing on the evolution of conversation protocols. (Leite et al. 2013) surveys the approaches working on Web service evolution until 2013. Our study of that work shows that the most related proposals are (Roohi and Salau¨ n 2011; Wombacher 2009; Jureta et al. 2007; Rinderle et al. 2006a,b) . (Roohi and Salau¨ n 2011) suggest a method to check CP reconfigurability. The authors consider two CPs, namely, an initial CP and a new CP 0 and two sets of peers PS and PS 0 obtained by projection from both CPs, respectively. Given a trace t in CP which consists in the history of the current execution (i.e., the sequence of interactions held between the peers), if t can also be executed in reconfigured peers generated from CP 0, then the reconfiguration can take place.

Wombacher (2009) uses a formal model based on annotated Finite State Automata (aFSA) to describe Web service interaction and which is specified using choreography. This approach aligns changes between updated choreography and the correspondent orchestration. Given an updated choreography, the changes, namely, adding and/or removing sequences of messages are propagated into distributed peers. The proposed solution is implemented into DYCHOR framework and needs human validation. In (Rinderle et al. 2006a,b) , the authors propose a controlled evolution method where propagating the changes into one peer requires to check its effect on other partner peers. This approach is implemented into DYCHOR. In (Preda et al. 2015; Fdhila et al. 2015) , both approaches study the evolution that might arise at the peers side. The authors propagate the change from one peer to other partners. The work proposed in (Fdhila et al. 2015) applies to Business Process Management (BPM) domain and Service Oriented Architecture (SOA). It describes service choreographies using tree-based model. The authors consider some changes such as “replace, delete, update, and insert” of behavioural fragments. (Preda et al. 2015) define a new language referred to as DIOC for programming distributed applications that are free from deadlocks and races by construction. The semantics of DIOC language relies on labelled transition systems. The approach given in (Preda et al. 2015) enables to update fragment of codes of distributed peers. This can be specified at the choreography level where blocks of code that can be updated dynamically must be tagged using “scope”. These “scope” blocks have to be known a priori when describing the choreography. The solutions given in (Preda et al. 2015; Roohi and Salau¨n 2011; Jureta et al. 2007) deal with run-time evolution.

To the best of our knowledge, we are the first who verify the evolution at the CP level such that its realisability must be preserved. Furthermore, we have no restriction on the application domain, yet we use a formal model which can be applied for design, verification, and implementation of different distributed systems, e.g. Web services, concurrent systems, Cyber Physical Systems, etc. Our result applies also for asynchronously communicating systems as far as these are synchronisable with no restriction on the buffer size.

7. CONCLUSION AND PERSPECTIVES

In this paper, we presented a preliminary solution for correct evolution of distributed system for which their interaction is described with a conversation protocol. We proposed a language which enables one to incrementally design distributed system that can be updated over time such that their realisability is preserved while applying and composing evolution operators.

In the near future we aim at formalising all properties and composition operators used in this paper. We intend to prove that our evolution operators and their properties preserve CP realisability. Our conjectures have also to be formally proved. We aim also at defining looping and parallel operators as well as extending our language with new operators for messages broadcast and multicast. Lastly, we are using theorem proving techniques in order to prove the correctness of CP evolution. Based on proofbased techniques, we aim at handling any number of peers and exchanged messages such that scalability is ensured.

References

Basu , S. and T. Bultan ( 2016 ). Automated Choreography Repair. In Proc. of FASE'16 , Volume 9633 of LNCS , pp. 13 - 30 . Springer.

Basu , S. , T. Bultan , and M. Ouederni ( 2012 ). Deciding Choreography Realizability . In Proc. of POPL'12 , pp. 191 - 202 . ACM.

Ben-Abdallah , H. and S. Leue ( 1997 ). Syntactic Detection of Process Divergence and Non-local Choice in Message Sequence Charts . In Proc of TACAS'97 , Volume 1217 of Lecture Notes in Computer Science, pp. 259 - 274 . Springer.

Brand , D. and P. Zafiropulo ( 1983 ). On Communicating Finite-State Machines . J. ACM 30 ( 2 ), 323 - 342 .

Bultan , T. ( 2006 ). Modeling interactions of web software . In Proc. of WWV'06 , pp. 45 - 52 . IEEE.

Farah , Z. , Y. Ait-Ameur , M. Ouederni , and K. Tari ( 2016 ). A Correct-by-Construction Model for Asynchronously Communicating Systems . International Journal on Software Tools for Technology Transfer . To appear.

Fdhila , W., C. Indiono , S. Rinderle-Ma , and M. Reichert ( 2015 ). Dealing with change in process choreographies: Design and implementation of propagation algorithms . Information systems 49 , 1 - 24 .

Gu ¨demann, M., G. Salau¨n, and M. Ouederni ( 2012 ). Counterexample Guided Synthesis of Monitors for Realizability Enforcement . In Proc. of ATVA'12 , Volume 7561 of LNCS , pp. 238 - 253 . Springer.

Hopcroft , J. E. and J. D. Ullman ( 1979 ). Introduction to Automata Theory, Languages and Computation . Addison Wesley.

Jureta , I. J ., S. Faulkner , and P. Thiran ( 2007 ). Dynamic Requirements Specification for adaptable and open Service-oriented Systems . Springer.

Leite , L. A. , G. A. Oliva , G. M. Nogueira , M. A. Gerosa , F. Kon , and D. S. Milojicic ( 2013 ). A Systematic Literature Review of Service Choreography Adaptation . Service Oriented Computing and Applications 7 ( 3 ), 199 - 216 .

Medvidovic , N. ( 1996 ). ADLs and dynamic Architecture Changes . In Proc. of SIGSOFT'96 workshops , pp. 24 - 27 . ACM.

Preda , M. D. , M. Gabbrielli , S. Giallorenzo , I. Lanese , and J. Mauro ( 2015 ). Dynamic Choreographies - Safe Runtime Updates of Distributed Applications . In Proc. of COORDINATION'15 , Volume 9037 of LNCS , pp. 67 - 82 . Springer.

Rinderle , S. , A. Wombacher , and M. Reichert (2006a). Evolution of process choreographies in DYCHOR . In Proc. of CoopIS'06 , Volume 4275 of LNCS , pp. 273 - 290 . Springer.

Rinderle , S. , A. Wombacher , and M. Reichert (2006b). On the Controlled Evolution of Process Choreographies . In Proc. of ICDE'06 , pp. 124 - 124 . IEEE.

Roohi , N. and G. Salau¨n ( 2011 ). Realizability and Dynamic Reconfiguration of Chor Specifications . Informatica (Slovenia) 35 ( 1 ), 39 - 49 .

Ryu , S. H. , F. Casati , H. Skogsrud , B. Benatallah , and R. Saint-Paul ( 2008 ). Supporting the Dynamic Evolution of Web Service Protocols in Serviceoriented Architectures. ACM Transactions on the Web (TWEB) 2(2 ), 13 .

Wombacher , A. ( 2009 ). Alignment of Choreography Changes in BPEL Processes . In Proc. of SCC'09 , pp. 1 - 8 . IEEE.