Real-Time issues are not usually considered when describing and composing web services. However, modern web services are usually involved in the software implementation of time-constrained business processes [1]. The satisfaction of time constraints is crucial in order to ensure the validity of systems where the response to a certain stimulation has to take place in a shortened period of time. Thus, the service composition problem becomes more complex, since time restrictions should be taken into account both in the choreography and orchestration processes in order to establish the temporal consistency of the web services. In this paper, we present a formal approach for real-time service orchestration and choreography. In this regard, we use UML-RT as a visual and user-friendly notation in order to model services and their interactions, Timed CSP as an underlying formal grounding to enable services verification and WS-BPEL as an execution language.
Web services are loosely-coupled modular software applications that interact with each other through web technologies. In order to enable inter and intra organizational integration, these web services should be composed to work together to carry out the integrated business process goals.
The choreography and orchestration are important emerging mechanism that deal with the problem of web services composition. Choreography is concerned with the web services interaction coordination, and orchestration is concerned with the creation of high level web services (called orchestrators) from existing ones.
Whenever web services are involved in the implementation of time-constrained
business processes [
Capturing time restrictions in orchestration and choreography requires the
usage of languages with enough expressive power to represent complex relations
about timely interaction between services. Moreover, it is very important to use
formal methods with a well defined syntax and semantics in order to ensure
the compositionally of timed web services and in order to verify the temporal
properties that they should fulfill. Several authors (e.g., [
Timed CSP and formal methods have the disadvantage of being tedious to
use. In order to overcome this problem we combine this language with UML
notations, specifically with timed sequence diagrams [
In the field of web services, the Web Service-Business Process Execution Language (WS-BPEL) is a commonly adopted standard with a rich set of constructs to compose services. In this paper, we establish a set of mapping rules to systematically derive code from Timed CSP processes to WS-BPEL.
Several works in the literature have addressed the composition of web services
[
This paper is organized as follows: Section 2 gives an overview of Timed CSP language. In Section 3, the timed web services and its constituents are defined. Both Section 4 and Section 5 describe proposed web services composition techniques. In Section 6, a mapping from Timed CSP to WS-BPEL is defined. Finally, brief conclusions drawn from this paper and some ongoing work is described in Section 7.
Timed CSP has been proposed as a specification language in order to model
and to reason on concurrent, parallel systems that must fulfill explicit time
constraints. Timed CSP in an extension over CSP [
t
P Q | P ⊲ Q | P k Q These terms has the following intuitive interpretations: – P is a process. – Stop is a deadlocked, stable process which will never engage in any external communication. It is the “broken program”. – Skip does nothing except to end successfully √. This process is equivalent to √ → ST OP . – W ait t does nothing, but it is ready to end after a delay t. – a → P is a process that is initially prepared to engage in an event a, and then it behaves as P . – P ; Q corresponds to the sequential composition of P and Q. It represents a process that behaves like P until P chooses to terminates and becomes to behave like Q. The process Q is turned on at the exact moment that P terminates. – P Q corresponds to a process that is willing to behave like either P or Q. The choice is made by the environment. The decision is taken on the first visible event (The process is non deterministic only if the first visible event of P and Q are equal).
t – P ⊲ Q, is the process that initially gives P the priority of turning on. If no visible event from P has occurred in t units of time, the process behaves as Q, and P never turns on. – P k Q represents a parallel composition of processes P and Q. A variety of semantic models were defined for the Timed CSP language.
The Timed CSP operational semantic model is given in terms of two relations: an evolution relation, which describes the situation in which a process becomes another one by simply allowing time to pass, and a timed transition relation, which describes when a process becomes another one by performing an action at a particular time.
The denotational model is used in order to provide formal semantics to Timed CSP terms. It also allows to specify the required behavior of a process, that is, its desired properties.
The properties to be satisfied by a system or a process are defined in terms of timed failures (or timed traces). This definition characterizes some timed failures (timed traces) as acceptable and some others as non-acceptable. A process complies with its specification only if all its executions are acceptable, that is, none of its executions violates its specification.
Likewise, if we denote (tr, ℵ) as a timed failure and S(tr, ℵ) as a predicate in the timed failure, then it is said that P satisf ies or complies with S(tr, ℵ) if S(tr, ℵ) holds for any timed failure (trace) of P .
P sat S(tr, ℵ) ⇔ ∀(s, ℵ) ∈ tf ailure(P ) : S(tr, ℵ)
The specification of a process in terms of timed traces allows the description
of both safety and liveness properties [
Services are self-contained active entities. Real-time services are services that must behave under certain time restrictions. Thus, the operation of a real-time service can only be considered correct if it delivers a valid result in a predefined time range.
A real-time service is conceptually equal to a capsule in UML-RT. Thus, in this paper it is used the same visual representation of an UML-RT capsule to represent real-time services. Figure 1 shows the elements involved in a communication with services.
S1
P: In-Out provides <<Interfaces>>
In inbound request <<Interfaces>>
Out outbound requests <<Protocol Role>>
In-out inbound request outbound requests
A real-time service Si communicates with other services through a set of interaction ports Pk and according to a pre-established communication protocol. It is important to mention that ports in our approach are active and therefore they have an associated behavior.
Each port can be associated to one or two interfaces. This interfaces represents access points that control the behavior of the whole service. We can distinguish between two types of interfaces: – Provided interfaces that describe the set of input requests and represent the set of public operations provided by the service. – Required interfaces that describe the set of output requests and represent the set of public operations required by the service.
The set of input and output requests are encapsulated in protocols and protocol roles.
Definition 1: Real-time services Real-time services are modular software applications that interact with each other through interfaces. This definition coincide of the definition of a process in Timed CSP conceptual framework. Thus, a real-time service can be represented by a process P in Timed CSP.
A real-time service has an internal and an external timed behavior: – Internal timed behavior. It describes the behavior of the service that is associated with the accomplishment of its internal tasks. This behavior can be represented as a set of timed events that may be observed during the service execution. These are the timed traces σ = h(σ1, t1), (σ2, t2) . . . (σn, tn)i with ∀i ∈ 1..n, σi ∈ α(P ), α(P ) the set of all action of P and ti the time occurrence of the event σi. – External timed behavior. It describes the set of interactions between a service and its environment (i.e., a system composed by other services). Moreover, it provides a black box that only shows an abstraction over the functionality that is provided by a service, which will also hide its internal actions. Formally, the internal behavior σint of a timed-service can be deduced from its internal one by hiding all its internal actions: σint = σ \ IN T , with IN T a set of internal action of a service.
It is possible to distinguish two types of real-time services: – Primitive services are services that are not able to be divided. – Composite services or orchestrators are a set of services that are composed of existing services.
The choreography is concerned with the interaction between services. This
interaction is carried out through a set of messages exchanged between the interfaces
or the ports of the services. Due to this message passing nature, undesirable
situations such as deadlocking can be reached if the behavior of the services is
inconsistent. In order to ensure behavior consistency between communicating
services, the communications between their interfaces or ports must be
coordinated.
Definition 2: Business Protocol The business protocol represents a valid
communication sequence (conversation) and can be specified by a timed sequence
diagram (as it is shown in figure 2) or its corresponding timed traces (by applying
the rules described in [
S1 Port
S1 t1 ex1 ey1 ex2 ey2 Port S2 t2>t1+5 S2
Protocol Behaviour
Definition 3: Deadlock free A communication between two services σ1 and σ2 is deadlock free if the parallel composition of the two services preserves the execution order of the messages and the temporal constraints specified in a conversation SD. Formally,
σ1||σ2 |=T SD
As an application example, let us consider a wire transfer order in an online banking system. Once the client has confirmed all data and has ordered to proceed through his/her web client, the transfer validation web service at the bank server generates a random key and sends it out to the client’s mobile phone by invoking another web service of the client’s mobile network operator. It also randomly selects one position in the matrix of secret codes that every client has and that each branch office provides to its clients. We call that value the code card matrix position (CCMP). Then, the transfer validation service requests the web client for the two codes: the one randomly generated and sent to the client’s cell phone and the one from the client’s code card. This process has to be completed in 15 seconds, from the time the proceed order is received until the time an SMS is delivered to the client’s cell phone. Afterwards, the client has 150 seconds to provide the requested codes. Otherwise the transfer would be canceled. The interaction between the transfer validation and the web client services is described in figure 3.
Alt
Web Client
Transfer Validation 0<t<150 timeout t>150
In our approach, the internal behavior of primitive services is modeled by
transforming its timed sequence diagram into a corresponding timed state diagram,
following a set of rules established in [
Proceed_Transfer \ Code_generation;
Code; Ask_CCMP timeout\ Cancellation I[0, 150]. Security_Codes \ Order_Transfer
Transfer Validation
Transfer_Receipt
The specification of composite services or orchestrators is deduced from the formal specification of its components (i.e, existing services) following a bottomup process, as it is shown in figure 5. These new services can be considered as black-boxes that interact with the environment through their ports. Definition 4: Orchestrators The behavior of an orchestrator Σ is defined by the parallel composition of its lower level timed web services σi, ..., σn, by hiding all their internal actions. Formally,
Σ =ki=1..n σi \ IN T
For example, the specification of the orchestrator that results from the composition of both services TV and WC services is like follows:
Orchestrator = (T V k W C) \ {Code Generation, Code} 1 In Timed CSP, the ? symbol represents “a waiting for requests” operation and the ! symbol represents a “send request” operation.
P
Pj Composition
Orchestration P1 … …
Pn Composition Orchestration
CCoommppoossiittiioonn Orchestration
Composition Orchestration P10 … P1k …
Pj0 … Pjl …
Pn0 …Pnm In this section we establish the transformation rules between Timed CSP and WS-BPEL XML format. Table 1 summarizes these rules.
Events to basic activities The main elements of Timed CSP framework are events. Events represent atomic indivisible actions in the behavior of a process and, thus, correspond to messages in WS-BPEL. These events may be either reception or sending actions. – The reception actions correspond to the basic activity < receive > .. < /receive >. – The sending actions may correspond to < reply > .. < /reply > or to < invoke > .. < /invoke > basic activities, depending on whether the sending action is an output-response to a previous request or a call to another service with input parameters, respectively.
Processes to structured activities – SKIP is a process that indicates a successful termination and can be mapped to the terminate activity. – ST OP is a deadlock stable process that does not engage in any external communication. This process models abnormal activity termination and, thus, it corresponds to terminate activity.
SKIP STOP P1; P2; …; Pn P1 || P2 || …|| Pn P
Q Wait t; a ? P Timed CSP
WS-BPEL empty terminate <sequence>
Activity P1 ….
Activity Pn <\sequence> <flow>
Activity P1 ….
Activity Pn <\flow> <pick> <\pick> <Onmessage…..\> <OnAlarm…\>
Wait for= “0 ” until=“t” < sequence > < invoke, receive or reply.../ > activityP < /sequence > – a → P is the process that is initially prepared to engage in an event a and, then, it behaves like P. This process corresponds to:
< sequence > < /sequence > < invoke, receive or reply.../ > activityP – P 1||P 2 corresponds to a parallel execution of the structured activities P1, P2.., Pn, expressed as < f low > P1, P2, Pn < /f low >. – Delay wait t corresponds to:
< wait > < /wait >
< f or > t < /f or > t – A time-sensitive choice (a → P ⊲ Q is a process that initially gives the turning on priority to the process (a → P ). If the event a does not occur in t units of time, a timeout occurs and the process behaves as Q and P never turns itself on. This choice corresponds to a “pick” activity with an < onM essage > activity and an < onAlarm > one.
< pick > < pick > < onM essage > .. < /onM essage >
ActivityP < onAlarm >< f or > n < /f or >< /onAlarm >
activityQ
Despite the fact that time in which processes and services have to take place is capital in system design, there exists few proposals that address the capture of time constraints when composing services. In this paper we have presented a set of techniques for the orchestration and choreography of timed web services that combines UML-RT, Timed CSP and WS-BPEL. This approach enables the verification of some of the properties of real-time services while using a user friendly notation.
The techniques presented above will set the grounding for a model based approach intended to develop time-constrained business processes based on web services. This approach will be defined as a set of transformations between different models, as in a Model-Driven Engineering (MDE) methodology.
The intended development process can be summarized as follows:
1. CIM level. The business processes are designed using timed activity
diagrams as presented in previous work [
UML diagrams and its corresponding Timed CSP and WS-BPEL processes. 3. PSM level. An implementation of the models is specified in programming languages like RT-CORBA, Java-RT, etc..