Verification of communicating data-driven web services

ABSTRACT

We study the verification of compositions of Web Service peers which interact asynchronously by exchanging messages. Each peer has access to a local database and reacts to user input and incoming messages by performing various actions and sending messages. The reaction is described by queries over the database, internal state, user input and received messages. We consider two formalisms for specification of correctness properties of compositions, namely Linear Temporal First-Order Logic and Conversation Protocols. For both formalisms, we map the boundaries of verification decidability, showing that they include expressive classes of compositions and properties. We also address modular verification, in which the correctness of a composition is predicated on the properties of its environment.

REFERENCES

• 1: Wave demo. http://www.db.ucsd.edu/wave.
• 2: Parosh Aziz Abdulla , Bengt Jonsson, Undecidable verification problems for programs with unreliable channels, Information and Computation, v.130 n.1, p.71-90, Oct. 10, 1996 [doi>10.1006/inco.1996.0083]
• 3: P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91--101, 1996.
• 4: Serge Abiteboul , Laurent Herr , Jan Van den Bussche, Temporal versus first-order logic to query temporal databases, Proceedings of the fifteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.49-57, June 04-06, 1996, Montreal, Quebec, Canada [doi>10.1145/237661.237674]
• 5: Daniela Berardi , Diego Calvanese , Giuseppe De Giacomo , Richard Hull , Massimo Mecella, Automatic composition of transition-based semantic web services with messaging, Proceedings of the 31st international conference on Very large data bases, August 30-September 02, 2005, Trondheim, Norway
• 6: 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]
• 7: Stefano Ceri , Piero Fraternali , Aldo Bongio , Marco Brambilla , Sara Comai , Maristella Matera, Designing Data-Intensive Web Applications, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2002
• 8: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 9: F. Curbera, Y. Goland, J. Klein, F. Leymann, D. Roller, S. Thatte, and S. Weerawarana. Business process execution language for Web services. http://dev2dev.bea.com/techtrack/BPEL4WS.jsp.
• 10: Mark H. Burstein , Jerry R. Hobbs , Ora Lassila , David Martin , Drew V. McDermott , Sheila A. McIlraith , Srini Narayanan , Massimo Paolucci , Terry R. Payne , Katia P. Sycara, DAML-S: Web Service Description for the Semantic Web, Proceedings of the First International Semantic Web Conference on The Semantic Web, p.348-363, June 09-12, 2002
• 11: Alin Deutsch , Monica Marcus , Liying Sui , Victor Vianu , Dayou Zhou, A verifier for interactive, data-driven web applications, Proceedings of the 2005 ACM SIGMOD international conference on Management of data, June 14-16, 2005, Baltimore, Maryland [doi>10.1145/1066157.1066219]
• 12: Alin Deutsch , Liying Sui , Victor Vianu, Specification and verification of data-driven web services, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 14-16, 2004, Paris, France [doi>10.1145/1055558.1055571]
• 13: A. Deutsch, L. Sui, V. Vianu, and D. Zhou. Verification of communicating data-driven web services. Technical Report CS2006-0853, University of California, San Diego, March 2006. Available from http://www.db.ucsd.edu.
• 14: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 15: H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of web service compositions. In International Conference on Automated Software Engineering (ASE), 2003.
• 16: 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]
• 17: Xiang Fu , Tevfik Bultan , Jianwen Su, Conversation protocols: a formalism for specification and verification of reactive electronic services, Theoretical Computer Science, v.328 n.1-2, p.19-37, 29 November 2004 [doi>10.1016/j.tcs.2004.07.004]
• 18: Xiang Fu , Tevfik Bultan , Jianwen Su, Realizability of Conversation Protocols With Message Contents, Proceedings of the IEEE International Conference on Web Services (ICWS'04), p.96, June 06-09, 2004 [doi>10.1109/ICWS.2004.92]
• 19: James E. Hanson , Prabir Nandi , Santhosh Kumaran, Conversation Support for Business Process Integration, Proceedings of the 6th International Enterprise Distributed Object Computing Conference, p.65-74, September 17-20, 2002
• 20: G. Holzmann. The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, 2003.
• 21: Richard Hull, Web Services Composition: A Story of Models, Automata, and Logics, Proceedings of the 2005 IEEE International Conference on Services Computing, p..18-xix, July 11-15, 2005 [doi>10.1109/SCC.2005.108]
• 22: Richard Hull , Michael Benedikt , Vassilis Christophides , Jianwen Su, E-services: a look behind the curtain, Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, p.1-14, June 09-11, 2003, San Diego, California [doi>10.1145/773153.773154]
• 23: Richard Hull , Jianwen Su, Tools for design of composite Web services, Proceedings of the 2004 ACM SIGMOD international conference on Management of data, June 13-18, 2004, Paris, France [doi>10.1145/1007568.1007722]
• 24: Richard Hull , Jianwen Su, Tools for composite web services: a short overview, ACM SIGMOD Record, v.34 n.2, June 2005 [doi>10.1145/1083784.1083807]
• 25: S. Nakajima, Verification of Web Service Flows with Model-Checking Techniques, Proceedings of the First International Symposium on Cyber Worlds (CW'02), p.0378, November 06-08, 2002
• 26: 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]
• 27: Marc Spielmann, Verification of relational transducers for electronic commerce, Journal of Computer and System Sciences, v.66 n.1, p.40-65, 01 February 2003 [doi>10.1016/S0022-0000(02)00029-6]
• 28: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symp. on Logic in Computer Science, 1986.
• 29: Web Services Flow Language(WSFL 1.0), 2001. http://www-3.ibm.com/ software/ solutions/webservices/pdf/WSFL.pdf.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.0 General

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Design, Management, Verification