11institutetext: Informatics Research Institute of Albacete,
University of Castilla-La Mancha, Campus Universitario s/n,
02071\. Albacete, SPAIN.
11email<EMAIL_ADDRESS>
# BPEL-RF: A formal framework for BPEL orchestrations integrating distributed
resources

José Antonio Mateo  Valentín Valero  Gregorio Díaz

###### Abstract

Web service compositions are gaining attention to develop complex web systems
by combination of existing services. Thus, there are many works that leverage
the advantages of this approach. However, there are only few works that use
web service compositions to manage distributed resources. In this paper, we
then present a formal model that combines orchestrations written in BPEL with
distributed resources, by using WSRF.

##  1 Introduction

Software systems are gaining complexity and concurrency with the appearance of
new computational paradigms such as Service-Oriented Computing (SOC), Grid
Computing and Cloud Computing. In this kind of systems, the services provider
needs to ensure some levels of quality and privacy to the final user in a way
that had never been raised. Therefore, it is necessary to develop new models
yielding the advantages of recent approaches as web services compositions, but
applied to these recent scenarios. To this end, we have worked up an
operational semantics to manage web services with associated resources by
using the existing machinery in distributed systems, web services
orchestrations.

The definition of a web service-oriented system involves two complementary
views: Choreography and Orchestration. On the one hand, the choreography
concerns the observable interactions among services and can be defined by
using specific languages, e.g., Web Services Choreography Description Language
(WS-CDL) [15]. On the other hand, the orchestration concerns the internal
behavior of a web service in terms of invocations to other services. Web
Services Business Process Execution Language (WS-BPEL) [1] is usually used to
describe these orchestrations, so this is considered the de facto standard
language for describing web services workflow in terms of web service
compositions.

In this scenario, developers require more standardization to facilitate
additional interoperability among these services. Thus, in January of 2004,
several members of the organization _Globus Alliance_ and the computer
multinational _IBM_ with the help of experts from companies such as _HP, SAP,
Akamai, etc._ defined the basis architecture and the initial specification
documents of a new standard for that purpose, Web Services Resource Framework
(WSRF) [9]. Although the web service definition does not consider the notion
of state, interfaces frequently provide the user with the ability to access
and manipulate states, i.e., data values that persist across, and evolve as a
result of web service interactions. It is then desirable to define web service
conventions to enable the discovery of, introspection on, and interaction with
stateful resources in standard and interoperable ways [4]. These observations
motivated the appearance of the WS-Resource approach to modeling states in web
services.

In WSRF, we can see a WS-Resource as a collection of properties _P_ identified
by an address _EPR_ and with a _timeout_ associated. This timeout represents
the lifetime of the WS-Resource. Without loss of generality, we have reduced
the resource properties set to only one allowing us to use the resource
identifier _EPR_ as the representative of this property. On the BPEL hand, we
have only taken into consideration the root scope avoiding any class of
nesting among scopes and we have only modeled the event and fault handling,
leaving the other handling types as future work.

##  2 Related Work

The use of WS-BPEL has been extensively studied by using different types of
formalism such as Petri nets, Finite State Machines and process algebras.
Regarding the use of WS-BPEL together with WS-RF there are few works, and they
only show a description of this union, without a formalization of the model.
In [14] Slomiski uses BPEL4WS in Grid environments and discusses the benefits
and challenges of extensibility in the particular case of OGSI workflows
combined with WSRF-based Grids. Other two works centered around Grid
environments are [10] and [7]. The first justifies the use of BPEL
extensibility to allow the combination of different GRIDs, whereas Ezenwoye et
al. [7] share their experience on BPEL to integrate, create and manage WS-
Resources that implement the factory/instance pattern.

On the Petri nets hand, Ouyang et al. [12] define the necessary elements for
translating BPEL processes into Petri nets. Thus, they cover all the important
aspects in the standard such as exception handling, dead path elimination and
so on. The model they consider differs from ours in that we formalize the
whole system as a composition of orchestrators with resources associated,
whereas they describe the system as a general scope with nested sub-scopes
leaving aside the possibility of administering resources. Furthermore, we have
also formalized the event handling and notification mechanisms. Another
extensive semantics for BPEL 2.0 is presented in [6] by Dumas et al, which
introduces two new interesting improvements. They define several patterns to
simplify some huge nets and introduce the semantics for the WS-BPEL 2.0 new
patterns. On the $\pi$-calculus hand, Dragoni and Mazzara [5] propose a
theoretical scheme focused on dependable composition for the WS-BPEL recovery
framework. In this approach, the recovery framework is simplified and analyzed
via a conservative extension of $\pi$-calculus. The aim of this approach
clearly differs from ours, but it helps us to have a bigger understanding of
the WS-BPEL recovery framework. Other work focused on the BPEL recovery
framework is [13]. Although this is more interested in the compensation
handler, they describe the corresponding rules that manage a web service
composition. Our work is therefore quite complete as we define rules for
nearly all possible activities. In addition, we also consider time
constraints. Finally, we would like to highlight the works of Farahbod et al.
[8] and Busi et al. [3]. In the first one, the authors extract an abstract
operational semantics for BPEL based on abstract state machines (ASM) defining
the framework BPELAM to manage the agents who perform the workflow activities.
In this approach time constraints are considered, but they do not formalize
the timed model. On the other hand, the goal of the latter one is fairly
similar to ours. They also define a $\pi$-calculus operational semantics for
BPEL and describe a conformance notion. They present all the machinery to
model web service compositions (choreographies and orchestrations). The main
differences with our work are that we are more restrictive with respect to
time constraints and we deal with distributed resources.

##  3 BPEL/WSRF

WS-Resource Framework [2] is a resource specification language developed by
OASIS and some of the most pioneering computer companies, whose purpose is to
define a generic framework for modeling web services with stateful resources,
as well as the relationships among these services in a Grid/Cloud environment.
This approach consists of a set of specifications that define the
representation of the WS-Resource in the terms that specify the messages
exchanged and the related XML documents. These specifications allow the
programmer to declare and implement the association between a service and one
or more resources. It also includes mechanisms to describe the means to check
the status and the service description of a resource, which together form the
definition of a WS-Resource. In Table 1 we show the main WSRF elements.

Name |  Describes
---|---
WS-ResourceProperties |  WSRF uses a precise specification to define the properties of the WS-Resources.
WS-Basefaults |  To standardize the format for reporting error messages.
WS-ServiceGroup |  This specification allows the programmer to create groups that share a common set of properties.
WS-ResourceLifetime |  The mission of this specification is to standardize the process of destroying a resource and identify mechanisms to monitor its lifetime.
WS-Notification |  This specification allows to a _NotificationProducer_ to send _notifications_ to a _NotificationConsumer_ in two ways: without following any formalism or with a predefined formalism.
Table 1: WSRF main elements

On the other hand, web services are becoming more and more important as a
platform for Business-to-Business integration. Web service compositions have
appeared as a natural and elegant way to provide new value-added services as a
combination of several established web services. Services provided by
different suppliers can act together to provide another service; in fact, they
can be written in different languages and can be executed on different
platforms. As we noticed in the introduction, we can use web service
compositions as a way to construct web service systems where each service is
an autonomous entity which can offer a series of operations to the other
services conforming a whole system. In this way, it is fairly necessary to
establish a consistent manner to coordinate the system participants such that
each of them may have a different approach, so it is common to use specific
languages such as WS-BPEL to manage the system workflow. WS-BPEL, for short
BPEL, is an OASIS orchestration language for specifying actions within web
service business processes. These actions are represented by the execution of
two types of activities (_basic_ and _structured_) that perform the process
logic. _Basic activities_ are those which describe elemental steps of the
process behavior and _structured activities_ encode control-flow logic, and
can therefore contain other basic and/or structured activities recursively
[1].

##  4 Operational Semantics

We use the following notation: ORCH is the set of orchestrators in the system,
Var is the set of integer variable names, PL is the set of necessary
partnerlinks, OPS is the set of operations that can be performed, EPRS is the
set of resource identifiers, and A is the set of basic or structured
activities that can form the body of a process. The specific algebraic
language, then, that we use for the activities is defined by the following
BNF-notation:

