A common problem in applying choreographies and orchestrations is ensuring and enforcing the consistency of the models which is often referred to as “conformance checking”. In this position paper, we introduce a concept for checking the conformance of WS-BPEL based orchestrations to ebBP-ST choreographies: First, the ebBP-ST and WS-BPEL models will be transformed into the process algebra CCS. Afterwards, the actual conformance check is performed by checking these CCS models for bisimulation equivalence.
Today, the concepts of choreography and orchestration are well-known and
widely accepted in the services community. While choreographies describe a
scenario from a global point of view, orchestrations concentrate on the local
implementations of each involved party. While the de-facto standard on the
orchestration level is the Web Services Business Process Execution Language
(WS-BPEL; [
Especially in the business-to-business integration (B2Bi) domain, the ebXML
Business Process Specification Schema (BPSS or ebBP; [
At the implementation level, this protocol has to be implemented for the involved partners. Figure 1 shows the basic architecture of these implementations: For each involved partner, the (existing) systems containing application logic are encapsulated as so-called backend systems. The actual orchestrations are realized by so-called control processes (one for each partner) which are realized in WS-BPEL. Within these WS-BPEL processes the automata structure defined in the choreography is reused in order to govern the control flow of the choreography. Nevertheless, the actual decision which activity should be performed next is not initiated by the control process but by the backend systems resp. the interaction partner.
As control processes do not contain application logic, it is clear that a rather
strict notion of conformance has to be used: A control process is not able to
know how the backend systems or the partner control process will continue in
the protocol execution and therefore all foreseen possibilities defined by the
choreography have to be implemented. (Weak) bisimulation ([
To actually check the conformance between ebBP-ST choreographies and
corresponding WS-BPEL orchestrations, the process definitions have to be
transformed into a common formal basis. We propose the process algebra Calculus of
Communicating Systems (CCS; [
After specifying the conformance notion and the process algebra to use, the overall approach to check the conformance is as follows: As ebBP-ST choreographies describe binary collaborations, the ebBP-ST choreography has to be implemented by two WS-BPEL orchestrations - one for each involved partner. Therefore, the ebBP-ST model as well as the two WS-BPEL orchestrations have to be transformed to CCS, resulting in three CCS representations. Afterwards each of the CCS orchestration models has to be checked against the CCS choreography model regarding bisimulation equivalence using a model checking tool like the Edinburgh Concurrency Workbench (CWB).