Verification of concurrency control protocols with PVS

Jozef Hooman

ABSTRACT

This lecture presents joint work with Dmitri Chkliaev and Peter van der Stok (Eindhoven University of Technology, The Netherlands).

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.