skip to main content
10.1145/1055558.1055571acmconferencesArticle/Chapter ViewAbstractPublication PagespodsConference Proceedingsconference-collections
Article

Specification and verification of data-driven web services

Published: 14 June 2004 Publication History

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]
S. Abiteboul, L. Herr, and J. V. den Bussche. Temporal versus first-order logic to query temporal databases. In Proc. ACM PODS, pages 49--57, 1996.]]
[2]
S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.]]
[3]
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.]]
[4]
A. J. Bonner and M. Kifer. An overview of transaction logic. Theor. Comput. Sci., 133(2):205--265, 1994.]]
[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]
S. Ceri, P. Fraternali, A. Bongio, M. Brambilla, S. Comai, and M. Matera. Designing data-intensive Web applications. Morgan-Kaufmann, 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]
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.]]
[12]
H. Davulcu, M. Kifer, C. R. Ramakrishnan, and I. V. Ramakrishnan. Logic based modeling and analysis of workflows. In Proc. ACM PODS, pages 25--33, 1998.]]
[13]
E. A. Emerson. Temporal and modal logic. In J. V. Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pages 995--1072. North-Holland Pub. Co/MIT Press, 1990.]]
[14]
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.]]
[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]
D. Georgakopoulos, M. F. Hornick, and A. P. Sheth. An overview of workflow management. From process modeling to workflow automation infrastructure. Distributed and Parallel Databases, 3(2):119--153, 1995.]]
[18]
D. Harel. On the formal semantics of statecharts. In Proc. LICS, pages 54--64, 1987.]]
[19]
R. Hull, M. Benedikt, V. Christophides, and J. Su. E-Services: a look behind the curtain. In Proc. ACM PODS, pages 1--14, 2003.]]
[20]
O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. J. of ACM, 47(2):312--360, 2000.]]
[21]
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1991.]]
[22]
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer Verlag, 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]
S. Narayanan and S. A. McIlraith. Simulation, verification and automated composition of Web services. In Proc. WWW, pages 77--88, 2002.]]
[25]
R. Reiter. Knowledge in action: logical foundations for specifying and implementing dynamical systems. MIT Press, 2001.]]
[26]
M. Spielmann. Abstract State Machines: Verification problems and complexity. Ph.D. thesis, RWTH Aachen, 2000.]]
[27]
M. Spielmann. Automatic verification of Abstract State Machines. In Proc. CAV, pages 431--442, 1999.]]
[28]
M. Spielmann. Verification of relational transducers for electronic commerce. JCSS., 66(1):40--65, 2003. Extended abstract in PODS 2000.]]
[29]
D. Wodtke and G. Weikum. A formal foundation for distributed workflow execution based on state charts. In Proc. ICDT, pages 231--246, 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.]]

Cited By

View all
  • (2022)Business ProcessesundefinedOnline publication date: 2-Mar-2022
  • (2018)Automatic verification of database-centric systemsACM SIGLOG News10.1145/3212019.32120255:2(37-56)Online publication date: 30-Apr-2018
  • (2015)Model-Based Testing for Composite Web Services in Cloud Brokerage ScenariosAdvances in Service-Oriented and Cloud Computing10.1007/978-3-319-14886-1_18(190-205)Online publication date: 28-Feb-2015
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PODS '04: Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems
June 2004
350 pages
ISBN:158113858X
DOI:10.1145/1055558
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 June 2004

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

SIGMOD/PODS04

Acceptance Rates

Overall Acceptance Rate 642 of 2,707 submissions, 24%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)4
  • Downloads (Last 6 weeks)0
Reflects downloads up to 30 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Business ProcessesundefinedOnline publication date: 2-Mar-2022
  • (2018)Automatic verification of database-centric systemsACM SIGLOG News10.1145/3212019.32120255:2(37-56)Online publication date: 30-Apr-2018
  • (2015)Model-Based Testing for Composite Web Services in Cloud Brokerage ScenariosAdvances in Service-Oriented and Cloud Computing10.1007/978-3-319-14886-1_18(190-205)Online publication date: 28-Feb-2015
  • (2014)Automatic Verification of Database-Centric SystemsACM SIGMOD Record10.1145/2694428.269443043:3(5-17)Online publication date: 4-Dec-2014
  • (2014)Web Service Compositions with Fuzzy PreferencesACM Transactions on Internet Technology10.1145/257623113:4(1-33)Online publication date: 1-Jul-2014
  • (2013)Foundations of data-aware process analysisProceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI symposium on Principles of database systems10.1145/2463664.2467796(1-12)Online publication date: 22-Jun-2013
  • (2012)A logical approach to data-aware automated sequence generationTransactions on Computational Science XV10.5555/2184162.2184169(192-216)Online publication date: 1-Jan-2012
  • (2012)A Logical Approach to Data-Aware Automated Sequence GenerationTransactions on Computational Science XV10.1007/978-3-642-28525-7_7(192-216)Online publication date: 2012
  • (2011)A quest for beauty and wealth (or, business processes for database researchers)Proceedings of the thirtieth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems10.1145/1989284.1989286(1-12)Online publication date: 13-Jun-2011
  • (2011)Coordination, Organisation and Model-driven Approaches for Dynamic, Flexible, Robust Software and Services EngineeringService Engineering10.1007/978-3-7091-0415-6_4(85-115)Online publication date: 2011
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media