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. We show that the verification of the protocol can be done compositionally by using specifications in which timing is expressed by local clock values. 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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
O. Babaoglu and R. Drumond. Streets of Byzantium: Network architectures for fast reliable broadcast.IEEE Transactions on Software Engineering 11(6):546–554, 1985.
J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg(Eds.).Real-Time: Theory in Practice. LNCS 600, Springer-Verlag, 1991.
K. Birman and T. Joseph. Reliable communication in the presence of failures.ACM Transactions on Computer Systems 5(1, pages 47–76, 1987.
F. Cristian, H. Aghili, and R. Strong. Approximate clock synchronization despite omission and performance failures and processor joins. InThe 16th International Symposium on Fault-Tolerant Computing. Wien, Austrian, 1986.
F. Cristian, H. Aghili, and R. Strong. Clock synchronization in the presence of omission and performance failures, and processor joins. InGlobal States and Time in Distributed Systems. Z. Yang and T.A. Marsland (Eds.), IEEE Computer Society Press, 1993.
F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to Byzantine agreement. InThe 15th Annual International Symposium on Fault-Tolerant Computing, pages 200 – 206. Ann Arbor, USA, 1985.
F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to Byzantine agreement. Research Report RJ 5244, IBM Almaden Research Center, 1989.
J.M. Chang and N. Maxemchuck. Reliable broadcast protocols.ACM Transactions on Computer Systems 2(3, pages 251–273, 1984.
F. Cristian. Synchronous atomic broadcast for redundant broadcast channels.Real-Time Systems 2, pages 195–212, 1990.
F. Cristian. Comments.Private Correspondence, 1993.
J. Hooman.Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.
L. Lamport and P.M. Melliar-Smith. Synchronizing clocks in the presence of faults.Journal of the ACM, 32(1):52–78, 1985.
J. Rushby and F. von Henke. Formal verification of algorithms for critical systems.IEEE Transactions on Software Engineering, 19(1):13–23, 1993.
F.B. Schneider. Understanding protocols for Byzantine clock synchronization. Technical report 87-859, Dept. of Computer Science, Cornell University, 1987.
N. Shankar. Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization. InFormal Techniques in Real-Time and Fault-Tolerant Systems, pages 217–236. J. Vytopil(Ed.), LNCS 571, Springer-Verlag, 1992.
P. Zhou and J. Hooman. A proof theory for asynchronously communicating real-time systems. InProc. of the 13th IEEE Real-Time Systems, pages 177–186. IEEE Computer Society Press, 1992.
J. Zwiers.Compositionality, Concurrency and Partial Correctness. LNCS 321, Springer-Verlag, 1989.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Zhou, P., Hooman, J. Formal specification and compositional verification of an atomic broadcast protocol. Real-Time Syst 9, 119–145 (1995). https://doi.org/10.1007/BF01088854
Issue Date:
DOI: https://doi.org/10.1007/BF01088854