More Web Proxy on the site http://driver.im/

research-article

Free access

Automatic verification of database-driven systems: a new frontier

Author:

Victor VianuAuthors Info & Claims

ICDT '09: Proceedings of the 12th International Conference on Database Theory

Pages 1 - 13

https://doi.org/10.1145/1514894.1514896

Published: 23 March 2009 Publication History

Abstract

We describe a novel approach to verification of software systems centered around an underlying database. Instead of applying general-purpose techniques with only partial guarantees of success, it identifies restricted but reasonably expressive classes of applications and properties for which sound and complete verification can be performed in a fully automatic way. This leverages the emergence of high-level specification tools for database-centered applications that not only allow fast prototyping and improved programmer productivity but, as a side effect, provide convenient targets for automatic verification. We present theoretical and practical results on verification of database-driven systems. The results are quite encouraging and suggest that, unlike arbitrary software systems, significant classes of database-driven systems may be amenable to automatic verification. This relies on a novel marriage of database and model checking techniques, of relevance to both the database and the computer aided verification communities.

References

[1]

M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable specifications of reactive systems. In Proc. ICALP Conference, 1989.

Digital Library

[2]

S. Abiteboul, O. Benjelloun, and T. Milo. The Active XML project: an overview. VLDB Journal, 17(5):1019--1040, 2008.

Digital Library

[3]

S. Abiteboul, L. Herr, and J. V. den Bussche. Temporal versus first-order logic to query temporal databases. In Proc. ACM Symp. on Principles of Database Systems (PODS), pages 49--57, 1996.

Digital Library

[4]

S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.

Digital Library

[5]

S. Abiteboul, L. Segoufin, and V. Vianu. Static analysis of Active XML systems. In Proc. ACM Symp. on Principles of Database Systems (PODS), pages 221--230, 2008.

Digital Library

[6]

S. Abiteboul, V. Vianu, B. Fordham, and Y. Yesha. Relational transducers for electronic commerce. Journal of Computer and System Sciences (JCSS), 61(2):236--269, 2000. Extended abstract in PODS 98.

Digital Library

[7]

N. Adam, V. Atluri, and W. Huang. Modeling and analysis of workflows using Petri nets. Journal of Intelligent Information Systems, 10(2):131--158, 1998.

Digital Library

[8]

D. Berardi, D. Calvanese, G. Giacomo, R. Hull, and M. Mecella. Automatic composition of transisiton-based semantic web services with messaging. In Proc. Int'l. Conf. on Very Large Databases (VLDB), 2005.

Digital Library

[9]

D. Berardi, D. Calvanese, G. D. Giacomo, R. Hull, M. Lenzerini, and M. Mecella. Modeling data & processes for service specifications in Colombo. In EMOI-INTEROP, 2005.

[10]

D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. Automatic composition of e-services that export their behavior. In Proc. Int'l. Conf on Service-Oriented Computing (ICSOC), pages 43--58, 2003.

[11]

D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. E-service composition by description logics based reasoning. In Description Logics, 2003.

[12]

D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. A tool for automatic composition of services based on logics of programs. In Technologies for E-Services, 5th International Workshop (TES), pages 80--94, 2004.

Digital Library

[13]

D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. Automatic service composition based on behavioral descriptions. Int. J. Cooperative Inf. Syst., 14(4):333--376, 2005.

[14]

D. Berardi, G. D. Giacomo, M. Lenzerini, M. Mecella, and D. Calvanese. Synthesis of underspecified composite e-services based on automated reasoning. In Proc. Int'l. Conf on Service-Oriented Computing (ICSOC), pages 105--114, 2004.

Digital Library

[15]

M. Bojanczyk, A. Muscholl, T. Schwentick, L. Segoufin, and C. David. Two-variable logic on words with data. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 7--16, 2006.

Digital Library

[16]

A. J. Bonner and M. Kifer. An overview of transaction logic. Theor. Comput. Sci., 133(2):205--265, 1994.

Digital Library

[17]

A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu. Rewriting systems with data. In Fundamentals of Computation Theory, 16th International Symposium (FCT), volume 4639 of Lecture Notes in Computer Science, pages 1--22. Springer, 2007.

Digital Library

[18]

A. Bouajjani, P. Habermehl, and R. Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295:85--106, 2003.

Digital Library

[19]

A. Bouajjani, Y. Jurski, and M. Sighireanu. A generic framework for reasoning about dynamic networks of infinite-state processes. In TACAS'07, volume 4424 of Lecture Notes in Computer Science, pages 690--705. Springer, 2007.

Digital Library

[20]

P. Bouyer. A logical characterization of data languages. Information Processing Letters, 84(2):75--85, 2002.

Digital Library

[21]

P. Bouyer, A. Petit, and D. Thérien. An algebraic approach to data languages and timed languages. Information and Computation, 182(2):137--162, 2003.

Digital Library

[22]

BPML.org. Business process modeling language. http://www.bpmi.org.

[23]

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.

Digital Library

[24]

D. Brand and P. Zafiropulo. On communicating finite-state machines. J. of the ACM, 30(2):323--342, 1983.

Digital Library

[25]

T. Bultan, X. Fu, R. Hull, and J. Su. Conversation specification: a new approach to design and analysis of e-service composition. In World Wide Web Conference, pages 403--410, 2003.

Digital Library

[26]

O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification of infinite structures. In Handbook of Process Algebra, pages 545--623. Elsevier Science, 2001.

[27]

S. Ceri, P. Fraternali, A. Bongio, M. Brambilla, S. Comai, and M. Matera. Designing data-intensive Web applications. Morgan-Kaufmann, 2002.

Digital Library

[28]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.

Digital Library

[29]

C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-efficient algorithms for the verification of temporal properties. Formal methods in system design, 1:275--288, 1992.

Digital Library

[30]

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.

Digital Library

[31]

H. Davulcu, M. Kifer, C. R. Ramakrishnan, and I. V. Ramakrishnan. Logic based modeling and analysis of workflows. In Proc. ACM Symp. on Principles of Database Systems (PODS), pages 25--33, 1998.

Digital Library

[32]

S. Demri and R. Lazić. LTL with the Freeze Quantifier and Register Automata. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 17--26, 2006.

Digital Library

[33]

S. Demri, R. Lazić, and A. Sangnier. Model checking freeze LTL over one-counter automata. In Proc. 11th Int'l. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 490--504, 2008.

Digital Library

[34]

A. Deutsch, R. Hull, F. Patrizi, and V. Vianu. Automatic verification of data-centric business processes. This proceedings.

Digital Library

[35]

A. Deutsch, M. Marcus, L. Sui, V. Vianu, and D. Zhou. A verifier for interactive, data-driven web applications. In Proc. ACM SIGMOD Int'l. Conf. on Management of Data (SIGMOD), pages 539--550, 2005.

Digital Library

[36]

A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web services. In Proc. ACM Symp. on Principles of Database Systems (PODS), pages 71--82, 2004.

Digital Library

[37]

A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web services. Journal of Computer and System Sciences (JCSS), 73(3):442--474, 2007.

Digital Library

[38]

A. Deutsch, L. Sui, V. Vianu, and D. Zhou. A system for specification and verification of interactive, data-driven Web applications. In Proc. ACM SIGMOD Int'l. Conf. on Management of Data (SIGMOD), pages 772--774, 2006.

Digital Library

[39]

A. Deutsch, L. Sui, V. Vianu, and D. Zhou. Verification of communicating data-driven Web services. In Proc. ACM Symp. on Principles of Database Systems (PODS), pages 90--99, 2006.

Digital Library

[40]

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.

Digital Library

[41]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about knowledge. MIT Press, 1996.

Digital Library

[42]

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.

Digital Library

[43]

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.

[44]

J. Garson. Quantification in modal logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, pages 249--307. Reidel, 1977.

[45]

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.

Digital Library

[46]

D. Harel. On the formal semantics of statecharts. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 54--64, 1987.

[47]

D. Harel. Statecharts: A visual formulation for complex systems. Sci. Comput. Program, 8(3):231--274, 1987.

Digital Library

[48]

