Specifying a Timestamp-based Protocol For Multi-step Transactions Using LTL

Authors: Rafat Alshorman, Walter Hussak

Abstract:

Most of the concurrent transactional protocols consider serializability as a correctness criterion of the transactions execution. Usually, the proof of the serializability relies on mathematical proofs for a fixed finite number of transactions. In this paper, we introduce a protocol to deal with an infinite number of transactions which are iterated infinitely often. We specify serializability of the transactions and the protocol using a specification language based on temporal logics. It is worthwhile using temporal logics such as LTL (Lineartime Temporal Logic) to specify transactions, to gain full automatic verification by using model checkers.

Keywords: Multi-step transactions, LTL specifications, Model Checking.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1058901

References:

[1] R. Alshorman and W. Hussak, A Serializability Condition for Multi-step Transactions Accessing Ordered Data, International Journal of Computer Science, Vol. 4, issue 1 (2009), pp. 13-20.
[2] R. Alshorman and W. Hussak, A CTL Specification of Serializability for Transactions Accessing Uniform Data, International Journal of Computer Science and Engineering , Vol. 3, issue 1 (2009), pp. 26-32.
[3] Skype Web site, http://www.skype.com
[4] Skype Heartbeats Archives, http://heartbeat.skype.com/2007/08/
[5] D. Rossi, M. Mellia and M. Meo, Evidences Behind Skype Outage, In proceedings of the IEEE International Conference on Communication (ICC-09), Dresde, Germany, June 2009, Link: http://www.tlcnetworks. polito.it/mellia/papers/Skype outage icc09.pdf
[6] A. Cimatti, E. Clarke, F. Giunchiglia and M. Roveri, NuSMV: a new symbolic model verifier, In proceedings of the 11th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1633, 1999, pp. 495-499.
[7] NuSMV v2.4 Tutorial, http://nusmv.fbk.eu/NuSMV/tutorial/v24/tutorial.pdf, NuSMV website.
[8] A. Cimatti, E. Clarke, F. Giunchiglia and M. Roveri, NuSMV: a new symbolic model verifier, In proceedings of the 11th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1633, 1999, pp. 495-499.
[9] NuSMV v2.4 Tutorial, http://nusmv.fbk.eu/NuSMV/tutorial/v24/tutorial.pdf, NuSMV website.
[10] R. Elmasri, S. Navathe, Fundamental of Database Systems, Addison- Wesley, Fourth Edition, 2004.
[11] S. Gnesi, Formal Specification and Verification of Complex Systems, Electronic Notes in Theoretical Computer Science Netherlands, Vol. 80, 2003, pp. 294-298.
[12] W-C. Peng and M-S. Chen, Mining user moving patterns for personal data allocation in a mobile computing system, In IEEE proceedings of 29th International Conference on Parallel Processing, 2000, pp. 573580.
[13] Z. Manna and A. Pnueli, Temporal verification of reactive systems: Safety, Springer-Verlag N.Y. Inc., 1995.
[14] K. Sen, G. Rosu and G. Agha, Generating Optimal Linear Temporal Logic Monitors by Coinduction, In proceedings of 8th Asian Computing Science Conference (ASIAN03), Lecture Notes in Computer Science, Springer-Verlag, Vol. 2896, 2003, pp. 260-275.
[15] V.C.S. Lee, K-W. Lam, S.H. Son and E.Y.M. Chan, On transaction processing with partial validation and timestamp ordering in mobile broadcast environments, IEEE Transactions on Computers, Vol. 51, issue 10 (2002), pp. 1196-1211.
[16] R. Alshorman and W. Hussak, Multi-step transactions specification and verification in a mobile database community, In proceedings of 3rd IEEE International Conference on Information Technologies: from Theory to Applications, IEEE, ICTTA 08, Damacus, Syria, IEEE Computer Society Press, 2008, pp. 1407-12.
[17] R. Pucella, The finite and the infinite in temporal logic, ACM SIGACT News, Vol. 36, issue 1 (2005), pp. 86-99.