VERIFIKASI DUA VARIAN PROTOKOL AD HOC ON DEMAND DISTANCE VECTOR DENGAN UPPAAL

Ika Oktavia Suzanti, Dr.-Ing. MHD. Reza M.I. Pulungan, S.Si., M.Sc.

2014 | Tesis | S2 Ilmu Komputer

Mobile Ad hoc Network (MANET) adalah sekumpulan wireless mobile yang terhubung satu sama lain secara dinamis tanpa infrastruktur yang tetap sehingga perubahan topologi dapat terjadi setiap saat. Protokol routing pada MANET memiliki dua model yaitu protokol routing reaktif yang membentuk tabel routing hanya saat dibutuhkan dan protokol routing proaktif yang melakukan pemeliharaan tabel routing secara berkala pada waktu tertentu. Properti umum yang harus dipenuhi oleh protokol jaringan ad-hoc adalah route discovery, packet delivery dan loop fredom. AODV merupakan protokol reaktif pada MANET yang memiliki standar waktu untuk menentukan berapa lama sebuah rute dapat digunakan (route validity) sehingga properti route discovery dan packet delivery harus dapat dipenuhi dalam waktu tertentu yang telah dispesifikasikan. Proses verifikasi protokol dilakukan dengan cara memodelkan spesifikasi protokol menggunakan teknik, tool, dan bahasa yang matematis. Pada penelitian ini bahasa yang digunakan untuk pemodelan protokol adalah timed automata, yaitu bahasa pemodelan yang dapat digunakan untuk memodelkan sistem yang memiliki ketergantungan terhadap waktu tertentu pada setiap prosesnya. Verifikasi dengan timed automata dapat dilakukan secara otomatis dengan mengggunakan tool model checker UPPAAL Protokol yang akan diverifikasi adalah protokol AODV Break Avoidance milik Ali Khosrozadeh dkk dan protokol AODV Reliable Delivery dari Liu Jian dan Li Fang-Min. Hasil dari verifikasi protokol ini membuktikan bahwa protokol AODV Break Avoidance mampu memenuhi properti route discovery dan protokol AODV Reliable Delivery mampu memenuhi properti packet delivery dalam kurun waktu sesuai dengan spesifikasi.

Manet is a group of wireless mobile that connected one to each other dynamically without fixed infrastructure so topology could change at anytime. MANET routing protocol has two models which are reactive routing protocol that built routing table only when needed and proactive routing protocol that maintain routing table periodically. General property which had to be satisfied by ad hoc network protocol are route discovery, packet delivery and loop freedom. AODV is a reactive protocol in MANET that has time standard to determine how long a route is valid to be used (route validity) so route discovery and packet delivery property should be satisfied in a specifically certain time. Protocol verification process done by modeling protocol specification using technique, tool and mathematic language. In this research protocol modeled using timed automata which is a modeling language that could be used to model a time dependent system in each process. Verification using timed automata can automatically done by UPPAAL tool model checker. Protocol which will be verified are AODV Break Avoidance by Ali Khosrozadeh et al. and AODV Reliable Delivery by Liu Jian and Li Fang-Min. Result of this protocol verification prove that AODV BA could satisfied route discovery property and AODV Reliable Delivery could satisfied packet delivery property within their specification time.

Kata Kunci : Verifikasi Protokol, AODV, UPPAAL.