Mechanical Verification of a Non-Blocking Atomic Commitment Protocol
Dmitri Chkliaev*, Peter van der Stok*, and Jozef Hooman**
* Eindhoven University of Technology, The NETHERLANDS
** University of Nijmegen, The NETHERLANDS
Abstract
This paper concerns the formal specification and mechanical verification of
atomic commitment protocols (ACP's) for distributed database systems.
In particular, we consider the non-blocking ACP of Babaoglu and Toueg,
combined with our own termination protocol for recovered participants.
A new method to specify such protocols has been developed.
In this method, timed state machines are used to specify the
processes, whereas the communication
mechanism between processes is defined using assertions.
All safety and liveness properties,
including a new improved termination property,
have been proved with the interactive proof checker of PVS.
We also show that the original
termination protocol of Babaoglu and Toueg has an error.
Keywords:
formal specification, mechanical verification, distributed
algorithms, fault-tolerance, PVS, atomic commitment protocols