Web services are exposed to consumers through standard interfaces. In general, because of the complexity of the demand of the consumer, a single service cannot reach this request and it therefore needs to contact one or more other services. This corresponds to Web services composition which allows multiple services to communicate and collaborate by exchanging messages and thus to implement a composite service that can perform complex tasks for consumers.

Several languages have been proposed to ensure this composition namely BPEL which is based on XML. Indeed, BPEL is used to define the abstract and executable business processes as a set of Web services coordinated recursively. Yet, it is necessary to make sure that these services can interact properly.

In this context, we propose D&A4WSC as a framework allowing the user to model the composition of Web services by the composition of open workflow nets (oWF-nets) [2]. It allows in special, the compatibility checking [3] and the generation of a BPEL process for the composite service. D&A4WSC is composed of four modules (as drawn in figure 1): a module for WSC modelling, an SMV translator, an analysis module and a BPEL generator of WSC. WSC modelling: Web services modelling is performed using oWF-nets as a subclass of Petri nets [4]. Each service is modeled by an oWF-net in which transitions represent the different tasks performed by the service, places define the conditions and output (resp. input) interface places send (resp. receive) messages to (resp. from) partners. SMV generation of WSC: In order to be checked by NuSMV, the composition of oWF-nets is converted to SMV code. In this code, we mapped the net evolution and the firing history in integer arrays in which this evolution will be saved. Analysis of WSC: D&A4WSC checks first for a syntactical compatibility, which consists of a test of conformance in the number and types of interfaces. Then, a semantic compatibility is enhanced, testing thus if the composition suffers from any problem like deadlocks. We characterized 3 classes of compatibility and showed how to model check them using NuSMV model checker [1]. Generation of BPEL process: BPEL allows the integration and orchestration of a large number of applications published in the form of services. Thus, we integrated in our framework a generator of a compatible composition into a BPEL process. This generator consists on translating oWF-nets to owfn files and then invoking the oWFN2BPEL to convert these files to BPEL.