A verifier for interactive, data-driven web applications

ABSTRACT

We present WAVE, a verifier for interactive, database-driven Web applications specified using high-level modeling tools such as WebML. WAVE is complete for a broad class of applications and temporal properties. For other applications, WAVE can be used as an incomplete verifier, as commonly done in software verification. Our experiments on four representative data-driven applications and a battery of common properties yielded surprisingly good verification times, on the order of seconds. This suggests that interactive applications controlled by database queries may be unusually well suited to automatic verification. They also show that the coupling of model checking with database optimization techniques used in the implementation of WAVE can be extremely effective. This is significant both to the database area and to automatic verification in general.

REFERENCES

• 1: Demo, http://www.cs.ucsd.edu/~Isui/project/index.html.
• 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: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 5: Nikolaj Bjørner , Anca Browne , Eddie Chang , Michael Colón , Arjun Kapur , Zohar Manna , Henny Sipma , Tomás E. Uribe, STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems, Proceedings of the 8th International Conference on Computer Aided Verification, p.415-418, August 03, 1996
• 6: 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]
• 7: BPML.org. Business process modeling language. http://www.bpmi.org.
• 8: 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.
• 9: 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
• 10: Costas Courcoubetis , Moshe Y. Vardi , Pierre Wolper , Mihalis Yannakakis, Memory Efficient Algorithms for the Verification of Temporal Properties, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.233-242, June 18-21, 1990
• 11: 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.
• 12: 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
• 13: 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]
• 14: 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]
• 15: A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web services. Invited to Journal of Computer Systems and Sciences, 2005 (submitted).
• 16: 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]
• 17: D. Florescu, K. Yagoub, P. Valduriez, and V. Issarny. WEAVE: A data-intensive web site management system(software demonstration). In (EDBT), 2000.
• 18: 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]
• 19: 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]
• 20: Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
• 21: G. Holzmann. The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, 2003.
• 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: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 25: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 26: G. Mecca, P. Merialdo, and P. Atzeni. Araneus in the era of xml. IEEE Data Engineering Bulletin, 22(3):19--26, 1999.
• 27: S. Merz. Model checking: a tutorial overview. 2001.
• 28: 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]
• 29: M. Spielmann. Abstract State Machines: verification problems and complexity. Ph.D. thesis RWTH Aachen 2000.
• 30: 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]
• 31: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symp. on Logic in Computer Science, 1986.
• 32: 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
• 33: Workflow management coalition, 2001. http://www.wfmc.org.
• 34: Web Services Flow Language(WSFL 1.0), 2001. http://www-3.ibm.com/ software/ solutions/ webservices/pdf/WSFL.pdf.