|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
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
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.