FORMAL VERIFICATION OF AN ACCESS CONCURRENCY CONTROL ALGORITHM FOR TRANSACTION TIME RELATIONS

Achraf Makni, Rafik Bouaziz, Faïez Gargouri

2006

Abstract

We propose in this paper to formally check the access concurrency control algorithm proposed in (Bouaziz, 2005). This algorithm is based on the optimistic approach and guarantees strong consistency for the transaction time relations. The specification of our model under PROMELA language allowed us to ensure the feasibility of the validation. We then could, using the SPIN model checkers, avoid errors of blocking type and check safety properties specified by temporal logic formulas.

Paper Citation

in Harvard Style

Makni A., Bouaziz R. and Gargouri F. (2006). FORMAL VERIFICATION OF AN ACCESS CONCURRENCY CONTROL ALGORITHM FOR TRANSACTION TIME RELATIONS . In Proceedings of the Eighth International Conference on Enterprise Information Systems - Volume 1: ICEIS, ISBN 978-972-8865-41-2, pages 269-272. DOI: 10.5220/0002487602690272

in Bibtex Style

@conference{iceis06,
author={Achraf Makni and Rafik Bouaziz and Faïez Gargouri},
title={FORMAL VERIFICATION OF AN ACCESS CONCURRENCY CONTROL ALGORITHM FOR TRANSACTION TIME RELATIONS},
booktitle={Proceedings of the Eighth International Conference on Enterprise Information Systems - Volume 1: ICEIS,},
year={2006},
pages={269-272},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002487602690272},
isbn={978-972-8865-41-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the Eighth International Conference on Enterprise Information Systems - Volume 1: ICEIS,
TI - FORMAL VERIFICATION OF AN ACCESS CONCURRENCY CONTROL ALGORITHM FOR TRANSACTION TIME RELATIONS
SN - 978-972-8865-41-2
AU - Makni A.
AU - Bouaziz R.
AU - Gargouri F.
PY - 2006
SP - 269
EP - 272
DO - 10.5220/0002487602690272