Path: Top > S1-Final Project > Electrical Engineering-STEI > 2008

PERANCANGAN DAN ANALISIS PROTOKOL MOBILE PAYMENT SYSTEM YANG MEMPERTIMBANGKAN FAKTOR NETWORK DENGAN SPIN MODEL CHECKER

Undergraduate Theses from JBPTITBPP / 2017-09-27 10:18:44
Oleh : MUHAMMAD HALIM ALFATH PRAMONO (NIM 13203140), Central Library Institute Technology Bandung
Dibuat : 2008, dengan 8 file

Keyword : Telepon genggam, Mobile payment system, Protokol, SPIN model checker, PROMELA, Delay, Message lost, Correctness properties, Claim transaction properties, Platform, Network

Pada penelitian sebelumnya yang telah dilakukan oleh saudara Mirza Azhari [11], telah terancang sebuah protokol mobile payment system yang terbukti memenuhi klaim atomicity, effectiveness, dan non-repudiation. Namun dalam prosesnya, protokol tersebut tidak memperhatikan keadaan network yang menjadi tempat berlangsungnya proses komunikasi pada protokol mobile payment system tersebut.




Pada Tugas Akhir ini penulis menganalisis pengaruh faktor-faktor network seperti delay dan message lost pada protokol mobile payment system hasil penelitian sebelumnya [11]. Penulis kemudian mengembangkan protokol yang sudah ada tersebut dengan memasukkan unsur network dalam prosesnya. Protokol hasil pengembangan tersebut kemudian disimulasikan dan diverifikasi dengan menggunakan program SPIN model checker.




Untuk bisa dijalankan pada program SPIN, model protokol dituliskan dahulu ke bahasa PROMELA (Process Meta Language). Bentuk bahasa PROMELA dari protokol kemudian dapat disimulasikan dan diverifikasi oleh SPIN. Hasil simulasi protokol dianalisis dengan menyesuaikan pada bentuk rancangan secara umum. Kemudian program SPIN memverifikasi Correctness properties dan Claim Transaction properties pada protokol yang bersangkutan.




Dari hasil simulasi dan verifikasi, protokol yang telah dikembangkan terbukti memenuhi klaim atomicity dan non-repudiation.

Deskripsi Alternatif :

On the previous research written by Mirza Azhari [11], several Mobile Payment Protocols have been designed. These protocols have proven Atomicity, Effectiveness, and Non-Repudiation Claims. But these protocols did not consider network factor in its process.




In this final project, the effects of network factors (delay and message lost) on previous protocol [11] are analyzed. Then protocols that consider network factor are developed. The new protocols that have been developed by concerning network factors are then simulated and verificated by using SPIN model checker program.




To run the model protocol in the SPIN program, the model protocol have to be written in PROMELA language. After that the simulations result from SPIN are then compared with the protocol design. The next step is to verificate correctness and claim transaction properties with the SPIN verification tools. As the result the new developed protocols are proven to be Atomic and Non repudiate.

Copyrights : Copyright Â(c) 2001 by ITB Central Library. Verbatim copying and distribution of this entire article is permitted by author in any medium, provided this notice is preserved.

Beri Komentar ?#(0) | Bookmark

PropertiNilai Properti
ID PublisherJBPTITBPP
OrganisasiC
Nama KontakUPT Perpustakaan ITB
AlamatJl. Ganesha 10
KotaBandung
DaerahJawa Barat
NegaraIndonesia
Telepon62-22-2509118, 2500089
Fax62-22-2500089
E-mail Administratordigilib@lib.itb.ac.id
E-mail CKOinfo@lib.itb.ac.id