VERIFIKASI PROTOKOL CTP (COMMAND TRANSFER PROTOCOL) MENGGUNAKAN SPIN/PROMELA

ERVIN KUSUMA DEWI, Dr.-Ing. MHD. Reza M.I. Pulungan, S.Si, M.Sc.

2014 | Tesis | S2 Ilmu Komputer

Command Transfer Protocol (CTP) dikembangkan oleh Lev Naumov. CTP dapat digunakan untuk menangani permasalahan pada cluster networking yaitu pertukaran data yang cepat, pertukaran data yang handal, mendukung pertukaran data yang besar dan broadcasting support. Verifikasi CTP dilakukan karena protokol CTP merupakan protokol baru, maka belum diketahui apakah protokol ini sesuai dengan spesifikasi yang dibuat. Penelitian ini membahas mengenai verifikasi protokol apakah protokol CTP sesuai dengan spesifikasinya. Proses verifikasi protokol dilakukan dengan cara memodelkan spesifikasi protokol menggunakan teknik, tools, dan bahasa yang matematis. Tools yang digunakan adalah model checker SPIN. SPIN cocok digunakan untuk verifikasi protokol karena SPIN menganalisa konsistensi logical pada sistem terdistribusi terutama untuk komunikasi data. Bahasa yang digunakan untuk pemodelan adalah PROMELA, yaitu bahasa pemodelan yang dapat digunakan untuk memodelkan sistem dan digunakan sebagai inputan pada SPIN. Hasil verifikasi protokol CTP menunjukkan bahwa sembilan properti yang dilakukan pengecekan adalah satisfy. Hasil percobaan dengan menggunakan jumlah 4, 7, 10 sampai 20 node tidak ditemukan error artinya dengan jumlah node yang berbeda properti CTP tetap satisfy. Kata Kunci : SPIN/PROMELA, Model Checking, Formal Method, Protokol.

Command Transfer Protocol (CTP) is developed by Lev Naumov. CTP can be used for handle problem on cluster networking those are rapid data interchange, reliable data interchange, huge data block interchange support, broadcasting support. To do verification CTP because CTP is new protocol, so that every one did not know protocol can be satisfaction specification protocol CTP. Discuses in this research is verification protocol CTP, what is protocol can be satisfied specification. Protocol verification process done by modeling protocol specification using technique, tools and mathematic logic. Tools used is the model checker SPIN. SPIN suitable for protocol verification because SPIN analyzing the logical consistency of a distributed system, especially for data communication. The language protocol modeling using PROMELA which is a modeling language that can be used to model the system and used as input to the SPIN Result of protocol verification so that nine property is satisfied. Result experiment using 4, 7, 10 and 20 nodes show no error, which mean using many different nodes the CTP property is satisfied. Keywords: SPIN/PROMELA, Model Checking, Formal Method, Protocol

Kata Kunci : SPIN/PROMELA, Model Checking, Formal Method, Protokol.