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

                         Rawand Guerfel and Zohra Sbaï

       Université de Tunis El Manar, Ecole Nationale d’Ingénieurs de Tunis,
                     BP. 37 Le Belvédère, 1002 Tunis, Tunisia
             guerfel.rawand@gmail.com, zohra.sbai@enit.rnu.tn



      Abstract. The Web services composition (WSC) has an enormous po-
      tential 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 compos-
      ite 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 compati-
      bility 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 gen-
eral, 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 tran-
sitions 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.
338    PNSE’14 – Petri Nets and Software Engineering




                           Fig. 1. The proposed approach



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 suf-
fers 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)