FORMAL VERIFICATION OF A NEW OPTIMISTIC CONCURRENCY CONTROL ALGORITHM FOR TEMPORAL DATABASES
Achraf Makni, Rafik Bouaziz, Faı̈ez Gargouri · 2007
Most of the concurrency control (CC) studies in the temporal database areas were carried out according to the pessimistic approach ([7][8][9]). To our knowledge, OCCA_SC/TTR [5] and OCCA_SC/VTR [15] algorithms, which ensure the strong consistency for transaction time relations and for valid time relations, respectively, are the only ones which adopt the optimistic approach. We propose in this paper a new optimistic CC algorithm intended for any type of temporal relations. This algorithm is limited to guarantee the consistency, knowing that many applications do not require the strong consistency. To be able to detect all the conflict and operation failure cases, we propose to maintain for each transaction, not only one writing set, but rather three sets, respectively relating to the granules of the insert, update and delete operations. In addition, to avoid the risk of false conflict detection, we use the new type of granule, defined as a temporal interval during which one or more tuples are valid [15]. As for its validation, it is achieved first under a theoretical formalism, then under the SPIN model checker. Errors of blocking type are then avoided and safety property, specified by a temporal logic formula, is guaranteed. 1