Alin Deutsch
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.
- Demo, http://www.cs.ucsd.edu/~Isui/project/index.html.Google Scholar
- S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. Google ScholarDigital Library
- S. Abiteboul, V. Vianu, B. Fordham, and Y. Yesha. Relational transducers for electronic commerce. JCSS, 61(2):236--269, 2000. Extended abstract in PODS 98. Google ScholarDigital Library
- T. Ball and S. Rajamani. The SLAM project: Debugging system software via static analysis. In POPL, 2002. Google ScholarDigital Library
- N. Bjorner, A. Browne, E. Chang, M. Coln, A. Kapur, Z. Manna, H. Sipma, and T. E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Computer Aided Verification (CAV), 1996. Google ScholarDigital Library
- A. Bonner and M. Kifer. An overview of transaction logic. Theor. Comput. Sci., 133(2), 1994. Google ScholarDigital Library
- BPML.org. Business process modeling language. http://www.bpmi.org.Google Scholar
- 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. Google ScholarDigital Library
- S. Ceri, P. Fraternali, A. Bongio, M. Brambilla, S. Comai, and M. Matera. Designing data-intensive Web applications. Morgan-Kaufmann, 2002. Google ScholarDigital Library
- C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-efficient algorithms for the verification of temporal properties. In Computer Aided Verification (CAV), 1990. Google ScholarDigital Library
- 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.Google Scholar
- DAML-S Coalition (A. Ankolekar et al).DAML-S: Web service description for the semantic Web. In The Semantic Web - ISWC, pages 348--363, 2002. Google ScholarDigital Library
- H. Davulcu, M. Kifer, C. Ramakrishnan,, and I. V. Ramakrishnan. Logic based modeling and analysis of workflows. In PODS, 1998. Google ScholarDigital Library
- A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web services. In PODS, 2004. Google ScholarDigital Library
- 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).Google Scholar
- M. F. Fernández, D. Florescu, A. Y. Levy, and D. Suciu. Declarative specification of web sites with Strudel. VLDB Journal, 9(1):38--55, 2000. Google ScholarDigital Library
- D. Florescu, K. Yagoub, P. Valduriez, and V. Issarny. WEAVE: A data-intensive web site management system(software demonstration). In (EDBT), 2000.Google Scholar
- X. Fu, T. Bultan, and J. Su. Analysis of Interacting BPEL Web Services. In WWW'04, 2004. Google ScholarDigital Library
- D. Georgakopoulos, M. Hornick, and A. Sheth. An overview of workflow management: From process modeling to workflow automation infrastructure. In Distributed and Parallel Databases, 1995. Google ScholarDigital Library
- R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Int. Conf. on Protocol Specification, Testing and Verification (PSTV), 1995. Google ScholarDigital Library
- G. Holzmann. The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, 2003. Google ScholarDigital Library
- R. Hull, M. Benedikt, V. Christophides, and J. Su. E-Services: a look behind the curtain. In PODS, 2003. Google ScholarDigital Library
- R. Hull and J. Su. Tools for design of composite web services (tutorial). In PODS, 2004. Google ScholarDigital Library
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1991. Google ScholarDigital Library
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer Verlag, 1995. Google ScholarDigital Library
- G. Mecca, P. Merialdo, and P. Atzeni. Araneus in the era of xml. IEEE Data Engineering Bulletin, 22(3):19--26, 1999.Google Scholar
- S. Merz. Model checking: a tutorial overview. 2001.Google Scholar
- S. Narayanan and S. McIlraith. Simulation, verification and automated composition of Web services. In WWW, 2002. Google ScholarDigital Library
- M. Spielmann. Abstract State Machines: verification problems and complexity. Ph.D. thesis RWTH Aachen 2000.Google Scholar
- M. Spielmann. Verification of relational transducers for electronic commerce. JCSS., 66(1):40--65, 2003. Extended abstract in PODS 2000. Google ScholarDigital Library
- M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symp. on Logic in Computer Science, 1986.Google Scholar
- D. Wodtke and G. Weikum. A formal foundation for distributed workflow execution based on state charts. In ICDT, 1997. Google ScholarDigital Library
- Workflow management coalition, 2001. http://www.wfmc.org.Google Scholar
- Web Services Flow Language(WSFL 1.0), 2001. http://www-3.ibm.com/ software/ solutions/ webservices/pdf/WSFL.pdf.Google Scholar
- A verifier for interactive, data-driven web applications
Recommendations
Action Language verifier: an infinite-state model checker for reactive software specifications
Action Language is a specification language for reactive software systems. In this paper, we present the syntax and the semantics of the Action Language and we also present an infinite-state symbolic model checker called Action Language Verifier (ALV) ...
Specification and verification of data-driven Web applications
We study data-driven Web applications 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 ...
Comments