This paper presents liveness properties that need to be preserved by Event-B models of distributed systems. Event-B is a formal technique for development of models of distributed systems related via refinement. In this paper we outline how enabledness preservation and non-divergence are related to the liveness properties of the B models of the distributed systems. We address the liveness issues related to our model of distributed transactions and outline the construction of proof obligations that need to be discharged to ensure liveness. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Yadav, D., & Butler, M. (2009). Verification of liveness properties in distributed systems. In Communications in Computer and Information Science (Vol. 40, pp. 625–636). https://doi.org/10.1007/978-3-642-03547-0_59
Mendeley helps you to discover research relevant for your work.