$\begin{array}[]{l}A::={\it throw}\;|\;{\it receive}(pl,op,v)\;|\;{\it
invoke}(pl,op,v_{1})\;|\\\ {\it
reply}(pl,v)\;|\;{\it\overline{reply}(pl,v_{2})}\;|\;{\it
assign}(expr,v_{1})\;|\;{\it wait}(timeout)\;|\\\ {\it empty}\;|\;{\it
exit}\;|\;\ \,\,A\,;A\,\,\;|\,\;A\,\|\,A\;\,|\,{\it while}(cond,A)\;|\\\ \
{\it pick}(\\{(pl_{i},op_{i},v_{i},A_{i})\\}_{i=1}^{n},A,timeout)\;|\\\ {\it
createResource}(EPR,val,timeout,A_{e{{}_{i}}})\;|\;{\it getProp}(EPR,v)\;|\\\
{\it setProp}(EPR,val)\;|\;{\it setTimeout}(EPR,timeout)\;|\\\ {\it
subscribe}(O,EPR,cond^{\prime},A_{e{{}_{i}}})\end{array}$

where ${\it O\in ORCH,EPR\in EPRS,pl,pl_{i}\in PL,op,op_{i}}$ ${\it\in
OPS,timeout\in{\rm I\\!N},expr}$ is an arithmetic expression constructed by
using the variables in Var and integers; ${\it v,v_{1},v_{2},v_{i}}$ range
over Var, and ${\it val\in\mathbb{Z}}$. A condition ${\it cond}$ is a
predicate constructed by using conjunctions, disjunctions, and negations over
the set of variables ${\it Var}$ and integers, whereas ${\it cond^{\prime}}$
is a predicate constructed by using the corresponding ${\it EPR}$ (as the
resource value) and integers.

BPEL basic activities used in our model are: _invoke_ to request services
offered by service providers, _receive_ and _reply_ to provide services to
partners, _throw_ to signal an internal fault explicitly, _wait_ to specify a
delay, _empty_ to do nothing, _exit_ to end the business process and _assign_
, which is used to copy data from a variable to another. And the _structured
activities_ used are: _sequence_ , which contains two activities that are
performed sequentially, _while_ to provide a repeated execution of one
activity, _pick_ that waits for the occurrence of exactly one event from a set
of events (including an alarm event), and then executes the activity
associated with that event, and, finally, _flow_ to express concurrency.
Another family of control flow constructs in BPEL includes event, fault and
compensation handlers. An event handler is enabled when its associated event
occurs, being executed concurrently with the main orchestrator activity.
Unlike event handlers, fault handlers do not execute concurrently with the
orchestrator main activity [12]. The correspondence among the syntax of WS-
BPEL, WSRF and our model is shown in Table 4.

WS-BPEL Syntax |  Metamodel
---|---
$<$process …$>$ |
$<$partnerLinks$>$ … $<$/partnerLinks$>$? |
$<$Variables$>$ … $<$/Variables$>$? |
$<$faultHandlers$>$ … $<$/faultHandlers$>$? |
$<$eventHandlers$>$ … $<$/eventHandlers$>$? |
(activities)* |
$<$/process$>$ |
|  (PL,Var,A,Af,$\mathcal{A}_{e}$)
throw/any fault |  throw
$<$receive partnerLink=“pl” operation=“op” variable=“v” createInstance=“no”$>$ $<$/receive$>$ |  receive(pl,op,v)
$<$reply partnerLink=“pl” variable=“v”$>$ $<$/reply$>$ |  reply(pl,v)
$<$invoke partnerLink=“pl” operation=“op”inputVariable=“v1” outputVariable=“v2”$>$ $<$/invoke$>$ |  invoke(pl,op,v1); $[\overline{reply}$(pl,op,v2)]
|
$<$empty$>$ … $<$/empty$>$ |  empty
$<$exit$>$ … $<$/exit$>$ |  exit
$<$assign$>$$<$copy$>$$<$from$>$expr$<$/from$>$$<$to$>$v1$<$/to$>$$<$/copy$>$$<$/assign$>$ |  assign(expr,v1)
$<$wait$>$$<$for$>$timeout$<$/for$>$ $<$/wait$>$ |  wait(timeout)
$<$sequence$>$ activity1 activity2 $<$/sequence$>$ $<$flow$>$ activity1 activity2 $<$/flow$>$ |  A${}_{1}\,;\,$ A2 —————– A${}_{1}\,\|\,$ A2
$<$while$>$$<$condition$>$cond$<$/condition$>$activity1$<$/while$>$ |  while(cond,A)
$<$pick createInstance=“no”$>$ $<$onMessage partnerLink=“pl” operation=“op”variable=“v”$>$ activity1 $<$/onMessage$>$ $<$onAlarm$>$$<$for$>$timeout$<$/for$>$activity1$<$/onAlarm$>$ $<$/pick$>$ |  pick($\\{(pl_{i},op_{i},v_{i},A_{i})\\}_{i=1}^{n},A$,timeout)
$<$invoke partnerLink=“Factory”operation=“CreateResource” inputVariable=“MessageIn”outputVariable=“MessageOut”$>$ $<$/invoke$>$$<$assign$>$$<$copy$>$$<$from variable=“MessageOut”$>$part=“param” query=“/test:CreateOut/wsa:endpointreference”$<$/from$>$ $<$to$>$ partnerlink=“Factory”$<$/to$>$$<$/copy$>$$<$/assign$>$ |  createResource(EPR,val,timeout,A${}_{e{{}_{i}}}$)
$<$wsrp:GetResourceProperty$>$property1$<$/wsrp:GetResourceProperty$>$ |  getProp(EPR,v)
$<$wsrp:SetResourceProperties$>$ $<$wsrp:Update$>$ property1 $<$/wsrp:Update$>$ $</$wsrp:SetResourceProperties$>$ |  setProp(EPR,val)
$<$wsrl:SetTerminationTime$>$ $<$wsrl:RequestedTerminationTime$>$ timeout $<$/wsrl:RequestedTerminationTime$>$ $<$/wsrl:SetTerminationTime$>$ |  setTimeout(EPR,timeout)
$<$wsnt:Subscribe$>$ $<$wsnt:ConsumerReference$>$O$<$/wsnt: ConsumerReference$>$ $<$wsnt:ProducerReference$>$EPR$<$/wsnt: ProducerReference$>$ $<$wsnt:Precondition$>$cond’$<$/Precondition$>$ $<$/wsnt:Subscribe$>$ |  subscribe(O,EPR,cond’,A${}_{e{{}_{i}}}$)
$<$wsnt:Notify$>$ $<$wsnt:NotificationMessage$>$ $<$wsnt:SubscriptionReference$>$O$<$/wsnt:SubscriptionReference$>$ $<$wsnt:ProducerReference$>$$EPR$$<$/wsnt:ProducerReference$>$ $<$wsnt:Message$>$ … $<$/wsnt:Message$>$ $<$/wsnt:NotificationMessage$>$ $<$/wsnt:Notify$>$ |  Spawn the associated event handler activity A${}_{e{{}_{i}}}$
Table 2: Conversion table

An orchestration is now defined as a tuple ${\it
O=(PL,Var,A,A_{f},\mathcal{A}_{e})}$, where $A$ and $A_{f}$ are activities
defined by the previous syntax and $\mathcal{A}_{e}$ is a set of activities.
Specifically, $A$ represents the normal workflow, $A_{f}$ is the fault
handling activity and $\mathcal{A}_{e}=\\{A_{e_{i}}\\}_{i=0}^{m}$ are the
event handling activities. The operational semantics is, then, defined at
three levels, the internal one corresponds to the evolution of one activity
without notifications. In the second one, we define the orchestration
semantics with notifications, whereas the third level corresponds to the
composition of different orchestrators and resources to conform the
choreography. We first introduce some definitions that are required in order
to define the operational semantics.

######  Definition 1 (States)

