PEMODELAN DAN VERIFIKASI FORMAL PROTOKOL EE-OLSR DENGAN UPPAAL CORA

RACHMAT WAHID SALEH, Dr.-Ing.MHD.M.I.Pulungan,S.Si.,M.Sc

2015 | Tesis | S2 Ilmu Komputer

Sistem Information and Communication Technology (ICT) adalah suatu bagian dari masyarakat yang sangat penting. Seiring dengan berjalannya waktu, sistem ICT terus berkembang menjadi sistem yang kompleks dan besar. Protokol komunikasi adalah salah satu contoh sistem ICT yang digunakan oleh seluruh masyarakat terutama pada penggunaan fasilitas Internet. Protokol OLSR adalah suatu protokol komunikasi jaringan wireless yang bersifat proaktif, table-driven dan berbasis pada algoritma link-state. Protokol EE- OLSR adalah varian dari protokol OLSR yang mengalami modifikasi pada konsep Willingness, protokol ini dinyatakan mampu meningkatkan penggunaan energi tanpa adanya pengurangan pada performa. Proses verifikasi protokol paling umum dilakukan dengan cara simulasi dan pengujian secara langsung. Namun proses simulasi dan pengujian tidak cukup untuk memverifikasi bahwa tidak ada subtle error atau design flaw pada suatu protokol. Model Checking merupakan sebuah metode algoritmik yang dijalankan secara fully-automatic untuk melakukan verifikasi pada sebuah sistem. UPPAAL adalah suatu model checker tool yang digunakan untuk memodelkan, simulasi, dan melakukan verifikasi terhadap suatu sistem yang dimodelkan pada jaringan Timed Automata. UPPAAL CORA adalah model checker tool untuk memverifikasi protokol EE-OLSR yang telah dimodelkan ke dalam bahasa pemodelan Priced Timed Automata, apakah protokol tersebut memenuhi properti energy efficient yang telah diformulasikan menggunakan bahasa spesifikasi formal dalam sintaks Weighted Computation Tree Logic. Hasil dari verifikasi protokol ini membuktikan bahwa protokol EE-OLSR mampu memenuhi properti energy efficient hanya ketika lalu lintas pengiriman paket terjadi.

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 : pemodelan, verifikasi, EE-OLSR, UPPAAL CORA