=Paper=
{{Paper
|id=Vol-1689/paper16
|storemode=property
|title=Towards correct Evolution of Conversation Protocols
|pdfUrl=https://ceur-ws.org/Vol-1689/paper16.pdf
|volume=Vol-1689
|authors=Sarah Benyagoub,Meriem Ouederni,Yamine Ait Ameur
|dblpUrl=https://dblp.org/rec/conf/vecos/BenyagoubOA16
}}
==Towards correct Evolution of Conversation Protocols==
https://ceur-ws.org/Vol-1689/paper16.pdf
Towards correct Evolution of Conversation
Protocols
Sarah Benyagoub Meriem Ouederni Yamine Ait Ameur
University of Mostaganem IRIT-INP of Toulouse IRIT-INP of Toulouse
benyagoub.sarah@univ-mosta.dz meriem.ouederni@enseeiht.fr yamine@enseeiht.fr
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.
System Evolution, Realisability, Conversation Protocols, Formal Verification, Behavioural Systems
1. INTRODUCTION analysis of interaction properties, e.g., realisability
checking. Although it is obvious to check realisability
Distributed software systems change dynamically in the case of synchronous communication, this re-
due to the evolution of their running environment alisability problem remains undecidable in the most
and/or requirements, their internal designing poli- general setting (Brand and Zafiropulo 1983) due the
cies, and/or their possible specification bugs which possibly ever-increasing queuing mechanism and
must be fixed. Such systems are usually composed unbounded buffers in the case of asynchronous
of distributed software entities (called peers) evolving communication.
concurrently in a distributed setting and interacting
with each other throughout messages exchanges to The recent work of (Basu et al. 2012) proposed
fulfil a common goal. a necessary and sufficient condition for verifying
if a CP can be implemented by a set of peers
In a top-down design of distributed software, the communicating asynchronously throughout FIFO
interaction among peers is usually modelled using buffers with no restriction on their buffer sizes. This
collaboration diagrams, Message Sequence Chains work solves the realisability issue for a subclass of
(MSCs) or conversation protocols (CP) (Bultan asynchronously communicating peers, namely, the
2006). Let us focus on CPs, these describe synchronisable systems, i.e., the system composed
interactions among peers by describing uniquely the of interacting peers behaves equally by applying
allowed sequences of sent messages. Here, it is synchronous or asynchronous communication. A
crucial to know if the set of interactions in a CP CP is realisable if there exists a set of peers
can be implemented. In other word, considering a implementing that CP, i.e., they send messages to
CP, one must check whether there exists a set of each other in the same order as CP, and such
peers where their composition generates the same that their composition is synchronisable. In (Basu
sequences of send messages as specified by the CP. et al. 2012), the full checking of CP realisability
This issue characterises the realisability problem. applies the following steps: i) peer projection from
CP; ii) checking synchronisability; and iii) checking
In order to formally specify, verify, and fix issues equivalence between CP and its distributed system.
which violate realisability, CP can be modelled using
Labelled Transition Systems (LTSs) where commu- Based on LTS model, we can verify CP realisability
nication follows either synchronous or asynchronous using existing techniques such as model checking
semantics. Using this model enables automated for systems with reasonable sizes (Basu et al.
c The Authors. Published by BISL. 1
Proceedings of . . .
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
2012) (i.e., number of states, transitions and how can we ensure realisability preservation? to
communicating peers) or theorem proving for answer these questions, we proceed as follows:
scalable systems (Farah et al. 2016).
• We first describe CP using LTS
Considering realisable CPs, we are interested in
studying the evolution of those CPs. In fact, • We rely on the realisability condition given
these specify cross-organisational interactions with in (Basu et al. 2012)
no centralised control between peers which can • We identify the set of behavioural properties
be administrated and executed by geographically which can hold by CP evolution yet they violate
distributed and autonomous companies. In order the realisability condition
to cope with new environment changes and end-
user requirements, system interaction and the • We suggest a set of evolution patterns and we
corresponding CP need to evolve continuously over show how the application of such patterns do
time. However, changing CP might result in knock- not violate CP realisability
on effects on its realisability. Hence, verifying the
• We propose a language for correct CP
correctness of CP evolution to ensure realisability
evolution
preservation must also be run continuously.
The remainder of this paper is structured as follows:
Regarding the literature, existing work such
Section 2 introduces the formal definitions and the
as (Rinderle et al. 2006b; Ryu et al. 2008; Roohi
background on which our proposal relies. Section 3
and Salaün 2011) give some solutions for system
presents the behavioural properties to be checked
evolution. In (Rinderle et al. 2006b; Ryu et al.
before application of CP evolution. In Section 4,
2008) the authors propagate the choreography
we suggest an algebra for CP evolution with no
updates into communicating peers. (Roohi and
violation of realisability. We present in Section 5
Salaün 2011) focuses on system reconfiguration
a case study to illustrate our approach. Section 6
meaning that for a CP which has been updated into
overviews related work. Lastly, we conclude our work
CP’, the authors check whether the traces that has
and present some perspectives in Section 7.
been executed in CP can be performed again in
CP’. This reconfiguration can be better applied for
run-time system to ensure execution consistency. 2. DEFINITIONS
All these approaches do not consider realisability
preservation. In this section, we present our behavioural model
for peers and CP. We, then, define how distributed
There exist other research approaches which can peers can be obtained by projection from a given
be applied as a posteriori evolution checking. CP. Lastly, we define synchronisable systems,
The approaches suggest solutions every time the and we present realisability condition considering
realisability check fails. For example, existing work asynchronous communication.
on enforcing CP realisability such as the one given
in (Güdemann et al. 2012) and recently on CP 2.1. Peer Model
repairability (Basu and Bultan 2016) can be used to
ensure the realisability of an already updated CP. We use Labeled Transition Systems (LTSs) for
modelling the CP and the peers included in that
Our statement is different than existing work and specification. This behavioural model defines the
it is as follows: an evolution is allowed if it order of sent messages in CP. At the peers level, the
does not violate the CP realisability. By doing so, LTS can be computed by projection from CP and they
we suggest a priori verification approach of CP describe the order in which those peers execute their
evolution. Instead of running the full realisability send and receive actions.
checking as described previously and detailed in
Section 2, our proposal consists in performing partial Definition 1 (Peer) A peer is an LTS P =
verification uniquely at the CP level in order to (S, s0 , Σ, T ) where S is a finite set of states, s0 ∈ S is
answer the question if there still exist a set of the initial state, Σ = Σ! ∪ Σ? ∪ {τ } is a finite alphabet
peers implementing the updated CP. In this work, partitioned into a set of send messages, receive
we consider the evolution at the CP level and messages, and the internal action, and T ⊆ S ×Σ×S
we study its realisability effect on the distributed is a transition relation.
peers. The main issue is considering that system
specifications may change over time (e.g., service We write m! for a send message m ∈ Σ! and m? for
upgrade or degrade by adding and/or removing a receive message m ∈ Σ? . We use the symbol τ
either messages exchanges or interacting peers), (tau in figures) for representing internal activities. A
l
− s0 where l ∈ Σ.
transition is represented as s →
2
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
Example 1 The right side of Figure 1 shows an synchronous system (P1 | . . . | Pn ) is the LTS
example of three peers LTSs. (S, s0 , Σ, T ) where:
• S = S1 × . . . × Sn
• s0 ∈ S such that s0 = (s01 , . . . , s0n )
• Σ = ∪i Σi
• T ⊆ S × Σ × S, and for s = (s1 , . . . , sn ) ∈ S and
Figure 1: CP (left side), Peers (right side) s0 = (s01 , . . . , s0n ) ∈ S
m
(interact) s −→ s0 ∈ T if ∃i, j ∈ {1, . . . , n} : m ∈ Σ!i ∩ Σ?j
Definition 2 (Conversation Protocol : CP) A con- m! m?
versation protocol CP for a set of peers {P1 , . . . , Pn } where ∃ si −−→ s0i ∈ Ti , and sj −−→ s0j ∈ Tj
is an LTS CP =< SCP , s0CP , LCP , TCP > where SCP such that ∀k ∈ {1, . . . , n}, k 6= i ∧ k 6= j ⇒ s0k =
is a finite set of states and s0CP ∈ SCP is the initial sk
state; LCP is a set of labels where a label l ∈ 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, In the asynchronous composition, the peers com-
TCP ⊆ SCP × LCP × SCP is the transition relation. municate with each other asynchronously through
We require that each message has a unique sender FIFO buffers. Each peer Pi is equipped with an
and receiver: ∀(Pi , m, Pj ), (Pi0 , m0 , Pj0 ) ∈ LCP : m = unbounded message buffer Qi . A peer can either
m0 =⇒ Pi = Pi0 ∧ Pj = Pj0 . send a message m ∈ Σ! to the tail of the receiver
buffer Qj at any state where this send message is
In the remainder of this paper, we denote a transition available, read a message m ∈ Σ? from its buffer
mPi ,Pj Qi if the message is available at the buffer head,
t ∈ TCP as s −−−−−→ s0 where s and s0 are source or evolve independently through an internal action.
and target states and mPi ,Pj is the transition label. Since reading from the buffer is not considered as an
observable action, it is encoded as an internal action
Example 2 The left side of Figure 1 shows an in the asynchronous system.
example of CP LTS.
Definition 5 (Asynchronous Composition) Given
Definition 3 (Projection) Peer LTSs Pi =<
a set of peers {P1 , . . . , Pn } with Pi = (Si , s0i , Σi , Ti ),
Si , s0i , Σi , Ti > are obtained by replacing in
CP =< SCP , s0CP , LCP , TCP > each label and Qi being its associated buffer, the asynchronous
(Pj , m, Pk ) ∈ LCP with m! if j = i with m? if composition ((P1 , Q1 ) || . . . || (Pn , Qn )) is the
k = i and with τ (internal action) otherwise; labeled transition system LT Sa = (Sa , s0a , Σa , Ta )
and finally removing the τ -transitions by applying where:
standard minimisation algorithms Hopcroft and
Ullman (1979). 1. Sa ⊆ S1 × Q1 × . . . × Sn × Qn where ∀i ∈
{1, . . . , n}, Qi ⊆ (Σ?i )∗
Example 3 Notice that the peers on Figure 1 are
obtained by projection from the CP shown on left 2. s0a ∈ Sa such that s0a = (s01 , , . . . , s0n , ) (where
side of the same Figure. denotes an empty buffer)
3. Σa = ∪i Σi
2.2. Synchronous Composition
4. Ta ⊆ Sa × Σa × Sa , and for s =
The synchronous composition of a set of peers (s1 , Q1 , . . . , sn , Qn ) ∈ Sa and s0 =
corresponds to the system in which the peer LTSs (s01 , Q01 , . . . s0n , Q0n ) ∈ Sa
communicate using synchronous communication. In
m!
this context, a communication between two peers (send) s −−→ s0 ∈ Ta if ∃i, j ∈
occurs if both agree on a synchronisation label, i.e., {1, . . . , n} where i 6= j : m ∈ Σ!i ∩ Σ?j ,
if one peer is in a state in which a message can be m!
(i) si −−→ s0i ∈ Ti , (ii) Q0j = Qj m,
sent, then the other peer must be in a state in which (iii) ∀k ∈ {1, . . . , n} : k 6= j ⇒ Q0k = Qk ,
that message can be received. One peer can evolve and (iv) ∀k ∈ {1, . . . , n} : k 6= i ⇒ s0k = sk
independently from the others through an internal τ
action. → s0 ∈ Ta if ∃i ∈ {1, . . . , n} : m ∈
(consume) s −
m?
Σ?i , (i) si −−→ s0i ∈ Ti , (ii) mQ0i = Qi ,
Definition 4 (Synchronous System) Given a set of (iii) ∀k ∈ {1, . . . , n} : k 6= i ⇒ Q0k = Qk ,
peers {P1 , . . . , Pn } with Pi = (Si , s0i , Σi , Ti ), the and (iv) ∀k ∈ {1, . . . , n} : k 6= i ⇒ s0k = sk
3
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
τ τ
(internal) s −→ s0 ∈ Ta if ∃i ∈ {1, . . . , n}, (i) si − → composition is well-formed, and (iii) the synchronous
si ∈ Ti , (ii) ∀k ∈ {1, . . . , n} : Q0k = Qk ,
0
version of the distributed system {P1 , . . . , Pn } is
and (iii) ∀k ∈ {1, . . . , n} : k 6= i ⇒ s0k = sk equivalent to CP .
We use LT Sak to define the bounded asynchronous In the remainder of this paper, we refer to a realisable
composition, where each message buffer is bounded CP as R(CP).
to size k. The definition of LT Sak can be obtained
from Def. 5 such that the maximum number of send Both synchronizability and realizability properties
messages that can be stored in the buffers is limited can be checked automatically using equivalence
to k. A system is synchronizable (Basu et al. 2012) checking as done in Basu et al. (2012). This check
when its behavior remains the same under both requires the modification of the asynchronous sys-
synchronous and asynchronous communication tem for hiding receptions (m? τ ), renaming emis-
semantics. This is checked by bounding buffers to sions into interactions (m! m), and removing τ -
k = 1 and comparing interactions in the synchronous transitions using standard minimization techniques.
system with send messages in the asynchronous The correctness of that approach is given in (Farah
system. et al. 2016).
Definition 6 (Synchronizability) Given a set of
3. BEHAVIOURAL PROPERTIES
peers {P1 , . . . , Pn }, the synchronous system (P1 |
. . . | Pn ) = (Ss , s0s , Ls , Ts ), and the 1-bounded In order to check the realisability of a CP that has
asynchronous system ((P1 , Q11 ) || . . . || (Pn , Q1n )) = been updated, we must ensure that the resulting
(Sa , s0a , La , Ta ), two states r ∈ Ss and s ∈ Sa are LTS does not hold some branching and/or sequential
synchronizable if there exists a relation Sync such structures which violate realisability condition. We
that Sync(r, s) and: define in the following some properties which enable
m m! us to check such structures.
• for each r −→ r0 ∈ Ts , there exists s −−→ s0 ∈
Ta , such that Sync(r0 , s0 ); 3.1. Branches related Properties
m! m
• for each s −−→ s0 ∈ Ta , there exists r −→ r0 ∈ Property 1 (Non-Deterministic Choice (NDC))
Ts , such that Sync(r0 , s0 ); Given a conversation protocol CP =<
m?
SCP , s0CP , LCP , TCP >, a state sCP ∈ SCP is
• for each s −−→ s0 ∈ Ta , Sync(r, s0 ). called non-deterministic branching state if :
The set of peers is synchronizable if Sync(s0s , s0a ). mPi ,Pj mPi ,Pj
• ∃{sCP −−−−−→ s0CP , sCP −−−−−→ s00CP } ⊆ TCP ,
and
Example 4 The system described in Figure 1 is not
synchronisable because peer 1 can send “a” and “c” • s0CP 6= s00CP
in sequence in the asynchronous system, whereas
“b” occurs before “c” in the synchronous system as This choice is referred to as non-deterministic
specified in the CP. choice.
In order to check CP realisability, there is a need We define in the following divergent choice (this
to check well-formedness. Well-formedness states is also called non-local branching choice in
that whenever the i-th peer buffer Qi is non- the literature) and it is different than process
empty, the system can eventually move to a state divergence (Ben-Abdallah and Leue 1997).
where Qi is empty. For every synchronizable set of
peers, if the peers are deterministic, i.e., for every Property 2 (Divergent-Choice) Given a conversa-
state, the possible send messages are unique, well- tion protocol CP =< SCP , s0CP , LCP , TCP >, a state
formedness is implied. sCP ∈ SCP is divergent branching state if :
The approach presented in Basu et al. (2012) mPi ,Pj m0Pj ,Pi
• ∃{s −−−−−→ s0CP , sCP −−−−−→ s00CP } ⊆ TCP ,
proposes a sufficient and necessary condition
and
showing that the realizability of conversation
protocols is decidable. • s0CP 6= s00CP , and
Definition 7 (Realizability) A conversation protocol • m 6= m0
CP is realizable if and only if (i) the peers computed
by projection from this protocol are synchronizable, This choice is referred to as divergent choice.
(ii) the 1-bounded system resulting from the peer
4
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
3.2. Sequences related Properties ⊗(k,sCP ) generates at a state sCP all the interleaved
behaviour of a set of transitions such that every
Given a CP, there is at least two partitions of generated branch must satisfy sequence related
peers where there exist no interaction between both properties. The operator ⊗(,sCP ) enables us to add
partitions. mPi ,Pj
self-loop of the form s −−−−−→ s where i 6= j
Property 3 (Independent Sequences (ISeq)) and such that sequence related properties must be
Given a conversation protocol CP =< preserved.
SCP , s0CP , LCP , TCP >, a transition sequence
mPi ,Pj m0Pk ,Pq
Definition 8 ⊗( ,sCP ) Given a CP =<
sCP −−−−−→ . . . s0CP −−−−−→ s00CP , where all SCP , s0CP , LCP , TCP >, a CP 0 =<
transitions are in TCP , is called independent SCP 0 , s0CP 0 , LCP 0 , TCP 0 > and a state sCP ∈ SCP , the
sequence if: sequential composition ⊗( ,sCP ) (CP, CP 0 ) means
that CP must be executed before CP 0 such that
• {Pi , Pj } ∩ {Pk , Pq } = ∅ Properties 3 and 4 do not hold.
The following property enables us to detect Definition 9 ⊗(+,sCP ) Given a CP =<
sequences in CP which lead to non-local emission SCP , s0CP , LCP , TCP >, a set {CPi0 }, i = 1..n
choices made by two different peers in the distributed such that CPi0 =< SCPi0 , s0CP 0 , LCPi0 , TCPi0 > and
system. To avoid that situation, every peer that i
a state sCP ∈ SCP , the branching composition
join the conversation at an intermediate state (i.e.,
⊗(+,sCP ) (CP, {CP10 , . . . , CPn0 }) means that there is a
different than the initial state) must be receiver the
choice at sCP between the remaining behaviour of
first time it shows up. Otherwise, if a peer would
CP (i.e., starting from sCP ) and all CPi0 such that:
like to send a message m at an intermediate state,
then this must be receiver in its last interaction before • Properties 1 and 2 do not hold at the state sCP ,
sending m. and
Property 4 (Divergent Sequences (DSeq)) • ∀CPi0 , ⊗( ,sCP ) (CP, CPi0 ) holds
Given a CP, there exists a transition sequence
mPi ,Pj m0Pk ,Pq Remark 1 The application of an operator
s0CP −−−−−→ . . . s0CP −−−−−→ s00CP where all ⊗(op,sCP ) (CP , CP 0 ) assumes that the initial state of
transitions are in TCP : CP 0 is fused with the state sCP .
• for every sender peer Pt appearing before state 4.2. Algebra for CP Evolution: syntax and
s0CP , t 6= k, or language
mPk ,Pt
• there is at least a transition sCP −−−−−→ s000
CP ∈ We introduce in Listing 1 a CP algebra which we
TCP such that: use for defining the evolution such that realisability
– s0CP is reachable from sCP , and is preserved. We refer to a state sf as final if there
is no outgoing transition at that state. We denote by
mPk ,Pt
– there is no transition in sCP −−−−−→ ECP a CP that evolutes over time while preserving
s000 0 m0Pk ,Pq
−−−−−→ s00CP where Pk is realisability. The expression ECP + stands for one or
CP . . . s
receiver. more ECP .
ECP ::= ECPb | ECP op ECPb +
4. COMPOSITIONAL REALISABILITY
(Pi ,m,Pj )
ECPb ::= s −−−−−−→ s0 | ∅
CP evolution stands for two possible tasks,
namely, adding and/or removing either messages op ::= ⊗(+,sf ) | ⊗( ,sf ) | ⊗(k,sf ) | ⊗(,sf )
and/or interacting peers. We define here how CP
realisability can be preserved by applying some Listing 1: CP Evolution Grammar
evolution patterns presented in the following.
4.3. Realisable CP Evolution
4.1. Evolution Patterns
Conjecture 1 ECPb is realisable.
We introduce in this paper two composition opera-
tors denoted as ⊗(+,sCP ) for branching composition Proof 1 This is obvious by default.
and ⊗( ,sCP ) for sequential composition. We also
assume other operators not presented here for lack Conjecture 2 Given an ECP =<
of space, namely, ⊗(k,sCP ) for parallel composition, SECP , s0ECP , LECP , TECP > and a ECPb such
and ⊗(,sCP ) for looping composition. The operator that R(ECP ) and R(ECPb ), sf ∈ SECP , then
5
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
behaviour is presented with dashed transitions on
R(⊗( ,sf ) (ECP , ECPb )) (1) Figure 3.
Sketch 1 This follows from Definition 7 and Proper-
ties 3 and 4. .
Conjecture 3 Given an ECP =< Figure 2: Toy CP
SECP , s0ECP , LECP , TECP > and a set of n ∈ N
ECPbi (i ∈ [0..n − 1]) such that R(ECP ) and
R(ECPb ), sf ∈ SECP , then
R(⊗(+,sf ) (ECP , {ECPb0 , . . . , ECPbn−1 })) (2)
Figure 3: Toy ECP
Sketch 2 This follows from Definition 7 and Proper-
ties 1 and 2.
Valid Evolution. In this example, the evolution is
z }| { valid and can be applied since it is possible to
We denote by ECP the set of all conversation generate ECP by application of the set of production
protocols resulting from any evolution and such that rules from the evolution grammar (Listing 1) as
z }| {
the realisability is preserved. ECP can be obtained follows. we try to rewrite ECP starting from the initial
by inductive composition using the aforementioned state of CP:
operators and the grammar. mP 1,P 2
1
CP = s0 −−− −−→ s1
Definition 10 (Correct Evolution) Given a CP and
mP 2,P 1
n CPb where n ∈ N , CPbi stands for the ith CPb 2
CPb0 = s1 −−− −−→ s2
such that i ∈ [0..n − 1], and R(CP ), then:
3 mP 2,P 3
z }| { CPb1 = s1 −−− −−→ s3
ECP = {ECP | ∀opj , j ∈ [0..n], opj ∈ OP,
4 mP 2,P 3
CPb2 = s2 −−− −−→ s4
ECP = op0 . . . opn (CP CPb0 . . . CPbn−1 )
5 mP 3,P 1
} CPb3 = s3 −−− −−→ s4
In the evolution context, an initial CP can be updated Production Rules for toy ECP
z }| {
into an ECP if and only if ECP ∈ ECP . ECP = ⊗( ,s3) (
We generalise in the following the result given ⊗( ,s2) (
previously in this section.
⊗(+,s1) (CP , {CPb0 , CPb1 })
Conjecture 4
R(CP ) , CP b2 )
R(CPb ), op ∈ OP R(op(CP,CP b ))
(3)
CP b3 )
z }| {
∀ECP ∈ ECP , R(ECP )
Sketch 3 It follows from Conjectures 1, 2, and 3
5.2. Real Example
and Definition 10.
For illustration purposes we specify the use of an
5. CASE STUDY application in the cloud. This system involves four
peers: a client (cl), a Web interface (int), a software
5.1. Toy Example application (appli), and a database (db). We show
first a conversation protocol (Figure 4) describing
This section shows some examples to better the requirements that the designer expects from the
understand our proposal. We first give an illustration composition-to-be. The conversation protocol starts
of CP evolution using a toy example where an initial with a login interaction (connect) between the client
CP and a possible evolution of that CP are shown on and the interface, followed by the access request
Figures 2 and 3, respectively. Notice that the added (access) triggered by the client. This request can
6
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
be repeated as far as necessary. Finally, the client
decides to logout from the interface (logout)
Figure 7: Peers Projection from CP on Figure 4
Figure 4: A realisable 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
Figure 5: Peers Projection from CP in Figure 4
Studying the evolution of software systems is not a
Invalid Evolution. We show on Figure 6 an updated new topic in itself. For instance, as stated in (Roohi
version of the CP given on Figure 4 describing the and Salaün 2011), dynamic reconfiguration (Medvi-
new requirements that the designer expects from dovic 1996) is dealt with in the context of distributed
the composition-to-be. The conversation protocol systems and software architectures, graph trans-
starts with a login interaction (connect) between the formation, software adaptation, or metamodelling.
client and the interface, followed by the setup of However, these do not study systems where their
the application triggered by the interface (setup). interaction is described with conversation protocols.
Then, the client can access and use the application In this section we restrict our study to the related ap-
as far as necessary (access). Finally, the client proaches focusing on the evolution of conversation
decides to logout from the interface (logout) and the protocols.
application stores some information (start/end time,
(Leite et al. 2013) surveys the approaches working
used resources, etc.) into a database (log).
on Web service evolution until 2013. Our study of
that work shows that the most related proposals
are (Roohi and Salaün 2011; Wombacher 2009;
Jureta et al. 2007; Rinderle et al. 2006a,b).
(Roohi and Salaün 2011) suggest a method to check
CP reconfigurability. The authors consider two CPs,
Figure 6: A non correct CP Evolution namely, an initial CP and a new CP 0 and two
sets of peers PS and PS 0 obtained by projection
Figure 7 shows the four peers obtained by projection. from both CPs, respectively. Given a trace t in CP
This set of peers seems to respect the behaviour which consists in the history of the current execution
specified in the conversation protocol, yet this is (i.e., the sequence of interactions held between the
difficult to be sure using only visual analysis, even peers), if t can also be executed in reconfigured
for such a simple example. In addition, as the peers generated from CP 0 , then the reconfiguration
CP involves looping behaviour, it is hard to know can take place.
whether the resulting distributed system is bounded
and finite, which would allow its formal analysis Wombacher (2009) uses a formal model based
using existing verification techniques. Actually, this on annotated Finite State Automata (aFSA) to
set of peers is not synchronisable (and therefore describe Web service interaction and which is
not realisable), because the trace of send messages specified using choreography. This approach aligns
“connect, access” is present in the 1-bounded changes between updated choreography and the
asynchronous system, but is not present in the correspondent orchestration. Given an updated
synchronous system. Synchronous communication choreography, the changes, namely, adding and/or
enforces the sequence “connect, setup, access” as removing sequences of messages are propagated
specified in the CP , whereas in the asynchronous into distributed peers. The proposed solution is
system peer cl can send connect! and access! in implemented into DYCHOR framework and needs
sequence. human validation. In (Rinderle et al. 2006a,b),
the authors propose a controlled evolution method
This kind of evolution resulting in non realisable CP where propagating the changes into one peer
can be avoided using our method with no need of CP
7
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
requires to check its effect on other partner peers. as extending our language with new operators for
This approach is implemented into DYCHOR. messages broadcast and multicast. Lastly, we are
using theorem proving techniques in order to prove
In (Preda et al. 2015; Fdhila et al. 2015), both the correctness of CP evolution. Based on proof-
approaches study the evolution that might arise based techniques, we aim at handling any number of
at the peers side. The authors propagate the peers and exchanged messages such that scalability
change from one peer to other partners. The is ensured.
work proposed in (Fdhila et al. 2015) applies to
Business Process Management (BPM) domain and
Service Oriented Architecture (SOA). It describes REFERENCES
service choreographies using tree-based model. The
authors consider some changes such as “replace, Basu, S. and T. Bultan (2016). Automated
delete, update, and insert” of behavioural fragments. Choreography Repair. In Proc. of FASE’16,
Volume 9633 of LNCS, pp. 13–30. Springer.
(Preda et al. 2015) define a new language
Basu, S., T. Bultan, and M. Ouederni (2012).
referred to as DIOC for programming distributed
Deciding Choreography Realizability. In Proc. of
applications that are free from deadlocks and races
POPL’12, pp. 191–202. ACM.
by construction. The semantics of DIOC language
relies on labelled transition systems. The approach Ben-Abdallah, H. and S. Leue (1997). Syntactic
given in (Preda et al. 2015) enables to update Detection of Process Divergence and Non-local
fragment of codes of distributed peers. This can be Choice in Message Sequence Charts. In Proc
specified at the choreography level where blocks of TACAS’97, Volume 1217 of Lecture Notes in
of code that can be updated dynamically must be Computer Science, pp. 259–274. Springer.
tagged using “scope”. These “scope” blocks have to
be known a priori when describing the choreography. Brand, D. and P. Zafiropulo (1983). On Communi-
The solutions given in (Preda et al. 2015; Roohi and cating Finite-State Machines. J. ACM 30(2), 323–
Salaün 2011; Jureta et al. 2007) deal with run-time 342.
evolution.
Bultan, T. (2006). Modeling interactions of web
To the best of our knowledge, we are the first who software. In Proc. of WWV’06, pp. 45–52. IEEE.
verify the evolution at the CP level such that its Farah, Z., Y. Ait-Ameur, M. Ouederni, and K. Tari
realisability must be preserved. Furthermore, we (2016). A Correct-by-Construction Model for Asyn-
have no restriction on the application domain, yet chronously Communicating Systems. Interna-
we use a formal model which can be applied for tional Journal on Software Tools for Technology
design, verification, and implementation of different Transfer . To appear.
distributed systems, e.g. Web services, concurrent
systems, Cyber Physical Systems, etc. Our result Fdhila, W., C. Indiono, S. Rinderle-Ma, and M. Re-
applies also for asynchronously communicating ichert (2015). Dealing with change in process
systems as far as these are synchronisable with no choreographies: Design and implementation of
restriction on the buffer size. propagation algorithms. Information systems 49,
1–24.
7. CONCLUSION AND PERSPECTIVES Güdemann, M., G. Salaün, and M. Ouederni (2012).
Counterexample Guided Synthesis of Monitors for
In this paper, we presented a preliminary solution Realizability Enforcement. In Proc. of ATVA’12,
for correct evolution of distributed system for which Volume 7561 of LNCS, pp. 238–253. Springer.
their interaction is described with a conversation
protocol. We proposed a language which enables Hopcroft, J. E. and J. D. Ullman (1979). Introduction
one to incrementally design distributed system that to Automata Theory, Languages and Computation.
can be updated over time such that their realisability Addison Wesley.
is preserved while applying and composing evolution
Jureta, I. J., S. Faulkner, and P. Thiran (2007). Dy-
operators.
namic Requirements Specification for adaptable
In the near future we aim at formalising all properties and open Service-oriented Systems. Springer.
and composition operators used in this paper. We Leite, L. A., G. A. Oliva, G. M. Nogueira,
intend to prove that our evolution operators and their M. A. Gerosa, F. Kon, and D. S. Milojicic
properties preserve CP realisability. Our conjectures (2013). A Systematic Literature Review of Service
have also to be formally proved. We aim also Choreography Adaptation. Service Oriented
at defining looping and parallel operators as well Computing and Applications 7 (3), 199–216.
8
Towards correct Evolution of Conversation Protocols
Benyagoub • Ouederni • Ait-Ameur
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. Salaü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 Service-
oriented 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.
9