Abstract
System availability is improved by the replication of data objects in a distributed database system. However, during updates, the complexity of keeping replicas identical arises due to failures of sites and race conditions among conflicting transactions. Fault tolerance and reliability are key issues to be addressed in the design and architecture of these systems. Event B is a formal technique which provides a framework for developing mathematical models of distributed systems by rigorous description of the problem, gradually introducing solutions in refinement steps, and verification of solutions by discharge of proof obligations. In this paper, we present a formal development of a distributed system using Event B that ensures atomic commitment of distributed transactions consisting of communicating transaction components at participating sites. This formal approach carries the development of the system from an initial abstract specification of transactional updates on a one copy database to a detailed design containing replicated databases in refinement. Through refinement we verify that the design of the replicated database confirms to the one copy database abstraction.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.R.: The B Book: Assigning Programs to Meaning. Cambridge University Press, Cambridge (1996)
Abrial, J.R.: Extending B without changing it. (For Distributed System). In: Proc. of 1st Conf. on B Method, pp. 169–191 (1996)
Abrial, J.R., Cansell, D., Mery, D.: A Mechanically Proved and Incremetal development of IEEE1394 Tree Identify Protocol. Formal Aspect of Computing 14, 215–227 (2003)
Abrial, J.R., Cansell, D.: Click’n’Prove - Interactive Proofs within Set Theory (2003)
Agrawal, D., Alonso, G., Stanoi, I.: Exploiting Atomic Broadcast in Replicated Database. In: Proc. of Europar 1997 (1997)
Babaoglu, O., Bartoli, A., Dini, G.: Replicated file management in large scale distributed system. In: Tel, G., Vitányi, P.M.B. (eds.) WDAG 1994. LNCS, vol. 857, pp. 1–16. Springer, Heidelberg (1994)
Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database System. Addison-Wesley, Reading (1987)
Birman, K.P., Schiper, A., Stephenson, P.: Lighweight causal and atomic group multicast. ACM Transaction on Computer System 9(3), 272–314 (1991)
Butler, M.: On the use of Data Refinement in the Development of Secure Communications Systems. Formal Aspects of Computing 14, 2–34 (2002)
Butler, M.: An Approach to Design of Distributed Systems with B AMN. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)
Butler, M., Walden, M.: Distributed System Development in B. In: Proc. of Ist Conf. in B Method, Nantes, pp. 155–168 (1996)
Cansell, D., Mery, D.: Foundations of B Method. Computing and Informatics 22, 1–31 (2003)
B Core UK Ltd. B-Toolkit Manuals (1999)
Ekwall, R., Schiper, A.: Replication: Understanding the advantage of atomic broadcast over quorum systems. Journal of Universal Computer Science 11(5), 703–711 (2005)
Fekete, A., Frans Kaashoek, M., Lynch, N.: Implementing Sequentially Consistent Shared Objects using Broadcast and Point-To-Point Communication. Journal of the ACM 45(1), 35–69 (1998)
Gray, J., Reuter, A.: Transaction Processing: Concepts and Technique. Morgan Kaufmann, San Francisco (1993)
Holliday, J.: Replicated Database Recovery using Multicast Communication. In: IEEE Intl. Symposium on Network Computing and Application, NCA 2001, pp. 104–107 (2001)
Kemme, B., Alonso, G.: A New Approach to developing and implementing eager database replication protocols. ACM Transaction on Database System 25(3), 333–379 (2000)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Melliar, P., Amir, Y., Moser, L., Agrawala, V.: Broadcast protocols for Distributed Systems. IEEE Transactions on Parallel and Distributed System 1(1), 17–25 (1990)
Metayer, C., Abrial, J.R., Voisin, L.: Event-B Language, RODIN Deliverables 3.2 (2005), http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf
Moser, L., Mellier, P., Agrawal, D., Budhia, R., Papadopoulos, C.: TOTEM: A fault tolerant multicast group communication. Communication of ACM 39(4), 54–63 (1996)
Ozsu, M.T., Valduriez, P.: Principles of Distribted Database Systems. Prentice-Hall, Englewood Cliffs (1999)
Rezazadeh, A., Butler, M.: Some Guidelines for Formal Development of Web-Based Applications in B-Method. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 472–492. Springer, Heidelberg (2005)
Patino-Martinez, M., Jimenez-Peris, R., Kemme, B., Alonso, G.: Consistent Database Replication at the Middleware Level. ACM Transactions on Computer Systems (TOCS) 23(4), 375–423 (2005)
Silaghi, B., Keleher, P., Bhattacharjee, B.: Multi-Dimensional Quorum Sets for Red-Few Write-Many Replica Control Protocols. In: Proc. of the 4th CCGRID/GP2PC, Chicago, IL (April 2004)
Schneider, S.: The B-Method. Palgrave Publications (2001)
Silberschatz, A., Korth, H., Sudarshan, S.: Database System Concepts. McGraw-Hill, New York (2001)
Stanoi, I., Agrawal, D., El Abbadi, A.: Using Broadbast Primitives in Replicated Data. In: Proceddings of 18th IEEE Intl. Conf. on Distributed Computing System, ICDCS 1998, pp. 148–155 (1998)
Steria- Atelier-B User and Reference Manuals (1997)
Yadav, D., Butler, M.: Application of Event B to Global Causal Ordering for Fault Tolerant Transactions. In: Proc. of REFT 2005, Newcastle upon Tyne, pp. 93–103 (2005), http://eprints.ecs.soton.ac.uk/10981/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Yadav, D., Butler, M. (2006). Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems Using Event B. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds) Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol 4157. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916246_18
Download citation
DOI: https://doi.org/10.1007/11916246_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48265-9
Online ISBN: 978-3-540-48267-3
eBook Packages: Computer ScienceComputer Science (R0)
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.