G. Hughes and M. Cresswell. An introduction to modal logic. Methuen, 1968.

[49]

R. Hull, M. Benedikt, V. Christophides, and J. Su. E-services: a look behind the curtain. In Proc. ACM Symp. on Principles of Database Systems (PODS), pages 1--14, 2003.

Digital Library

[50]

R. Hull and J. Su. Tools for design of composite web services. In Proc. ACM SIGMOD Int'l. Conf. on Management of Data (SIGMOD), pages 958--961, 2004.

Digital Library

[51]

M. Jurdzinski and R. Lazić. Alternation-free modal mu-calculus for data trees. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 131--140, 2007.

Digital Library

[52]

O. Kupferman and M. Vardi. Synthesizing distributed systems. In Proc. IEEE Conf. on Logic in Computer Science (LICS), 2001.

Digital Library

[53]

R. Lazić, T. Newcomb, J. Ouaknine, A. Roscoe, and J. Worrell. Nets with tokens which carry data. In ICATPN'07, volume 4546 of Lecture Notes in Computer Science, pages 301--320. Springer, 2007.

Digital Library

[54]

G. Mecca, P. Merialdo, and P. Atzeni. Araneus in the era of XML. IEEE Data Engineering Bulletin, 22(3):19--26, 1999.

[55]

S. Merz. Model checking: a tutorial overview. In Modeling and verification of parallel processes. Springer-Verlag New York, 2001.

Digital Library

[56]

R. Milner. Communicating and mobile systems: the π calculus. Cambridge University Press, 1999.

Digital Library

[57]

W. Mok and D. Paper. Using harel's statecharts to model business workflows. J. of Database Management, 13(3):17--34, 2002.

[58]

F. Neven, T. Schwentick, and V. Vianu. Finite State Machines for Strings Over Infinite Alphabets. ACM Transactions on Computational Logic, 5(3):403--435, 2004.

Digital Library

[59]

A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proc. IEEE Symp. on Foundations of Computer Science (FOCS), 1990.

Digital Library

[60]

E. L. Post. Recursive unsolvability of a problem of Thue. J. of Symbolic Logic, 12:1--11, 1947.

[61]

R. Reiter. Knowledge in action:logical foundations for specifying and implementing dynamical systems. MIT Press, 2001.

Digital Library

[62]

A. Sistla and E. Clarke. The complexity of propositional linear temporal logic. J. of the ACM, 32:733--749, 1985.

Digital Library

[63]

A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217--237, 1987.

Digital Library

[64]

M. Spielmann. Verification of relational transducers for electronic commerce. Journal of Computer and System Sciences (JCSS), 66(1):40--65, 2003. Extended abstract in PODS 2000.

Digital Library

[65]

B. Trankhtenbrot. The impossibility of an algorithm for the decision problem for finite models. Doklady Academii Nauk SSSR, 70:569--572, 1950.

[66]

W. M. P. van der Aalst. The application of petri nets to workflow management. Journal of Circuits, Systems, and Computers, 8(1):21--66, 1998.

[67]

W. M. P. van der Aalst and A. H. M. ter Hofstede. Workflow patterns: On the expressive power of (petri-net-based) workflow languages. In Proc. of the Fourth International Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, Denmark, August 28--30, 2002 / Kurt Jensen (Ed.), pages 1--20. Technical Report DAIMI PB-560, Aug. 2002. InternalNote: Submitted by: hr available online: http://www.daimi.aau.dk/CPnets/workshop02/cpn/papers/.

[68]

M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 332--344, 1986.

[69]

D. Wodtke and G. Weikum. A formal foundation for distributed workflow execution based on state charts. In Proc. of Intl. Conf. on Database Theory (ICDT), pages 231--246, 1997.

Digital Library

[70]

Workflow management coalition, 2001. http://www.wfmc.org.

[71]

Web Services Flow Language(WSFL 1.0), 2001. http://www-3.ibm.com/software/solutions/webservices/pdf/WSFL.pdf.

Cited By

