Modeling of BPEL Composite Services Using Clustered Coloured Petri-Nets

Client requests often span over several web services and these services have to be invoked in some sequence based on business logic of a composite service. BPEL language is used for specification of web service composition and has become the industry standard. Unfortunately BPEL lacks sound formal semantics which leads to errors in service composition. It is therefore necessary to model and verify BPEL specification before execution. In this paper, we model certain BPEL activities using Coloured Petri-Nets(CPN). CPN is similar to Petri-Nets(PN) with an extra advantage that it has programmable elements. Our models are compact, yet feature-complete as compared to other models. Moreover, we propose an algorithm to identify structurally similar sub-parts of CPN model and replace them with a transition. The sub-part replaced forms a separate CPN. This not only reduces the size of model but allows the sub-parts moved out to be verified independently. Further, we get a model of constant size when each subtask of an activity is same.