Pemodelan dan Verifikasi Formal Stabilitas Rute pada Protokol Routing Babel Menggunakan MoDeST

VITTALIS AYU, Dr.-Ing. MHD Reza M.I. Pulungan, S.Si., M.Sc.

2016 | Tesis | S2 Ilmu Komputer

Protokol routing Babel merupakan protokol routing distance vector yang memiliki performa fast convergence dan fastest route repair time. Namun disamping kecepatan konvergensi yang dimilikinya, Babel memiliki frekuensi perubahan rute yang paling besar daripada protokol routing BATMAN dan OLSR. Frekuensi perubahan rute ini perlu dikurangi untuk meningkatkan stabilitas pemilihan rute yang terjadi pada Babel. Pengembangan protokol Babel untuk meningkatkan stabilitas pemilihan rute dilakukan oleh Jonglez dengan menerapkan hysteresis. Verifikasi formal merupakan sebuah proses untuk membuktikan terpenuhi atau tidaknya properti dari suatu sistem berdasarkan spesifikasi formal dari properti yang diinginkan. Studi tentang stabilitas dapat dilakukan dengan metode verifikasi formal, salah satunya adalah dengan teknik model checking. Pada penelitian ini dilakukan metode verifikasi formal untuk membuktikan bahwa penggunaan hysteresis dalam proses pemilihan rute dapat meningkatkan stabilitas pemilihan rute protokol routing Babel. Pemodelan dilakukan untuk menggambarkan abstraksi dari real system disertai dengan aspek non-determinisme, probabilitas dan waktu. Pemodelan dilakukan dengan bahasa MoDeST. Hasil dari penelitian ini membuktikan bahwa penggunaan hysteresis meningkatkan probabilitas terpilihnya suatu rute tertentu sehingga rute tersebut akan sering dipilih.

Babel routing protocol is a distance vector routing protocol which has fast convergence and fastest route repair time.Beside its fast convergence, Babel has the greatest route change frequency compared to BATMAN and OLSR. Route change frequencies occurance need to be surpressed to improve Babel route selection stability. The research done by Jonglez made an improvement on Babel routing protocol to minimize its route change frequency by using hysteresis method. Formal verification is a process to prove whether a certain property of a system matched its desired specification. Study about stability can be done by using formal verification method, especially model checking. This research implementing formal verification method to examine whether the usage of hysteresis in Babal routing protocol route selection process can improve and satisfy stability property. System modelling was done by observe the system abstraction and build a model using model checking language MoDeST. The result of this research proved that hysteresis method usage does satisfy stability property by improving the probability of certain route so that route always eventually chosen.

Kata Kunci : Verifikasi Formal, Protokol Routing, Babel, MoDeST