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: Parosh Aziz Abdulla , Bengt Jonsson, Channel Representations in Protocol Verification, Proceedings of the 12th International Conference on Concurrency Theory, p.1-15, August 20-25, 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: Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
• 4: Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.359-364, July 27-31, 2002
• 5: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 6: H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of Web Service Compositions. In Proc. ASE'03, 2003.
• 7: Xiang Fu , Tevfik Bultan , Jianwen Su, Analysis of interacting BPEL web services, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988756]
• 8: Steve Graham , Doug Davis , Simeon Simeonov , Toufic Boubez , Ryo Neyama , Yuichi Nakamura, Building Web Services with Java: Making Sense of Xml, Soap, Wsdl, and Uddi, Sams, Indianapolis, IN, 2001
• 9: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521 ]
• 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: Srini Narayanan , Sheila A. McIlraith, Simulation, verification and automated composition of web services, Proceedings of the 11th international conference on World Wide Web, May 07-11, 2002, Honolulu, Hawaii, USA [doi>10.1145/511446.511457]
• 16: James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 17: M. Pistore, M. Roveri, and P. Busetta. Requirements-Driven Verification of Web Services. In Proc. WS-FM'04, 2004.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.1 MODELS AND PRINCIPLES
      H.1.1 Systems and Information Theory

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
      D.2.4 Software/Program Verification
          Subjects: Model checking; Formal methods

  E. Data
  E.4 CODING AND INFORMATION THEORY
      Subjects: Formal models of communication

General Terms:
Design, Verification

Keywords:
BPEL, asynchronous communications, formal verification, web service composition