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

Girish Chandra | Zendy; Divakar Yadav | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Girish Chandra,

Divakar Yadav

Publication year - 2015

Publication title -

international journal of computer applications

Language(s) - English

Resource type - Journals

ISSN - 0975-8887

DOI - 10.5120/ijca2015905409

Subject(s) - computer science , timestamp , timestamp based concurrency control , concurrency control , concurrency , event (particle physics) , mechanism (biology) , programming language , computer security , distributed concurrency control , database transaction , physics , quantum mechanics , philosophy , epistemology

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research