Formal Development and Verification of Quorum Based Static Voting Replica Control Protocol Using Event-B

Abstract

 Modelling is imperative for the development of complex systems. Formal modelling of complex systems is a difficult task. Data replication improves availability of data in distributed environment on same time maintaining consistency is a challenging issue. Majority based replica control protocol is used to maintain consistency but if half of the sites are unavailable due to  network partitioning or any failure reason, system will not proceed further. Quorum based static voting replica control protocol is one solution in which even half of the sites are not available but most promising sites on which the frequency of transaction is high are available then system allows to execute if quorum test succeeds. We are using formal methods to define the system using mathematical notations. Event-B is a formal method, which is based upon event driven approach. Event-B is used to develop a model in distributed environment. In this paper, we have done formal development and verification of quorum based static voting replica control protocol using Event-B.