Rigorous Design of Lazy Replication System Using Event-B

Eager replication is a technique of replication that ensures high consistency. Unfortunately, it degrades the system performance by increasing the response time and sacrificing availability. Lazy replication is a technique that provides high availability and ensures that database will eventually be in a consistent state. A formal rigorous reasoning is required to precisely understand the behavior of such techniques and to understand how they achieve the objectives. Event-B is a formal technique that is used for specifying and reasoning about complex systems. In this paper, we present a formal development of lazy replication system using Event-B. We outline our model for distributed environment where same database is replicated at all the sites. After updating the database locally within transactional framework messages are broadcast to other sites so that they can change their replicas.