Formal Specification and Compositional Verification of an Atomic Broadcast Protocol

Ping Zhou and Jozef Hooman

Appeared in: Real-Time Systems, Volume 9, Number 2, pages 119-145, 1995.

An extended abstract appeared in: Dependable Computing for Critical Applications 4, Cristian, F.; Le Lann, G.; Lunt, T. (eds.), Dependable Computing and Fault-Tolerant Systems Series, Volume 9, Springer-Verlag, pages 291-308, 1995.

ABSTRACT

We apply a formal method based on assertions to specify and verify an atomic broadcast protocol. The protocol is implemented by replicating a server process on all processors in a network. We show that the verification of the protocol can be done compositionally by using specifications in which timing is expressed by local clock values. First the requirements of the protocol are formally described. Next the underlying communication mechanism, the assumptions about local clocks, and the failure assumptions are axiomatized. Also the server process is represented by a formal specification. Then we verify that parallel execution of the server processes leads to the desired properties by proving that the conjunction of all server specifications and the axioms about the system implies the requirements of the protocol.

Postscript