We define a state as a pair s=($\sigma,\rho$), where $\sigma$ represents the
variable values and $\rho$ captures the resource state. Thus,
${\it\sigma:Var\rightarrow\mathbb{Z}}$, and
$\it{\rho=\\{(EPR_{i},v_{i},Subs_{i},t_{i},A_{e{{}_{i}}})\\}_{i=1}^{r}}$,
where $r$ is the number of resources in the system. Each resource has its own
identifier, ${\it EPR_{i}}$, and, at each state, has a particular value,
$v_{i}$, and a lifetime, $t_{i}$, initialized with the createResource
function, which can be changed by using the function setTimeout. Moreover,
$\it{Subs_{i}=\\{(O_{i_{j}},cond^{\prime}_{i_{j}},A_{e{{}_{s}{{}_{{}_{i}{{}_{{}_{j}}}}}}})\\}_{j=1}^{s_{i}}}$
is the set of resource notification subscribers, their associated delivery
conditions and the event handling activity ${\it
A_{e{{}_{s}{{}_{{}_{i}{{}_{{}_{j}}}}}}}}$ that must be thrown in the case that
${\it cond^{\prime}_{i_{j}}}$ holds; $s_{i}$ is the number of orchestrations
currently subscribed to this resource and ${\it O_{i_{j}}\in ORCH}$ are the
subscriber’s identifiers. The operations are defined as follows: ${\it
OPS=\\{op_{i}|\ op_{i}:\mathbb{Z}^{Var}\rightarrow\mathbb{Z}^{Var}\\}}$. Given
a state $s=(\sigma,\rho)$, a variable $v$ and an expression $e$, we denote by
$s^{\prime}=(\sigma[e/v],\rho)$ the state obtained from $s$ by changing the
value of $v$ for the evaluation of $e$ and ${\it
s{{}^{+}}=(\sigma,\rho^{\prime})}$, where
${\it\rho^{\prime}=\\{(EPR_{i},v_{i},Subs_{i},t_{i}-1,A_{e{{}_{i}}})|t_{i}>1\\}_{i=1}^{r}}$.

Next we define some notation that we use in the operational semantics. We
employ the notation $\it{EPR_{i}\in\rho}$ to denote that there is a tuple
$\it{(EPR_{i},v_{i},Subs_{i},t_{i},A_{e{{}_{i}}})}$ ${\it\in\rho}$,
$i\in[1\ldots r]$. Given a predicate $\it{cond}$, we use the function
$\it{cond(s)}$ to mean the resulting value of this predicate at the state
$\it{s}$. Besides, ${\it\rho[w/EPR]_{1}}$ is used to denote that the new value
in $\rho$ of the resource $\it{EPR}$ is $\it{w}$, $\it{\rho[t/EPR]_{2}}$
denotes a change in the $\it{timeout}$ attribute of the resource in $\rho$ and
$\it{Add\\_subs(\rho,EPR_{i},O_{i_{j}},cond^{\prime}_{i_{j}},A_{e{{}_{s}{{}_{{}_{i}{{}_{{}_{j}}}}}}})}$
denotes that
$\it{(O_{i_{j}},cond^{\prime}_{i_{j}},A_{e{{}_{s}{{}_{{}_{i}{{}_{{}_{j}}}}}}})}$
is added to the subscribers of the resource $\it{EPR_{i}\in\rho}$ or ${\it
cond^{\prime}=cond^{\prime}_{i_{j}}}$ in the case that $\it{O_{i_{j}}}$ was
already in ${\it Subs_{i}}$. We need two additional functions. One of them, to
extract the event handling activities that will be launched when the
subscriber condition holds at the current state ${\it s}$: ${\it
N(O,s)=\\{A_{e{{}_{s}{{}_{{}_{i}{{}_{{}_{j}}}}}}}|(O_{i_{j}},cond^{\prime}_{i_{j}},A_{e{{}_{s}{{}_{{}_{i}{{}_{{}_{j}}}}}}})\in
Subs_{i},O_{i{{}_{j}}}=O,}$ ${\it cond^{\prime}_{i_{j}}=true\\}_{i=1}^{r}}$
and the other one is used to launch the activities when the resource lifetime
expires: ${\it
T(O,s)=\\{A_{e{{}_{r}{{}_{{}_{i}}}}}|(EPR_{i},v_{i},Subs_{i},1,A_{e{{}_{r}{{}_{{}_{i}}}}})\in\rho,O=}$
${\it O_{i{{}_{j}}}\in Subs_{i}\\}_{i=1}^{r}}$. Now, a partnerlink is a pair
$(O_{i},O_{j})$ representing the two roles in communication: sender and
receiver.

######  Definition 2 (Activity Operational semantics)

We specify the activity operational semantics by using two types of
transition:

  1. a.

(A,s)$\xrightarrow{a}(A^{\prime},s^{\prime})$, a $\in$ Act (Action
transitions).

  2. b.

(A,s)$\xrightarrow{}_{1}(A^{\prime},s^{+})$ (Delay transitions).

where Act is the set of actions that can be performed, namely: $Act=\\{\tau$,
throw, receive(pl,op,v), reply(pl,v), invoke(pl,op,v1),
$\overline{reply}$(pl,v2), assign(e,v1), empty, wait(timeout), exit,
pick({(pli,opi,vi,Ai)}${}_{i=1}^{n}$,A,timeout), while(cond,A),
createResource(EPR,val,timeout,A${}_{e_{i}}$), setProp(EPR,val),
getProp(EPR,v), setTimeout(EPR,timeout), and
subscribe(O,EPR,cond′,A${}_{e{{}_{i}}})$}. Notice that we have included a
${\it\tau}$-action that represents an empty movement.

_Action transitions_ capture a state change by the execution of an action
$a\in Act$, which can be empty ($\tau$). _Delay transitions_ capture how the
system state changes when one time unit has elapsed. In Tables 4,5, we show
the rules of these transitions.

