文章基本信息

标题：Modeling and Verification of Payment System in E-Banking
本地全文：下载
作者：Iqra Obaid ; Syed Asad Raza Kazmi ; Awais Qasim 等
期刊名称：International Journal of Advanced Computer Science and Applications(IJACSA)
印刷版ISSN：2158-107X
电子版ISSN：2156-5570
出版年度：2017
卷号：8
期号：8
DOI：10.14569/IJACSA.2017.080825
出版社：Science and Information Society (SAI)
摘要：Formal modeling and verification techniques have been used to ensure the reliability and accuracy of multiple systems to be verified. In contrast to ordinary testing techniques which exhibit the presence of flaws and errors in a system, formal methods prove their absence. Electronic banking (e-banking) services have become very popular with the escalating development in the information and communication technology. Due to the presence of complexity, an e-banking system requires an efficient security model. One important approach to ensure the reliability and security of the e-banking system is through the use of formal methodologies. This study explores the opportunity of modeling interbank payment system through a case study of 1-link Automated Teller Machine (ATM). A generic verification system SPIN (Simple Promela Interpreter) is, therefore, employed to model and then to verify the integrity and security of payment system in e-banking. Linear temporal logic formulas are further summarized to assure the security of the e-banking system. The principal conclusion of the work includes a complete procedure of verification and modeling of the payment system in 1-link ATMs.
关键词：E-banking; model checking; Simple Promela Interpreter (SPIN); formal methods; Linear Temporal Logic (LTL) formula; Promela introduction