@inbook{c47ac38ea1f9491d99ac3287f38c0802,
title = "Specification and verification of an atomic broadcast protocol",
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. 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.",
author = "P. Zhou and J.J.M. Hooman",
year = "1995",
language = "English",
isbn = "3-211-82649-1",
series = "Dependable computing and fault-tolerant systems",
publisher = "Springer",
pages = "291--308",
editor = "F. Cristian and {Lann, le}, G. and T. Lunt",
booktitle = "Dependable Computing for Critical Applications (Proceedings 4th International Working Conference, San Diego CA, USA, January 4-6, 1994)",
address = "Germany",
}