International Journal of Information Technology and Computer Science (IJITCS)
IJITCS Vol. 7, No. 5, 8 Apr. 2015
Cover page and Table of Contents: PDF (size: 458KB)
Temporal Logics Specifications for Debit and Credit Transactions
Full Text (PDF, 458KB), PP.10-17
Views: 0 Downloads: 0
Author(s)
Index Terms
Debit And Credit Transactions, Temporal Logics Specifications, Model Checking, Serializability of Transactions
Abstract
Recently, with the emergence of mobile technology and mobile banking, debit and credit transactions have been the most common transactions that are widely spreading, using such technologies. In this research, we specify the concurrent debit and credit transactions in temporal logics such as CTL (Computational Tree Logic) and LTL (Linear-Time Temporal Logic). These specifications describe the infinite histories that may be produced by the iterations of such concurrent transactions infinitely many times. We represent the infinite histories as a model of temporal logics formulae. Then, model checkers, such as NuSMV or SPIN, can carry out exhaustive checks of the correctness of the concurrent debit and credit transactions. Moreover, in this paper, we presume that the serializability condition is too strict. Therefore, a relaxed condition has been suggested to keep the database consistent. Moreover, the relaxed condition is easier to encode into temporal logics formulae.
Cite This Paper
Rafat M. Alshorman, "Temporal Logics Specifications for Debit and Credit Transactions", International Journal of Information Technology and Computer Science(IJITCS), vol.7, no.5, pp.10-17, 2015. DOI:10.5815/ijitcs.2015.05.02
Reference
[1]L. Lamport, Secefying systems, the TLA+ language and tools for hardware and software engineers, Microsoft Research. Addison-Wesley, 2002.
[2]S. Gnesi, “Formal Specification and Verification of Complex Systems”, Electronic Notes in Theoretical Computer Science Netherlands, Vol. 80, pp. 294-298, 2003.
[3]Z. Manna and A. Pnueli, “Temporal verification of reactive systems: Safety”, Springer-Verlag N.Y. Inc., 1995.
[4]R. Alshorman and W. Hussak, “A CTL Specification of Serializability for Transactions Accessing Uniform Data”, International Journal of Computer Science and Engineering, Vol. 3, No. 1, pp. 26-32, 2009.
[5]Skype Heartbeats Archives, http://heartbeat.skype.com/2007/08/.
[6]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.tlc-networks.polito.it/mellia/papers/Skype_outage_icc09.pdf
[7]“NuSMV v2.4 Tutorial”, NuSMV website. Link: http://nusmv.fbk.eu/NuSMV/tutorial/v24/tutorial.pdf
[8]Skype Web site, http://www.skype.com
[9]R. Alshorman and W. Hussak, “A Serializability Condition for Multi-step Transactions Accessing Ordered Data”, International Journal of Computer Science, Vol. 4, No. 1, pp. 13-20, 2009.
[10]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, pp. 495-499, 1999.
[11]W. Hussak and J.A. Keane, “Algebraic Specification of Serializability for Partitioned Transactions”, International Journal of Computer Systems Science and Engineering, Vol.1, No.1, pp. 60-67, 2007.
[12]W. Hussak, "Serializable Histories in Quantified Propositional Temporal Logic", International Journal of Computer Mathematics, Vol. 81, No. 10, pp. 1203-1211, 2004.
[13]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, pp. 1407-12, 2008.
[14]C.H. Papadimitriou, “The theory of database concurrency control”. Computer Science Press, Pockville, Maryland, 1986.
[15]R. Elmasri, S. Navathe, “Fundamental of Database Systems”, Addison-Wesley, Fourth Edition, 2004.
[16]“Mobile Payments: Three Winning Strategies for Banks,” Swift White Paper, 2012.
[17]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, No. 10, pp. 1196-1211, 2002.
[18]Ph. Schnoebelen, the complexity of temporal logic model checking, In AiML, 2002.
[19]R. Pucella, “The finite and the infinite in temporal logic”, ACM SIGACT News, Vol. 36, No. 1, pp. 86-99, 2005.
[20]K. Sen, G. Rosu and G. Agha, “Generating Optimal Linear Temporal Logic Monitors by Coinduction”, In proceedings of 8th Asian Computing Science Conference (ASIAN’03), Lecture Notes in Computer Science, Springer-Verlag, Vol. 2896, pp. 260-275, 2003.
[21]S. Koussoube, R. Noussi and B. O.Konfe ,” A Formal Description of Problem Frames”, International Journal of Information Technology and Computer Science, Vol. 6, No. 4, pp. PP.56-65, 2014. DOI: 10.5815/ijitcs.2014.04.07.