Mechanical Verification of a Non-Blocking Atomic Commitment Protocol

Dmitri Chkliaev, Peter van der Stok and Jozef Hooman

Appeared in: Proceedings 2000 ICDCS Workshop on Distributed System Validation and Verification (DSVV'2000), IEEE, pages E 96 - E 103, April 2000.

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.

Postscript PVS dump file Transparances DSVV'2000