Specification and Verification of an Atomic Broadcast Protocol
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.
KeywordsServer Process Clock Synchronization Local Clock Broadcast Protocol Conjunction Rule
Unable to display preview. Download preview PDF.
- J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg(Eds.). Real-Time: Theory in Practice. LNCS 600, 1991.Google Scholar
- F. Cristian, H. Aghili, and R. Strong. Clock synchronization in the presence of omission and performance failures, and processor joins. In Global States and Time in Distributed Systems. Z. Yang and T.A. Marsland (Eds.), 1993.Google Scholar
- F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to Byzantine agreement. In The 15th Annual International Symposium on Fault-Tolerant Computing, pages 200-206. Ann Arbor, USA, 1985.Google Scholar
- F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to Byzantine agreement. Technical Report RJ 5244, IBM Almaden Research Center, 1989.Google Scholar
- F. Cristian. Synchronous atomic broadcast for redundant broadcast channels. Real-Time Systems 2, pages 195-212, 1990.Google Scholar
- F. Cristian. Comments. Private Correspondence, 1993.Google Scholar
- J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.Google Scholar
- N. Shankar. Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization. In LNCS 600, pages 217-236, 1992.Google Scholar
- P. Zhou and J. Hooman. A proof theory for asynchronously communicating real-time systems. In Proc. of the 13th IEEE Real-Time Systems, pages 177-186, 1992.Google Scholar
- P. Zhou and J. Hooman. Formal specification and compositional verification of an atomic broadcast protocol. Technical report CSN 94/05, Eindhoven University of Technology, To appear in Real-Time Systems, 1994.Google Scholar
- J. Zwiers. Compositionality, Concurrency and Partial Correctness. LNCS 321, Springer-Verlag, 1989.Google Scholar