Paper: Specifying and proving serializability in temporal logic (at LICS 1991)
Authors: Doron Peled Shmuel Katz Amir PnueliAbstract
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} }