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}
}

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 ...

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 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML

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

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

Copyright © Mon Nov 2 21:04:31 2009 by Michael Ley (ley@uni-trier.de)