ACM SIGMOD Anthology ACM SIGMOD dblp.uni-trier.de

Verifiable Properties of Database Transactions.

Michael Benedikt, Timothy Griffin, Leonid Libkin: Verifiable Properties of Database Transactions. PODS 1996: 117-127
@inproceedings{DBLP:conf/pods/BenediktGL96,
  author    = {Michael Benedikt and
               Timothy Griffin and
               Leonid Libkin},
  title     = {Verifiable Properties of Database Transactions},
  booktitle = {Proceedings of the Fifteenth ACM SIGACT-SIGMOD-SIGART Symposium
               on Principles of Database Systems, June 3-5, 1996, Montreal,
               Canada},
  publisher = {ACM Press},
  year      = {1996},
  isbn      = {0-89791-781-2},
  pages     = {117-127},
  ee        = {http://doi.acm.org/10.1145/237661.237692, db/conf/pods/BenediktGL96.html},
  crossref  = {DBLP:conf/pods/96},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX

Abstract

It is often necessary to ensure that database transactions preserve integrity constraints that specify valid database states. While it is possible to monitor for violations of constraints at run-time, rolling back transactions when violations are detected, it is preferable to verify correctness statically, before transactions are executed. This can be accomplished if we can verify transaction safety with respect to a set of constraints by means of calculating weakest preconditions. We study properties of weakest preconditions for a number of transaction and specification languages. We show that some simple transactions do not admit weakest preconditions over first-order logic. We also show that the class of transactions that admit weakest preconditions over first-order logic cannot be captured by any transaction language. We consider a strong local from of verifiability, and show that it is different from the general form. We define robustly verifiable transactions as those that can be statically analyzed regardless of extensions to the signature of the specification language, and we show that the class of robustly verifiable transactions over first order logic is exactly the class of transactions that admit the local form of verifiability. We discuss the implications of these results for the design of verifiable transaction languages.

Copyright © 1996 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.


Load The ACM SIGMOD Anthology, CDROM Edition, Volume 1-3, PODS '82-'98. and ... Load The ACM SIGMOD Anthology, Silver Edition, DVD 1, Proceedings. and ... BibTeX

Printed Edition

Proceedings of the Fifteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 3-5, 1996, Montreal, Canada. ACM Press 1996, ISBN 0-89791-781-2
Contents BibTeX

Online Edition: ACM Digital Library

[Index Terms]
[Full Text in PDF Format, 1048 KB]

References

[1]
Serge Abiteboul, Richard Hull, Victor Vianu: Foundations of Databases. Addison-Wesley 1995, ISBN 0-201-53771-0
Contents BibTeX
[2]
Serge Abiteboul, Victor Vianu: Transactions and Integrity Constraints. PODS 1985: 193-204 BibTeX
[3]
Serge Abiteboul, Victor Vianu: Procedural Languages for Database Queries and Updates. J. Comput. Syst. Sci. 41(2): 181-229(1990) BibTeX
[4]
Serge Abiteboul, Victor Vianu: Datalog Extensions for Database Queries and Updates. J. Comput. Syst. Sci. 43(1): 62-124(1991) BibTeX
[5]
...
[6]
Ralph-Johan Back: Proving Total Correctness of Nondeterministic Programs in Infinitary Logic. Acta Inf. 15: 233-249(1981) BibTeX
[7]
Michael Benedikt, Guozhu Dong, Leonid Libkin, Limsoon Wong: Relational Expressive Power of Constraint Query Languages. PODS 1996: 5-16 BibTeX
[8]
...
[9]
Rudolf Berghammer, Birgit Elbl, Ulf R. Schmerl: Formalizing Dijkstra's Predicate Transformer wp in Weak Second-Order Logic. Theor. Comput. Sci. 146(1&2): 185-197(1995) BibTeX
[10]
Val Tannen, Ramesh Subrahmanyam: Logical and Computational Aspects of Programming with Sets/Bags/Lists. ICALP 1991: 60-75 BibTeX
[11]
Edsger W. Dijkstra: Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18(8): 453-457(1975) BibTeX
[12]
Edsger W. Dijkstra: A Discipline of Programming. Prentice-Hall 1976
BibTeX
[13]
Ronald Fagin: Finite-Model Theory - A Personal Perspective. Theor. Comput. Sci. 116(1&2): 3-31(1993) BibTeX
[14]
Ronald Fagin, Larry J. Stockmeyer, Moshe Y. Vardi: On Monadic NP vs. Monadic co-NP. Inf. Comput. 120(1): 78-92(1995) BibTeX
[15]
...
[16]
...
[17]
...
[18]
Arding Hsu, Tomasz Imielinski: Integrity Checking for Multiple Updates. SIGMOD Conference 1985: 152-168 BibTeX
[19]
...
[20]
Neil Immerman: Languages that Capture Complexity Classes. SIAM J. Comput. 16(4): 760-778(1987) BibTeX
[21]
Neil Immerman, Sushant Patnaik, David W. Stemple: The Expressiveness of a Family of Finite Set Languages. PODS 1991: 37-52 BibTeX
[22]
Dino Karabeg, Victor Vianu: Simplification Rules and Complete Axiomatization for Relational Update Transactions. ACM Trans. Database Syst. 16(3): 439-475(1991) BibTeX
[23]
Leonid Libkin, Limsoon Wong: New Techniques for Studying Set Languages, Bag Languages and Aggregate Functions. PODS 1994: 155-166 BibTeX
[24]
Leonid Libkin, Limsoon Wong: Some Properties of Query Languages for Bags. DBPL 1993: 97-114 BibTeX
[25]
William McCune, Lawrence J. Henschen: Maintaining state constraints in relational databases: a proof theoretic basis. J. ACM 36(1): 46-68(1989) BibTeX
[26]
Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX
[27]
Xiaolei Qian: An Effective Method for Integrity Constraint Simplification. ICDE 1988: 338-345 BibTeX
[28]
Xiaolei Qian: An Axiom System for Database Transactions. Inf. Process. Lett. 36(4): 183-189(1990) BibTeX
[29]
Xiaolei Qian: The Expressive Power of the Bounded-Iteration Construct. Acta Inf. 28(7): 631-656(1991) BibTeX
[30]
...
[31]
Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989) BibTeX
[32]
David W. Stemple, Subhasish Mazumdar, Tim Sheard: On the Modes and Meaning of Feedback to Transaction Designers. SIGMOD Conference 1987: 374-386 BibTeX

Referenced by

  1. Timothy Griffin, Richard Hull: A Framework for Implementing Hypothetical Queries. SIGMOD Conference 1997: 231-242
  2. Michael Benedikt, H. Jerome Keisler: Expressive Power of Unary Counters. ICDT 1997: 291-305
BibTeX
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (info@acm.org), Corrections: anthology@acm.org
DBLP: Copyright © by Michael Ley (ley@uni-trier.de), last change: Sat May 16 23:34:15 2009