doi: 10.7763/IJIET.2012.V2.86
Modeling and Verification of Deadlock Potentials of a Concurrency Control Mechanism in Distributed Databases Using Hierarchical Colored Petri Net
Saeid Pashazadeh
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.
Keywords
- Colored Petri net
- concurrency control mechanism
- verification
- two phase locking
- state space analysis
How to 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. https://doi.org/10.7763/IJIET.2012.V2.86
Copyright & License
Copyright © 2012 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).