CFP last date
20 January 2025
Call for Paper
February Edition
IJCA solicits high quality original research papers for the upcoming February edition of the journal. The last date of research paper submission is 20 January 2025

Submit your paper
Know more
The week's pick
Responsive image
SFLA-Based Line Balancing and Task Optimization in Master-Slave Controlled Hanger Transportation Systems for Garment Production

Duc Hoang Nguyen
Random Articles
Reseach Article

Formal Development of Basic Timestamp Concurrency Control Mechanism using Event-B

by Girish Chandra, Divakar Yadav
journal cover thumbnail

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 123 - Number 8
Year of Publication: 2015
Authors: Girish Chandra, Divakar Yadav
10.5120/ijca2015905409

Girish Chandra, Divakar Yadav . Formal Development of Basic Timestamp Concurrency Control Mechanism using Event-B. International Journal of Computer Applications. 123, 8 ( August 2015), 7-11. DOI=10.5120/ijca2015905409

@article{ 10.5120/ijca2015905409,
author = { Girish Chandra, Divakar Yadav },
title = { Formal Development of Basic Timestamp Concurrency Control Mechanism using Event-B },
journal = { International Journal of Computer Applications },
issue_date = { August 2015 },
volume = { 123 },
number = { 8 },
month = { August },
year = { 2015 },
issn = { 0975-8887 },
pages = { 7-11 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume123/number8/21977-2015905409/ },
doi = { 10.5120/ijca2015905409 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T23:12:06.379652+05:30
%A Girish Chandra
%A Divakar Yadav
%T Formal Development of Basic Timestamp Concurrency Control Mechanism using Event-B
%J International Journal of Computer Applications
%@ 0975-8887
%V 123
%N 8
%P 7-11
%D 2015
%I Foundation of Computer Science (FCS), NY, USA
Abstract

Formal methods are mathematical techniques that are used to develop model of complex systems. They provide mathematical proofs for ensuring correctness of model. Through formal methods, it may possible to identify and remove errors at prior stage of development. Event-B is a formal method that is used to develop those systems that can be modeled as discrete transition systems. It rigorously describes the problem and verifies the correctness of model by discharging proof obligations. It performs the consistency checking by preserving invariants of model. In this paper, we have done formal verification of basic time stamp mechanism using Event-B. Basic time stamp is concurrency control mechanism to control concurrent execution of transactions. The main objective of timestamp is to execute transactions such that their execution is equivalent to serial execution in time stamp order.

References
  1. Butler, M. and Maamria, I.. Practical theory extension in Event-B. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Theories of Programming and Formal Methods, volume 8051 of Lecture Notes in Computer Science, pages 6781. Springer, 2013.
  2. Hallerstede, S. and Leuschel, M.: Experiments in program verification using Event-B. Formal Aspects of Computing, 24: pp. 97125, (2012).
  3. Yadav D. and 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).
  4. Butler, M.and Yadav D.: An incremental development of the mondex system in Event-B. Formal Aspects of Computing, 20(1):61-77, (2008).
  5. Banach R.: Retrenchment for Event-B: UseCase-wise development and Rodin integration. Formal Aspects of Computing, 23, pp. 113131, (2011).
  6. Ozsu M. and Valduriez P.: Principles of Distributed Database Systems Pearson Education (Singapore) Pte.Ltd. India (2004).
  7. Bernstein, P. and Goodman, N.: Timestamp Based Algorithms for Concurrency Control in Distributed Database Systems. In: Proc. of 6th Int. Conf. on Very Large Databases (1980).
  8. Bernstein, P., Hadzilacos, V. and Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley (1987).
  9. Suryavanshi, R. and Yadav, D. “Modeling of Multiversion Concurrency Control System Using Event-B” in Federated Conference on Computer Science and Information systems (FedCSIS), indexed and published by IEEE, 9-12 September, Wroclaw, Poland, 2012.
  10. Suryavanshi, R. and Yadav, D. :Formal Development of Byzantine Immune Total Order Broadcast System using Event-B. In: ICDEM 2010, F. Andres and R. Kannan (eds.) LNCS, Vol. 6411, Springer, pp.317-324, (2010).
  11. Yadav, D. and Butler, M.: Formal Development of a Total Order Broadcast for Distributed Transactions Using Event-B. Lecture Notes in Computer Science 5454, springer-Verlag Berlin Heidelberg, pp.152-176, (2009).
  12. Basin, D., Furst, A., Hoang, T.S., Miyazaki, K. and Sato, N. Abstract Data Types in Event-B - An Application of Generic Instantiation. CoRR, 2012.
  13. Metayer, C., Abrial, J R. and Voison L.: Event-B language. RODIN deliverables 3.2, http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf, (2005).
  14. Hallerstede, S.: On the purpose of Event-B proof obligations. FormalAspects of Computing, 23: pp. 133150, (2011).
  15. Abrial, J-R. From Z to B and then Event-B: Assigning Proofs to Meaningful Programs. In E.B. Johnsen and L. Petre, editors, IFM, volume 7940 of Lecture Notes in Computer Science, pages 115. Springer, 2013.
  16. Banach, R.: Retrenchment for Event-B: UseCase-wise development and Rodin integration. Formal Aspects of Computing, 23, pp. 113131, (2011).
  17. Abrial, J R.: A system development process with Event-B and the Rodin platform. In: Lecture Notes In Computer Science 4789, Springer, pp.1-3,(2007).
Index Terms

Computer Science
Information Sciences

Keywords

Formal Methods Formal Specifications Event-B Database Transaction Basic Timestamp Mechanism.

Powered by PhDFocusTM