PEMODELAN DAN VERIFIKASI FORMAL PROTOKOL EE-OLSR DENGAN UPPAAL CORA; FORMAL MODELING AND VERIFICATION OF EE-OLSR PROTOCOL WITH UPPAAL CORA

Insani, Rachmat Wahid S, Reza M.I. Pulungan

2015 | Disertasi | FMIPA

Information and Communication Technology (ICT) systems are one of the important aspects on society. ICT systems are growing and much more to become a complex and large systems. Communication protocol is one of the ICT system used by society, particularly when it comes for internet utilization. Optimized Link State Routing (OLSR) protocol is a communication protocol for wireless network based on proactive, table-driven and link-state algorithm. Energy-Efficient OLSR (EE-OLSR) is a variant of OLSR protocol which have been modified in Willingness concept, this protocol claimed to be able to improve the energy utilization without any loss in performance. Protocol verification processes are commonly run by simulation and direct testing method. However, simulation and direct testing method is not capable enough to verify that there are no subtle error or design flaw in the protocol. Model Checking is an algorithmic method run in fully automatic in order to verify a system. UPPAAL is a model checker tool used for modeling, simulation and verifying a system modeled by networks of Timed Automata. UPPAAL CORA is a model checker tool, it is used to verify a protocol is able to satisfy energy efficient property formulated by formal specification language using Weighted Computation Tree Logic syntax. The result of this verification on the protocol is the EE-OLSR protocol is able to satisfy the energy efficient property when the packet transmission occur.

Kata Kunci : modeling; verificationl EE-OLSRl UPPAAL CORA.