Serializability preserving extensions of concurrency control protocols

D. Chkliaev, J.J.M. Hooman, P.D.V. Stok, van der

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

The verification system PVS is used to obtain mechanized support for the formal specification and verification of concurrency control protocols, concentrating on database applications. A method to verify conflict serializability has been formulated in PVS and proved to be sound and complete with the interactive proof checker of this tool. The method has been used to verify a few basic protocols. Next we present a systematic way to extend these protocols with new actions and control information. We show that if such an extension satisfies a few simple correctness conditions, the new protocol is serializable by construction.
Original languageEnglish
Title of host publicationPerspectives of System Informatics (Proceedings PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999)
EditorsD. Bjorner, M. Broy, A.V. Zamulin
Place of PublicationBerlin
PublisherSpringer
Pages180-193
ISBN (Print)3-540-67102-1
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
Volume1755
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Serializability preserving extensions of concurrency control protocols'. Together they form a unique fingerprint.

Cite this