Towards Global and Local Types for Adaptation

Abstract

Choreographies allow designers to specify the protocols followed by participants of a distributed interaction. In this context, adaptation may be necessary to respond to external requests or to better suit a changing environment (a self-update). Adapting the behavior of a participant requires to update in a coordinated way possibly all the participants interacting with him. We propose a language able to describe a choreography together with its adaptation strategies, and we discuss the main issues that have to be solved to enable adaptation on a participant code dealing with many interleaved protocols.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Modern complex distributed software systems face the great challenge of adapting to varying contextual conditions, user requirements or execution environments. Service-oriented Computing (SOC), and service-oriented architectures in general, have been designed to support a specific form of adaptation: services can be dynamically discovered and properly combined in order to achieve an overall service composition that satisfies some specific desiderata that could be known only at service composition time. Rather sophisticated theories have been defined for checking and guaranteeing the correctness of these service assemblies (see, e.g., the rich literature on choreography/orchestration languages [2, 14], behavioral contracts [6, 7], and session types [4, 5, 12]). In this paper, we consider a more fine-grained form of adaptation that can occur when the services have been already combined but have not yet completed their task. This form of adaptation may arise, for instance, when the desiderata dynamically change or when some unexpected external event occurs. In particular in the context of computer-supported case management, e.g. for health-care or financial services, changes are the norm rather than the exception. This has lead to an increasing interest both from academia and industry in the development of technologies supporting dynamic changes in choreographies and processes, collectively referred to as adaptive case management (ACM) [17, 19] and being addressed in the recent proposal for a Case Management Model and Notation (CMMN) from OMG [18]. For such technologies, it is crucial that modifications occur in a consistent and coordinated manner in order to avoid breaking the correctness of the overall service composition.

In this paper, we initiate the investigation of new models and theories for service composition that properly take into account this form of adaptation. First of all, we extend a previous language for the description of service choreographies [2] with two operators: the first one allows for the specification of adaptable scopes that can be dynamically modified, while the second may dynamically update code in one of such scopes. This language is designed for the global description of dynamically adaptable multi-party interaction protocols. As a second step in the development of our theory, we define a service behavioral contract language for the local description of the input-output communications. In order to support adaptation, also in this case we enhance an existing service contract language [2] with two new operators for adaptable scope declaration and code update, respectively. The most challenging aspect to be taken into account is the fact that, at the local level, peers should synchronize their local adaptations in order to guarantee a consistent adaptation of their behavior. As mentioned above, these two languages are expected to be used to describe multi-party protocols from global and local perspectives, respectively. The relationship between the two languages is formalized in terms of a projection function which allows us to obtain endpoint specifications from a given choreography.

The complete theory that we plan to develop will also consider a concrete language for programming services; such a language will include update mechanisms like those provided by, for instance, the Jorba service orchestration language [13]. The ultimate aim of our research is to define appropriate behavioral typing techniques able to check whether the concretely programmed services correctly implement the specified multi-party adaptable protocols. This will be achieved by considering the global specification of the protocol, by projecting such specification on the considered peer, and then by checking whether the actual service correctly implements the projected behavior. In order to clarify our objective, we discuss an example inspired by a health-care scenario [16]. Two adaptable protocols are described by using the proposed choreography languages: the first protocol describes the interaction between the doctor and the laboratory agents, while the second involves a doctor, a nurse, and a patient. In case of emergency, the doctor may speed up the used protocols by interrupting running tests and avoiding the possibility that the nurse refuses to use a medicine she does not trust —this possibility is normally allowed by the protocol. Then, using a $\pi$-calculus-like language, we present the actual behavior of the doctor and discuss the kinds of problems that we will have to address in order to define appropriate behavioral type checking techniques.

Structure of the Paper. The next section introduces choreography and endpoint languages with adaptation constructs, and the projection function that relates global and local specifications. Then, in Sect. 3 we outline a concrete specification language and discuss the health-care scenario. In Sect. 4 we present some concluding remarks and briefly review related works.

Disclaimer. This paper discusses ongoing work supported by the “Behavioural Types for Reliable Large-Scale Software Systems” (BETTY) Cost Action. Our main aim is to report about the current state of this research activity.

2 Choreography and Endpoint Languages for Adaptation

