Formal Verification of an Optimistic Concurrency Control Algorithm using SPIN

To contribute to the promotion of concurrency controllers for temporal databases, we propose in this paper to formally check the access concurrency control algorithm proposed using SPIN. This algorithm is based on the optimistic approach and must guarantee strong consistency for transaction time relations. SPIN provides a software model checking with a powerful tool to detect errors. It is an appropriate tool for analyzing the logical consistency of concurrent systems. The main target consists of retrieving and correcting blocking error type, on the one hand, and ensuring the validity of the considered system properties specified by temporal logic formulae, on the other hand