Modeling Timestamp Ordering Method Using Colored Petri Net

Concurrency control methods are designed for preserving consistency of database systems when several concurrent transactions are running. Various concurrency control methods were developed that each one is appropriate for special applications and cases. One of the most common methods that guarantee serializability is timestamp ordering method (TO). This method is one of the timestamp-based methods. Conflicting read and write operations are executed such that scheduling of transactions be equivalent with serial schedule that transactions with lower time stamp precedes transactions with higher time stamp. TO is one of the widely used concurrency control mechanisms. This paper presents a hierarchical colored Petri net model of TO that can be used for formal verification of this algorithm. This model can be used as an important component in modeling and verification of database systems.