In the paper, we use the following sets: channels, ranged over by $a, a', \ldots$; scope names, ranged over by $X, X', \ldots$; and roles/participants, ranged over by $r, r_1, r_2, \ldots$. Also, we use $T, T', \ldots$ to denote sets of roles.

2.1 Choreography Language

Syntax. We describe here the syntax of our choreography language. To this end, we first define a set of so-called choreography terms. Then, by requiring some well-formedness conditions on such terms, we obtain actual choreographies.

The syntax of choreography terms is as follows:

$$\begin{aligned} \begin{array} {lllllllllll} C \,{::=}\; &{} a_{r_1\rightarrow r_2} &{} (\text {interaction}) &{} | &{} C\; ;\; C &{} (\text {sequence})\\ \quad | &{} C\ \mathbf {|}\ C &{} (\text {parallel}) &{} | &{} C + C &{} (\text {choice})\\ \quad | &{} C^* &{} (\text {star}) &{} | &{} \mathbf {1}&{} (\text {one})\\ \quad | &{} \mathbf {0}&{} (\text {nil})\\ \quad | &{} X:T[C] &{} (\text {scope}) &{} | &{} {X}_{r}\{C\} &{} (\text {update}) \end{array} \end{aligned}$$

The basic element of a choreography term $C$ is an interaction $a_{r_1\rightarrow r_2}$, with the intended meaning that participant $r_1$ sends a message to participant $r_2$ over channel $a$. Two terms $C_1$ and $C_2$ can be composed in sequence ($C_1 \ ; \ C_2$), in parallel ($C_1 \ \mathbf {|}\ C_2$), and using nondeterministic choice ($C_1 + C_2$). Also, a choreography term may be iterated zero or more times using the Kleene star $^*$. The empty choreography term, which just successfully terminates, is denoted by $\mathbf {1}$. The deadlocked choreography term $\mathbf {0}$ is needed for the definition of the semantics: we will assume that it is never used when writing a choreography (see Definition 1).

The two last operators deal with adaptation. Adaptation is specified by defining a scope that delimits a choreography term that, at runtime, may be replaced by a new choreography term, coming from either inside or outside the system. Adaptations coming from outside may be decided by the user through some adaptation interface, by some manager module, or by the environment. In contrast, adaptations coming from inside represent self-updates, decided by a part of the system towards itself or towards another part of the system, usually as a result of some interaction producing unexpected values. Adaptations from outside and from inside are indeed quite similar, e.g., an update decided by a manager module may be from inside if the manager behavior is part of the choreography term, from outside if it is not. Construct $X:T[C]$ defines a scope named $X$ currently executing choreography term $C$ — the name is needed to designate it as a target for a particular adaptation. Type $T$ is the set of roles (possibly) occurring in the scope. This is needed since a given update can be applied to a scope only if it specifies how all the involved roles are adapted. Operator ${X}_{r}\{C\}$ defines internal updates, i.e., updates offered by a participant of the choreography term. Here $r$ denotes the participant offering the update, $X$ is the name of the target scope, and $C$ is the new choreography term.

Not all choreography terms generated by the syntax above are useful choreographies. To formally define the choreography terms which actually represent choreographies, we rely on some auxiliary definitions. The set of roles inside a choreography term $C$, denoted $roles(C)$, is defined inductively as follows:

$$\begin{aligned} roles(a_{r_1\rightarrow r_2})&= \{r_1, r_2\} \quad \qquad ~\, roles( {X}_{r}\{C\}) = \{r\} \\ roles(X:T[C])&= T \cup roles(C) \,\,\,\quad roles(C^*) = roles(C) \\ roles(C_1\; ;\; C_2)&= roles(C_1\ \mathbf {|}\ C_2) = roles(C_1 + C_2) = roles(C_1) \cup roles(C_2) \\ roles(\mathbf {1})&= roles(\mathbf {0}) = \emptyset \end{aligned}$$

Notice that for ${X}_{r}\{C\}$ we consider role $r$ but not the roles in $C$. This is because ${X}_{r}\{C\}$ may correspond to an external update on some different choreography term. We are now ready to define choreographies.

Definition 1

(Choreography). A choreography term $C$ is a choreography if:

• 1. $C$ does not contain occurrences of $\mathbf {0}$;

• 2. all names of scopes in $C$ are pairwise distinct;

