Verifikasi Dua Varian Protokol Ad hoc On demand Distance Vector dengan UPPAAL
Abstrak: Mobile Ad-hoc Network
(MANET) adalah sekumpulan wireless mobile yang terhubung satu sama lain tanpa
infrastruktur yang tetap sehingga perubahan topologi dapat terjadi setiap saat.
Protokol routing 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. Properti umum yang harus
dipenuhi oleh protokol jaringan ad-hoc adalah route discovery, packet delivery
dan loop fredom.
AODV merupakan protokol reaktif MANET yang memiliki standar waktu berapa
lama sebuah rute dapat digunakan (route validity), sehingga properti route
discovery dan packet delivery harus dapat dipenuhi dalam waktu tersebut. Proses
verifikasi protokol dilakukan dengan memodelkan spesifikasi protokol
menggunakan teknik, tool, dan bahasa matematis.
Pada penelitian ini bahasa pemodelan yang digunakan adalah timed
automata, yaitu bahasa pemodelan untuk memodelkan sistem yang memiliki
ketergantungan terhadap waktu tertentu pada setiap prosesnya. Verifikasi
protokol dilakukan secara otomatis dengan mengggunakan tool model checker
UPPAAL.
Protokol yang diverifikasi adalah protokol AODV Break Avoidance milik Ali
Khosrozadeh dkk dan protokol AODV Reliable Delivery dari Liu-Jian dan Fang-Min.
Hasil verifikasi protokol membuktikan bahwa protokol AODV Break Avoidance mampu
memenuhi properti route discovery dan protokol AODV Reliable Delivery mampu
memenuhi properti packet delivery dalam waktu sesuai dengan spesifikasi.
Penulis: Ika Oktavia Suzanti,
M. Reza M.I. Pulungan
Kode Jurnal: jptinformatikadd150274
