---
abstract: 'We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous address or name based communication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly relations between behavioural contracts and choreographic descriptions are considered, where a contract for each communicating party is, e.g., derived by projection. The considered relations are induced as the maximal preoders which preserve contract compliance and global traces: we show maximality to hold (permitting services to be discovered/substituted independently for each party) when contract refinement preorders with all the above asymmetric communication means are considered and, instead, not to hold if the standard symmetric CCS/pi-calculus communication is considered (or when directly relating choreographies to behavioral contracts via a preorder, no matter the communication mean). The obtained maximal preorders are then characterized in terms of a new form of testing, called compliance testing, where not only tests must succeed but also the system under test (thus relating to controllability theory), and compared with classical preorders such as may/must testing, trace inclusion, etc. Finally, recent work about adaptable choreographies and behavioural contracts is presented, where the theory above is extended to update mechanisms allowing choreographies/contracts to be modified at run-time by internal (self-adaptation) or external intervention.'
author:
- Mario Bravetti    Gianluigi Zavattaro
title: Choreographies and Behavioural Contracts on the Way to Dynamic Updates
---

Introduction
============

Choreographies and Orchestrations
=================================

We start by presenting the choreography and orchestration calculi (representing individual service behaviour) and then we relate them by projection.

The Choreography Calculus
-------------------------

We assume a denumerable set of action names ${\cal N}$, ranged over by $a,b,c,\dots$ and a set of roles [Roles]{} ranged over by $r, s, l$.

[**(Choreographies)**]{} The set of $Choreographies$, ranged over by $H, L, \cdots$ is defined by the following grammar: $$H \ \ ::= \ \ \quad a_{r \rightarrow s} \quad | \quad
                    H+H \quad | \quad
                    H;H \quad | \quad
                    H|H \quad | \quad
                    H^*$$ The invocations $a_{r \rightarrow s}$ means that role $r$ invokes the operation $a$ provided by the role $s$. The other operators are choice $\_+\_$, sequential $\_;\_$, parallel $\_|\_$, and repetition $\_^*$.

The operational semantics of choreographies considers two auxiliary terms ${\mathbf{1}}$ and ${\mathbf{0}}$. They are used to model the completion of a choreography, which is relevant in the operational modeling of sequential composition. The formal definition is given in Table \[choreosem\] where we take $\eta$ to range over the set of labels $\{ a_{r \rightarrow s}\ |\ a \in {\cal N}, r,s \in Roles \} \cup \{ \surd\}$ (the label $\surd$ denotes successful completion). The rules in Table \[choreosem\] are rather standard for process calculi with sequential composition and without synchronization; in fact, parallel composition simply allows for the interleaving of the actions executed by the operands (apart from completion labels $\surd$ that are required to synchronize).

