This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06)
Formal Verification of an Optimistic Concurrency Control Algorithm using SPIN
Budapest, Hungary
June 15-June 17
ISBN: 0-7695-2617-9
ASCII Text
x 
 
Achraf Makni, Rafik Bouaziz, Faiez Gargouri, "Formal Verification of an Optimistic Concurrency Control Algorithm using SPIN," Temporal Representation and Reasoning, International Syposium on, pp. 160-167, Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/TIME.2006.15,
author = {Achraf Makni and Rafik Bouaziz and Faiez Gargouri},
title = {Formal Verification of an Optimistic Concurrency Control Algorithm using SPIN},
journal ={Temporal Representation and Reasoning, International Syposium on},
volume = {0},
year = {2006},
issn = {1530-1311},
pages = {160-167},
doi = {http://doi.ieeecomputersociety.org/10.1109/TIME.2006.15},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Temporal Representation and Reasoning, International Syposium on
TI - Formal Verification of an Optimistic Concurrency Control Algorithm using SPIN
SN - 1530-1311
SP160
EP167
A1 - Achraf Makni,
A1 - Rafik Bouaziz,
A1 - Faiez Gargouri,
PY - 2006
KW - null
VL - 0
JA - Temporal Representation and Reasoning, International Syposium on
ER -
 
Achraf Makni, Economiques et de Gestion de Sfax, Tunisia
Rafik Bouaziz, Economiques et de Gestion de Sfax, Tunisia
Faiez Gargouri, Multim?dia de Sfax, Tunisia
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 in [4], 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.
Citation:
Achraf Makni, Rafik Bouaziz, Faiez Gargouri, "Formal Verification of an Optimistic Concurrency Control Algorithm using SPIN," time, pp.160-167, Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.