Abstract
We propose a model for multi-user data-driven communicating Web applications. An arbitrary number of users may access the application concurrently through Web sites and Web services. A Web service may have an arbitrary number of instances. The interaction between users and Web application is data-driven. Synchronous communication is done by shared access to the database and global application state. Private information may be stored in a local state. Asynchronous communication is done by message passing. A version of first-order linear time temporal logic (LTL-FO) is proposed to express behavioral properties of Web applications. The model is used to formally specify a significant fragment of an e-business application. Some of its desirable properties are expressed as LTL-FO formulas. We study a decision problem, namely whether the model satisfies an LTL-FO formula. We show the undecidability of the unrestricted verification problem and discuss some restrictions that ensure decidability.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)
SWSF Committee (2005), http://www.w3.org/Submission/SWSF-SWSO/
Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web services. In: PODS Proceedings, pp. 71–82 (2004)
Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. Journal of Computer and Systems Sciences 73(3), 442–474 (2007)
Deutsch, A., Sui, L., Vianu, V., Zhou, D.: Verification of communicating data-driven web services. In: PODS Proceedings, pp. 90–99 (2006)
Deutsch, A., Sui, L., Vianu, V., Zhou, D.: A system for specification and verification of interactive, data-driven web applications. In: SIGMOD Conference, pp. 772–774 (2006)
Fan, W., Geerts, F., Gelade, W., Neven, F., Poggi, A.: Complexity and composition of synthesized web services. In: PODS Proceedings, pp. 231–240 (2008)
Hull, R., Benedikt, M., Christophides, V., Su, J.: E-services: A look behind the curtain. In: PODS Proceedings, pp. 1–14 (2003)
Hull, R., Su, J.: Tools for composite web services: a short overview. SIGMOD Record 34(2), 86–95 (2005)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Narayanan, S., McIlraith, S.A.: Simulation, verification, and automated composition of web services. In: Proc. Int. World-Wide Web Conference (2002)
Papazoglou, M.P.: Web Services: Principles and Technology. Prentice-Hall, Englewood Cliffs (2008)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symp. on Logic in Computer Science (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marcus, M. (2010). Specification and Verification of Multi-user Data-Driven Web Applications. In: Laneve, C., Su, J. (eds) Web Services and Formal Methods. WS-FM 2009. Lecture Notes in Computer Science, vol 6194. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14458-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-14458-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14457-8
Online ISBN: 978-3-642-14458-5
eBook Packages: Computer ScienceComputer Science (R0)