Abstract
Distributed systems have complex designs which are difficult to understand and verify. A rigorous specification of such systems using mathematical techniques such as formal methods is required to understand their precise behavior. Safety property implies that the system is free from deadlocks and safe with respect to the invariants, while the liveness property ensures that the system eventually makes progress. Various group communication protocols are one of the building blocks of reliable distributed systems applications. One of the message ordering protocols is the causal order broadcast in which message delivery at various processes takes places as per causal order. This paper presents how the liveness properties are preserved by message passing in causal order using Event-B. An incremental model for causal order-based message passing is constructed using Event-B specification. The properties of causal order broadcast are first specified using an abstract model, and then, details are added with each refinement step. Liveness property is ascertained by ensuring enabledness preservation and non-divergence among various refinements and is expressed as invariants in the model of causal order broadcast system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Kindler, E. (1994). Safety and liveness properties: A survey. Bulletin of the European Association for Theoretical Computer Science, 53, 268–272.
Lamport, L. (1977). Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 3(2), 125–143.
Abrial, J. R. (1996) The B Book. Assigning programs to meanings. Cambridge University Press, Cambridge.
Butler, M., & Yadav, D. (2008). An incremental development of mondex system in Event-B. Formal Aspects of Computing, 20(1), 61–77.
Bodeveix, J. P., Dieumegard, A., & Filali, M. (2020). Event-B formalization of a variability-aware component model patterns framework. Science of Computer Programing, 199, 102511.
Lahbib, A., et al. (2020). An event-B based approach for formal modelling and verification of smart contracts. In International Conference on Advanced Information Networking and Applications. Springer.
Metayer, C., Abrial, J. R., & Voison, L. (2005). Event-B language. RODIN deliverables 3.2, http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf.
Suryavanshi, R., & Yadav, D. (2012). Rigorous design of lazy replication system using Event-B. In International Conference on Contemporary Computing. Springer.
Girish C., & Yadav, D. (2010). Analyzing data flow in trustworthy electronic payment systems using event-B. In International Conference on Data Engineering and Management. Springer.
Yadav, D., & Butler, M. (2009). Formal development of a total order broadcast for distributed transactions using Event-B. Method, Models and Tool for Fault-Tolerance Lecture Notes in Computer Science (LNCS), 5454, 152–176.
Lahouij, A., et al. (2020). An Event-B based approach for cloud composite services verification. Formal Aspects of Computing, 32(4), 361–393.
Yadav, D., & Butler, M. (2006). Rigorous design of fault-tolerant transactions for replicated database systems using Event-B. LNCSIn M. Butler, C. B. Jones, A. Romanovsky, & E. Troubitsyna (Eds.), Fault-Tolerant Systems (Vol. 4157, pp. 343–363). Springer.
B Core UK Ltd. B-Toolkit Manuals (1999)
Steria, Atelier-B User and Reference Manuals (1997)
Abrial, J. R., & Cansell, D. (2003) Click’n’Prove—Interactive Proofs within Set Theory.
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T. S., Mehta, F., & Voisin Rodin, L. (2010). an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer (STTT), 12(6), 447466.
Lamport, L. (1978). Time, clocks, and the ordering of events in a distributed system. Communication, ACM, 21(7), 558–565.
Yadav, D., & Butler, M. (2007). Formal specifications and verification of message ordering properties in a broadcast system using Event-B. In Technical Report. School of Electronics and Computer Science, University of Southampton.
Birman, K., Schiper, A., & Stephenson, P. (1991). Lightweight causal and atomic group multicast. ACM Transactions Computer System, 9(3), 272–314.
Pooja, Y., Suryavanshi, R., Singh, A. K., & Yadav, D. (2019). Formal verification of causal order-based load distribution mechanism using Event-B. Data engineering and applications (pp. 229–241). Springer.
Abrial, J.-R. (1996). Extending B without changing it (for developing distributed systems). In H. Habrias (Ed.), First B Conference.
Yadav, D., & Butler, M. Formal development of broadcast systems and verification of ordering properties using Event-B.
Yadav, D., & Butler, M. (2009). Verification of liveness properties in distributed systems. In International Conference on Contemporary Computing (pp. 625–636). Springer.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Yadav, P., Suryavanshi, R., Yadav, D. (2022). Formal Verification of Liveness Properties in Causal Order Broadcast Systems Using Event-B. In: Gupta, D., Khanna, A., Kansal, V., Fortino, G., Hassanien, A.E. (eds) Proceedings of Second Doctoral Symposium on Computational Intelligence . Advances in Intelligent Systems and Computing, vol 1374. Springer, Singapore. https://doi.org/10.1007/978-981-16-3346-1_16
Download citation
DOI: https://doi.org/10.1007/978-981-16-3346-1_16
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-3345-4
Online ISBN: 978-981-16-3346-1
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)