CFP last date
20 June 2024
Reseach Article

Rigorous Design of Partition-Aware Total Order Broadcast System using Event-B

by Raghuraj Suryavanshi, Divakar Yadav
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 26 - Number 8
Year of Publication: 2011
Authors: Raghuraj Suryavanshi, Divakar Yadav

Raghuraj Suryavanshi, Divakar Yadav . Rigorous Design of Partition-Aware Total Order Broadcast System using Event-B. International Journal of Computer Applications. 26, 8 ( July 2011), 35-39. DOI=10.5120/3123-4297

@article{ 10.5120/3123-4297,
author = { Raghuraj Suryavanshi, Divakar Yadav },
title = { Rigorous Design of Partition-Aware Total Order Broadcast System using Event-B },
journal = { International Journal of Computer Applications },
issue_date = { July 2011 },
volume = { 26 },
number = { 8 },
month = { July },
year = { 2011 },
issn = { 0975-8887 },
pages = { 35-39 },
numpages = {9},
url = { },
doi = { 10.5120/3123-4297 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
%0 Journal Article
%1 2024-02-06T20:12:17.512032+05:30
%A Raghuraj Suryavanshi
%A Divakar Yadav
%T Rigorous Design of Partition-Aware Total Order Broadcast System using Event-B
%J International Journal of Computer Applications
%@ 0975-8887
%V 26
%N 8
%P 35-39
%D 2011
%I Foundation of Computer Science (FCS), NY, USA

In distributed system, the sites communicate with each other by exchange of messages. A total order broadcast is a reliable broadcast that ensures delivery of messages to the sites in the same order. For the fault tolerant applications, ordering algorithm must support the network partitions and site failure. In this paper, we present a formal model of total order broadcast system in the presence of network partition and site failures. We have used Event-B as a formal technique for the development of our model. In this technique system is built in several stages by gradually introducing the details in the refinement steps. We outline an abstract model specifying total order broadcast and introducing the details in the refinement level for considering the case of network partitioning and site failure.

  1. D´efago, X., Schiper, A., Urb´an, P. 2004 Total order broadcast and multicast algorithms: Taxonomy and survey. ACM Comput. Surv. 36(4), 372–421.
  2. Hadzilacos, V., Toueg, S. 1994 A modular approach to fault-tolerant broadcasts and related problems. Technical Report TR 94 -1425. Cornell University.
  3. Suryavanshi, R., Yadav, D. 2010 Formal Development of Byzantine Immune Total Order Broadcast System using Event-B. In ICDEM 2010, F. Andres, R. Kannan, Eds. LNCS, Vol. 6411, Springer.
  4. Hinchey, M., Bowen, J.P. and Glass, R. 1996 Formal methods: Point-counterpoint. Computer, 29(4):18–19.
  5. Jones, C., Jackson, D. and Wing, J. 1996 Formal methods light. Computer, 29(4): 20–22.
  6. Saiedian, H. 1996 An invitation to formal methods, Computer, 29(4):16–17.
  7. Butler, M. 1997 An Approach to Design of Distributed Systems with B. In Proceedings 1997 10th Int. Conf. of Z Users: The Z Formal Specification Notation (ZUM), vol.1212, LNCS, pp.223-241.
  8. Butler, M., Walden, M. 1996 Distributed System Development in B. In Proceedings of Ist Conf. in B Method, Nantes, pp.155-168.
  9. Rezazadeh, A., Butler, M. 2005 Some Guidelines for formal development of web based application in B Method. In Proceedings of 4th Intl. Conf. of B and Z users, Guildford, LNCS, Springer, pp 472-491.
  10. Abrial, J.R. 1996 The B-Book: Assigning programs to meanings. Cambridge University Press.
  11. Abrial, J.R. 1996 Extending B without changing it for developing distributed systems. In First B Conference.
  12. Yadav, D., Butler, M. 2005 Application of Event B to Global Causal Ordering for Fault Tolerant Transactions. In Proceedings of REFT 2005, Newcastle upon Tyne, pp 93-103.
  13. Butler, M. and Yadav, D. An incremental development of the mondex system in Event-B. In Formal Aspects of Computing, 20(1):61–77, 2008.
  14. Abrial, J.R. and Voison, L. 2005 Event-B language. Technical Report, Deliverables 3.2, EU Project IST-511599-RODIN,
  15. Abrial, J.R. 2007 A system development process with Event-B and the Rodin platform. In proceedings of ICFEM 2007, Butler, M., Hinchey, L. Petrie, Eds. vol.4789, LNCS, Springer, pp.1-3.
  16. Stanoi, I., Agrawal, D., Abbadi, A., 1998 Using broadcast primitives in replicated databases. In Proc. of 18th IEEE Intl. Conf. on Distributed Computing System,ICDCS, pages 148–155.
  17. Baldoni, R., Cimmino, S., Marchetti, C., 2005 Total order communications: A practical analysis. In EDCC 2005, Mario Dal Cin, Mohamed Kaˆaniche, and Andr´as Pataricza, Eds, LNCS Vol. 3463, pages 38–54. Springer.
  18. Birman, K., Schiper, A.,Stephenson, P., 1991 Lightweigt causal and atomic group multicast. ACM Trans. Comput. Syst., 9(3):272–314,.
  19. Marchetti, C., Cimmino, S., Baldoni, R., 2006 A classification of total order specifications and its application to fixed sequencer-based implementations. Journal of Parallel and Distributed Computing, 66(1):108–127.
Index Terms

Computer Science
Information Sciences


Total order broadcast Formal methods Event-B sequencer