Serializability Preserving Extensions of Concurrency Control Protocols
Peter van der Stok
To be published in: Proc. of the 3rd int. conf. Perspective of System Informatics, LNCS 1999
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.
PostScript