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

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