Analysis of communication models in web service compositions

ABSTRACT

In this paper we describe an approach for the verification of Web service compositions defined by sets of BPEL processes. The key aspect of such a verification is the model adopted for representing the communications among the services participating in the composition. Indeed, these communications are asynchronous and buffered in the existing execution frameworks, while most verification approaches assume a synchronous communication model for efficiency reasons. In our approach, we develop a parametric model for describing Web service compositions, which allows us to capture a hierarchy of communication models, ranging from synchronous communications to asynchronous communications with complex buffer structures. Moreover, we develop a technique to associate with a Web service composition the most adequate communication model, i.e., the simplest model that is sufficient to capture all the behaviors of the composition. This way, we can provide an accurate model of a wider class of service composition scenarios, while preserving as much as possible an efficient performance in verification.

References

1. P. A. Abdulla and B. Jonsson. Channel representations in protocol verification. In CONCUR, pages 1--15, 2001.]]
2. T. Andrews, F. Curbera, H. Dolakia, J. Goland, J. Klein, F. Leymann, K. Liu, D. Roller, D. Smith, S. Thatte, I. Trickovic, and S. Weeravarana. Business Process Execution Language for Web Services (version 1.1), 2003.]]
3. D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323--342, 1983.]]
4. A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella. NuSMV 2: An OpenSource tool for symbolic model checking. In Proc. CAV'02, 2002.]]
5. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. Elsevier, 1990.]]
6. H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of Web Service Compositions. In Proc. ASE'03, 2003.]]
7. X. Fu, T. Bultan, and J. Su. Analysis of Interacting BPEL Web Services. In Proc. WWW'04, 2004.]]
8. S. Graham, S. Simenov, T. Boubez, G. Daniels, D. Davis, Y. Nakamura, and R. Neyama. Building Web Services with Java: Making Sense of XML, SOAP, WSDL and UDDI. Sams, 2001.]]
9. G. J. Holzmann. The model checker SPIN. Software Engineering, 23(5):279--295, 1997.]]
10. R. M. Karp and R. E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147--195, 1969.]]
11. R. Kazhamiakin and M. Pistore. A Parametric Communication Model for the Verification of BPEL4WS Compositions. In Proc. WS-FM'05, 2005.]]
12. R. Khalaf, N. Mukhi, and S. Weeravarana. Service Oriented Composition in BPEL4WS. In Proc. WWW2004, 2004.]]
13. J. Koehler and B. Srivastava. Web service composition: Current solutions and open problems. In Proc. of ICAPS'03 Workshop on Planning for Web Services, 2002.]]
14. S. Nakajima. Model-checking verification for reliable web service. In Proc. OOPSLA'02 Workshop on OOWS, 2002.]]
15. S. Narayanan and S. McIlraith. Simulation, Verification and Automated Composition of Web Services. In Proc. WWW2002, 2002.]]
16. J. L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1981.]]
17. M. Pistore, M. Roveri, and P. Busetta. Requirements-Driven Verification of Web Services. In Proc. WS-FM'04, 2004.]]

Index Terms

• Computing methodologies

  • Modeling and simulation

    • Simulation theory

      • Systems theory

• Mathematics of computing

  • Information theory

• Security and privacy

  • Cryptography

    • Mathematical foundations of cryptography

• Software and its engineering

  • Software creation and management

    • Designing software

      • Software implementation planning

        • Software design techniques

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Model checking

• Theory of computation

  • Computational complexity and cryptography

    • Communication complexity

  • Logic

    • Verification by model checking