Aiswarya CCalvanese DDi Cosmo FMontali M(2024)Verification of Unary Communicating Datalog ProgramsProceedings of the ACM on Management of Data10.1145/36515902:2(1-26)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651590
Ghilardi SGianola AMontali MRivkin AElkind E(2023)Safety verification and universal invariants for relational action basesProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/362(3248-3257)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/362
Calvanese DGianola AMazzullo AMontali MWilliams BChen YNeville J(2023)SMT safety verification of ontology-based processesProceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence and Thirteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v37i5.25772(6271-6279)Online publication date: 7-Feb-2023
https://dl.acm.org/doi/10.1609/aaai.v37i5.25772
Show More Cited By

Recommendations

Recency-Bounded Verification of Dynamic Database-Driven Systems
PODS '16: Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems

We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a (DMS) modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations ...
Automatic verification of parameterized systems
Automatic verification of database-centric systems

We present an overview of results on verification of temporal properties of infinite-state transition systems arising from processes that carry and manipulate unbounded data. The techniques bring into play tools from logic, database theory, and model ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ICDT '09: Proceedings of the 12th International Conference on Database Theory

March 2009

334 pages

ISBN:9781605584232

DOI:10.1145/1514894

Editor:
Ronald Fagin
IBM Research

Copyright © 2009 ACM.

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 March 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

Division of Information and Intelligent Systems

Conference

EDBT/ICDT '09

EDBT/ICDT '09: EDBT/ICDT '09 joint conference

March 23 - 25, 2009

St. Petersburg, Russia

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

35
Total Citations
View Citations
538
Total Downloads

Downloads (Last 12 months)60
Downloads (Last 6 weeks)4

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Aiswarya CCalvanese DDi Cosmo FMontali M(2024)Verification of Unary Communicating Datalog ProgramsProceedings of the ACM on Management of Data10.1145/36515902:2(1-26)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651590
Ghilardi SGianola AMontali MRivkin AElkind E(2023)Safety verification and universal invariants for relational action basesProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/362(3248-3257)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/362
Calvanese DGianola AMazzullo AMontali MWilliams BChen YNeville J(2023)SMT safety verification of ontology-based processesProceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence and Thirteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v37i5.25772(6271-6279)Online publication date: 7-Feb-2023
https://dl.acm.org/doi/10.1609/aaai.v37i5.25772
Exibard LFiliot EKhalimov A(2023)Church synthesis on register automata over linearly ordered data domainsFormal Methods in System Design10.1007/s10703-023-00435-w61:2-3(290-337)Online publication date: 10-Oct-2023
https://doi.org/10.1007/s10703-023-00435-w
Chirkova RDoyle JReutter J(2021)Ensuring Data Readiness for Quality Requirements with Help from Procedure ReuseJournal of Data and Information Quality10.1145/342815413:3(1-15)Online publication date: 27-Apr-2021
https://dl.acm.org/doi/10.1145/3428154
Alam MHalder RPinto J(2021)A deductive reasoning approach for database applications using verification conditionsJournal of Systems and Software10.1016/j.jss.2020.110903175(110903)Online publication date: May-2021
https://doi.org/10.1016/j.jss.2020.110903
Calvanese DGhilardi SGianola AMontali MRivkin A(2021)Model Completeness, Uniform Interpolants and Superposition CalculusJournal of Automated Reasoning10.1007/s10817-021-09596-x65:7(941-969)Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s10817-021-09596-x
Calvanese DGhilardi SGianola AMontali MRivkin A(2020)SMT-based verification of data-aware processes: a model-theoretic approachMathematical Structures in Computer Science10.1017/S0960129520000067(1-43)Online publication date: 3-Apr-2020
https://doi.org/10.1017/S0960129520000067
Faran RKupferman O(2020)On Synthesis of Specifications with ArithmeticSOFSEM 2020: Theory and Practice of Computer Science10.1007/978-3-030-38919-2_14(161-173)Online publication date: 17-Jan-2020
https://doi.org/10.1007/978-3-030-38919-2_14
Calvanese DGhilardi SGianola AMontali MRivkin A(2019)Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary AchievementsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.311.9311(53-58)Online publication date: 31-Dec-2019
https://doi.org/10.4204/EPTCS.311.9
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents