Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Sixth Annual IEEE Symposium on

Logic in Computer Science (LICS 1991)

Paper: Specifying and proving serializability in temporal logic (at LICS 1991)

Authors: Doron A. Peled Shmuel Katz Amir Pnueli

Abstract

Serializability of database transactions is first defined within the framework of linear temporal logic. For commutativity-based serializability, an alternative specification is given in a temporal logic whose semantic interpretation is especially tailored for reasoning about equivalence sequences of histories. The alternative specification method is given in ISTL* and is limited to the specification of concurrency control algorithms based on commutativity. A formal verification system for serializability that uses classical logic reasoning is provided. Within it, proving serializability of transactions executing a concurrency control algorithm is done along the same lines as proving properties of concurrent programs. Serializability for the multiversion-timestamp algorithm is verified

BibTeX

  @InProceedings{PeledKatzPnueli-Specifyingandprovin,
    author = 	 {Doron A. Peled and Shmuel Katz and Amir Pnueli},
    title = 	 {Specifying and proving serializability in temporal logic},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {232--244},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski