D&A4WSC as a Design and Analysis Framework of Web Services Composition

Abstract

The Web services composition (WSC) has an enormous potential for the organizations in the B2B area. In fact, different services collaborate through the exchange of messages to implement complex business processes. BPEL is one of the most used languages to develop such cooperation. However, a composition is not with added value if it is not compatible. This property garantees a placement of a correct composite web service. In this context, we develop a verification approach of the WSC compatibility. We propose, hence, a framework named D&A4WSC which allows to model the WSC by oWF-nets, to check their compatibility with the model checker NuSMV and to translate them if they are compatible in BPEL processes using the oWFN2BPEL compiler.

Keywords

• Open workflow nets
• Model checking
• Compatibility
• BPEL

-

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.

PNSE’14 – Petri Nets and Software Engineering 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.

References

1. Cimatti , A. , Clarke , E.M. , Giunchiglia , F. , Roveri , M. : Nusmv: A new symbolic model verifier . In: Proceedings of the 11th International Conference on Computer Aided Verification . pp. 495 - 499 . Springer-Verlag ( 1999 )

2. Lohmann , N. , Kleine , J.: Fully-automatic translation of open workflow net models into simple abstract bpel processes . In: Modellierung 2008 . Volume 127 of LNI ., GI . pp. 57 - 72 ( 2008 )

3. Martens , A. : On compatibility of web services . In: Petri Net Newsletter . pp. 12 - 20 ( 2003 )

4. Sbaï , Z. , Barkaoui , K. : Vérification formelle des processus workflow - extension aux workflows inter-organisationnels. Revue Ingénierie des Systèmes d'Information: Ingénierie des systèmes collaboratifs . 18 ( 5 ), 33 - 57 ( 2013 )