Modeling Basic Two Phase Locking Distributed Database Concurrency Control Algorithm Using Rebeca

Concurrency control algorithms in distributed database systems are one of the main parts of a distributed DBMS. Designing an efficient and reliable distributed concurrency control algorithm is very important in designing of distributed database system. Nowadays, model checking of reactive systems is an important aspect of designing a reliable system. It provides a series of defined features and guarantees some of system properties. In this paper, we are going to model one of the most important concurrency control algorithms called Basic Two Phase locking algorithm with Rebeca modeling language to validate its properties. We also show that Rebeca is suitable for modeling a concurrency control algorithm and it is not as complicated as proof theory approach. Through this work, we do model checking by abstracting from some of design points that in our opinion doesn’t affect final results. This way, we recognize visible variables as output of system. Model checking will show system’s reduced behavior.

Keywords:

Distributed Database Concurrency Control Algorithm , Model Checking , Modeling Language , and Rebeca