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