Specification and verification of an atomic broadcast protocol

P. Zhou, J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

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.
Original languageEnglish
Title of host publicationDependable Computing for Critical Applications (Proceedings 4th International Working Conference, San Diego CA, USA, January 4-6, 1994)
EditorsF. Cristian, G. Lann, le, T. Lunt
Place of PublicationWien
PublisherSpringer
Pages291-308
ISBN (Print)3-211-82649-1
Publication statusPublished - 1995

Publication series

NameDependable computing and fault-tolerant systems
Volume9
ISSN (Print)0932-5581

Fingerprint Dive into the research topics of 'Specification and verification of an atomic broadcast protocol'. Together they form a unique fingerprint.

Cite this