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

ERVIN KUSUMA DEWI, Reza M.I. Pulungan

2014 | Disertasi | PROGRAM STUDI S2 ILMU KOMPUTER

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

Kata Kunci : SPIN/PROMELA; Model Checking; Formal Method; Protokol