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. 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.
|Title of host publication||Dependable Computing for Critical Applications (Proceedings 4th International Working Conference, San Diego CA, USA, January 4-6, 1994)|
|Editors||F. Cristian, G. Lann, le, T. Lunt|
|Place of Publication||Wien|
|Publication status||Published - 1995|
|Name||Dependable computing and fault-tolerant systems|