(Throw) ${(throw,s)\xrightarrow{throw}(empty,s)}$ (Exit)
$(exit,s)\xrightarrow{exit}(empty,s)$ (Receive)
${(receive(pl,op,v),s)\xrightarrow{receive(pl,op,v^{\prime})}(empty,s^{\prime})}$
where ${\it v\in Var,v^{\prime}\in\mathbb{Z},op\in OPS,pl\in PL}$, and ${\it
s^{\prime}=(op(\sigma[v^{\prime}/v]),\rho)}$. (Invoke)
${(invoke(pl,op,v_{1}),s)\xrightarrow{invoke(pl,op,v_{1})}(empty,s)}$
${\bf(\overline{Reply})}$
${(\overline{reply}(pl,v_{2}),s)\xrightarrow{\overline{reply}(pl,v^{\prime}_{2})}(empty,s^{\prime})}$
where ${\it v_{2}\in Var,v^{\prime}_{2}\in\mathbb{Z},pl\in PL}$, and ${\it
s^{\prime}=(\sigma[v^{\prime}_{2}/v_{2}],\rho)}$. (Reply)
${(reply(pl,v),s)\xrightarrow{reply(pl,v)}(empty,s)}$ (Assign)
${(assign(expr,v_{1}),s)\xrightarrow{assign(expr,v_{1})}(empty,s^{\prime})}$
where ${\it v_{1}\in Var,expr}$ is an arithmetic expression, and ${\it
s^{\prime}=(\sigma[expr/v_{1}],\rho)}$. (Seq1)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(A^{\prime}_{1},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{a}(A^{\prime}_{1};A_{2},s^{\prime})\end{array}$
(Seq2)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(empty,s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{a}(A_{2},s^{\prime})\end{array}$
(Seq3)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(empty,s),(a=throw\vee
a=exit)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{a}(empty,s)\end{array}$ (Par1)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(A^{\prime}_{1},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(A^{\prime}_{1}||A_{2},s^{\prime})\end{array}$
(Par2)
$\begin{array}[]{c}\displaystyle(A_{2},s)\xrightarrow{a}(A^{\prime}_{2},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(A_{1}||A^{\prime}_{2},s^{\prime})\end{array}$
(Par3)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(empty,s),(a=throw\vee
a=exit)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(empty,s)\end{array}$ (Par4)
$\begin{array}[]{c}\displaystyle(A_{2},s)\xrightarrow{a}(empty,s),(a=throw\vee
a=exit)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(empty,s)\end{array}$ (Par5)
${(empty||empty,s)\xrightarrow{\tau}(empty,s)}$ (While1)
$\begin{array}[]{c}\displaystyle cond(s)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(while(cond,A),s)\xrightarrow{\tau}(A;(while(cond,A),s))\end{array}$
(While2) $\begin{array}[]{c}\displaystyle\neg cond(s)\\\
\rule{113.81102pt}{0.28453pt}\\\
\displaystyle(while(cond,A),s)\xrightarrow{\tau}(empty,s)\end{array}$ (Pick)
$(pick(\\{(pl_{i},op_{i},v_{i},A_{i})\\}_{i=1}^{n},A,t),s)\xrightarrow{pick(pl_{i},op_{i},v^{\prime}_{i},A_{i})}(A_{i},s^{\prime})$
$\textrm{where}\ {\it t\geq 1,v_{i}\in
Var,v^{\prime}_{i}\in\mathbb{Z},op_{i}\in OPS,pl_{i}\in PL,}\ \textrm{and}\
{\it s^{\prime}=(op_{i}(\sigma[v^{\prime}_{i}/v_{i}]),\rho)}.$ (CR)
$(createResource(EPR,val,t,A_{e{{}_{i}}}),s)\xrightarrow{createResource(EPR,val,t,A_{e{{}_{i}}})}(empty,s^{\prime})$
$\textrm{where}\ {\it t\geq 1,val\in\mathbb{Z}}\ \textrm{and}\
\it{s^{\prime}=(\sigma,\rho\cup\\{EPR,val,\emptyset,t,A_{e{{}_{i}}}\\})},\
\textrm{if}\ {\it EPR\notin\rho}.\ \textrm{Otherwise,
}{\it\rho^{\prime}=\rho}.$ (GetProp) $\begin{array}[]{c}\displaystyle{\it
s=(\sigma,\rho),EPR\in\rho}\\\ \rule{170.71652pt}{0.28453pt}\\\
\displaystyle(getProp(EPR,v),s)\xrightarrow{getProp(EPR,v^{\prime})}(empty,s^{\prime})\end{array}$
where ${\it v\in Var,v^{\prime}\in\mathbb{Z}}$ and ${\it
s^{\prime}=(\sigma[v^{\prime}/v],\rho)}$. (GetProp2)
$\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\notin\rho}\\\
\rule{142.26378pt}{0.28453pt}\\\
\displaystyle(getProp(EPR,v),s)\xrightarrow{throw}(empty,s)\end{array}$
(SetTime) $\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\in\rho}\\\
\rule{184.9429pt}{0.28453pt}\\\
\displaystyle(setTimeout(EPR,t),s)\xrightarrow{setTimeout(EPR,t)}(empty,s^{\prime})\end{array}$
where ${\it t\geq 1}$,$\ {\it s^{\prime}=(\sigma,\rho[t/EPR]_{2})}$.
(SetTime2) $\begin{array}[]{c}\displaystyle{\it
s=(\sigma,\rho),EPR\notin\rho}\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(setTimeout(EPR,t),s)\xrightarrow{throw}(empty,s)\end{array}$
(SetTime3) $\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\in\rho}\\\
\rule{170.71652pt}{0.28453pt}\\\
\displaystyle(setTimeout(EPR,0),s)\xrightarrow{throw}(empty,s)\end{array}$

Table 3: Action and delay transition rules without notifications.

When a resource has used up its lifetime or when a subscription condition
holds, a specific notification is sent to the corresponding resource
subscribers, which is captured by the rules in Table 6. In these rules, the
parallel operator has been extended to spawn some event handling activities,
which must run in parallel with the normal activity of an orchestrator. We
therefore introduce the rules by using the following syntax for the activities
in execution: $\it{(A,\mathcal{A}_{e})}$, where ${\it A}$ represents the
normal system workflow, and ${\it\mathcal{A}_{e}=\\{A_{e_{i}}\\}_{i=0}^{m}}$
are the handling activities in execution. Given any activity ${\it A}$, we
write for short ${\it A||\mathcal{A}_{e}}$ to denote
${\it(A||(A_{e{{}_{1}}}||(\ldots||A_{e{{}_{m}}})))}$. We assume in this
operator that those event handling activities that were already in
$\mathcal{A}_{e}$ will not be spawned twice.

######  Definition 3 (Operational semantics with notifications)

We extend both types of transition to act on pairs ${\it(A,\mathcal{A}_{e})}$.
The transitions have now the following form:

  1. a.

$(O:(A,\mathcal{A}_{e}),s)\xrightarrow{a}(O:(A^{\prime},\mathcal{A}^{\prime}_{e}),s^{\prime})$,
a $\in$ Act

  2. b.

$(O:(A,\mathcal{A}_{e}),s)\xrightarrow{}_{1}(O:(A^{\prime},\mathcal{A}^{\prime}_{e}),s^{+})$

(Throw) ${(throw,s)\xrightarrow{throw}(empty,s)}$ (Exit)
$(exit,s)\xrightarrow{exit}(empty,s)$ (Receive)
${(receive(pl,op,v),s)\xrightarrow{receive(pl,op,v^{\prime})}(empty,s^{\prime})}$
where ${\it v\in Var,v^{\prime}\in\mathbb{Z},op\in OPS,pl\in PL}$, and ${\it
s^{\prime}=(op(\sigma[v^{\prime}/v]),\rho)}$. (Invoke)
${(invoke(pl,op,v_{1}),s)\xrightarrow{invoke(pl,op,v_{1})}(empty,s)}$
${\bf(\overline{Reply})}$
${(\overline{reply}(pl,v_{2}),s)\xrightarrow{\overline{reply}(pl,v^{\prime}_{2})}(empty,s^{\prime})}$
where ${\it v_{2}\in Var,v^{\prime}_{2}\in\mathbb{Z},pl\in PL}$, and ${\it
s^{\prime}=(\sigma[v^{\prime}_{2}/v_{2}],\rho)}$. (Reply)
${(reply(pl,v),s)\xrightarrow{reply(pl,v)}(empty,s)}$ (Assign)
${(assign(expr,v_{1}),s)\xrightarrow{assign(expr,v_{1})}(empty,s^{\prime})}$
where ${\it v_{1}\in Var,expr}$ is an arithmetic expression, and ${\it
s^{\prime}=(\sigma[expr/v_{1}],\rho)}$. (Seq1)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(A^{\prime}_{1},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{a}(A^{\prime}_{1};A_{2},s^{\prime})\end{array}$
(Seq2)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(empty,s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{a}(A_{2},s^{\prime})\end{array}$
(Seq3)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(empty,s),(a=throw\vee
a=exit)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{a}(empty,s)\end{array}$ (Par1)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(A^{\prime}_{1},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(A^{\prime}_{1}||A_{2},s^{\prime})\end{array}$
(Par2)
$\begin{array}[]{c}\displaystyle(A_{2},s)\xrightarrow{a}(A^{\prime}_{2},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(A_{1}||A^{\prime}_{2},s^{\prime})\end{array}$
(Par3)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{a}(empty,s),(a=throw\vee
a=exit)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(empty,s)\end{array}$ (Par4)
$\begin{array}[]{c}\displaystyle(A_{2},s)\xrightarrow{a}(empty,s),(a=throw\vee
a=exit)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{a}(empty,s)\end{array}$ (Par5)
${(empty||empty,s)\xrightarrow{\tau}(empty,s)}$ (While1)
$\begin{array}[]{c}\displaystyle cond(s)\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(while(cond,A),s)\xrightarrow{\tau}(A;(while(cond,A),s))\end{array}$
(While2) $\begin{array}[]{c}\displaystyle\neg cond(s)\\\
\rule{113.81102pt}{0.28453pt}\\\
\displaystyle(while(cond,A),s)\xrightarrow{\tau}(empty,s)\end{array}$ (Pick)
$(pick(\\{(pl_{i},op_{i},v_{i},A_{i})\\}_{i=1}^{n},A,t),s)\xrightarrow{pick(pl_{i},op_{i},v^{\prime}_{i},A_{i})}(A_{i},s^{\prime})$
$\textrm{where}\ {\it t\geq 1,v_{i}\in
Var,v^{\prime}_{i}\in\mathbb{Z},op_{i}\in OPS,pl_{i}\in PL,}\ \textrm{and}\
{\it s^{\prime}=(op_{i}(\sigma[v^{\prime}_{i}/v_{i}]),\rho)}.$ (CR)
$(createResource(EPR,val,t,A_{e{{}_{i}}}),s)\xrightarrow{createResource(EPR,val,t,A_{e{{}_{i}}})}(empty,s^{\prime})$
$\textrm{where}\ {\it t\geq 1,val\in\mathbb{Z}}\ \textrm{and}\
\it{s^{\prime}=(\sigma,\rho\cup\\{EPR,val,\emptyset,t,A_{e{{}_{i}}}\\})},\
\textrm{if}\ {\it EPR\notin\rho}.\ \textrm{Otherwise,
}{\it\rho^{\prime}=\rho}.$ (GetProp) $\begin{array}[]{c}\displaystyle{\it
s=(\sigma,\rho),EPR\in\rho}\\\ \rule{170.71652pt}{0.28453pt}\\\
\displaystyle(getProp(EPR,v),s)\xrightarrow{getProp(EPR,v^{\prime})}(empty,s^{\prime})\end{array}$
where ${\it v\in Var,v^{\prime}\in\mathbb{Z}}$ and ${\it
s^{\prime}=(\sigma[v^{\prime}/v],\rho)}$. (GetProp2)
$\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\notin\rho}\\\
\rule{142.26378pt}{0.28453pt}\\\
\displaystyle(getProp(EPR,v),s)\xrightarrow{throw}(empty,s)\end{array}$
(SetTime) $\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\in\rho}\\\
\rule{184.9429pt}{0.28453pt}\\\
\displaystyle(setTimeout(EPR,t),s)\xrightarrow{setTimeout(EPR,t)}(empty,s^{\prime})\end{array}$
where ${\it t\geq 1}$,$\ {\it s^{\prime}=(\sigma,\rho[t/EPR]_{2})}$.
(SetTime2) $\begin{array}[]{c}\displaystyle{\it
s=(\sigma,\rho),EPR\notin\rho}\\\ \rule{142.26378pt}{0.28453pt}\\\
\displaystyle(setTimeout(EPR,t),s)\xrightarrow{throw}(empty,s)\end{array}$
(SetTime3) $\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\in\rho}\\\
\rule{170.71652pt}{0.28453pt}\\\
\displaystyle(setTimeout(EPR,0),s)\xrightarrow{throw}(empty,s)\end{array}$

Table 4: Action and delay transition rules without notifications.

(Subs) $\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\in\rho}\\\
\rule{227.62204pt}{0.28453pt}\\\
\displaystyle(subscribe(O,EPR,cond^{\prime},A_{e{{}_{i}}}),s)\xrightarrow{subscribe(O,EPR,cond^{\prime},A_{e{{}_{i}}})}(empty,s^{\prime})\end{array}$
where ${\it
s^{\prime}=(\sigma,Add\\_subs(\rho,EPR,O,cond^{\prime},A_{e{{}_{i}}}))}$
(Subs2) $\begin{array}[]{c}\displaystyle{\it s=(\sigma,\rho),EPR\notin\rho}\\\
\rule{227.62204pt}{0.28453pt}\\\
\displaystyle(subscribe(O,EPR,cond^{\prime}),s)\xrightarrow{throw}(empty,s)\end{array}$
(Wait1D) $\begin{array}[]{c}\displaystyle t>1\\\
\rule{113.81102pt}{0.28453pt}\\\
\displaystyle(wait(t),s)\xrightarrow{}_{1}(wait(t-1),s^{+})\end{array}$
(Wait2D) ${(wait(1),s)\xrightarrow{}_{1}(empty,s^{+})}$ (ReceiveD)
${(receive(pl,op,v),s)\xrightarrow{}_{1}(receive(pl,op,v),s^{+})}$ (InvokeD)
${(invoke(pl,op,v_{1},v_{2}),s)\xrightarrow{}_{1}(invoke(pl,op,v_{1},v_{2}),s^{+})}$
(EmptyD) ${(empty,s)\xrightarrow{}_{1}(empty,s^{+})}$ (SequenceD)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{}_{1}(A^{\prime}_{1},s^{+})\\\
\rule{113.81102pt}{0.28453pt}\\\
\displaystyle(A_{1};A_{2},s)\xrightarrow{}_{1}(A_{1}^{\prime};A_{2},s^{+})\end{array}$
(ParallelD)
$\begin{array}[]{c}\displaystyle(A_{1},s)\xrightarrow{}_{1}(A^{\prime}_{1},s^{+})\wedge(A_{2},s)\xrightarrow{}_{1}(A^{\prime}_{2},s^{+})\\\
\rule{142.26378pt}{0.28453pt}\\\
\displaystyle(A_{1}||A_{2},s)\xrightarrow{}_{1}(A^{\prime}_{1}||A^{\prime}_{2},s^{+})\end{array}$
(Pick1D)
${(pick(\\{(pl_{i},op_{i},v_{i},A_{i})\\}_{i=1}^{n},A,1),s)\xrightarrow{}_{1}(A,s^{+})}$
(Pick2D) $\begin{array}[]{c}\displaystyle t>1\\\
\rule{284.52756pt}{0.28453pt}\\\
\displaystyle(pick(\\{(pl_{i},op_{i},v_{i},A_{i})\\}_{i=1}^{n},A,t),s)\xrightarrow{}_{1}(pick(\\{pl_{i},op_{i},v_{i},A_{i}\\}_{i=1}^{n},A,t-1),s^{+})\end{array}$

Table 5: Action and delay transition rules without notifications.

(Notif1)
$\begin{array}[]{c}\displaystyle(A,s)\xrightarrow{a}(A^{\prime},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{170.71652pt}{0.28453pt}\\\
\displaystyle(O:(A,\mathcal{A}_{e}),s)\xrightarrow{a}(O:(A^{\prime},\mathcal{A}_{e}||N(O,s^{\prime})),s^{\prime})\end{array}$
(Notif2)
$\begin{array}[]{c}\displaystyle(A_{e{{}_{i}}},s)\xrightarrow{a}(A^{\prime}_{e{{}_{i}}},s^{\prime}),a\neq
exit,a\neq throw\\\ \rule{170.71652pt}{0.28453pt}\\\
\displaystyle(O:(A,\mathcal{A}_{e}),s)\xrightarrow{a}(O:(A,\mathcal{A}^{\prime}_{e}||N(O,s^{\prime})),s^{\prime})\end{array}$
where $\mathcal{A}^{\prime}_{e}=\\{A^{\prime}_{e{{}_{i}}}\\},\
A^{\prime}_{e{{}_{i}}}=A^{\prime}_{e{{}_{j}}},j\neq i$. (Notif3)
$\begin{array}[]{c}\displaystyle(A,s)\xrightarrow{throw}(empty,s)\\\
\rule{170.71652pt}{0.28453pt}\\\
\displaystyle(O:(A,\mathcal{A}_{e}),s)\xrightarrow{throw}(O:(A_{f},\mathcal{A}_{e})),s)\end{array}$
(Notif4) $\begin{array}[]{c}\displaystyle(A,s)\xrightarrow{exit}(empty,s)\\\
\rule{170.71652pt}{0.28453pt}\\\
\displaystyle(O:(A,\mathcal{A}_{e}),s)\xrightarrow{exit}(O:(empty,empty)),s)\end{array}$
(NotifD)
$\begin{array}[]{c}\displaystyle(A,s)\xrightarrow{}_{1}(A^{\prime},s^{+}),(A_{e{{}_{i}}},s)\xrightarrow{}_{1}(A^{\prime}_{e{{}_{i}}},s^{+}),\forall
i\\\ \rule{170.71652pt}{0.28453pt}\\\
\displaystyle(O:(A,\mathcal{A}_{e}),s)\xrightarrow{}_{1}(O:(A^{\prime},\mathcal{A}^{\prime}_{e}||T(O,s)),s^{+})\end{array}$

