PEMODELAN DAN VERIFIKASI FORMAL STABILITAS RUTE PADA PROTOKOL ROUTING BABEL MENGGUNAKAN MODEST; MODELING AND FORMAL VERIFICATION OF ROUTE STABILITY OF BABEL ROUTING PROTOCOL USING MODEST

AYU, VITTALIS, Reza M.I. Pulungan

2016 | Disertasi | FMIPA

Babel (Chroboczek, 2011) is a distance vector routing protocol which has fast convergence and fastest route repair time (Abolhasan et al., 2009). Beside its fast convergence, Babel has the greatest route change frequency compared to BATMAN and OLSR (Abolhasan et al., 2009). Route change frequencies occurance need to be surpressed to improve Babel route stability. The research done by Jonglez et al. (2014) 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 : Formal verification, Protokol Routing, Babel, MoDeST