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

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.

Authors:

• Rafat Alshorman
• Walter Hussak

Keywords:

• Multi-step transactions
• LTL specifications
• Model Checking.

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.