Advertisement

Specification and Verification of an Atomic Broadcast Protocol

  • Ping Zhou
  • Jozef Hooman
Conference paper
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 9)

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.

Keywords

Server Process Clock Synchronization Local Clock Broadcast Protocol Conjunction Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    J.W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg(Eds.). Real-Time: Theory in Practice. LNCS 600, 1991.Google Scholar
  2. [2]
    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
  3. [3]
    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
  4. [4]
    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
  5. [5]
    J.M. Chang and N. Maxemchuck. Reliable broadcast protocols. ACM Trans. on Computer Systems 2(3), pages 251–273, 1984.CrossRefGoogle Scholar
  6. [6]
    F. Cristian. Synchronous atomic broadcast for redundant broadcast channels. Real-Time Systems 2, pages 195-212, 1990.Google Scholar
  7. [7]
    F. Cristian. Comments. Private Correspondence, 1993.Google Scholar
  8. [8]
    J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.Google Scholar
  9. [9]
    J. Rushby and F. von Henke. Formal verification of algorithms for critical systems. IEEE Trans. on Software Engineering, 19(1):13–23, 1993.CrossRefGoogle Scholar
  10. [10]
    N. Shankar. Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization. In LNCS 600, pages 217-236, 1992.Google Scholar
  11. [11]
    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
  12. [12]
    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
  13. [13]
    J. Zwiers. Compositionality, Concurrency and Partial Correctness. LNCS 321, Springer-Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Ping Zhou
    • 1
  • Jozef Hooman
    • 1
  1. 1.Department of Mathematics and Computing ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations