JURNAL : Pemodelan dan Verifikasi Formal Pengaruh Mobility pattern Terhadap Handoff Latency pada Jaringan WiMAX

ABSTRAK - Untuk mengurangi handoff latency dan meningkatkan keberhasilan dari skema HHO konvensional, dilakukan pengembangan skema handover pada standard protokol WiMAX IEEE 802.16e dengan menambahkan mobility pattern. Keunggulan skema handover dengan mobility pattern adalah mengurangi handoff latency hingga 50%, sedangkan kelemahannya sering terjadi kesalahan dalam penentuan Target base station. Verifikasi formal dilakukan untuk mengetahui kelemahan tersebut. Skema handover dimodelkan dengan continuous-time Markov chain (CTMC). Model difokuskan untuk memperkirakan pengaruh algoritma mobility pattern terhadap handoff latency dari mekanisme Hard Handover WiMAX. Langkah-langkah untuk membangun model sebagai berikut: Mereprensentasikan state space, memberikan penomoran pada semua, menggenerasikan rate transisi matriks (infinitesimal generator). Kemudian model yang dibentuk dituangkan pada tool PRISM, untuk dilakukan verifikasi formal. Probabilistic model checking pada penelitian melakukan pendekatan kuantitatif (qunatitative properties) dan kualitatif (qualitative properties). Verifikasi formal terhadap properti-properti yang berkaitan dengan handover pada jaringan WiMAX menunjukkan bahwa 70% dari MS yang melakukan scanning dengan mobility pattern sukses melakukan handover, 24 % diantaranya melakukan scanning konvensional akibat kesalahan dalam penentuan TBS sehingga handoff latency yang dihasilkan lebih besar jika dibandingkan dengan sistem yang hanya menggunakan metode scanning konvensional.

Kata kunci— WiMAX, handover, mobility pattern, CTMC, PRISM, handoff latency

PENDAHULUAN - alam suatu jaringan yang mendukung mobilitas, aspek penting yang perlu diperhatikan adalah handover, yaitu proses perpindahan dari sebuah sel base station (BS) ke base station lainnya dengan menjamin adanya keberlangsungan komunikasi. Walaupun handover bertujuan untuk menjaga keberlangsungan komunikasi, namun mekanisme tersebut menimbulkan handoff latency yang dapat mengganggu kualitas layanan. Salah satu teknologi jaringan wireless yang mendukung mobilitas adalahWiMAX. Mekanisme handover pada standard WiMAX yang mendukung mobilitas, IEEE 802.16m diklasifikasikan menjadi dua tipe, yaitu hard handover (HHO) dan soft handover (SHO). HHO merupakan mekanisme default yang dimiliki oleh protokol IEEE 802.16m, sedangkan SHO merupakan mekanisme opsional dengan biaya dan kompleksitas yang lebih besar [1]. Untuk mengurangi handoff latency dan meningkatkan keberhasilan dari skema HHO konvensional pengembangan skema handover dilakukan pada standard protokol WiMAX IEEE 802.16e dengan menambahkan mobility pattern [2]. Keunggulan skema handover dengan mobility pattern diperkuat dengan penelitian yang membandingkan lima metode untuk mengurangi handoff latency [3]. Penelitian tersebut menyatakan bahwa mobility pattern merupakan metode terbaik untuk mengurangi handoff latency hingga 50% dibandingkan dengan empat metode lainnya. Probabilistic Model Checking varian dari model checking adalah sebuah prosedur otomatis untuk suatu kemunculan jika suatu properti yang diinginkan berada pada sebuah model sistem probabilistic [4]. Penelitian yang menggunakan metode formal untuk melakukan analisis skema handover sudah banyak dilakukan. Chowdhurry menyatakan, perilaku proses handover mengalami perubahan dalam domain waktu yang kontinyu terhadap kemunculan suatu event. Untuk model jaringan dengan perubahan yang terjadi dalam domain kontinyu, analisis performa secara akurat hanya mungkin dilakukan jika sistem dimodelkan dengan CTMC [5]. Penelitian yang dilakukan adalah membuat sebuah algoritma untuk meminimalkan konsumsi energi dan memodelkan skema handover tersebut dengan CTMC, namun penelitian tersebut tidak memperhatikan handoff latency. Evaluasi performa dilakukan pada proses soff handoff dari jaringan seluler CDMA menggunakan pemodelan proses birth death yang merupakan varian dari CTMC [6]. Begitu juga dengan penelitian yang dilakukan yang menunjukkan bahwa proses birth death bisa digunakan untuk memodelkan proses HHO dari protokol jaringan wireless cellular untuk mengevaluasi performa dengan memperhatikan blocking probability dan dropping probability[7].