BAB I PENDAHULUAN BAB I PENDAHULUAN 1.1
Latar Belakang Komunikasi antar komputer memerlukan sebuah protokol. Protokol
merupakan sekumpulan peraturan atau perjanjian untuk menentukan format dan transmisi data. Tujuan utama komunikasi data adalah mengirimkan data dan informasi dari suatu sumber ke tujuan tanpa mengalami kesalahan. Misalnya komunikasi data yaitu mengirim pesan, data, dan fungsi lainya yang harus dipenuhi oleh sisi pengirim (transmitter) dan sisi penerima (receiver) agar komunikasi keduanya benar. Komunikasi antar komputer dengan menggunakan protokol sering dilakukan, namun belum ada pembuktian, apakah protokol yang digunakan sudah tidak terdapat kesalahan (bugs), cacat (defect) dan memenuhi spesifikasi yang dibutuhkan untuk komunikasi data sehingga tidak merugikan pengguna. Kejadian pada tahun 1996, Roket Ariane 5 meledak setelah 40 menit diluncurkan karena cacat (defect) pada Control Software yang mengakibatkan kerugian besar (Baier dan Katoen, 2008). Maka dari itu perlu dilakukan verifikasi protokol yang digunakan untuk menangani kompleksitas, mengurangi jumlah kesalahan (bugs) yang hasilnya dapat mengurangi cost (biaya dan waktu). Pemaparan di atas membuka pandangan betapa pentingnya verifikasi, untuk melakukan verifikasi bisa menggunakan metode formal verification. Verification
membuktikan
bahwa
suatu
implementasi
Formal
betul-betul
mengimplementasikan apa saja yang dijabarkan dalam spesifikasi. Formal Verification dapat dilakukan dengan menggunakan equivalence checking, model checking dan theorem proving. Yang paling umum digunakan adalah model checking, karena dengan metode ini, proses verifikasi dapat dilaksanakan secara otomatis dan memiliki tools supports (Clarke dkk, 1996). SPIN merupakan salah satu tools yang digunakan untuk membuat spesifikasi sistem dan melakukan verifikasi terhadap sistem tersebut (Raharjo, 2002). SPIN cocok digunakan untuk verifikasi protokol karena SPIN menganalisa konsistensi logical pada sistem
1
2
terdistribusi terutama untuk komunikasi data. Selain itu kelebihan dari SPIN adalah kebutuhan komputasionalnya yang relative rendah (Peng dkk, 2000). PROMELA merupakan bahasa pemodelan untuk verifikasi suatu desain dan digunakan sebagai masukan pada tools SPIN. SPIN fokus pada pembuktian kebenaran pada process interaction (Holzmann, 1997). PROMELA dapat memuat tiga tipe objek yaitu processes, variables, dan message channels. Commands Transfer Protocol (CTP) merupakan protokol baru yang dikembangkan oleh
Naumov (2005) yang digunakan untuk menyelesaikan
permasalahan komunikasi parallel networking atau disebut protokol terdistribusi. Protokol ini merupakan protokol yang baru dikembangkan dalam project CAMEL (Cellular Automata Modeling Environment & Library) serta diimplementasikan pada projek CAMEL dan digunakan untuk library pada C++. Karena protokol CTP merupakan protokol baru, maka belum diketahui apakah protokol ini sesuai dengan spesifikasi yang dibuat. Penelitian kali ini membahas mengenai verifikasi protokol CTP yaitu apakah protokol sesuai dengan spesifikasinya. Implementasi protokol CTP dalam bentuk class, di dalam class terdapat beberapa fungsi CTP yang diberi nama CCTPNet
yaitu
:
IPAddr,
SmartBuffer,
NetSender,
NetReceiver,
CCTPReceiverData, CCTPErrorInfo, CCTPNet, CCTPStartusDlg. Requirement dari protokol CTP akan diverifikasi dengan menggunakan SPIN/PROMELA. 1.2 Rumusan Masalah Berdasarkan latar belakang yang telah dipaparkan, maka rumusan masalah dalam penelitian kali ini adalah bagaimana mendefinisikan, memodelkan protokol CTP dalam bahasa PROMELA dan memverifikasi dengan tools model checker SPIN untuk membuktikan apakah protokol CTP memenuhi properti. 1.3 Batasan Masalah
Batasan masalah menjaga agar penelitian tetap fokus. Batasan dalam permasalahan ini antara lain : 1. Penelitian ini fokus pada protokol CTP.
3
2. Sembilan properti yang akan diverifikasi adalah idle, hak tertinggi (precedence), confirm, deadlock, mengosongkan daftar pengiirman, command yang dikirim diterima, transmisi tidak berhasil namun node menerima command, transmisi sukses namun node tidak menerima semua command, dan paralelisme. 3. Arsitektur jaringan komputer yang digunakan adalah cluster networking. 1.4 Keaslian penelitian Berdasarkan studi pustaka yang telah dilakukan, penulis dapat menyatakan bahwa penelitian yang membahas tentang verifikasi protokol CTP menggunakan tools SPIN/PROMELA belum pernah dilakukan. Namun telah dilakukan penelitian sebelumnya mengenai verifikasi protokol dengan menggunakan SPIN/PROMELA yang akan dipaparkan pada tinjauan pustaka. 1.5 Tujuan Penelitian Tujuan dari penelitian ini adalah menerapkan metode formal verification yaitu model checking untuk membuktikan apakah protokol CTP memenuhi spesifikasi. Memodelkan bahaviour protokol CTP menggunakan bahasa PROMELA serta menuliskan properti CTP dalam bahasa LTL (Liniear Temporal Lagic) lalu pemodelan serta LTL tersebut digunakan untuk masukan pada verifier SPIN dan dilakukan verifikasi. 1.6 Manfaat Penelitian Manfaat dari penelitian ini adalah dapat memberikan informasi mengenai verifikasi protokol CTP menggunakan SPIN serta dapat digunakan sebagai penerus untuk penelitian selanjutnya dengan menggunakan metode yang sama untuk memverifikasi berbagai protokol komunikasi. 1.7 Metode Penelitian 1. Studi Literatur Tahap ini dilakukan dengan menelaah sumber-sumber yang tertulis, jurnal, buku teks, e-book, tugas akhir, karya ilmiah lainya yang relevan dengan
4
topik.
Referensi
yang
dibutuhkan adalah
memodelkan protokol
menggunakan SPIN/PROMELA. 2. Analisis Pada tahap ini dilakukan analisa behaviour (perilaku) protokol CTP. Behaviour tersebut digunakan untuk merancang pemodelan. 3. Desain Pada tahapan ini dilakukan perancangan pemodelan yaitu memodelkan behaviour CTP ke dalam diagram activity. Diagram activity memudahkan pemodelan ke dalam bahasa PROMELA. 4. Pemodelan protokol Pada tahap ini akan dimodelkan protokol menggunakan bahasa PROMELA sesuai dengan behaviour dari protokol CTP. Pemodelan tersebut meliputi mtype, message channel, dan proctype (proses). 5. Verifikasi Tahap ini dilakukan verifikasi properti protokol CTP, apakah sesuai dengan requirement protokol CTP. Properti di fomulasikan dalam bahasa LTL (Linear Temporal Logic). Model dan properti protokol menjadi masukan untuk verifier. Proses verifikasi dilakukan secara otomatis pada verifier yaitu SPIN. 6. Kesimpulan Tahap ini akan membahas hasil verifikasi yaitu jumlah transisi state, memori yang digunakan, lama running verifikasi serta satisfy atau tidak. Hasil dari verifikasi protokol dalam memenuhi atau tidak memenuhi properti dijadikan kesimpulan penelitian. 1.8 Sistematika Penulisan Sistematika penulisan dalam penelitian ini terdiri atas : BAB I PENDAHULUAN menjelaskan latar belakang masalah, rumusan masalah, batasan masalah, keaslian penelitian, tujuan penelitian, manfaat penelitian, metodologi penelitian dan sistematika penulisan.
5
BAB II TINJAUAN PUSTAKA menjelaskan penelitian yang telah dilakukan dan memiliki keterkaitan dengan penelitian yang dilakukan. BAB III LANDASAN TEORI menjelaskan berbagai materi yang berhubungan serta diperlukan dalam penelitian, sehingga dapat membantu dalam proses pencapaian hasil penelitian. BAB IV ANALISIS DAN PERANCANGAN SISTEM menjelaskan tentang analisis dari protokol CTP yaitu menganalisis komunikasi, behaviour, message channel serta perancangan komunikasi dalam bentuk sequence chart. Selain itu, pemodelan behaviour dari CTP dijelaskan pada bab ini. BAB V IMPLEMENTASI menjelaskan formalisasi properti dalam LTL (Linear Temporal Logic). Setelah itu melakukan verifikasi berdasarkan requirement protokol CTP. BAB VI HASIL PENELITIAN DAN PEMBAHASAN menjelaskan hasil akhir dari hasil verifikasi disertai penjelasan-penjelasan dari setiap output verifikasi. BAB VII KESIMPULAN DAN SARAN menjelaskan kesimpulan dari hasil penelitian serta saran untuk pengembangan penelitian selanjutnya
