Abstract—Formal methods are widely used for studying and verifying characteristics of concurrency control mechanisms (CCMs) and protocols in distributed databases. Colored Petri net (CPN) has high modeling capabilities and is one of the best methods for formal analysis and verification of CCMs. In this paper, a novel model of CCM based on two phase locking (2PL) using CPN has presented. State space analysis of model permits us to prove that all schedules of concurrent execution of transactions using 2PL in a case study is deadlock free nor not. Then a simple case study along with its state space analysis has presented. Results show that CPN is proper method for modeling CCM using 2PL and proving deadlock freeness property of all schedules of transactions.
Index Terms—Colored Petri net, concurrency control mechanism, verification, two phase locking, state space analysis
Saeid Pashazadeh is with the Department at Faculty of Electrical and Computer Engineering in University of Tabriz in Iran (e-mail: s_pashazadeh@yahoo.com).
Cite: Saeid Pashazadeh, "Modeling and Verification of Deadlock Potentials of a Concurrency Control Mechanism in Distributed Databases Using Hierarchical Colored Petri Net," International Journal of Information and Education Technology vol. 2, no. 2, pp. 77-82, 2012.