We use the verification system PVS to obtain mechanized support for the
formal verification of concurrency control protocols, concentrating on
database applications.
A method to verify conflict serializability of transactions 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.
As another application, we discuss the formal specification and mechanical
verification of a non-blocking atomic commitment protocol of Babaoglu and Toueg.
An error has been found in the original termination part of the protocol and
we have verified the correctness of our own improved protocol with PVS.