JURNAL : Pemodelan dan Verifikasi Formal Protokol EE-OLSR dengan UPPAAL CORA

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

Kata kunci—pemodelan, verifikasi, EE-OLSR, UPPAAL CORA.

PENDAHULUAN - Mobile Ad Hoc Network (MANET) adalah jaringan komputer bersifat spontan, yang berkomunikasi melalui suatu media nirkabel. Setiap node dapat bergabung atau memisahkan diri kapan saja, serta bebas bergerak sesuai keinginan. MANET tidak memiliki infrastruktur terpusat, seluruh node yang berpartisipasi berfungsi sebagai node akhir dan router. Jaringan MANET memiliki sebuah topologi yang dinamis, dimana setiap node dapat bergerak secara acak, kondisi penyebaran radio berubah dengan cepat sepanjang waktu, serta bandwidth yang terbatas [1]. Sejak mobile host ditenagai oleh baterai, penggunaan energi baterai secara efisien sangatlah penting. Umur baterai dapat mempengaruhi performa komunikasi jaringan secara keseluruhan [2]. Optimized Link State Routing (OLSR) adalah protokol routing yang didasarkan pada link-state algorithm dan bersifat proaktif, protokol ini banyak digunakan dan dikembangkan sehingga berbagai macam studi terus dilakukan untuk memperbaiki serta meningkatkan kinerja protokol OLSR [3]. OLSR tradisional memberikan keunggulan dalam menemukan rute diantara dua node di dalam jaringan dalam waktu yang singkat dikarenakan polanya yang proaktif, namun OLSR dapat menghabiskan banyak sumber daya dalam proses pemilihan node MPR serta dalam pertukaran informasi Topology Control. Energy Efficient OLSR (EE-OLSR) adalah suatu protokol yang dinyatakan dapat meningkatkan tingkat efisiensi energi untuk memperpanjang umur jaringan tanpa adanya pengurangan pada performa [2]. Model Checking adalah suatu teknik verifikasi yang menyelidiki seluruh kemungkinan system state dengan cara brute force [4]. Model Checking juga merupakan sebuah metode algoritmik yang dijalankan secara fully-automatic untuk melakukan verifikasi pada sebuah sistem [5]. UPPAAL adalah suatu model checker tool yang digunakan untuk memodelkan, simulasi, dan melakukan verifikasi terhadap suatu sistem yang dimodelkan pada Timed Automata [6]. UPPAAL CORA adalah suatu varian dari UPPAAL untuk menganalisa Cost Optimal Reachability. UPPAAL CORA dikembangkan oleh tim yang telah mengembangkan UPPAAL sebelumnya. UPPAAL CORA menggunakan Linearly Priced Timed Automata (LPTA) sebagai bahasa pemodelannya. Penelitian ini dilakukan dengan memodelkan dan memverifikasi protokol EE-OLSR tersebut menggunakan tool model checker UPPAAL CORA.