Formal Specification and Compositional Verification of an Atomic BroadcastProtocol

摘要

We apply formal methods to specify and verify an atomic broadcast protocol. Theprotocol 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. The requirements of the protocol are formally described. underlying communication mechanism, clock synchronization assumption, and failure assumptions are axiomatized. The server process is also represented by a formal specification. We verify that parallel execution of the server processes leads to the desired properties, by proving that the conjunction of all server specifications and axioms about the system implies the requirements of the protocol.