Table 6: Action and delay transition rules with notifications.

Finally, the outermost semantic level corresponds to the choreographic level,
which is defined upon the two previously levels. In Table 7, we define the
transition rules related to the evolution of the choreography as a whole.

######  Definition 4 (Choreography operational semantics)

A choreography is defined as a set of orchestrators that run in parallel
exchanging messages: $C=\\{O_{i}\\}_{i=1}^{c}$, where $c$ is the number of
orchestrators presented in the choreography. A choreography state is then
defined as follows:
$S_{c}=\\{(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\\}_{i=1}^{c}$, where
$A_{i}$ is the activity being performed by $O_{i}$ at this state,
${A_{e}}^{i}$ are the event handling activities that are currently being
performed by $O_{i}$, and $s_{i}$ its current state.

(Chor1)
$\begin{array}[]{c}\displaystyle(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\xrightarrow{exit}(O_{i}:(empty,empty),s_{i})\\\
\rule{256.0748pt}{0.28453pt}\\\
\displaystyle\\{(O_{j}:(A_{j},{\mathcal{A}_{e}}^{j}),s_{j})\\}_{j=1}^{c}\xrightarrow{exit}\\{(O_{j}:(empty,empty),s_{j})\\}_{j=1}^{c}\end{array}$
(Chor2)
$\begin{array}[]{c}\displaystyle(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\xrightarrow{a}(O_{i}:(A^{\prime}_{i},{\mathcal{A}^{\prime}_{e}}^{i}),s^{\prime}_{i}),\
a\neq exit,\ a\neq receive,\ a\neq invoke,\\\ \hskip 139.41832pta\neq reply,\
a\neq\overline{reply},\ a\neq pick\\\ \rule{284.52756pt}{0.28453pt}\\\
\displaystyle\\{(O_{j}:(A_{j},{\mathcal{A}_{e}}^{j}),s_{j})\\}_{j=1}^{c}\xrightarrow{a}\\{(O_{j}:(A^{\prime}_{j},{\mathcal{A}^{\prime\prime}_{e}}^{j}),s^{\prime}_{j})\\}_{j=1}^{c}\end{array}$
such that $A^{\prime}_{j}=A_{j},\
{\mathcal{A}^{\prime\prime}_{e}}^{j}={\mathcal{A}_{e}}^{j}||N(O_{j},s^{\prime}_{j}),\forall
j\neq i,j\in\\{1,\ldots,c\\}$. (Chor3)
$\begin{array}[]{c}\displaystyle(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\xrightarrow{}_{1}(O_{i}:(A^{\prime}_{i},{\mathcal{A}^{\prime}_{e}}^{i}),{s_{i}}^{+}),\
\forall i\in\\{1\ldots c\\},\textrm{and rules chor4,\ chor5,}\\\ \hskip
199.16928pt\textrm{chor6 are not applicable}\\\
\rule{284.52756pt}{0.28453pt}\\\
\displaystyle\\{(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\\}_{i=1}^{c}\xrightarrow{}_{1}\\{(O_{i}:(A^{\prime}_{i},{\mathcal{A}^{\prime\prime}_{e}}^{i}),{s_{i}}^{+})\\}_{i=1}^{c}\end{array}$
such that $A^{\prime}_{i}=A_{i},\
{\mathcal{A}^{\prime\prime}_{e}}^{i}={\mathcal{A}_{e}}^{i}||T(O_{i},{s_{i}}^{+})$.
(Chor4)
$\begin{array}[]{c}\displaystyle(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\xrightarrow{invoke(pl,op,v_{1})}(O_{i}:(A^{\prime}_{i},{\mathcal{A}^{\prime}_{e}}^{i}),s_{i}),\
pl=(O_{i},O_{j}),\ s_{i}=(\sigma_{i},\rho_{i}),\\\
(O_{j}:(A_{j},{\mathcal{A}_{e}}^{j}),s_{j})\xrightarrow{receive(pl,op,\sigma_{i}(v_{1}))}(O_{j}:(A^{\prime}_{j},{\mathcal{A}^{\prime}_{e}}^{j}),s^{\prime}_{j})\\\
\rule{284.52756pt}{0.28453pt}\\\
\displaystyle\\{(O_{k}:(A_{k},{\mathcal{A}_{e}}^{k})),s_{k})\\}_{k=1}^{c}\xrightarrow{invoke(pl,op,v_{1})}\\{(O_{k}:(A^{\prime}_{k},{\mathcal{A}^{\prime\prime}_{e}}^{k}),s^{\prime}_{k})\\}_{k=1}^{c}\end{array}$
where $A^{\prime}_{k}=A_{k},\
{\mathcal{A}^{\prime\prime}_{e}}^{k}={\mathcal{A}_{e}}^{k}||N(O_{k},s^{\prime}_{k})$
if $k\neq i,k\neq j$. (Chor5)
$\begin{array}[]{c}\displaystyle(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\xrightarrow{reply(pl,v)}(O_{i}:(A^{\prime}_{i},{\mathcal{A}^{\prime}_{e}}^{i}),s_{i}),\
pl=(O_{i},O_{j}),\ s_{i}=(\sigma_{i},\rho_{i}),\\\
(O_{j}:(A_{j},{\mathcal{A}_{e}}^{j}),s_{j})\xrightarrow{\overline{reply}(pl,\sigma_{i}(v))}(O_{j}:(A^{\prime}_{j},{\mathcal{A}^{\prime}_{e}}^{j}),s^{\prime}_{j})\\\
\rule{284.52756pt}{0.28453pt}\\\
\displaystyle\\{(O_{k}:(A_{k},{\mathcal{A}_{e}}^{k}),s_{k})\\}_{k=1}^{c}\xrightarrow{reply(pl,\sigma_{i}(v))}\\{(O_{k}:(A^{\prime}_{k},{\mathcal{A}^{\prime\prime}_{e}}^{k}),s^{\prime}_{k})\\}_{k=1}^{c}\end{array}$
where $A^{\prime}_{k}=A_{k},\
{\mathcal{A}^{\prime\prime}_{e}}^{k}={\mathcal{A}_{e}}^{k}||N(O_{k},s^{\prime}_{k})$
if $k\neq i,k\neq j$. (Chor6)
$\begin{array}[]{c}\displaystyle(O_{i}:(A_{i},{\mathcal{A}_{e}}^{i}),s_{i})\xrightarrow{invoke(pl,op,v_{1})}(O_{i}:(A^{\prime}_{i},{\mathcal{A}^{\prime}_{e}}^{i}),s_{i}),\
pl=(O_{i},O_{j}),\ s_{i}=(\sigma_{i},\rho_{i}),\\\
(O_{j}:(A_{j},{\mathcal{A}_{e}}^{j}),s_{j})\xrightarrow{pick(pl,op,\sigma_{i}(v_{1}),A)}(O_{j}:(A^{\prime}_{j},{\mathcal{A}^{\prime}_{e}}^{j}),s^{\prime}_{j})\\\
\rule{284.52756pt}{0.28453pt}\\\
\displaystyle\\{(O_{k}:(A_{k},{\mathcal{A}_{e}}^{k}),s_{k})\\}_{k=1}^{c}\xrightarrow{invoke(pl,op,v_{1})}\\{(O_{k}:(A^{\prime}_{k},{\mathcal{A}^{\prime\prime}_{e}}^{k}),s^{\prime}_{k})\\}_{k=1}^{c}\end{array}$
where $A^{\prime}_{k}=A_{k},\
{\mathcal{A}^{\prime\prime}_{e}}^{k}={\mathcal{A}_{e}}^{k}||N(O_{k},s^{\prime}_{k})$
if $k\neq i,k\neq j$.

Table 7: Choreography transition rules.

######  Definition 5 (Labeled transition system)

For a choreography $C$, we define the semantics of $C$ as the labeled
transition system obtained by the application of rules in Table 7, starting at
the state ${s_{0}}_{c}$:

${\it lts}(C)=(\mathcal{Q},{s_{0}}_{c},\rightarrow)$

where $\mathcal{Q}$ is the set of reachable choreography states, and
$\rightarrow\,\,=\,\,\rightarrow_{1}\,\cup\,\\{\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\,|\,$ for all basic activity $a$, or $a=\tau\,\\}$.

###### Example 1

Let us consider the choreography ${\it C=(O_{1},O_{2})}$, where

${\it O_{i}=(PL_{i},Var_{i},A_{i},A_{f{{}_{i}}},\mathcal{A}_{e{{}_{i}}})}$,
i=1, 2,${\it Var_{1}=\\{v_{1},v_{3}\\}}$, ${\it Var_{2}=\\{v_{2},v_{4}\\}}$,
${\it A_{f{{}_{1}}}=exit}$, and ${\it A_{f{{}_{2}}}=exit}$. Suppose that ${\it
s_{0{{}_{1}}}}$ and ${\it s_{0{{}_{2}}}}$ are the initial states of $O_{1}$
and $O_{2}$, respectively, and all the variables are initially $0$. Then,
${\it A_{1}=assign(5,v_{1});}$ ${\it
receive(pl_{1},add,v_{3});reply(pl_{1},v_{3})}$ and ${\it
A_{2}=assign(1,v2);invoke(pl_{1},add,v_{2})}$. In Fig. 1 we show a piece of
the labeled transition system of $C$, where:

$\begin{array}[]{ll}A^{\prime}_{1}=&{\it receive}(pl_{1},add,v_{3});{\it
reply}(pl_{1},v_{3}).\par\\\ A^{\prime}_{2}=&{\it
invoke}(pl_{1},add,v_{2}).\\\
A^{\prime\prime}_{2}=&{\it\overline{reply}}(pl_{1},v_{4}).\par\\\
A^{\prime\prime}_{1}=&{\it reply}(pl_{1},v_{3}).\par\end{array}$
$\\{(O_{1}:(A_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A_{2},\emptyset),s_{0{{}_{2}}})\\}$$\\{(O_{1}:(A^{\prime}_{1},\emptyset),s^{\prime}_{1}),(O_{2}:(A_{2},\emptyset),s_{0{{}_{2}}})\\}$$\\{(O_{1}:(A^{\prime}_{1},\emptyset),s^{\prime}_{1}),(O_{2}:(A^{\prime}_{2},\emptyset),s^{\prime}_{2})\\}$$\\{(O_{1}:(A^{\prime}_{1},\emptyset),{s^{\prime}_{1}}),(O_{2}:(A^{\prime\prime}_{2},\emptyset),{s^{\prime}_{2}})\\}$$\\{(O_{1}:(A^{\prime\prime}_{1},\emptyset),{s^{\prime\prime}_{1}}),(O_{2}:(A^{\prime\prime}_{2},\emptyset),{s^{\prime}_{2}})\\}$$\\{(O_{1}:(empty,\emptyset),s^{\prime\prime}_{1}),(O_{2}:(empty,\emptyset),s^{\prime\prime}_{2})\\}$$\\{(O_{1}:(empty,\emptyset),s^{\prime\prime}_{1}),(O_{2}:(A^{\prime\prime}_{2},\emptyset),s^{\prime}_{2})\\}$assign($5$,$v_{1}$)assign($1$,$v_{2}$)invoke(pl1,add,v2)receive(pl1,add,v3)reply(pl1,v3)$\overline{reply}$(pl1,v4)
Figure 1: A piece of ${\it lts}(C)$ without notifications.

##  5 Case study: Online auction service

The case study concerns a typical online auction process, which consists of
three participants: the online auction system and two buyers, A1 and A2. A
seller owes a good that wants to sell to the highest possible price.
Therefore, he introduces the product in an auction system for a certain time.
Then, buyers (or bidders) may place bids for the product and, when time runs
out, the highest bid wins. In our case, we suppose the resource is the product
for auction, the value of the resource property is the current price (only the
auction system can modify it), the resource subscribers will be the buyers,
their subscription conditions hold when the current product value is higher
than their bid, and the resource lifetime will be the time in which the
auction is active. Finally, when the lifetime has expired, the auction system
sends a notification to the buyers with the result of the process (the
identifier of the winner, $v_{w}$) and, after that, all the processes finish.
Let us consider the choreography ${\it C=(O_{sys},O_{1},O_{2})}$, where ${\it
O_{i}=(PL_{i},Var_{i},A_{i},A_{f{{}_{i}}},\mathcal{A}_{e{{}_{i}}})}$, i=1,2,
${\it Var_{sys}=\\{v_{w},v_{EPR},}$ ${\it end\\_bid\\}}$, ${\it
Var_{1}=\\{v_{1},v_{w{{}_{1}}}\\},\ Var_{2}=\\{v_{2},v_{w_{2}}\\},\
A_{f{{}_{1}}}=exit,}$ and ${\it A_{f{{}_{2}}}=exit}$. Variable $v_{EPR}$
serves to temporarily store the value of the resource property before sending;
$v_{1}$, $v_{2}$, $v_{w}$, $v_{w_{1}}$, $v_{w_{2}}$ are variables used for the
interaction among participants, and, finally, $end\\_bid$ is reset when the
auction lifetime expires. Suppose ${\it s_{0{{}_{sys}}},s_{0{{}_{1}}}}$ and
${\it s_{0{{}_{2}}}}$ are the initial states of $O_{sys}$, $O_{1}$ and
$O_{2}$, respectively, and all the variables are initially $0$:

${\it A_{sys}=assign(1,end\\_bid);createResource(EPR,25,48,A_{not});}$${\it
while(end\\_bid>0,A_{bid})}$. ${\it
A_{1}=subscribe(O_{1},EPR,EPR>=0,A_{cond_{1}});}$ ${\it
while(v_{w{{}_{1}}}==0,A_{pick_{1}})}$ ${\it
A_{2}=subscribe(O_{2},EPR,EPR>=0,A_{cond_{2}});}$${\it
while(v_{w{{}_{2}}}==0,A_{pick_{2}})}$, being: ${\it
A_{not}=assign(0,end\\_bid);(invoke(pl_{3},bid\\_finish_{1},v_{w})||}$${\it
invoke(pl_{4},bid\\_finish_{2},v_{w})})$ ${\it
A_{bid}=pick((pl_{1},cmp,v_{1},setProp(EPR,v_{EPR})),}$${\it(pl_{2},cmp,v_{2},setProp(EPR,v_{EPR})),}$
$\indent\hskip 14.22636pt{\it empty,48)}$ ${\it
A_{cond_{1}}=getProp(EPR,v_{EPR});invoke(pl_{1},{bid\\_up}_{1},v_{EPR})}$
${\it
A_{cond_{2}}=getProp(EPR,v_{EPR});invoke(pl_{2},{bid\\_up}_{2},v_{EPR})}$
${\it A_{pick_{1}}=pick((pl_{1},bid\\_up_{1},v_{1},{\it
invoke}(pl_{1},cmp,v_{1});subscribe(O_{1},EPR,EPR>=}$${\it v_{1},}$
${\it,A_{cond_{1}})),(pl_{3},bid\\_finish_{1},v_{1},empty),empty,48)}$ ${\it
A_{pick_{2}}=pick((pl_{2},bid\\_up_{2},v_{2},{\it
invoke}(pl_{2},cmp,v_{2});subscribe(O_{2},EPR,EPR>=}$${\it v_{2},}$
${\it,A_{cond_{2}})),(pl_{4},bid\\_finish_{2},v_{2},empty),empty,48)}$

In Fig. 2 we show a part of the labeled transition system of $C$, where:

$\begin{array}[]{ll}A^{\prime}_{sys}={\it while}(end\\_bid>0,A_{bid}).\\\
A^{\prime}_{1}={\it while}(v_{w{{}_{1}}}==0,A_{pick_{1}})\\\
A^{\prime}_{2}={\it while}(v_{w{{}_{2}}}==0,A_{pick_{2}})\\\
A^{\prime\prime}_{1}={\it
A_{pick_{1}};while}(v_{w{{}_{1}}}==0,A_{pick_{1}})\\\
A^{\prime\prime}_{2}={\it
A_{pick_{2}};while}(v_{w{{}_{2}}}==0,A_{pick_{2}})\par\\\
A^{\prime\prime}_{sys}={\it A_{bid};while}(end\\_bid>0,A_{bid}).\end{array}$

Let us note that the operations $bid\\_up_{1}$ and $bid\\_up_{2}$ are used to
increase the current bid by adding a random amount to the corresponding
variable $v_{i}$, the operations $bid\\_finish_{1}$, $bid\\_finish_{2}$ reset
the value of $v_{w}$ to finish both buyers. Finally, $cmp$ is an auction
system operation that receives as parameter a variable of the buyers, $v_{i}$,
and if the variable value is greater than the current value of $v_{EPR}$, then
$v_{EPR}$ is modified with this new value. After that, by means of the
activity $setProp(EPR,v_{EPR})$, we can update the value of the resource
property with the new bid.

Chor0Chor1Chor21Chor2Chor3Chor4Chor6Chor5Chor20Chor7Chor8Chor9Chor10Chor11Chor12Chor13Chor14assign(1,end_bid);createResource(EPR,25,48,Anot)subscribe(O1,EPR,EPR$>=$0,A${}_{cond_{1}}$)exitsubscribe(O2,EPR,EPR$>=$0,A${}_{cond_{2}}$)A${}_{cond_{1}};$A${}_{cond_{2}}$A${}_{pick_{1}}||$A${}_{pick_{2}}$Abidsubscribe(O1,EPR,EPR$>=$0,A${}_{cond_{1}}$)A${}_{cond_{1}}$A${}_{pick_{1}}$AbidA${}_{cond_{2}}$A${}_{pick_{2}}$AbidAnotA${}_{pick_{1}}||$A${}_{pick_{2}}$

Figure 2: A piece of ${\it lts}(C)$ for the online auction service.

$\begin{array}[]{ll}Chor_{0}=\\{(O_{sys}:(A_{sys},\emptyset),s_{0{{}_{sys}}}),(O_{1}:(A_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{1}=\\{(O_{sys}:(A^{\prime}_{sys},\emptyset),s^{\prime}_{0{{}_{sys}}}),(O_{1}:(A_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{2}=\\{(O_{sys}:(A^{\prime}_{sys},\emptyset),s^{\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{3}=\\{(O_{sys}:(A^{\prime}_{sys},A_{cond_{1}};A_{cond_{2}}),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{4}=\\{(O_{sys}:(A^{\prime}_{sys},\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{5}=\\{(O_{sys}:(A^{\prime\prime}_{sys},\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{6}=\\{(O_{sys}:(A^{\prime}_{sys},A_{cond_{1}}),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{7}=\\{(O_{sys}:(A^{\prime}_{sys},\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{8}=\\{(O_{sys}:(A^{\prime\prime}_{sys},\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{9}=\\{(O_{sys}:(A^{\prime}_{sys},A_{cond_{2}}),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{10}=\\{(O_{sys}:(A^{\prime}_{sys},\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{11}=\\{(O_{sys}:(A^{\prime\prime}_{sys},\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{12}=\\{(O_{sys}:(A^{\prime}_{sys},A_{not}),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}&Chor_{13}=\\{(O_{sys}:(empty,\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(A^{\prime\prime}_{1},\emptyset),s_{0{{}_{1}}}),(O_{2}:(A^{\prime\prime}_{2},\emptyset),s_{0{{}_{2}}})\\}\\\
Chor_{14}=\\{(O_{sys}:(empty,\emptyset),s^{\prime\prime\prime}_{0{{}_{sys}}}),(O_{1}:(empty,\emptyset),s_{0{{}_{1}}}),(O_{2}:(empty,\emptyset),s_{0{{}_{2}}})\\}&\\\
\end{array}$

##  6 Conclusions and Future Work

We have presented in this paper a formal model for the description of
composite web services with resources associated, and orchestrated by a well-
know business process language (BPEL). The main contribution has therefore
been the integration of WSRF, a resource management language, with BPEL,
taking into account the main structural elements of BPEL, as its basic and
structured activities, notifications, event handling and fault handling.
Furthermore, special attention has been given to timed constraints, as WSRF
consider that resources can only exist for a certain time (lifetime). Thus,
resource leasing is considered in this work, which is a concept that has
become increasingly popular in the field of distributed systems. To deal with
notifications, event handling and fault handling, the operational semantics
has been defined at three levels, the outermost one corresponding to the
choreographic view of the composite web services.

As future work, we plan to extend the language with some additional elements
of BPEL, such as termination and compensation handling. Compensation is an
important topic in web services due to the possibility of faults. We are also
working on a semantics based on timed colored petri nets.

## Acknowledgement

Partially supported by the Spanish Government (co-financed by FEDER funds)
with the project TIN2009-14312-C02-02 and the JCCLM regional project
PEII09-0232-7745.

## References

  * [1] T. Andrews et. al.  BPEL4WS – Business Process Execution Language for Web Services, Version 1.1, 2003. http://www.ibm.com/developerworks/library/specification/ws-bpel/.
  * [2] T. Banks, _Web Services Resource Framework (WSRF) - Primer_ , OASIS, 2006.
  * [3] N. Busi, R. Gorrieri, C. Guidi, R. Lucchi and G. Zavattaro, Choreography and Orchestration: A Synergic Approach for System Design. In International Conference of Service Oriented Computing (ICSOC), Lecture Notes in Computer Science, vol. 3826, pp. 228-240, 2005.
  * [4] K. Czajkowski, D. Ferguson, I. Foster, J. Frey, S. Graham, I. Sedukhin, D. Snelling, S. Tuecke and W. Vambenepe, _The WS-Resource Framework Version 1.0_ , http://www.globus.org/wsrf/specs/ws-wsrf.pdf, 2004.
  * [5] N. Dragoni and M. Mazzara, A formal Semantics for the WS-BPEL Recovery Framework - The $pi$-Calculus Way. In International Workshop on Web Services and Formal Methods (WS-FM). Lecture Notes in Computer Science, vol. 6194, pp. 92-109, 2009.
  * [6] M. Dumas, R. Heckel and N. Lohmann, A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In International Workshop on Web Services and Formal Methods (WS-FM). Lecture Notes in Computer Science, vol. 4937, pp. 77-91, 2008.
  * [7] O. Ezenwoye, S.M. Sadjadi, A. Cary, and M. Robinson, Orchestrating WSRF-based GridServices. Technical Report FIU-SCIS-2007-04-01, 2007.
  * [8] R. Farahbod, U. Glässer and M. Vajihollahi, A Formal Semantics for the Business Process Execution Language for Web Services. In Joint Workshop on Web Services and Model-Driven Enterprise Information Services (WSMDEIS), pp. 122-133, 2005.
  * [9] I. Foster, J. Frey, S. Graham, S. Tuecke, K. Czajkowski, D. Ferguson, F. Leymann, M. Nally, T. Storey and S. Weerawaranna, _Modeling Stateful Resources with Web Services_ , Globus Alliance, 2004.
  * [10] F. Leyman. Choreography for the Grid: towards fitting BPEL to the resource framework. Journal of Concurrency and Computation : Practice & Experience, vol. 18, issue 10, pp. 1201-1217, 2006.
  * [11] N. Lohmann, E. Verbeek, C. Ouyang and C. Stahl. Comparing and Evaluating Petri Net Semantics for BPEL. Journal of Business Process Integration and Management, vol. 4, issue 1, pp. 60-73, 2009.
  * [12] C. Ouyang, E. Verbeek, W.M.P. van der Aalst, S. Breutel, M. Dumas and A.H.M. ter Hofstede. Formal semantics and analysis of control flow in WS-BPEL. Science of Computing Programming, vol. 67, issue 2-3, pp. 162-198, 2007.
  * [13] Z. Qiu, S. Wang, G. Pu and X. Zhao. Semantics of BPEL4WS-Like Fault and Compensation Handling. World Congress on Formal Methods (FM), pp. 350-365, 2005.
  * [14] A. Slomiski. On using BPEL extensibility to implement OGSI and WSRF Grid workflows. Journal of Concurrency and Computation : Practice & Experience, vol. 18, pp. 1229-1241, 2006.
  * [15] Web Services Choreography Description Language Version 1.0 (WS-CDL).  http://www.w3.org/TR/ws-cdl-10/.