Verifikasi Formal Algoritma Terdistribusi Untuk Masalah Alokasi Kanal Berbasis Mutual Exclusion Pada Jaringan Selular Menggunakan Promela/Spin

Andi Yulia Muniar (Program Studi Teknik Informatika, STMIK AKBA, Makassar)
Armin Lawi (Fakultas Teknik, Universitas Hasanuddin, Makassar)
Merna Baharuddin (Fakultas Teknik, Universitas Hasanuddin, Makassar)

Jurnal Inspiration
Vol 2, No 1 (2012): Jurnal Inspiration Volume 2 Issue 1

Penelitian ini bertujuan membangun model formal algoritma terdistribusi (distributed algorithm) untuk masalah alokasi kanal berbasis Mutual Exclusion pada jaringan selular yang mana hanya ada satu kanal dalam jaringan selular dan jarak minimum reuse-nya tidak terhingga (infinity) menggunakan bahasa pemrograman PROMELA. Serta memverifikasi kebenaran algoritma dari spesifikasi masalah sistem terdistribusi dan menganalisis kinerja algoritma dengan menggunakan tools SPIN. Masalah mendasar dari Distributed Mutual Exclusion (DME) adalah pada waktu yang bersamaan hanya satu proses yang dapat masuk pada critical section. Dengan kata lain tidak ada dua proses yang berada di critical section pada saat yang bersamaan. Jika proses-proses ingin mengeksekusi critical resource pada waktu yang bersamaan, maka proses-proses tersebut harus bersaing untuk masuk ke dalam critical section. Hasil penelitian yang diperoleh yaitu dalam membangun model formal yang pertama dilakukan adalah merancang algoritma terdistribusi (distributed algorithm) untuk masalah alokasi kanal berbasis Mutual Exclusion kemudian algoritma diterjemahkan ke dalam bahasa pemrograman PROMELA, yang kemudian memverifikasi kebenaran algoritma tools SPIN.