Logic in Computer Science (LICS 1991)

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

Authors: Doron 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 Peled and Shmuel Katz and Amir Pnueli},
    title = 	 {Specifying and proving serializability in temporal logic},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {232--244},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }