7
978-1-4673-4766-2/12/$31.00 ©2012 IEEE Towards Change and Verification Support in Collaborative Business Processes * Ismaïl Khriss Département de mathématiques, informatique et génie Université du Québec à Rimouski Rimouski, Canada [email protected] Mohammed El Koutbi , Youssef Dkiouak ENSIAS, Mohamed V – Souissi University SIME laboratory, MIS research team Rabat, Morocco [email protected], [email protected] Abstract—The automation of business processes raises several challenges for enterprises. One of those challenges relates to the maintenance and verification of business processes, more precisely how to facilitate changes within existing business processes even at the run-time. Furthermore, changing a collaborative business process can have an impact on the contract specified between the involved parties. Thus, a business process may need to adapt and meet reliably the new contract. In this paper, we discuss an approach to support change and verification for such collaborative processes. This approach consists of (1) a protocol, called Change Protocol for Collaboration (CPC), for managing the changes that can have an incidence on the contract; (2) an algorithm for supporting migration of running business process instances to their new schemas; and (3) a verification framework for supporting of the accuracy of changes before their adoption. Keywords—Collaborative business process; change support; verification; correctness, soundness. I. INTRODUCTION The automation of business processes raises several challenges for enterprises. The various parts played by the business departments and/or partners make the processes more complex. Complexity comes from the number of actions necessary to carry out a business process, the number of implied roles, the inter-dependencies between those roles, and their continual evolution. One of those challenges relates to the maintenance of business processes within multi-partners collaborations, more precisely how to facilitate changes within existing multi-partner processes, possibly even at the run-time. Complex multi-partner collaborations require defining some appropriate collaboration contract or agreement between the partners involved. These collaboration agreements may also be changed, changes possibly initiated by one of the partners. In [12], we presented an approach to support adaptability in collaborative business processes. This approach consisted on a protocol, called Change Protocol for Collaboration (CPC), for managing the changes that can have an incidence on the contract; and an algorithm for supporting migration of running business process instances to their new schemas. In this work, we also stressed the importance of ensuring the accuracy of changes before their implementation. In fact, errors in business processes can cause big financial losses; therefore, the need for identifying and correcting these possible errors has become critical. The rest of the paper is organized as follows. First, we give an overview of the CPC protocol and present the algorithm of process instances migration. Then, we discuss the change verification life cycle focusing on a set of rules that must be checked before and during a change in a business process. Finally, we conclude and discuss possible future work. II. DESCRIPTION OF THE CPC PROTOCOL AND THE MIGRATION ALGORITHM To illustrate process changes, we introduce a simple choreography (see Fig. 1) between four partners. A Buyer wants to perform a purchase order. After receiving the PORequest, the Seller asks for a credit authorization from the FinancialInst. If the credit is not accepted, the order is canceled. Otherwise, processing proceeds by making a shipping order to the Shipper. Then, the Buyer is informed of the order status. Fig. 2 presents the collaborative process that it is conformed to the choreography. Note that the process is completed by flows between data objects and internal activities such as Process Order and Invoicing. Each pool separately represents, in fact, the private process of the corresponding partner. The private processes are the ones that are deployed in each partner’s server. The two figures follow the BPMN language (version 2.0). Changes to a collaborative business process can have an impact on the contract specified between the involved parties. For instance, the changes in the choreography may affect the buyer-seller contract in a B2B (Business to Business) system.

[IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

  • Upload
    youssef

  • View
    212

  • Download
    0

Embed Size (px)

Citation preview

Page 1: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

978-1-4673-4766-2/12/$31.00 ©2012 IEEE

Towards Change and Verification Support in Collaborative Business Processes

* Ismaïl KhrissDépartement de mathématiques, informatique et génie

Université du Québec à RimouskiRimouski, Canada

[email protected]

Mohammed El Koutbi , Youssef DkiouakENSIAS, Mohamed V – Souissi University

SIME laboratory, MIS research teamRabat, Morocco

[email protected], [email protected]

Abstract—The automation of business processes raises several challenges for enterprises. One of those challenges relates to the maintenance and verification of business processes, more precisely how to facilitate changes within existing business processes even at the run-time. Furthermore, changing a collaborative business process can have an impact on the contract specified between the involved parties. Thus, a business process may need to adapt and meet reliably the new contract.In this paper, we discuss an approach to support change and verification for such collaborative processes. This approach consists of (1) a protocol, called Change Protocol for Collaboration (CPC), for managing the changes that can have anincidence on the contract; (2) an algorithm for supporting migration of running business process instances to their new schemas; and (3) a verification framework for supporting of the accuracy of changes before their adoption.

Keywords—Collaborative business process; change support; verification; correctness, soundness.

I. INTRODUCTION

The automation of business processes raises several challenges for enterprises. The various parts played by the business departments and/or partners make the processes more complex. Complexity comes from the number of actions necessary to carry out a business process, the number of implied roles, the inter-dependencies between those roles, and their continual evolution. One of those challenges relates to the maintenance of business processes within multi-partners collaborations, more precisely how to facilitate changes within existing multi-partner processes, possibly even at the run-time.

Complex multi-partner collaborations require defining some appropriate collaboration contract or agreement between the partners involved. These collaboration agreements may also be changed, changes possibly initiated by one of the partners. In [12], we presented an approach to support adaptability in collaborative business processes. This approach consisted on a protocol, called Change Protocol for Collaboration (CPC), for

managing the changes that can have an incidence on the contract; and an algorithm for supporting migration of running business process instances to their new schemas. In this work, we also stressed the importance of ensuring the accuracy of changes before their implementation. In fact, errors in business processes can cause big financial losses; therefore, the need for identifying and correcting these possible errors has become critical.

The rest of the paper is organized as follows. First, we give an overview of the CPC protocol and present the algorithm of process instances migration. Then, we discuss the change verification life cycle focusing on a set of rules that must be checked before and during a change in a business process. Finally, we conclude and discuss possible future work.

II. DESCRIPTION OF THE CPC PROTOCOL AND THE MIGRATION ALGORITHM

To illustrate process changes, we introduce a simple choreography (see Fig. 1) between four partners. A Buyerwants to perform a purchase order. After receiving the PORequest, the Seller asks for a credit authorization from the FinancialInst. If the credit is not accepted, the order is canceled. Otherwise, processing proceeds by making a shipping order to the Shipper. Then, the Buyer is informed of the order status. Fig. 2 presents the collaborative process that it is conformed to the choreography. Note that the process is completed by flows between data objects and internal activities such as Process Order and Invoicing. Each pool separately represents, in fact, the private process of the corresponding partner. The private processes are the ones that are deployed in each partner’s server. The two figures follow the BPMN language (version 2.0).

Changes to a collaborative business process can have an impact on the contract specified between the involved parties. For instance, the changes in the choreography may affect the buyer-seller contract in a B2B (Business to Business) system.

Page 2: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

Fig.1 An example of a choreography.

Fig. 2 A collaborative process conformed to the choreography of Fig. 1.

Fig.3 An example of a change in the choreography of Fig1.

Page 3: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

Fig. 4: The impact of the change on the collaborative process.

Fig. 3 shows an example of a change in the choreography. Its impact on the collaborative process is described in Fig. 4. Fig. 4 shows also how each business process executed at each end-point may need to be adapted to meet the new contract. For this reason, we proposed an approach to support adaptability for collaborative business processes, what we called Change Protocol for Collaboration (CPC). In this section, we first present the protocol's key features. Then, we describealgorithms of master and slave sides.

The CPC protocol is a two-phase commit-like protocol and consists of five messages: Notify, Accept, Deny, Proceed and Cancel (see Fig. 5 and Fig. 6). When a trading partner (playing the Master role) wants to change its business process, and this change can affect its partners (playing the Slave role), it sends a message notifying its partners of this change (1). Upon receiving this message, the slaves enter the Notified state (a slave is initially in state Idle). The slaves can then accept (2) or deny (2') adapting their business processes. When a slave agrees to the change, it enters the Accepted state; otherwise, it enters the Denied state. For the master process, two cases are then to be considered. If it receives an Accept message from all its slaves, it sends a Proceed message to inform its partners that they should adapt their business processes (3). Upon receiving this message, a slave enters the Proceed state. The second case is when the master receives a Deny message from a slave: in this case, it sends a Cancel message to all its slaves informing them that the change is canceled (3'). All slaves then enter the Canceled state. Note that canceling a change does not mean that a slave has a power to veto; it only means that this slave

cannot adapt its business process in order to meet the new requirement. The master will then simply react by resubmitting the change after replacing the partners (slaves) that denied.

Fig. 5: Successful termination of a change.

Fig. 6: Cancellation of a change.

Page 4: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

In the following, we present the pseudo code of master and slaves processes:

Master Process Receive ChangeRequestDenied = FalseFor each address in ChangeRequest.slaves do

Slave = address Slave.Notify WaitforSlaveAnswer If Receive AcceptMessage then

Do nothing Else if Receive DenyMessage then

Denied = trueExit WaitForSlaveAnswer

End ifEnd forIf not Denied then

For each address in ChangeRequest.slaves do Slave = address Slave.Proceed

End forelse

For each address in ChangeRequest.slaves do Slave = address Slave.Cancel

End forEnd if

End process

Slave ProcessReceive NotifyMessageGetAuthorizationMaster = NotifyMessage.masterAddressIf authorized then

Master.acceptElse

Master.denyDatabase.RecordChangeDenied

End ifWait masterResponseIf Receive ProceedMessage then

Database.ProgramMigrationElse if Receive CancelMessage then

Database.RecordChangeCancelledEnd if

End process

The GetAuthorization activity in the slave process has two aspects. The first is purely business related, while the second is technical. First of all, the change should be authorized according to the organization's policies. Then, a technical authorization should be obtained. The latter is obtained after verifying that the changed business process is correct. If so, the authorization activity should propose a set of modifications to be made to the local business process so that it satisfies the new contract. This local business process should be then validated and completed (manually) by the business analysts as well as the technical team. If a problem occurs at any stage, a Denymessage is generated. Note that the verification process can have a positive impact to verify the correctness of the change before its deployment.

The Program Migration activity consists in effectively migrating the running business process instances to the new schema, but only when the scope of changes is Instance or the Running_Instances field of the Notify message is True. When the scope of changes is Schema, the new schema is scheduled to become effective for all new business process instances based on the Notify message’s Effective_Date and Expiration_Date fields. The Record activities (Record Change Denied and Record Change Canceled) consist only in recording those events for administration purposes. A detailed description of the CPC protocol can be found in [12].

III. VERIFICATION ISSUES

We aim to propose a complete framework for verifying the accuracy of changes before their adoption. This framework will cover all steps of a change in a collaborative business process. When a change is specified, the new schema can be verified syntactically and semantically using the adopted modeling and specification languages. During the change deployment, some choreographic rules can be checked to trust the coherence of the change. This is done at the level of schema and instance migrations. After the change is successfully deployed, some existing techniques of process mining can be used to check the conformance of the change after deployment. This framework will thus put the verification as a central task in all steps of the life cycle of a process change (at the design and run time levels).

In the following, we will present different facets of the verification framework beginning from formal notations, formal properties, tool support, etc. This synthesis will guide us to select the appropriate techniques and tools for this important framework.

A. Formal notationsDifferent verification techniques and tools have been used

for business processes. In this section, we will present an overview of these prominent techniques and tools such as: Petri Nets, EPC, State Machines, Process Algebras, etc.

Petri netsPetri nets (PN) is a language for modeling and validating

systems in which concurrency, communication, and synchronization play a major role. The classical PN is a directed bipartite graph with two node types called places and transitions. The nodes are connected via directed arcs. Places are represented by circles and transitions by rectangles.

In [1], Aalst et al. discuss a mapping from BPEL to Petri nets by giving several examples. Each BPEL construct is mapped into a Petri net pattern. Schmidt and Stahl [19]describe the tool BPEL2PN that implements the transformation when abstracting from data. The authors provide a formal semantics of BPEL and a tool BPEL2PNML [4] used to perform a translation. Yang et al. [24] consider coloured Petri nets (CPN) as a more compact way to model business processes than ordinary Petri nets. They show how to map most of the basic and structured activities of BPEL and the Web Service Choreography Interface to coloured Petri nets.

Page 5: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

EPCsThe concept of Event-driven Process Chains (EPCs)

provides an intuitive modeling language to model business processes. An EPC consists of three main elements: Functions, Events and Connectors. EPCs are used in a large variety of other systems, and many verification approaches exist. To illustrate the maturity of process verification, we point out to the analysis of the entire SAP reference model described in [16]. The SAP reference model contains more than 600 non-trivial process models expressed in terms of Event-driven Process Chains (EPCs). These EPCs have been automatically translated into YAWL models and analyzed these models using WofYAWL.

State machines It is well known that using state machines in programming

reactive (event-driven) systems to have a lot of benefits. However, while the traditional Finite State Machines (FSMs) are an excellent tool for tackling smaller problems, it's also generally known that they tend to become unmanageable even for moderately involved systems. Due to the phenomenon known as "state explosion," the complexity of a traditional FSM tends to grow much faster than the complexity of the reactive system it describes.

Fu et al. [8] present a framework to verify properties of a web service composition consisting of multiple BPEL processes that communicate asynchronously. Each BPEL process is translated to a guarded automaton. Subsequently, these guarded automata are mapped to Promela. The combination of these translations provides a map from (a part of) BPEL to Promela. Nakajima et al. [17] consider the translation of BPEL activities into Promela is split into two parts. First, a BPEL activity is mapped to an extended finite automaton. This provides a formal model for BPEL activities. Second, the automaton is represented in Promela. In [11],Kazhamiakin et al. focus on three communication models of business processes: synchronous, ordered asynchronous, and unordered asynchronous. They give a number of communicating BPEL processes. Each process is transformed into a state transition system, and subsequently; these systems are composed in parallel, resulting in yet another state transition system.

Process AlgebrasProcess algebras are a model of computation for concurrent

systems. Their syntax represents processes, parallel composition of processes, synchronous communication between processes through channels, creation of fresh channels, replication of processes, and non-determinism.

In [14], Magee et al. present a process algebra named FSP (Finite State Process). Each FSP represents a finite labeled transition system. They also present a tool for FSP named Labeled Transition System Analyzer. This tool takes as input an FSP and translates it into a labeled transition system. Subsequently, this labeled transition is analyzed. In [7], Foster et al. show how the Labeled Transition System Analyzer tool can be exploited to check if a web service composition implemented in BPEL satisfies a web service composition specification captured by Message Sequence Charts (MSCs). Both the BPEL process and the MSC are translated into FSPs.

The authors of [13] introduce a process algebra named the BPE-calculus to model most activities of BPEL. The focus is on links and dead-path-elimination. Given the syntax of the BPE-calculus, in terms of a grammar, and the semantics of the BPE-calculus, in terms of a collection of axioms and rules, the Process Algebra Compiler generates a module. In [6], Ferraraet al. present a two-way mapping between the process algebra LOTOS and BPEL. Most BPEL activities, including fault handlers, compensation handlers and event handlers are considered. By going from BPEL to LOTOS, the toolbox for Construction and Analysis of Distributed Processes, can be exploited for the verification of BPEL processes. In [21],Tremblay et al. suggest to translate a BPEL activity to a LOTOS process and to map its specification, expressed as a path expression, to a mu-calculus expression. Mazzara et al. [15] extend the Pi-calculus with event notification, by adding two new constructs: one to notify an event and another to associate a scope with an event.

B. Formal propertiesIn this section, we summarize important properties to verify

in a collaborative business process when a change occurs. Basically, changes can take place at the schema and instance levels. Instance changes are often applied in an ad-hoc manner and become necessary in conjunction with real-world exceptions. In the following, we summarize the most important features to verify based on [2, 3, 20 and 22]:

� Correctness: or sometimes called soundness, is the most important aspect of workflow and business process management systems. In general, workflowsand business processes model reactive systems, and the usual verifications address the problem of determining if the system reacts to an extern event and if so, if the system reacts in a proper way (issues concerning liveness, fairness, deadlock-avoidance, termination, etc.).

� Conformance: is an important issue in collaborative processes. In fact, private processes of all partners in the collaboration should behave in conformance with the choreography.

� Change realization: is an important issue in dynamic change where it should be possible to migrate automatically all running instances to the new schema. The challenge here is to correctly and efficiently adapt instance states and face the problem of determining what happens with the elements that are being processed in a distributed way.

C. Supported toolsThere are a wide variety of commercial and open source

workflow and business process management (BPM) offerings available [23]. More than forty Java workflow engines are published as open source projects. Based on a comprehensive literature survey, Intalio/Apache ODE [9], jBPM [10], OpenWFE [18] and Enhydra Shark [5] were selected to study the support of verification and change. Intalio/Apache ODE is built around the standards-based Eclipse STP BPMN modeler and Apache ODE BPEL engine. jBPM is part of JBOSS (a

Page 6: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

commercial company), Enhydra Shark supports XPDL v1.0 and OpenWFE is an active project on SourceForge.

Intalio/Apache ODE (Orchestration Director Engine) executes business processes following the BPEL standard. It supports both long and short living process executions to orchestrate all the services that are part of the application. It relies on WSDL to express web service interfaces. The main features of this workflow engine are: the high level API to the engine that allows you to integrate the core with virtually any communication layer and the Hot-deployment of business processes with change support.

JBoss jBPM is an extensible and flexible process engine that can run as a standalone server or embedded in any Java application. It comprises a process definition tool called JBoss jBPM Graphical Process Designer. It acts as an Eclipse plugin, to provide support for defining processes in jPDL both in a graphical format and in XML format. jPDL (jBPM Process Definition Language) is the process language utilized by the system.

Enhydra Shark is a Java workflow engine offering from Together Teaml¨osungen and ObjectWeb. The system contains a Process Definition Tool called Together Workflow Editor (TWE) or JaWE.

OpenWFE is an extensible and scalable workflow engine. Access libraries for Java, Ruby, Python, Perl, and .NET make it easy to write custom interfaces or agents for a workflowenabled system. This workflow engine comprises a web-based workflow design environment called Droflo, which can be used to graphically define process models, which are then translated to OpenWFE’s process definition language in XML format. OpenWFE uses its own process definition language.

Table I summarizes the features of these products relating to the previous discussed verification aspects. A ‘+’ in the tableindicates that direct support for a criterion is present, and a ‘–’indicates that there is no support for the criterion.

TABLE I. TOOLS AND PROPERTIES IN BUSINESS COLLABORATIVE PROCESSES

Criterion Apache ODE

Enhydra Shark

OpenWFE

JBoss jBPM

Formal notations

Pi-calculs

- (XPDL) -(XPDL,POOL)

-

Correctness + + + +Conformance - - - -Change realization

+ - - -

Based on the Table I, one can conclude that Intalio/Apache ODE seems to be a good candidate for our verification framework. It will be enriched by several verification tools and techniques for the design and run time phases. The CPCprototype has been implemented in Java based on this platform.

The formalisms more likely to be used are pi-calculus and Petri nets. Because of the selection of Intalio/Apache ODE

which based on pi-calculus, we plan to combine it with the use of CPN that supports well: abstraction, time, non-determinism and concurrency in a natural way. In addition, colored tokens in CPN can favorably be used to model data and resource patterns in the system. We can thus use all techniques and tools described in the Petri nets sub-section.

Pi-calulus and Petri nets will be used in conjunction with the BPMN 2.0 notation where three basic models of processes have been proposed: private processes, public processes and choreography. Several types of diagrams can be used to support these three models. For our work, we focus on threetypes of diagrams: choreography diagram (as in figures 1 and 3), collaboration diagrams (as in figures 2 and 4) and business process diagrams (showing only the local view of a partner).Note that figures 2 and 4 show a collaboration between four partners. The same diagram can be used to model collaborations between public processes. Recall that a public process includes only activities that are used to communicate between partners hiding any internal details. Hence, we model a collaborative business process using three views: Choreography Diagram (ChD), Collaboration Diagram (CoD)and Business process Diagram (BpD).

Assume that we have a collaborative business process modeled by a ChD1, CoD1 and a set of BpD1i. When a master decides to implement a change, it proposes a new contract in form of ChD2 and CoD2. Before proposing this change to partners, the master should verify the following set of rules:

R1: Check the correctness of ChD2.R2: Check consistency between ChD2 and CoD2.

During the change initiation by the master, all the partners (master and slaves) should check the rules R3, R4 and R5. When accepting the change, each partner proposes its new BpD2i and verifies its correctness.R3: Check the correctness of each BpD2i.R4: Check the conformance between BpD2i and ChD2. R5: Check the conformance between BpD1i and BpD2i to find equivalent states. The absence of equivalent states means that no running instance can be migrating to the new ChD2.

The following rules are performed during the execution of an instance migration to conform to the new ChD2.

R6: The service invocation activity is skipped if the service type, its provider and the value of its input parameters did not change (i.e., already executed by I1 and, therefore, belongs to T). However, a synchronization message is sent to the provider. Thismessage will inform the provider (i.e., the partner) about the progress of the migrated instance on the requester’s side and, thus, will synchronize the different partners involved in the process. In fact, the synchronization message will simply contain the message to be sent to the partner.R7: Receiving a synchronization message has the same effect as receiving the message it contains. This means that a process can continue its execution if it is waiting for this message (for instance, the process is executing a receive activity).R8: The waiting activity of a period of time P1 is executed only for a period of time P1-P2. P2 is equal to the time when the next

Page 7: [IEEE 2012 International Conference on Complex Systems (ICCS) - Agadir, Morocco (2012.11.5-2012.11.6)] 2012 IEEE International Conference on Complex Systems (ICCS) - Towards change

activity B scheduled to be executed minus the time when the last activity A has been executed. The wait activity should beexecuted before activity B. The idea here is to ensure the business process will not wait unnecessarily.R9: All invoke activities (not already compensated) that are executed by I1 and cannot be reached by I2 should be compensated in reverse order of their execution.

CONCLUSION

In this paper, we proposed a set of verification rules and tools to support the migration in a collaborative business process. The main interesting features of this verification life cycle are that it distinguishes three levels: choreography,collaboration, and private (local) business process, acting in a smooth manner: before, during and after a process change. We plan in a near future to propose and adapt formal techniques of bi-simulation and graph similarity in the context of collaborative business processes in order to identify the suitable equivalent state between two schemas. We also plan to support modeling and checking some important non-functional requirements like privacy and security.

REFERENCES

[1] W. M. P. van der Aalst and Christian Stahl. “ Modeling Business Processes A Petri Net-Oriented Approach”, The MIT Press, May 2011.

[2] W. M. P. van der Alast. “Structural Characterization of Sound Workflow nets”, Computing Science Report 96/23, Eindhoven University of Technology, Eindhoven, 1996.

[3] W.M.P. van der Aalst. Discovery, “ Verification and Conformance of Workflows with Cancellation”. In H. Ehrig, R. Heckel, G. Rozenberg, and G. Taentzer, editors, Proceedings of the 4th International Conference on Graph Transformation (ICGT 2008), volume 5214 of Lecture Notes in Computer Science, pages 18-37. Springer-Verlag, Berlin, 2008.

[4] BPEL2PNML are available under an open-source license at http://www.bpm.fit.qut.edu.au/projects/babel/tools.

[5] Enhydra Shark are available at www.enhydra.org/.[6] A. Ferrara. “Web services: a process algebra approach”. In M. Aiello,

M. Aoyama, F. Curbera, and M.P. Papazoglou, editors, Proceedings of 2nd ACM International Conference on Service Oriented Computing, pages 242-251, New York, NY, USA, November 2004.

[7] H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of web service compositions. In Proceedings of 18th IEEE International Conference on Automated Software Engineering, pages 152-163, Montreal, Canada, October 2003.

[8] X. Fu, T. Bultan, and J. Su, “ Synchronizability of conversations among web services”. IEEE Transactions on Software Engineering, 31(12):1042{1055, December 2005.

[9] Intalio/Apache ODE ode.apache.org are available at www.ode.apache.org/.

[10] JBPM are available at www.jboss.org/jbpm.[11] R. Kazhamiakin and M. Pistore.” Parametric communication model for

the verification of BPEL4WS compositions”. In M. Bravetti, L. Kloul, and G. Zavattaro, editors, Proceedings of the 2nd International Workshop on Web Services and Formal Methods, volume 3670 of Lecture Notes in Computer Science, pages 318-332, Versailles, France, September 2005. Springer-Verlag.

[12] I. Khriss, E. Lévesque, G. Tremblay and A. Jacques,” Towards Adaptability Support in Collaborative Business Processes”. International MCETECH Conference on e-Technologies, pages 34-45, IEEE Computer Society, Montréal, Canada, Jan. 2008.

[13] M. Koshkina and F. van Breugel. “Modelling and verifying web service orchestration by means of the concurrency workbench”. ACM SIGSOFT Software Engineering Notes, 29(5), September 2004.

[14] J.Magee and J. Kramer.” Concurrency: State Models and Java Programs”. Wiley, New York, NY, USA, second edition, 2006.

[15] M. Mazarra and R. Lucchi.” A framework for generic error handling in business processes”. In Proceedings of the 1st International Workshop on Web Services and Formal Method, volume 105 of Electronic Notes J.

[16] J. Mendling, W.M.P. van der Aalst, B. van Dongen, and E. Verbeek. Errors in the SAP Reference Model. BPTrends, 4(6):1–5, June 2006.

[17] S. Nakajima. “Model-checking behavioral specication of BPEL applications”. In Proceedings of the International Workshop on Web Languages and Formal Methods, volume 151(2) of Electronic Notes in Theoretical Computer Science, pages 89-105, New Castle, UK, July 2005. Elsevier.

[18] Openwfe are available at www.openwfe.org.[19] K. Schmidt and C. Stahl. “A Petri net semantic for BPEL4WS,

validation and application”. In E. Kindler, editor, Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets, pages 1-6, Paderborn, Germany, 2004.

[20] S. Rinderle , M. Reichert, P. Dadam, “Correctness criteria for dynamic changes in workflow systems”, Data & Knowledge Engineering 50 (2004) 9–34.

[21] G. Tremblay and J. Chae. “Towards specifying contracts and protocols for web services”. In H. Mili and F. Khendek, editors, Proceedings of the MCeTech Montreal Conference on eTechnologies, pages 73{85, Montreal, Canada, January 2005.

[22] M.Weske.“Business Process Management Concepts, Languages, Architectures ”, pages 267-301, Springer-Verlag Berlin Heidelberg 2007.

[23] P. Wohed, B. Andersson, A.H.M. ter Hofstede, N.C. Russell, and W.M.P. van der Aalst. Patterns-based Evaluation of Open Source BPM Systems: The Cases of jBPM, OpenWFE, and Enhydra Shark. BPM Center Report BPM-07-12, BPMcenter.org, 2007.

[24] Y. Yang, Q. Tan, Y. Xiao, J. Yu, and F. Liu. “Exploiting hierarchical CP-nets to increase reliability of web services workflow”. In Proceedingof the International Symposium on Applications and the Internet, pages 116-122, Phoeniz, AZ, USA,January 2006. IEEE.