Mechanical Verification of a Non-Blocking
Atomic Commitment Protocol
Peter van der Stok and
Appeared in: Proceedings 2000 ICDCS Workshop on Distributed System Validation
and Verification (DSVV'2000),
IEEE, pages E 96 - E 103, April 2000.
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
We also show that the original
termination protocol of Babaoglu and Toueg has an error.
PVS dump file