Verification of Liveness Properties in Distributed Systems

Abstract. 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. Key words: Formal Methods, Distributed Systems, Event-B, Liveness Properties

• Type: Journal
• Year: 2009
• Where: IC3
• Authors: Divakar Yadav, Michael Butler
• Keywords: Applied Computing, Distributed Systems, IC3 2009, Liveness Properties, Paper