ABSTRACT
This paper presents a set of tools and techniques for analyzing interactions of composite web services which are specified in BPEL and communicate through asynchronous XML messages. We model the interactions of composite web services as conversations, the global sequence of messages exchanged by the web services. As opposed to earlier work, our tool-set handles rich data manipulation via XPath expressions. This allows us to verify designs at a more detailed level and check properties about message content. We present a framework where BPEL specifications of web services are translated to an intermediate representation, followed by the translation of the intermediate representation to a verification language. As an intermediate representation we use guarded automata augmented with unbounded queues for incoming messages, where the guards are expressed as XPath expressions. As the target verification language we use Promela, input language of the model checker SPIN. Since SPIN model checker is a finite-state verification tool we can only achieve partial verification by fixing the sizes of the input queues in the translation. We propose the concept of synchronizability to address this problem. We show that if a composite web service is synchronizable, then its conversation set remains same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite web services with unbounded input queues can be completely verified using a finite state model checker such as SPIN.
- R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification of MSC graphs. In Proceedings of 28th International Colloquium on Automata, Languages, and Programming, volume 2076 of LNCS, pages 797 -- 808. Springer, 2001.]] Google ScholarDigital Library
- Business Process Execution Language for Web Services (BPEL), Version 1.1. http://www.ibm.com/developerworks/library/ws-bpel, May 2003.]]Google Scholar
- Business Process Modeling Language (BPML). http://www.bpmi.org.]]Google Scholar
- A. Brown, M. Fuchs, J. Robie, and P. Wadler. MSL a model for W3C XML Schema. In Proceedings of 10th World Wide Web Conference (WWW), pages 191--200, 2001.]] Google ScholarDigital Library
- T. Bultan, X. Fu, R. Hull, and J. Su. Conversation specification: A new approach to design and analysis of e-service composition. In Proceedings of 12th World Wide Web Conference (WWW), pages 403 -- 410, May 2003.]] Google ScholarDigital Library
- T. Bultan and T. Yavuz-Kahveci. Action language verifier. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE), pages 382--386, 2001.]] Google ScholarDigital Library
- J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In IEEE Symposium on Logic in Computer Science, pages 428--439, 1990.]]Google Scholar
- DAML-S (and OWL-S) 0.9 Draft Release. http://www.daml.org/services/daml-s/0.9/, May 2003.]]Google Scholar
- H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of web service compositions. In Proceedings of the 18th IEEE International Conference on Automated Software Engineering Conference (ASE 2003), 2003.]]Google ScholarDigital Library
- X. Fu, T. Bultan, and J. Su. Model checking interactions of composite web services. UCSB Computer Science Department Technical Report (2004-05). (Available at http://www.cs.ucsb.edu/~su/tmp/Map2SPIN.pdf).]]Google Scholar
- X. Fu, T. Bultan, and J. Su. Conversation protocols: A formalism for specification and verification of reactive electronic services. In Proceedings of 8th International Conference on Implementation and Application of Automata (CIAA), volume 2759 of LNCS, pages 188--200, 2003. Full version to appear in a special issue of Theoretical Computer Science.]] Google ScholarDigital Library
- G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston, Massachusetts, 2003.]]Google ScholarDigital Library
- R. Hull, M. Benedikt, V. Christophides, and J. Su. E-services: A look behind the curtain. In Proceedings of 22nd ACM Symposium on Principles of Database Systems (PODS), pages 1 -- 14, 2003.]] Google ScholarDigital Library
- IBM. IBM Business Process Execution Language for Web Service Java Run Time (BPWS4J). http://www.alphaworks.ibm.com/tech/bpws4j.]]Google Scholar
- Gerry Miller. .Net vs. J2EE. Communications of the ACM, 46(6):64--67, June 2003.]] Google ScholarDigital Library
- Message Sequence Chart (MSC). ITU-T, Geneva Recommendation Z.120, 1994.]]Google Scholar
- S. Narayanan and S. A. Mcllraith. Simulation, verification and automated composition of web services. In Proceedings of the 11th International World Wide Web Conference, 2002.]] Google ScholarDigital Library
- A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13(1):45--60, 1981.]]Google ScholarCross Ref
- Simple Object Access Protocol (SOAP) 1.1. W3C Note 08, May 2000. http://www.w3.org/TR/SOAP/.]]Google Scholar
- W. M. P. van der Aalst et al. Verification of workflow task structures: A petri-net-based approach. Information Systems, 25(1):43--69, 2000.]] Google ScholarDigital Library
- Joseph Williams. The web services debate J2EE vs. .Net. Communications of the ACM, 46(6):59--63, June 2003.]] Google ScholarDigital Library
- Web Service Analysis Tool (WSAT). http://www.cs.ucsb.edu/~su/WSAT.]]Google Scholar
- Web Service Choreography Interface (WSCI) 1.0. http://www.w3.org/TR/2002/NOTE-wsci-20020808/, August 2002.]]Google Scholar
- Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/wsdl, March 2001.]]Google Scholar
- Extensible Markup Language (XML). http://www.w3c.org/XML.]]Google Scholar
- XML Path Language (XPath) Version 1.0. http://www.w3.org/TR/xpath, 1999.]]Google Scholar
- XML Schema. http://www.w3c.org/XML/Schema.]]Google Scholar
Index Terms
- Analysis of interacting BPEL web services
Recommendations
Synchronizability of Conversations among Web Services
We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages ...
Model checking XML manipulating software
ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysisThe use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, ...
Model checking XML manipulating software
The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, ...
Comments