Specification and verification of data-driven web services

ABSTRACT

We study data-driven Web services provided by Web sites interacting with users or applications. The Web site can access an underlying database, as well as state information updated as the interaction progresses, and receives user input. The structure and contents of Web pages, as well as the actions to be taken, are determined dynamically by querying the underlying database as well as the state and inputs. The properties to be verified concern the sequences of events (inputs, states, and actions) resulting from the interaction, and are expressed in linear or branching-time temporal logics. The results establish under what conditions automatic verification of such properties is possible and provide the complexity of verification. This brings into play a mix of techniques from logic and automatic verification.

REFERENCES

• 1: 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]
• 2: Serge Abiteboul , Richard Hull , Victor Vianu, Foundations of Databases: The Logical Level, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 3: Serge Abiteboul , Victor Vianu , Brad Fordham , Yelena Yesha, Relational transducers for electronic commerce, Journal of Computer and System Sciences, v.61 n.2, p.236-269, Oct. 2000 [doi>10.1006/jcss.2000.1708]
• 4: Anthony J. Bonner , Michael Kifer, An overview of transaction logic, Theoretical Computer Science, v.133 n.2, p.205-265, Oct. 24, 1994 [doi>10.1016/0304-3975(94)90190-2]
• 5: E. Borger, E. Gradel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997.
• 6: BPML. org. Business process modeling language. http://www.bpmi.org.
• 7: M. Brambilla, S. Ceri, S. Comai, P. Fraternali, and I. Manolescu. Specification and design of workflow-driven hypertexts. Journal of Web Engineering, 1(1), 2002.
• 8: 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
• 9: A. K. Chandra and M. Vardi. The implication problem for functional and inclusion dependencies is undecidable. SIAM J. Comp., 14(3):671--677, 1985.
• 10: 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.
• 11: 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
• 12: Hasan Davulcu , Michael Kifer , C. R. Ramakrishnan , I. V. Ramakrishnan, Logic based modeling and analysis of workflows, Proceedings of the seventeenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.25-33, June 01-04, 1998, Seattle, Washington, United States [doi>10.1145/275487.275491]
• 13: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 14: Mary Fernández , Daniela Florescu , Alon Levy , Dan Suciu, Declarative specification of Web sites with S, The VLDB Journal — The International Journal on Very Large Data Bases, v.9 n.1, p.38-55, March 2000 [doi>10.1007/s007780050082]
• 15: D. Florescu, K. Yagoub, P. Valduriez, and V. Issarny. WEAVE: A data-intensive web site management system (software demonstration). In Proc. of the Conf. on Extending Database Technology (EDBT), 2000.
• 16: M. R. Garey and D. S. Johnson. Computers and Intractability. Freeman, 1979.
• 17: Dimitrios Georgakopoulos , Mark Hornick , Amit Sheth, An overview of workflow management: from process modeling to workflow automation infrastructure, Distributed and Parallel Databases, v.3 n.2, p.119-153, April 1995 [doi>10.1007/BF01277643]
• 18: D. Harel. On the formal semantics of statecharts. In Proc. LICS, pages 54--64, 1987.
• 19: 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]
• 20: Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000 [doi>10.1145/333979.333987]
• 21: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 22: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 23: G. Mecca, P. Merialdo, and P. Atzeni. Araneus in the era of XML. IEEE Data Engineering Bulletin, 22(3):19--26, 1999.
• 24: 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]
• 25: Knowlege in action: logical foundations for specifying and implementing dynamical systems, MIT Press, Cambridge, MA, 2001
• 26: M. Spielmann. Abstract State Machines: Verification problems and complexity. Ph.D. thesis, RWTH Aachen, 2000.
• 27: Marc Spielmann, Automatic Verification of Abstract State Machines, Proceedings of the 11th International Conference on Computer Aided Verification, p.431-442, July 06-10, 1999
• 28: 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]
• 29: Dirk Wodtke , Gerhard Weikum, A Formal Foundation for Distributed Workflow Execution Based on State Charts, Proceedings of the 6th International Conference on Database Theory, p.230-246, January 08-10, 1997
• 30: Workflow management coalition, 2001. http://www.wfmc.org.
• 31: Web Services Description Language(WSFL 1.0), 2001. http://www.w3.org/TR/2001/NOTE-wsdl-20010315.
• 32: Web Services Flow Language(WSDL 1.1), 2001. http://www-3.ibm.com/ software/ solutions /webservices/pdf/WSFL.pdf.