• 3. $C$ is well-typed, i.e. for every scope $X:T[C']$ occurring in $C$:

  • $roles(C') \subseteq T$ and

  • every update prefix ${X}_{r}\{C''\}$ occurring in $C$ is such that $roles(C'') \subseteq T$.

We use $type(X)$ to denote the type $T$ associated to the unique scope $X:T[C']$.

Semantics. We now define the semantics of choreography terms via a labeled transition system. As in the syntax, the most interesting part of the semantics concerns update constructs. Recall that $T$ is a set of roles. In the definition below, we use $C [C'/X]$ to denote the substitution that replaces all scopes $X:T[C'']$ with name $X$ occurring in $C$ (not inside update prefixes) with $X:T[C']$. As usual, transition $C \xrightarrow {\,\alpha \,} C'$ intuitively says that choreography term $C$ may evolve to $C'$ by performing an action represented by a label $\alpha$. Our set of labels includes $\surd$ (termination), $a_{r_1\rightarrow r_2}$ (interaction), and ${X}_{r}\{C\}$ (update).

Table 1. Semantics of Choreography Terms

Definition 2

The semantics of choreography terms is the smallest labeled transition system closed under the rules in Table 1.

We briefly comment on the rules in Table 1. Rules in the first four rows of the table are standard (cf. [2]). Rule (One) defines termination for the empty choreography term. Rule (Comm) executes an interaction, making it visible in the label. While rule (Seq) allows the first component of a sequential composition to compute, rule (SeqTick) allows it to terminate, starting the execution of the second component. Rule (Par) allows parallel components to interleave their executions. Rule (ParTick) allows parallel components to synchronize their termination. Rule (Cho) selects a branch in a nondeterministic choice. Rule (Star) unfolds the Kleene star. Note that the unfolding may break uniqueness of scopes with a given name—we will come back to this point later on. Rule (StarTick) defines termination of a Kleene star.

The remaining rules in Table 1 deal with adaptation. Rule (CommUpd) makes an internal adaptation available, moving the information to the label. Adaptations propagate through sequence, parallel composition, and Kleene star using rules (SeqUpd), (ParUpd), and (StarUpd), respectively. Note that, while propagating, the update is applied to the continuation of the sequential composition, to parallel terms, and to the body of Kleene star. Notably, the update is applied to both enabled and non enabled occurrences of the desired scope. Rule (ScopeUpd) allows a scope to update itself (provided that the names coincide), while propagating the update to the rest of the choreography term.Rule (Scope) allows a scope to compute.

We can now define the notion of closed traces that correspond to computations of stand-alone choreography terms.

Definition 3

(Traces). Given a choreography term $C_0$ a trace is a (possibly infinite) sequence $C_0 \xrightarrow {\alpha _1} C_1 \xrightarrow {\alpha _2} C_2 \xrightarrow {\alpha _3} \cdots$.

In order to model choreography terms that can be externally updated we need to introduce the notion of open transitions.

Definition 4

(Open transitions). The choreography term $C$ has an open transition of the form $C \xrightarrow {{X}_{}\{C''\}} C[C''/X]$ if:

• there is a choreography $C_0$ with a trace $C_0 \xrightarrow {\alpha } \cdots \xrightarrow {\alpha '} {C}_0^{'}|C$;

• ${C}_0^{'} \xrightarrow { {X}_{r}\{C''\}} {C}_0^{''}$ where $r \not \in roles(C)$ and $X$ is the name of a scope in $C$.

We can now define the notion of open traces corresponding to computations including also open transitions.

Definition 5

(Open Traces). Given a choreography term $C_0$ an open trace is a (possibly infinite) sequence $C_0 \xrightarrow {\alpha _1} C_1 \xrightarrow {\alpha _2} C_2 \xrightarrow {\alpha _3} \cdots$ where every $C_i \xrightarrow {\alpha _{i+1}} C_{i+1}$ is either a transition of the semantics in Table 1 or an open transition.

As we have said, in a choreography we assume scope names to be unique. However, uniqueness is not preserved by transitions. Nevertheless a slightly weaker property (arising from the fact that we consider Kleene star as the only form of recursion) is indeed preserved, and it simplifies the implementation of the adaptation mechanisms at the level of endpoints.

Proposition 1

Let $C$ be a choreography and let $C'$ be a choreography term reachable from $C$ via zero or more transitions (possibly open). For every $X$, $C'$ contains at most one occurrence of a scope named $X$ which is enabled (i.e., which can compute).

An Example. Below we give an example of an adaptable choreography to illustrate the features introduced above. The example is based on a health-care workflow inspired by field study [16] carried out in previous work. The field study was also considered as inspiration for recent work on session types for health-care processes [11] and adaptable declarative case management processes [17], but the combination of session types and adaptability has not been treated previously.

In the considered scenario, doctors, nurses and patients employ a distributed, electronic health-care record system where each actor (including the patient) uses a tablet pc/smartphone to coordinate the treatment. Below, iteration $C^+$ stands for $C;C^*$.

$$\begin{aligned} X:\{D,N\}&[\bigl (( {prescribe_{D\rightarrow N}} )^+ ;\\&({sign_{D\rightarrow N}} + {X}_{D}\{{sign_{D\rightarrow N}} \} ; up_{D\rightarrow N}) ; {trust_{N\rightarrow D}} \bigr )^+] ;\\&\qquad \qquad \qquad \qquad \qquad \qquad \quad \qquad \qquad {medicine_{N\rightarrow P}} \end{aligned}$$

where $D, N, P$ denote participant doctors, nurses, and patients, respectively.

The doctor first records one or more prescriptions, which are sent to the nurse’s tablet $({prescribe_{D\rightarrow N}})^+$. When receiving a signature, ${sign_{D\rightarrow N}}$, the nurse informs the doctor if the prescription is trusted. If not trusted then the doctor must prescribe a new medicine. If trusted, the nurse proceeds and gives the medicine to the patient, which is recorded at the patient’s smartphone, ${medicine_{N\rightarrow P}}$. However, instead of signing and waiting for the nurse to trust the medicine, in emergency cases the doctor may update the protocol so that the possibility of not trusting the prescription is removed: the nurse would have to give the medicine to the patient right after receiving the signature. In the example, this is done by a self-update (${X}_{D}\{{sign_{D\rightarrow N}}\}$) of the running scope. In other scenarios, this could have been done by an entity not represented in the choreography, such as the hospital director, thus resulting in an external update. The doctor notifies the protocol update to the nurse using the ${up_{D\rightarrow N}}$ interaction.

Now consider the further complication that the doctor may run a test protocol with a laboratory, after prescribing a medicine and before signing:

$$ X'\{D,L\}: [ {orderTest_{D\rightarrow L}} \; ;\; ({results_{L\rightarrow D}} + {X'}_D\{\mathbf {1}\}) ] $$

We allow the test protocol also to be adaptable, since the doctor may decide that there is an emergency while waiting for the results, and thus also having to interrupt the test protocol. If the two protocols are performed in interleaving by the same code, then the updates of the two protocols should be coordinated. We illustrate this in Sect. 3 below.

2.2 Endpoint Language

Since choreographies are at the very high level of abstraction, defining a description of the same system nearer to an actual implementation is of interest. In particular, for each participant in a choreography (also called endpoint) we would like to describe the actions it has to take in order to follow the choreography. The syntax of endpoint processes is as follows:

$$\begin{aligned} \begin{array} {llllllllll} P \,{::=}\; &{} \overline{a}_r &{} (\text {output}) &{} |\,\, a_r &{} (\text {input})\\ \quad | &{} P\; ;\; P &{} (\text {sequence}) &{} |\,\, P\ \mathbf {|}\ P &{} (\text {parallel})\\ \quad | &{} P+P &{} (\text {choice}) &{} |\,\, P^* &{} (\text {star})\\ \quad | &{} \mathbf {1}&{} (\text {one}) &{} |\,\, \mathbf {0}&{} (\text {zero})\\ \quad | &{} X[P]^F &{} (\text {scope}) &{} |\,\, {X}_{(r_1,\ldots ,r_n)}\{P_1,\ldots ,P_n\} &{} (\text {update}) \end{array} \end{aligned}$$

where $F$ is either $A$, denoting an active (running) scope, or $\varepsilon$, denoting a scope still to be started ($\varepsilon$ is omitted in the following).

As for choreographies, endpoint processes contain some standard operators and some operators dealing with adaptation. Communication is performed by $\overline{a}_r$, denoting an output on channel $a$ towards participant $r$. Dually, $a_r$ denotes an input from participant $r$ on channel $a$. Intuitively, an output $\overline{a}_r$ in role $s$ and an input $a_s$ in role $r$ should synchronize. Two endpoint processes $P_1$ and $P_2$ can be composed in sequence ($P_1 \ ; \ P_2$), in parallel ($P_1 \ \mathbf {|}\ P_2$), and using nondeterministic choice ($P_1 + P_2$). Endpoint processes can be iterated using a Kleene star $^*$. The empty endpoint process is denoted by $\mathbf {1}$ and the deadlocked endpoint process is denoted by $\mathbf {0}$.

Adaptation is applied to scopes. $X[P]^F$ denotes a scope named $X$ executing process $P$. $F$ is a flag distinguishing scopes whose execution has already begun ($A$) from scopes which have not started yet ($\varepsilon$). The update operator ${X}_{(r_1,\ldots ,r_n)}\{P_1,\ldots ,P_n\}$ provides an update for scope named $X$, involving roles $r_1,\ldots ,r_n$. The new process for role $r_i$ is $P_i$.

Endpoints are of the form $[\![ P ]\!]_r$, where $r$ is the name of the endpoint and $P$ its process. Systems, denoted $S$, are obtained by composition of parallel endpoints:

$$\begin{aligned} \begin{array} {rllllllll} S \,{::=}\; [\![ P ]\!]_r &{}\qquad (\text {endpoint}) &{} \quad | S \mathbf {|\!|}S &{}\qquad (\text {parallel system})\\ \end{array} \end{aligned}$$

As for choreographies, not all systems are endpoint specifications. By a slight abuse of notation we extend $type(X)$ to endpoints associating a set of roles to each scope name $X$. Endpoint specifications are defined as follows.

Definition 6

A system $S$ is an endpoint specification if the following conditions hold:

• (i) no active scopes are present

• (ii) endpoint names are unique

• (iii) all roles $r$ occurring in terms of the form $\overline{a}_r$, $a_r$, or such that $r \in type(X)$ for some scope $X$ are endpoints of $S$

• (iv) a scope with name $X$ con occur (outside updates) only in endpoints $r \in type(X)$

• (v) every update has the form ${X}_{type(X)}\{P_1,\ldots ,P_n\}$

• (vi) outputs $\overline{a}_r$ and inputs $a_r$ included in ${X}_{type(X)}\{P_1,\ldots ,P_n\}$ are such that $r \in type(X)$.

In this presentation, we do not formally define a semantics for endpoints: we just point out that it should include labels corresponding to all the labels of the semantics of choreography terms, plus some additional labels corresponding to partial activities, such as an input. We also highlight the fact that all scopes which correspond to the same choreography scope evolve together: their scope start transitions (transforming a scope from inactive to active) are synchronized, as well as their scope end transitions (removing it). The fact that choreographies feature at most one scope with a given name is instrumental in ensuring this property.

2.3 Projection

Since choreographies provide system descriptions at the high level of abstraction and endpoint specifications provide more low level descriptions, a main issue is to derive from a given choreography an endpoint specification executing it. This is done using the notion of projection.

Definition 7

(Projection). The projection of a choreography $C$ on a role $r$, denoted by ${C}\!\upharpoonright _{r}$, is defined by the clauses below

$$\begin{aligned} {a_{r_1\rightarrow r_2}}\!\upharpoonright _{r}&= {\left\{ \begin{array}{ll}{\overline{a}_{r_2}} &{} {if r = r_1}\\ a_{r_1} &{} if r = r_2 \\ \mathbf {1}&{} {otherwise}\end{array}\right. } \\ { {X}_{r'}\{C\}}\!\upharpoonright _{r}&= {\left\{ \begin{array}{ll} {X}_{(r_1,\ldots ,r_n)}\{{C}\!\upharpoonright _{r_1},\ldots ,{C}\!\upharpoonright _{r_n}\} {with \{r_1,\ldots ,r_n\}= type(X)} &{} \!\!\!\!{if r = r'}\\ \mathbf {1}&{} \!\!\!\!\!\!\!\!{otherwise}\end{array}\right. } \\ {X:T[C]}\!\upharpoonright _{r}&= {\left\{ \begin{array}{ll} X[{C}\!\upharpoonright _{r}] &{} {if r \in type(X)}\\ \mathbf {1}&{} {otherwise} \end{array}\right. } \end{aligned}$$

and is an homomorphism on the other operators. The endpoint specification resulting from a choreography $C$ is obtained by composing in parallel roles $[\![{C}\!\upharpoonright _{r}]\!]_r$, where $r \in roles(C)$.

As an example, the endpoint projection obtained from the prescribe choreography introduced in Sect. 2.1 is $[\![ P_\mathtt{N } ]\!]_N \mathbf {|\!|}[\![ P_\mathtt{D } ]\!]_D \mathbf {|\!|}[\![ P_\mathtt{P } ]\!]_P$ where processes $P_\mathtt{N }$, $P_\mathtt{D }$, and $P_\mathtt{P }$ are as follows (we omit unnecessary $\mathbf {1}$ processes):

$$\begin{aligned} P_\mathtt{N }&= X[((prescribe_D)^+ \; ; \; ( sign_D + up_D \;) ; \; \overline{trust}_D)^+] \; ; \;\overline{medicine}_P\\ P_\mathtt{D }&= X[((\overline{prescribe}_N)^+ \; ; \; (\overline{sign}_N + X_{D,N}\{\overline{sign}_N, sign_D\} \; ; \; \overline{up}_N );trust_N)^+] \\ P_\mathtt{P }&= medicine_N \end{aligned}$$

One can see that the system $S$ obtained by projecting a choreography is an endpoint specification. Ideally, traces of the projected system should correspond to the traces of the original choreography. Actually, we conjecture that this occurs only for choreographies satisfying suitable connectedness conditions that we plan to formalize extending those in [14]. This is not an actual restriction, since choreographies that do not respect the conditions can be transformed into choreographies that respect them [15].

Conjecture 1

Traces of projection of connected choreographies correspond to traces of the original choreography.

We point out two main aspects of the correspondence. First, labels ${X}_{r}\{C\}$ of transitions of the choreography should be mapped to labels $[{X}{(r_1,\ldots ,r_n)}$ $\{P_1,\ldots ,P_n\}]_r$ of the transitions of the endpoint specification, where $type(X) = \{r_1,\ldots ,r_n\}$ and $P_1 = {C}\!\upharpoonright _{r_1},\ldots , P_n = {C}\!\upharpoonright _{r_n}$ are obtained by projection from $C$. Second, endpoint traces should not consider unmatched input and output labels.

3 Typing a Concrete Language

As demonstrated by our examples, choreography and endpoint terms provide a useful language for expressing protocols with adaptation. In this section, we investigate the idea of using such protocols as specifications for a programming language with adaptation. We plan to follow the approach taken in multiparty session types [12], where choreographies (and endpoints) are interpreted as behavioral types for typing sessions in a language modeled as a variant of the $\pi$-calculus. In the sequel, we investigate the core points of such a language by giving an implementation that uses the protocols specified in the examples of the previous sections. In particular, we discuss what are the relevant aspects for developing a type system for such a language, whose types are the choreographies introduced in Sect. 2.1.

In both prescribe and test protocols, the doctor plays a key role since (s)he initiates the workflow with prescriptions, decides when tests have to be requested, and decides when the protocols have to be interrupted due to an emergency. A possible implementation of the doctor could be given by the following program:

$$\begin{aligned} \begin{array}{lrl} 1. &{} P_\mathtt{D }\ =\ &{} \overline{\mathsf {pr}}(k);\ X[\ \mathtt {repeat}\ \{\mathtt {repeat}\ \{\\ 2. &{} &{} \qquad \quad k:\overline{prescribe}_{N}\langle e_{pr}\rangle ;\ \overline{\mathsf {test}}(k');\ \\ 3. &{} &{} \qquad \quad X'[k':\overline{orderTest}_{L}\langle e_o\rangle ;\\ 4. &{} &{} \qquad \quad \quad (k':{results}_{L}(x) + \\ 5. &{} &{} \qquad \quad \quad \quad X'_{(D,L)}\{ X_{(D,N)}\{k:\overline{sign}_{N}\langle e_s\rangle ,k:{sign}_{D}(z)\},\mathbf {1}\})]\\ 6. &{} &{} \qquad \}\ \mathtt {until}\ \mathsf {ok}(x);\\ 7. &{} &{} (k:\overline{sign}_{N}\langle e_s\rangle + X_{(D,N)}\{k:\overline{sign}_{N}\langle e_s\rangle ,k:{sign}_{D}(z)\} \; ; \; k:\overline{up}_{N}\langle \rangle ); \\ 8. &{} &{} k:{trust}_{N}(t) \} \ \mathtt {until}\ \mathsf {trusted}(t)\ ] \end{array} \end{aligned}$$

In the code there are two kinds of communication operations, namely protocol initiation operations, where a new protocol (or session) is initiated, and in-session operations where protocol internal operations are implemented. The communication $\overline{\mathsf {pr}}(k)$ is for initiating a protocol called $\mathsf {pr}$ and its semantics is to create a fresh protocol identifier $k$ that corresponds to a particular instance of protocol $\mathsf {pr}$. In-session communications are standard.

The novelty in the process above is in the scope $X[\ldots ]$ and update $X_{\ldots }\{\ldots \}$, which state respectively that the program can be adapted at any time in that particular point, and that an adaptation is available. Interestingly enough, the way the program $P_D$ uses the protocols needs care. If the doctor wants to adapt to emergency while waiting for tests, both the test protocol and the prescription protocol need to be adapted as shown in line 5. If the doctor adapts to emergency after having received tests that are ok, then only the prescription protocol needs to be adapted. One can see that session $pr$ can be typed using the prescribe endpoint specification and session $test$ using the test endpoint specification. The update of $X$ in line 4 does not appear in the protocol test since it acts as an external update for a different protocol.

4 Concluding Remarks and Related Work

Adaptation is a pressing issue in the design of service-oriented systems, which are typically open and execute in highly dynamic environments. There is a rather delicate tension between adaptation and the correctness requirements defined at service composition time: we would like to adapt the system’s behavior whenever necessary/possible, but we would also like adaptation actions to preserve overall correctness.

In this paper, we have reported ongoing work on adaptation mechanisms for service-oriented systems specified in terms of choreographies. By enhancing an existing language for choreographies with constructs defining adaptation scopes and dynamic code update, we obtained a simple, global model for distributed, adaptable systems. We also defined an endpoint language for local descriptions, and a projection mechanism for obtaining (low-level) endpoint specifications from (high-level) choreographies.

We now briefly comment on related works. The work in [9] is closely related, and indeed was a source of inspiration for the current work. It develops a framework for rule-based adaptation in a choreographic setting. Both choreographies and endpoints are defined; their relation is formally defined via projection. The main difference w.r.t. the work described here is our choice of expressing adaptation in terms of scopes and code update constructs, rather than using rules. Also, we consider choreographies as types and we allow multiple protocols to interleave inside code. These problems are not considered in [9].

Our work is also related to the recent work [8], which considers self-adaptive systems monitored by different global descriptions. The description specifies also when the used monitor should change, and the new monitor to be used is determined by an adaptation function. A main difference is that in their approach the code does not change because processes should be able to implement all the global descriptions since the very beginning.

Our approach bears some similarities with works on multiparty sessions [4, 12], and in particular with works dealing with exceptions in multiparty sessions [3]. Our focus so far has been on formally relating global and local descriptions of choreographies via projection and trace correspondence; investigating correctness properties (e.g., communication safety) via typing in our setting is part of ongoing work. We also note that exceptions and adaptation are similar but conceptually different phenomena: while the former are typically related to foreseen unexpected behaviors in (low-level) programs, adaptation appears as a more general issue, for it should account for (unforeseen) interactions between the system and its (varying) environment.

We have borrowed inspiration also from [17], in which adaptive case management is investigated via Dynamic Condition Response (DCR) Graphs, a declarative process model.

Finally, the adaptation constructs we have considered for choreographies and endpoints draw inspiration from the adaptable processes defined in [1]. The application of adaptable processes in session-typed models of structured communications (focusing on the case of binary sessions) has been studied in [10].

An immediate topic for future work is the full formalization of the concrete language and its typing disciplines. Other avenues for future research include the investigation of refinement theories with a testing-like approach, enabled by having both systems and adaptation strategies modeled in the same language, and the development of prototype implementations.