$$\begin{array}{ccc}
a_{r \rightarrow s} {\stackrel{a_{r \rightarrow s}}{\longrightarrow}} {\mathbf{1}}&
{\mathbf{1}}{\stackrel{\surd}{\longrightarrow}} {\mathbf{0}}&
H^* {\stackrel{\surd}{\longrightarrow}} {\mathbf{0}}\\
\\
{\frac{^{\textstyle H {\stackrel{\eta}{\longrightarrow}} H'}}{_{\textstyle H\!+\!L {\stackrel{\eta}{\longrightarrow}} H'}}} 
&         
{\frac{^{\textstyle H {\stackrel{\eta}{\longrightarrow}} H' \quad \eta \neq \surd}}{_{\textstyle H;\!L {\stackrel{\eta}{\longrightarrow}} H';\!L}}}                  
\qquad
&
{\frac{^{\textstyle H {\stackrel{\surd}{\longrightarrow}} H' \quad L {\stackrel{\eta}{\longrightarrow}} L'}}{_{\textstyle H;\!L {\stackrel{\eta}{\longrightarrow}} L'}}}        
\\
\\
{\frac{^{\textstyle H {\stackrel{\surd}{\longrightarrow}} H' \quad L {\stackrel{\surd}{\longrightarrow}} L'}}{_{\textstyle H \!{\,|\,}\! L {\stackrel{\surd}{\longrightarrow}} H' \!{\,|\,}\! L'}}}  
\qquad
&
{\frac{^{\textstyle H {\stackrel{\eta}{\longrightarrow}} H' \quad \eta \neq \surd}}{_{\textstyle H \!{\,|\,}\! L {\stackrel{\eta}{\longrightarrow}} H' \!{\,|\,}\! L}}}                                     
&
{\frac{^{\textstyle H {\stackrel{\eta}{\longrightarrow}} H' \quad \eta \neq \surd}}{_{\textstyle H^* {\stackrel{\eta}{\longrightarrow}} H' ; H^*}}}  
\end{array}$$

Choreographies are especially useful to describe the protocols of interactions within a group of collaborating services. To clarify this point, we present a simple example of a protocol described with our choreography calculus.

\[BSB\] [**(Buyer/Seller/Bank)**]{} Let us consider the following choreography composed of three roles: [*Buyer*]{}, [*Seller*]{} and [*Bank*]{} $$\begin{array}{l}
Request_{Buyer \rightarrow Seller};
(\ Offer_{Seller \rightarrow Buyer} {\,|\,}PayDescr_{Seller \rightarrow Bank}\ ); \\
\hspace{.5cm} Payment_{Buyer \rightarrow Bank};
(\ Confirm_{Bank \rightarrow Seller} {\,|\,}Receipt_{Bank \rightarrow Buyer}\ )
\end{array}$$ According to this choreography, the [*Buyer*]{} initially sends an item request to the [*Seller*]{} that subsequently, in parallel, replies with an offer and sends a payment description to the [*Bank*]{}. Then the [*Buyer*]{} performs the actual payment to the [*Bank*]{}. The latter in parallel replies with a receipt and sends a payment confirmation to the [*Seller*]{}.

The Orchestration Calculus
--------------------------

As for choreographies, we assume a denumerable set of action names ${\cal N}$, ranged over by $a,b,c,\dots$. We use $\tau \notin {\cal N}$ to denote an internal (unsynchronizable) computation.

\[orcsys\] [**(Orchestrations and Systems)**]{} The syntax of orchestrations is defined by the following grammar $$\begin{array}{lll}
C &\ ::=\ &      {\mathbf{0}}\quad | \quad 
               {\mathbf{1}}\quad | \quad
               \tau  \quad | \quad
               a  \quad | \quad
          \overline{a}_l \quad | \quad               
\\[.2cm]
  & &             
               C ; C \quad | \quad
               C\!+\!C \quad | \quad
               C \!{\,|\,}\! C \quad | \quad
               C^* 
\end{array}$$ The set of all orchestrations $C$ is denoted by ${\cal P}_{orc}$.\
The syntax of systems (orchestration compositions) is defined by the following grammar $$P \ \ ::= \ \   [C]_l \quad | \quad
                P {{|\!|}}P \quad 
$$ A system $P$ is well-formed if: $(i)$ every orchestration subterm $[C]_l$ occurs in $P$ at a different role $l$ and $(ii)$ no output action with destination $l$ is syntactically included inside an orchestration subterm occurring in $P$ at the same role $l$, i.e. actions $\overline{a}_l$ cannot occur inside a subterm $[C]_l$ of $P$. The set of all well-formed systems $P$ is denoted by ${\cal P}$. In the following we will just consider well-formed systems and, for simplicity, we will call them just systems.

We take $\alpha$ to range over the set of syntactical actions $SAct = {\cal N} \cup \{ \overline{a}_l \; | \; a \in {\cal N} \wedge l \in {Roles} \} \cup \{ \tau \}$.

The operational semantics of contracts is defined by the rules in Table \[contsem\] (plus symmetric rules). The operational semantics of systems is defined by the rules in Table \[contcompsem\] plus symmetric rules. We take $\beta$ to range over the set $Act$ of actions executable by contracts and systems, i.e. $Act =  SAct \cup
\{ a_l \; | \; a \in {\cal N} \wedge l \in {Roles} \} \cup
\{ a_{r \rightarrow s}\ |\ a \in {\cal N} \wedge r,s \in {Roles} \} \cup 
\{ \overline{a}_{r s}\ |\ a \in {\cal N} \wedge r,s \in {Roles} \}$. We take $\lambda$ to range over the set of transition labels ${\cal L} = Act \cup \{ \surd \}$, where $\surd$ denotes successful termination.

$$\begin{array}{cc}
{\mathbf{1}}{\stackrel{\surd}{\longrightarrow}} {\mathbf{0}}&
\alpha {\stackrel{\alpha}{\longrightarrow}} {\mathbf{1}}\\
\\
\multicolumn{2}{c}{
{\frac{^{\textstyle C {\stackrel{\lambda}{\longrightarrow}} C'}}{_{\textstyle C\!+\!D {\stackrel{\lambda}{\longrightarrow}} C'}}} 
\qquad         
{\frac{^{\textstyle C {\stackrel{\lambda}{\longrightarrow}} C' \quad \lambda \neq \surd}}{_{\textstyle C;\!D {\stackrel{\lambda}{\longrightarrow}} C';\!D}}}                  
\qquad

{\frac{^{\textstyle C {\stackrel{\surd}{\longrightarrow}} C' \quad D {\stackrel{\lambda}{\longrightarrow}} D'}}{_{\textstyle C;\!D {\stackrel{\lambda}{\longrightarrow}} D'}}}        
}\\
\\
\qquad
{\frac{^{\textstyle C {\stackrel{\surd}{\longrightarrow}} C' \quad D {\stackrel{\surd}{\longrightarrow}} D'}}{_{\textstyle C \!{\,|\,}\! D {\stackrel{\surd}{\longrightarrow}} C' \!{\,|\,}\! D'}}}  
\qquad
&
{\frac{^{\textstyle C {\stackrel{\lambda}{\longrightarrow}} C' \quad \lambda \neq \surd}}{_{\textstyle C \!{\,|\,}\! D {\stackrel{\lambda}{\longrightarrow}} C' \!{\,|\,}\! D}}}                           
\\
\\
C^* {\stackrel{\surd}{\longrightarrow}} {\mathbf{0}}&
{\frac{^{\textstyle C {\stackrel{\lambda}{\longrightarrow}} C' \quad \lambda \neq \surd }}{_{\textstyle C^* {\stackrel{\lambda}{\longrightarrow}} C' ; C^*}}}  
\end{array}$$

$$\begin{array}{clclc}
{\frac{^{\textstyle C {\stackrel{a}{\longrightarrow}} C' \quad }}{_{\textstyle [C]_r {\stackrel{a_r}{\longrightarrow}} [C']_r}}} 
& \qquad &
{\frac{^{\textstyle C {\stackrel{\overline{a}_{s}}{\longrightarrow}} C' \quad }}{_{\textstyle [C]_r {\stackrel{\overline{a}_{rs}}{\longrightarrow}} [C']_r}}} 
& \qquad &
{\frac{^{\textstyle P {\stackrel{\lambda}{\longrightarrow}} P' \quad \lambda \neq \surd }}{_{\textstyle P  {{|\!|}}Q {\stackrel{\lambda}{\longrightarrow}} P' {{|\!|}}Q}}} 
\\
\\
\multicolumn{5}{c}{
{\frac{^{\textstyle P {\stackrel{a_s}{\longrightarrow}} P' \quad
          Q {\stackrel{\overline a_{rs}}{\longrightarrow}} Q'}}{_{\textstyle P {{|\!|}}Q {\stackrel{a_{r\rightarrow s}}{\longrightarrow}} P' {{|\!|}}Q'}}} 
\qquad
{\frac{^{\textstyle P {\stackrel{\surd}{\longrightarrow}} P' \quad
Q {\stackrel{\surd}{\longrightarrow}} Q'}}{_{\textstyle P {{|\!|}}Q {\stackrel{\surd}{\longrightarrow}} P' {{|\!|}}Q'}}}
}
\\
\end{array}$$

Here and in the remainder of the paper we use the following notations: $P {\stackrel{\lambda}{\longrightarrow}}$ to mean that there exists $P'$ such that $P {\stackrel{\lambda}{\longrightarrow}} P'$ and, given a sequence of labels $w=\lambda_1 \lambda_2 \cdots \lambda_{n-1}\lambda_n$ (possibly empty, i.e., $w = {\varepsilon}$), we use $P {\stackrel{w}{\longrightarrow}} P'$ to denote the sequence of transitions $P {\stackrel{\lambda_1}{\longrightarrow}} P_1 {\stackrel{\lambda_2}{\longrightarrow}}
\cdots {\stackrel{\lambda_{n-1}}{\longrightarrow}} P_{n-1} {\stackrel{\lambda_n}{\longrightarrow}} P'$ (in case of $w={\varepsilon}$ we have $P'=P$, i.e., $P {\stackrel{{\varepsilon}}{\longrightarrow}} P$). Moreover, for completely specified systems $P$ (i.e. terms $P$ not included as subterms in a larger term $P'$), we do not consider transitions corresponding to unmatched input and output actions: namely, we consider only transitions labeled with $\tau$ (local internal actions), $\surd$ (global successful termination) and $a_{r\rightarrow s}$ (completed interactions).

We now define the notion of correct composition of orchestrations. This notion is the same as in [@fsen07]. Intuitively, a system composed of orchestrations is correct if all possible computations may guarantee completion; this means that the system is both deadlock and livelock free (there can be an infinite computation, but given any possible prefix of this infinite computation, it must be possible to extend it to reach a successfully completed computation).

\[correctcomposition\] [**(Correct orchestration composition)**]{} System $P \in {\cal P}$ is a correct orchestration composition, denoted $P\!\downarrow$, if for every $P'$ such that $
P \; {\stackrel{w}{\longrightarrow}} \; P' 
$ there exists $P''$ such that $
P' \; {\stackrel{w'}{\longrightarrow}} \; P'' \; {\stackrel{\surd}{\longrightarrow}}. 
$

Choreography Implementation, Projection and Well-Formedness
-----------------------------------------------------------

We are now ready to formalize the notion of correct implementation of a choreography. With $P {\stackrel{\tau^*}{\longrightarrow}} P'$ we denote the existence of a (possibly empty) sequence of $\tau$-labeled transitions starting from the system $P$ and leading to $P'$. Given the sequence of labels $w = \lambda_1 \cdots \lambda_n$, we write $P \stackrel{w}{\Longrightarrow} P'$ if there exist $P_1, \cdots, P_m$ such that $P {\stackrel{\tau^*}{\longrightarrow}} P_1 {\stackrel{\lambda_1}{\longrightarrow}} P_2 {\stackrel{\tau^*}{\longrightarrow}} \cdots {\stackrel{\tau^*}{\longrightarrow}}
 P_{m-1} {\stackrel{\lambda_n}{\longrightarrow}} P_m {\stackrel{\tau^*}{\longrightarrow}} P'$.

Intuitively, a system implements a choreography if it is a correct composition of orchestrations and all of its conversations (i.e. the possible sequences of message exchanges), are admitted by the choreography.

\[impl\][**(Choreography implementation)**]{} Given the choreography $H$ and the system $P$, we say that $P$ implements $H$ (written $P \propto H$) if

-   $P$ is a correct orchestration composition and

-   given a sequence $w$ of labels of the kind $a_{r \rightarrow s}$, if $P \stackrel{w \surd}{\Longrightarrow} P'$ then there exists $H'$ such that $H \stackrel{w \surd}{\longrightarrow} H'$.

Note that it is not necessary for an implementation to include all possible conversations admitted by a choreography.

[**(Implementation of Buyer/Seller/Bank)**]{} As an example, we present a possible implementation of the choreography reported in the Example \[BSB\]. $$\begin{array}{l}
\ [\overline{Request}_{Seller} ; Offer ;
\overline{Payment}_{Bank} ; Receipt
]_{Buyer}\ 
{{|\!|}}\\
\ [Request ; (\overline{Offer}_{Buyer} {\,|\,}\overline{PayDescr}_{Bank});Confirm]_{Seller} 
\ {{|\!|}}\\
\ [PayDescr ; Payment; (\overline{Receipt}_{Buyer} {\,|\,}\overline{Confirm}_{Seller})]_{Bank}
\end{array}$$

We now present the notion of choreography projection, which yields an orchestration $C$ for each role of a choreography $H$. The definition is very simple thanks to the idea, we introduced in [@SC07], of projecting communication atoms and then applying homomorphism over all the algebra operators.

[**(Choreography projection)**]{} \[def:proj\] Given a choreography $H$, the projection $H$ on the role $r$, denoted with ${[\![H]\!]}_r$, is defined inductively on the syntax of $H$ in such a way that $${[\![a_{r \rightarrow s}]\!]}_t\ =\
\left \{
\begin{array}{ll}
\overline{a}_s \qquad  & \mbox{if $t=r$} \\
a                           & \mbox{if $t=s$} \\ 
{\mathbf{1}}& \mbox{otherwise}
\end{array}
\right .$$ and that it is a homomorphism with respect to all operators.

It is interesting to observe that given a choreography $H$, the system obtained composing its projections is not ensured to be an implementation of $H$. For instance, consider the choreography $
a_{r \rightarrow s}\ ;\ b_{t \rightarrow u} 
$. The system obtained by projection is $
[\overline{a}_s]_r\ {{|\!|}}\ [a]_s\ {{|\!|}}\ [\overline{b}_u]_t\ {{|\!|}}\ [b]_u
$. Even if this is a correct composition of orchestrations, it is not an implementation of $H$ because it comprises the conversation $b_{t \rightarrow u} a_{r \rightarrow s}$ which is not admitted by $H$.

The problem is not in the definition of the projection, but in the fact that the above choreography cannot be implemented preserving the message exchanges specified by the choreography. In fact, in order to guarantee that the communication between $t$ and $u$ is executed after the communication between $r$ and $s$, it is necessary to add a further message exchange (for instance between $s$ and $r$) which is not considered in the choreography. In order to have the guarantee that the system obtained by projection is consistent with the initial choreography, it is reasonable to consider a subset of [*well formed*]{} choreographies. The most general and intuitive notion of well formedness, we introduced in [@SC07], can be obtained by considering only all those choreographies for which the system obtained by projection is ensured to be a correct implementation.

\[wellFormed\][**(Well formed choreography)**]{} A choreography $H$, defined on the roles $r_1,\cdots,r_n$, is [*well formed*]{} if $
[\, {[\![H]\!]}_{r_1}\, ]_{r_1}\ {{|\!|}}\ \cdots\ {{|\!|}}\ [\, {[\![H]\!]}_{r_n}\,]_{r_n}
\propto\ H
$

It is worthwhile to note that well formedness is decidable. In fact, given a choreography $H$, it is sufficient to take the corresponding system $P$ obtained by projection, then consider $P$ and $H$ as finite state automata, and finally check whether the language of the first automaton is included in the language of the second one. Note that the terms $P$ and $H$ can be seen as finite state automata thanks to the fact that their infinite behaviours are defined using Kleene-star repetitions instead of general recursion.

This decidability result clearly follows from the fact that we restrict to finite state choreographies. In the literature, more general syntactic versions of well formedness exist (see e.g. [@CHY07]). In the next section we report a syntactic characterisation of well formedness.

Contract-based Service Discovery
================================

We now define the notion of behavioural contract which will allow us to reason about service compliance and retrieval independently of the language used for implementing service behaviour.

Contracts are defined as labeled transition systems, where transition labels are the typical internal $\tau$ action and the input/output actions $a,\overline{a}_l$, where the outputs (as for the orchestration calculus) are directed to a destination address denoted by a role $r \in Roles$. We first define the class of labeled transition systems of interest for defining contracts.

[**(Finite Connected LTS with Termination Transitions)**]{} A finite connected labeled transition system (LTS) with termination transitions is a tuple ${\cal t} = (S,{\cal L},{\stackrel{}{\longrightarrow}},s_h,s_0)$ where $S$ is a finite set of states, $L$ is a set of labels, the transition relation ${\stackrel{}{\longrightarrow}}$ is a finite subset of $(S-\{s_h\})
 \times ({\cal L} \cup \{ \surd \}) \times S$ such that $(s, \surd, s') \in {\stackrel{}{\longrightarrow}}$ implies $s' = s_h$, $s_h \in S$ represents a halt state, $s_0 \in S$ represents the initial state, and it holds that every state in $S$ is reachable (according to ${\stackrel{}{\longrightarrow}}$) from $s_0$.

As in orchestrations, in a finite connected LTS with termination transitions we use $\surd$ transitions (leading to the halt state $s_h$) to represent successful termination. On the contrary, if we get (via a transition different from $\surd$) into a state with no outgoing transitions (like, e.g., $s_h$) then we represent an internal failure or a deadlock.

[**(Behavioural Contract)**]{}\[contractdef\] \[def:contract\] A behavioural contract is a finite connected LTS with termination transitions, that is a tuple $(S,{\cal L},{\stackrel{}{\longrightarrow}},s_h,s_0)$, where ${\cal L} = \{a,\overline{a}_l,\tau
\ |\ a \in {\cal N} \wedge l \in Roles \}$, i.e. labels are either a receive (input) on some operation $a \in {\cal N}$ or an invoke (output) directed to some operation $a \in {\cal N}$ at some role $l$ or internal $\tau$ actions.

Orchestrations $C \in {\cal P}_{orc}$ give rise to a behavioral contract as the labeled transition system obtained by their semantics (where the initial state $s_0$ is $C$, the halt state $s_h$ is ${\mathbf{0}}$ and the other states in $S$ are terms $C'$ reachable by $C$). We can, therefore, use $C \in {\cal P}_{orc}$ as a way to denote such a behavioral contract.

In the following we will present the theory of behavioral contracts by abstracting from the particular process algebra used to denote them: contracts represent orchestration behavior in a [*language independent way*]{}. We will therefore take terms $C$ belonging to a generic set ${\cal P}_{con}$ being any set of terms (generated by the syntax of a process algebra) that give rise to all possible behavioral contracts as their semantics (in the form of finite connected LTSes as in Definition \[contractdef\]). For instance ${\cal P}_{con}$ can be basic CCS (with recursion) over ${\cal L}$ prefixes and extended with successful termination ${\mathbf{1}}$, see [@libroCubo; @sensoria].

Contract Compositions and Contract Compliance
---------------------------------------------

Similarly as for orchestrations, we consider [*contract compositions*]{} $P$ as parallel compositions of contracts $C$, where the syntax and semantics of $P$ is defined as for the syntax (Definition \[orcsys\]) and semantics (Table \[contcompsem\]) of systems, where we now take $C$ belonging to the arbitrary set ${\cal P}_{con}$, instead of $C \in {\cal P}_{orc}$. With a little abuse of notation in this section we will use ${\cal P}$ to denote the set of such contract compositions $P$ (the same notation used for set of systems in the previous section). When reasoning about contract compositions $P$, it will be fundamental to consider (as we did for the particular orchestration language of the previous section) correct contract compositions, denoted by $P\downarrow$. The notion of [*correct contract composition*]{} (also called [*contract compliance*]{}) $P$ is defined exactly as for correct orchestration composition, see Definition \[correctcomposition\] (the only difference now being that $P$ is composed of terms $C$ belonging to the arbitrary set ${\cal P}_{con}$, instead of $C \in {\cal P}_{orc}$).

Independent Subcontracts
------------------------

We are now ready to define the notion of independent subcontract pre-order. Given a contract $C \in {\cal P}_{con}$, we use $oroles(C)$ to denote the subset of $Roles$ of the roles of the destinations of all the output actions occurring inside $C$.

\[defsubfam\] [**(Independent Subcontract pre-order)**]{} A pre-order $\leq$ over ${\cal P}_{con}$ is an independent subcontract pre-order if, for any $n \geq 1$, contracts $C_1, \dots, 
C_n \in {\cal P}_{con}$ and $C_1', \dots, C_n' \in {\cal P}_{con}$ such that $\forall i \ldotp C_i' \leq C_i$, and distinguished role names $l_1, \dots, l_n \in {Roles}$ such that $\forall i \ldotp l_i \notin oroles(C_i) \cup oroles(C_i')$, we have $$([C_1]_{l_1} \; {{|\!|}}\dots  {{|\!|}}\; 
[C_n]_{l_n})\!\downarrow  \quad \Rightarrow 
\quad ([C_1']_{l_1} \; {{|\!|}}\dots  {{|\!|}}\; [C_n']_{l_n})\!\downarrow$$

It is easy to see that, if we do not introduce any asymmetry in the behaviour of invokes and receives, there is no maximal independent subcontract pre-order, i.e. there is no optimal solution to the problem of locally retrieving services based on their contracts.

This can be easily seen by considering, e.g., the trivially correct system $[C_1]_l {{|\!|}}[C_2]_{l'}$ with $C_1 = a$ and $C_2 = \overline{a}_l$. Consider the two independent subcontract pre-orders $\leq^1$ and $\leq^2$ such that the unique pairs they possess besides the identity on all contracts $C$ are $$a+c;{\mathbf{0}}\leq^1 a\
$$ and $$\overline{a}_l+\overline{c}_{l};{\mathbf{0}}\leq^2 \overline{a}_l$$ No pre-order $\leq$ could have both $$a+c;{\mathbf{0}}\leq a\
\mbox{\ and\ }\ 
\overline{a}_l+\overline{c}_{l};{\mathbf{0}}\leq \overline{a}_l$$ because if we refine $C_1$ with $a+c;{\mathbf{0}}$ and $C_2$ with $\overline{a}_l+\overline{c}_l;{\mathbf{0}}$ we achieve the incorrect system $a+c.{\mathbf{0}}{{|\!|}}\overline{a}_l+\overline{c}_l;{\mathbf{0}}$ that can deadlock after synchronization on channel $c$.

We now show that, by assuming a more practical form of communication, where invokes and receives have an asymmetric behaviour, there exists a maximal independent subcontract pre-order. This con be achieved in several ways: $(i)$ constraining the structure of behavioural contracts by considering only [*output persistent*]{} ones (a contract chooses internally to perform an output/invoke: it must execute it to reach successful termination) as in WS-BPEL [@wsbpel-spec] or in session types [@CHY07]; $(ii)$ strengthening the notion of compliance (yielding so-called strong compliance [@mscs09; @coord07]): when an output is performed a corresponding input is required to be already enabled, like in ready-send of Message Passing Interface $(iii)$ moving to asynchronous communication, e.g. via message queues [@libroCubo; @wsfm08].

In the following we will detail the first of the above approaches. In Section \[summary\] we will survay other approaches.

Output Persistence
------------------

The main results reported in this paper are consequences of a property of systems that we call [*output persistence*]{}.

\[outper\][**(Output persistence)**]{} Let $C \in {\cal P}_{con}$ be a behavioural contract. It is output persistent if given $C {\stackrel{w}{\longrightarrow}} C'$ with $C' {\stackrel{\overline{a}_l}{\longrightarrow}}$ then: $C' {\stackrel{\surd}{\longrightarrow}\!\!\!\!\!\!\!\! /\ \  }$ and if $C' {\stackrel{\alpha}{\longrightarrow}} C''$ with $\alpha \neq \overline{a}$ then also $C'' {\stackrel{\overline{a}_l}{\longrightarrow}}$.

The output persistence property states that once a contract decides to execute an output, its actual execution is mandatory in order to successfully complete the execution of the contract. This property typically hold in languages for the description of service behaviours or for service orchestrations (WS-BPEL [@wsbpel-spec] or session types [@CHY07]) in which output actions cannot be used as guards in external choices (see e.g. the [pick]{} operator of WS-BPEL which is an external choice guarded on input actions). In these languages, a process instance always decides [*internally*]{} to execute an output action (output action cannot be involved in an external choice). In fact, if we consider potential outputs that can disappear without being actually executed (as in an external choice among outputs $\overline{a}+\overline{b}$ or in a mixed choice $a+\overline{b}$ in which, e.g., the possible $\overline{b}$ is no longer executable after the output or input on $a$) we have that there exists no maximal subcontract pre-order family, as we have shown with the above counterexample.

Notice that, if we instead assume output persistence of contracts, as we do in this paper, subcontracts cannot add reachable outputs on new types. For instance an output persistent contract $a+\tau.\overline{c_l}$ adding a new output on $c_l$ with respect to $a$, similarly to the pre-order $\leq^2$ in the counterexample above, would not be a correct subcontract because when composed in parallel with the other initial contract $\overline{a}_l$ would lead to a deadlock.

In the context of process algebra with parallel composition as that of ${\cal P}_{orc}$, a syntactical characterization that guarantees output persistence has been introduced in [@fsen07]. The idea is to require that every output prefix (i.e. the term $\overline{a}_l$) is preceded by an internal $\tau$ prefix, i.e. the syntax of Definition \[orcsys\] includes $\tau;\overline{a}_l$ instead of $\overline{a}_l$. Choreography projection must be also modified in order to produce, for each role, an output persistent contract that can be then used for discovering services via refinement (see following Section \[chorconf\]). In particular, we have to modify the rule concerning generation of output in orchestrations as follows: $${[\![a_{r \rightarrow s}]\!]}_t\ =\ \tau;\overline{a}_s \qquad \mbox{if $t=r$}$$

In the following we will take ${\cal P}_{opcon}$ to be any set of terms (generated by the syntax of a process algebra) that give rise to all possible output persistent behavioral contracts as their semantics (in the form of finite connected LTSes as in Definition \[contractdef\]). Moreover we will consider systems ${\cal P}$ to be compositions of contracts in ${\cal P}_{opcon}$.

Compliance Testing is the Maximal Preorder {#subrel}
------------------------------------------

We will show that the maximal independent subcontract pre-order can be achieved defining a more coarse form of refinement in which, given any system composed of a set of contracts, refinement is applied to one contract only (thus leaving the others unchanged). This form of refinement, that we call [*compliance testing*]{}, is a form of testing where both the test and the system under test must reach success.

Given a system $P \in {\cal P}$, we use $roles(P)$ to denote the subset of $Roles$ of the roles of contracts syntactically occurring inside $P$: e.g. $roles([C]_{l_1} {{|\!|}}[C']_{l_2}) = \{ l_1, l_2 \}$.

[**(Subcontract Relation)**]{} \[defsubrel\] A contract $C' \in {\cal P}_{opcon}$ is a subcontract of a contract $C \in {\cal P}_{opcon}$ denoted $C' \preceq C$, if and only if for all $l \in {Roles}$ such that $l \notin oroles(C_i) \cup oroles(C_i')$ and $P \in {\cal P}$ such that $l \notin roles(P)$ we have $
([C]_l {{|\!|}}P)\!\downarrow 
$ implies $
([C']_l {{|\!|}}P)\!\downarrow
$

\[hard\] There exists a maximal independent subcontract pre-order and it corresponds to the (compliance testing based) subcontract relation “$\preceq$”. Formally, for any pre-order $\leq$ over ${\cal P}_{opcon}$ that is an independent subcontract pre-order, we have that $\leq$ is included in $\preceq$.

Properties of the Maximal Preorder and I/O Knowledge
----------------------------------------------------

We now discuss some properties of the maximal independent subcontract pre-order (compliance testing), comparing it with other approaches and other classical preorders. We also show a sound characterization that is decidable.

In the following we will use $I(C)$ to stand for the subset of ${\cal N}$ of the input actions $a$ syntactically occurring in $C$ and “$C {{\setminus \!\!\!\!\; \setminus}}M$”, with $M \subseteq {\cal N}$, to stand for “$C \{{\mathbf{0}}/ a | a \in M \}$”.

\[lemmuccio\] Let $C,C' \in {\cal P}_{opcon}$ be contracts. We have $$C' {{\setminus \!\!\!\!\; \setminus}}(I(C') - I(C)) \preceq C \quad \Leftrightarrow \quad C'  \; \preceq C
$$

The proposition above is a direct consequence of the fact that, due to output persistence of contracts, compliant tests $P$ of a contract $[C]_l$ cannot perform reachable outputs directed to $l$ that $C$ cannot receive. For instance $[a]_l {{|\!|}}[\tau;\overline{a}_l + \tau;\overline{b}_l]_{l'}$ is not a correct contract composition.

From the proposition above we can derive two fundamental properties of the maximal independent subcontract pre-order:

-   External choices on inputs can be extended, for instance: $$a+b \preceq  a$$ by directly applying the above proposition.

-   Internal choices on outputs can be reduced, for instance: $$\tau;\overline{a}_l  \preceq   \tau;\overline{a}_l + \tau;\overline{b}_l$$ because the lefthand term is more deterministic (typical property in testing).

These two properties are assumed when considering subtyping in the theory of session types [@CHY07], in our setting they were instead obtained as a consequence of considering the maximal independent subcontract preorder over output persistent contracts.

Notice that, when considering behavioural contracts that communicate just with standard CCS channel name based communication [@sfm09; @fundaInfo08; @fsen07], i.e. where outputs are just written as $\overline{a}$ instead of being directed to a certain role $l$ as in $\overline{a}_l$, the proposition above does not hold. This is due to “capturing” behaviour. For instance it does not hold that $a+b \preceq  a$, as can be seen by considering the correct contract composition $$[a] {{|\!|}}[\tau;\overline{a};b ] {{|\!|}}[\tau;\overline{b}]$$ and the incorrect one $$[a+b] {{|\!|}}[\tau;\overline{a};b ] {{|\!|}}[\tau;\overline{b}]$$ where the leftmost contract can “capture” the $\overline{b}$ that was received by the middle contract in the correct composition.

This problem can be faced by resorting to knowledge about the input and output actions syntactically occurring in the initial contracts (e.g. those obtained by projection from a choreography) when defining the notion of independent subcontract preorder $\leq$, see [@sfm09; @fundaInfo08; @fsen07]. In this way $C' \preceq_{I,O} C$ denotes that $C'$ is a subcontract of $C$ assuming that the other contracts (the test) can only perform input on $I$ and output on $O$. Therefore, exploiting knowledge we can recover the above proposition and we have: $$a+b \preceq_{{\cal N},{\cal N}-\{ b \}}  a$$

### Resorting to Fair Testing {#should}

This section is devoted to the definition of an actual procedure for determining that two contracts are in subcontract relation. This is achieved resorting to the theory of fair testing, called [*should-testing*]{} [@RV05]. As a side effect we will also show that subcontract relation is coarser than fair testing preorder.

In the following we denote with $\preceq_{test}$ the [*should-testing*]{} pre-order defined in [@RV05] where we consider the set of actions used by terms as being ${\cal L} \cup \{ \overline{a} \mid a \in {\cal N} \}$ (i.e. we consider located and unlocated input and output actions and $\surd$ is included in the set of actions of terms under testing as any other action). We denote here with $\surd'$ the special action for the success of the test (denoted by $\surd$ in [@RV05]). In the following we consider $\lambda$ to range over ${\cal L} \cup \{ 
\overline{a} \mid a \in {\cal N} \}$.

In order to resort to the theory defined in [@RV05], we define a normal form for contracts of our calculus that corresponds to terms of the language in [@RV05]. The normal form of the contract $C$ (denoted with ${\cal NF}(C)$) is defined as follows, by using the operator $rec_{X} \theta$ (defined in [@RV05]) that represents the value of $X$ in the solution of the minimum fixpoint of the finite set of equations $\theta$, $$\begin{array}{rll}
{\cal NF}(C) & = & rec_{X_1} \theta \qquad\mbox{where $\theta$ is the set of equations}
\\
X_i & = & \sum_{j} \lambda_{i,j} ; X_{der(i,j)}
\end{array}$$ where, assuming to enumerate the states in the labeled transition system of $P$ starting from $X_1$, each variable $X_i$ corresponds to the $i$-th state of the labeled transition system of $P$, $\lambda_{i,j}$ is the label of the $j$-th outgoing transition from $X_i$, and ${der(i,j)}$ is the index of the state reached with the $j$-th outgoing transition from $X_i$. We assume empty sums to be equal to ${\mathbf{0}}$, i.e. if there are no outgoing transitions from $X_i$, we have $X_i = {\mathbf{0}}$.

\[finale\] Let $C,C' \in {\cal P}_{opcon}$ be two contracts. We have $${\cal NF}(C' {{\setminus \!\!\!\!\; \setminus}}\!I(C')\!-\!I(C)) \preceq_{test} {\cal NF}(C) \quad \Rightarrow
\quad C' \preceq C$$

The opposite implication $
C' \preceq C
 \Rightarrow 
{\cal NF}(C' {{\setminus \!\!\!\!\; \setminus}}\! I(C')\!-\!I(C)) \preceq_{test} {\cal NF}(C) 
$ does not hold in general. This can be easly seen by considering uncontrollable contracts, i.e. contracts for which there is no compliant test. For instance the contract ${\mathbf{0}}$, any other contract $a;b;{\mathbf{0}}$ or $c;d;{\mathbf{0}}$ or more complex examples like $a.{\mathbf{1}}+a.b.{\mathbf{1}}$. These contracts are all equivalent according to our subcontract relation, but of course not according to fair testing.

### Comparison with Traditional Testing and Trace Preorders

Notice that Theorem \[finale\] says that the subcontract relation is coarser than fair testing preorder (where tests are assumed to be capable of observing $\surd$ actions of the system under test). The equivalent uncontrollable contracts that we have shown in the previous section show that this inclusion is strict: this is due to the fact that, besides requiring the success of the test, we impose also that the tested process should successfully complete its execution.

Another significant difference of compliance testing respect to traditional one proposed by De Nicola-Hennessy [@DH84] is in the treatment of divergence: we do not follow the traditional catastrophic approach, but the fair approach as in the theory of should-testing of Rensink-Vogler [@RV05]. In fact, we do not impose that all computations must succeed, but that all computations can always be extended in order to reach success.

Concerning trace preorder, it is not coarser than subcontract relation (compliance testing) due to the possible presence in the system under test of traces not leading to success: these traces are not observable by (compliant) tests. For instance the equivalent uncontrollable contracts that we have shown in the previous section have completely different traces. In this respect compliance testing differs from standard testing theories which imply trace inclusion.

Contract-based Choreography Conformance {#chorconf}
---------------------------------------

We are now in place for the definition of relations $C \triangleleft_r H$ indicating whether the contract $C$ can play the role $r$ in the choreography $H$.

[**(Conformance relation)**]{} Given a well-formed choreography $H$ with roles $r_1, \cdots, r_n$, a relation among contracts, roles $r$ of $H$ and $H$, denoted with $C \triangleleft_{r} H$, is a [*conformance relation*]{} if, for every $r_i$, with $1 \leq i \leq n$, there exists at least a contract $C_i$ such that $C_i \triangleleft_{r_i} H$, and it holds that: $
\mbox{if}\  
C_1 \triangleleft_{r_1} H , \cdots, C_n \triangleleft_{r_n} H 
\ \mbox{then}\ 
[C_1]_{r_1} {{|\!|}}\cdots {{|\!|}}[C_n]_{r_n} 
\propto H
$.

It is interesting to observe that, differently from subcontract relation defined on contracts in the previous Section \[subrel\], there exists no maximal conformance relation. For instance, consider the choreography $H = a_{r \rightarrow s}|b_{r \rightarrow s}$. We could have two different conformance relations $\triangleleft^1$ and $\triangleleft^2$, the first one such that $$(\tau;\overline{a}_s | \tau;\overline{b}_s) \triangleleft^1_r H
\qquad \qquad
(\tau;a;b\ +\ \tau;b;a) \triangleleft^1_s H$$ and the second one such that $$(\tau;\overline{a}_s;\tau;\overline{b}_s + \tau;\overline{b}_s;\tau;\overline{a}_s) 
\triangleleft^2_r H
\qquad \qquad
(a | b) \triangleleft^2_s H$$ It is easy to see that it is not possible to have a conformance family that comprises the union of the two relations $\triangleleft^1$ and $\triangleleft^2$. In fact, the system $$[\tau;\overline{a}_s;\tau;\overline{b}_s\ +\ \tau;\overline{b}_s;\tau;\overline{a}_s]_r\ {{|\!|}}\
[\tau;a;b\ +\ \tau;b;a]_s$$ is not a correct composition because the two contracts may internally select two incompatible orderings for the execution of the two message exchanges (and in this case they stuck).

In the remainder of this section we define a mechanism that, exploiting the notion of subcontract relation defined in the previous section and, in particular, its sound characterization based on fair testing, permits to effectively characterize an interesting conformance relation.

We now present the notion of [*testing consonance*]{} (see [@libroCubo]) between contracts and roles of a given choreography, and we prove that it is a conformance family.

[**(Testing Consonance)**]{} We say that the contract $C$ is [*testing consonant*]{} with the role $r$ of the well formed choreography $H$ (written $C \otimes^r_{test} H$) if $${\cal NF}\big(  C {{\setminus \!\!\!\!\; \setminus}}I(C) - I({[\![H]\!]}_r) \big) \preceq_{test} 
 {\cal NF}\big( {[\![H]\!]}_r \big)$$

Given a well-formed choreography $H$, we have that the testing consonance relation $C \otimes^r_{test} H$ is a conformance relation.

Summary of Results {#summary}
------------------

We now summarize the results that we have obtained about contract refinement and choreography conformance for different forms of communication.

The first mean of classification of possible scenarios is based on the [*amount of knowledge*]{} about the (initial) behavioural description of the other roles the conformance relation may depend on. We considered: knowledge about the whole choreography (full knowledge about the behaviour of other roles) or knowledge restricted to input types (receive operations) and/or output types (invoke operations) that the other roles may use. The second mean of classification of possible scenarios is based on the [*kind of service compliance*]{} assumed (i.e. of the principle assumed for assessing when multiple services work well together and form a correct system). We considered: $(i)$ “normal” compliance, as reported in this paper, where service interaction via invoke and receive primitives is based on synchronous handshake communication and both receive and invoke primitives may wait indefinitely (with no exception occurring) for a communication to happen, see [@sfm09; @fundaInfo08; @fsen07] and [@libroCubo; @sensoria; @SC07] where, in addition to the standard CCS synchronization, locations expressing a unique address for every system contract are introduced and outputs are directed to a location (as in the thoery presented in this paper); $(ii)$ “strong compliance”, where we additionally require that, whenever a service may perform an invoke on some operation, the invoked service must be already in the receive state for that operation as for the ready-send primitive of the Message Passing Interface [@mscs09; @coord07]; $(iii)$ “queue-based compliance”, where service interaction via invoke and receive primitives is based on asynchronous communication: the receiving service puts invoke requests in an unbounded queue [@libroCubo; @wsfm08].

Concerning service compliance we considered in all cases the fair termination property presented in this paper. Our results are summarized in the following.

-   Knowledge about the whole choreography (direct conformance relation with respect to a choreography for a certain role): the maximal independent conformance relation does not exist, no matter which kind of service compliance (among those mentioned above) is considered.

-   Knowledge about other initial contracts limited to input/output types they use (conformance by means of refinement of a single contract parameterized on the I/O knowledge about the others, as in this paper):

    -   In the case of “normal compliance” we have that: for unconstrained contracts the maximal independent conformance relation does not exist; for contracts such that the output persistence property holds the maximal independent conformance relation exists and knowledge about input types is not significant; for output persistent contracts where locations expressing a unique address for every system contract are introduced and outputs are directed to a location, as for the theory in this paper, the maximal relation exists and knowledge about both input and output types is not significant.

    -   In the case of “strong compliance” we have that: for unconstrained contracts (where outputs are directed to a location identifying a unique system contract) the maximal relation exists and knowledge about both input and output types is not significant.

    -   In the case of “queue-based compliance” we have that: for unconstrained contracts (where outputs are directed to a location identifying a unique system contract) the maximal relation exists and knowledge about both input and output types is not significant.

For every maximal refinement relation above (apart from the queue-based one), we provide a sound characterization that is decidable, by resorting to an encoding into should-testing [@RV05]. As a consequence we obtain:

-   An algorithm (based on that in [@RV05]) to check refinement.

-   A classification of the maximal refinement relations with respect to existing pre-orders as, e.g., (half) bisimulation, (fair/must) testing, trace inclusion.

    In particular we show that the maximal refinement relations are coarser with respect to bisimulation and must testing preorders (up to some adequate encoding and treatment of fairness) in that, e.g., they allow external non-determinism on inputs to be added in refinements.

Related Work and Conclusion
===========================

Among our main contributions we can mention (i) the formalisation of the relationship between global choreographic descriptions and systems obtained as parallel compositions of peers, (ii) the definition of suitable notions of contract refinement, and (iii) the proposal of mechanisms for dynamic updates for both the choreography and the orchestration calculi. Concerning (i), we have defined well-formedness for choreographies based on natural projection and the notion of implementation. We have introduced the simple technique of obtaining orchestrations by projection, defining it for communication actions and then exploiting omomorphism over all the process algebraic operators. Moreover our approach leads to a more general notion of well-formedness w.r.t. other approaches like, e.g., [@CHY07], where it is defined in terms of three connectedness constraints similar to those we have defined in Section \[sec:connect\]. Concerning (ii), our main contribution is related to the idea of refining all peers guaranteeing that all of them continue to reach local success. This differs from other popular approaches, like those initiated by Fournet et al. [@FHRR04] or Padovani et al. [@CCLP06], where the focus is on the success of one specific peer (usually, the so-called, [*client*]{}). Concerning (iii), it is worth to mention that [@ivan] has been a source of inspiration for the present work: the main difference is our choice of expressing adaptation in terms of scopes and code update constructs, rather than using rules. This approach appears more adequate for the definition of a general theory of behavioural typing to be used on more general languages where multiple protocols/choreographies can interleave inside the same program.

Now some remarks concerning future work. We are working on applying the theory of updatable choreographies/orchestrations in the context of session types for typing a concrete language with session spawning, where choreographies play the role of global types attached to sessions and we use orchestrations for checking, via typing rules, that the code actually conforms with the specified global types. In this context, extending our contract refinement theory to updatable choreographies/orchestrations (thus getting updatable behavioural contracts) would make it possible to define a notion of semantic subtyping. We also plan to work on the complete characterization of compliance testing: work in this direction has been done in [@BH13] where however testing is characterized only for controllable processes (i.e. processes for which there exists a compliant test) and fairness is not considered (a testing notion similar to our compliance testing is considered, where both the test and the system under test must succeed, but in the flavour of traditional testing of [@DH84] without assuming fairness).

[BBM05]{} Bernardi G., Hennessy M.: Mutually Testing Processes - (Extended Abstract). *Proc. CONCUR 2013*: LNCS 8052, Springer, 2013, 61–75. [doi:[[10.1007/978-3-642-40184-8\_6](http://dx.doi.org/10.1007/978-3-642-40184-8_6)]{}]{}

Boreale, M., Bravetti, M.: Advanced Mechanisms for Service Composition, Query and Discovery. *Rigorous Software Engineering for Service-Oriented Systems*, LNCS 6582, Springer, 2011, 282–301. [doi:[[10.1007/978-3-642-20401-2\_13](http://dx.doi.org/10.1007/978-3-642-20401-2_13)]{}]{}

Bravetti M., Carbone M., Hildebrandt T., Lanese I., Mauro J., Perez J.A. and Zavattaro G.: Towards Global and Local Types for Adaptation. *Proc. of [*2nd International Workshop on Behavioural Types – SEFM’13 Collocated Workshops*]{}* pages 1–12, volume 8378 of [*Lecture Notes in Computer Science*]{}, Springer-Verlag, 2013. [doi:[[10.1007/978-3-319-05032-4\_1](http://dx.doi.org/10.1007/978-3-319-05032-4_1)]{}]{}

Bravetti, M., Guidi, C., Lucchi, R., Zavattaro, G.: Supporting e-commerce systems formalization with choreography languages. *Proc. SAC’05, track on E-Commerce Technologies*,ACM PRESS, 2005, 831–835. [doi:[[10.1145/1066677.1066867](http://dx.doi.org/10.1145/1066677.1066867)]{}]{}

Bravetti, M., Lanese, I., Zavattaro, G.: Contract-Driven Implementation of Choreographies. *Proc. TGC 2008*: LNCS 5474, Springer, 2009, 1–18. [doi:[[10.1007/978-3-642-00945-7\_1](http://dx.doi.org/10.1007/978-3-642-00945-7_1)]{}]{}

Bravetti, M., Zavattaro, G.: Contract based Multi-party Service Composition, *Proc. FSEN’07*, LNCS 4767, Springer, 2007, 207–222. [doi:[[10.1007/978-3-540-75698-9\_14](http://dx.doi.org/10.1007/978-3-540-75698-9_14)]{}]{}

Bravetti, M., Zavattaro, G.: A Theory for Strong Service Compliance, *Proc. Coordination’07*, LNCS 4467, Springer, 2007, 96–112. [doi:[[10.1007/978-3-540-72794-1\_6](http://dx.doi.org/10.1007/978-3-540-72794-1_6)]{}]{}

Bravetti, M., Zavattaro, G.: Towards a Unifying Theory for Choreography Conformance and Contract Compliance, *Proc. SC’07*, LNCS 4829, Springer, 2007, 34–50. [doi:[[10.1007/978-3-540-77351-1\_4](http://dx.doi.org/10.1007/978-3-540-77351-1_4)]{}]{}

Bravetti, M., Zavattaro, G.: Contract Compliance and Choreography Conformance in the Presence of Message Queues, *Proc. WS-FM’08*, volume to appear of [*LNCS*]{}, 2008. [doi:[[10.1007/978-3-642-01364-5\_3](http://dx.doi.org/10.1007/978-3-642-01364-5_3)]{}]{}

Bravetti, M., Zavattaro, G.: A Foundational Theory of Contracts for Multi-party Service Composition, *Fundamenta Informaticae* 89(4):451–478, IOS Press, 2008. Bravetti, M., Zavattaro, G.: Contract-Based Discovery and Composition of Web Services, *9th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Web Services (SFM-09:WS)*, LNCS 5569, Springer, 2009, 34–50. [doi:[[10.1007/978-3-642-01918-0\_7](http://dx.doi.org/10.1007/978-3-642-01918-0_7)]{}]{}

Bravetti, M., Zavattaro, G.: A Theory of Contracts for Strong Service Compliance, *Mathematical Structure in Computer Science* 19(3):601–638, Cambridge University Press, 2009. [doi:[[10.1017/S0960129509007658](http://dx.doi.org/10.1017/S0960129509007658)]{}]{}

Bravetti, M., Zavattaro, G.: Service Discovery and Composition based on Contracts and Choreographic Descriptions, *Adaptive Web Services for Modular and Reusable Software Development: Tactics and Solutions*, IGI Global, 2012. [doi:[[10.4018/978-1-4666-2089-6](http://dx.doi.org/10.4018/978-1-4666-2089-6)]{}]{}

Carbone M., Honda K., Yoshida N.: Structured Communication-Centred Programming for Web Services. In [*ESOP’07*]{}, volume to appear of LNCS, 2007. [doi:[[10.1007/978-3-540-71316-6\_2](http://dx.doi.org/10.1007/978-3-540-71316-6_2)]{}]{}

Carpineti S., Castagna G., Laneve C., Padovani L.: A Formal Account of Contracts for Web Services. In [*WS-FM’06*]{}, volume 4184 of LNCS, pages 148-162, 2006. [doi:[[10.1007/11841197\_10](http://dx.doi.org/10.1007/11841197_10)]{}]{}

Dalla Preda M., Giallorenzo S., Lanese I., Mauro J., Gabbrielli M.: [AIOCJ:]{} [A]{} Choreographic Framework for Safe Adaptive Distributed Applications. *Proc. SLE 2014*: LNCS 8706, Springer, 2014, 161–170. [doi:[[10.1007/978-3-319-11245-9\_9](http://dx.doi.org/10.1007/978-3-319-11245-9_9)]{}]{}

De Nicola R., Hennessy M.: Testing Equivalences for Processes. , volume 34: 83–133, 1984. [doi:[[10.1016/0304-3975(84)90113-0](http://dx.doi.org/10.1016/0304-3975(84)90113-0)]{}]{}

Fournet C., Hoare C.A.R, Rajamani S.K., Rehof J.: Stuck-Free Conformance. In [*Proc. CAV’04*]{}, volume 3114 of LNCS, pages 242–254, 2004. [doi:[[10.1007/978-3-540-27813-9\_19](http://dx.doi.org/10.1007/978-3-540-27813-9_19)]{}]{}

Lanese I., Guidi C., Montesi F., Zavattaro G.: Bridging the gap between Interaction- and Process-Oriented Choreographies. *Proc. of [*6th IEEE International Conferences on Software Engineering and Formal Methods*]{}* (SEFM’08), pages 323–332, IEEE Computer Society press, 2008. [doi:[[10.1109/SEFM.2008.11](http://dx.doi.org/10.1109/SEFM.2008.11)]{}]{}

Rensink A., Vogler W.: Fair testing. , volume 205(2): 125-198, 2007 [doi:[[10.1016/j.ic.2006.06.002](http://dx.doi.org/10.1016/j.ic.2006.06.002)]{}]{}

OASIS. .

W3C. . .
