Abstract:
Pembuatan spesifikasi dan verifikasi merupakan dua tahap penting dalam rekayasa protokol. Spesifikasi
digunakan untuk mendeskripsikan perilaku dari protokol sedangkan verifikasi adalah proses
untuk menjamin bahwa spesifikasi tersebut memenuhi properti yang diharapkan dari protokol tersebut.
Salah satu pendekatan yang digunakan dalam pembuatan spesifikasi dan verifikasi protokol
adalah metode formal. Dengan pendekatan ini spesifikasi sistem biasanya berupa Finite Transition
Systems dan properti dari protokol dinyatakan dalam logika temporal.
Salah satu teknik pembuatan spesifikasi dan verifikasi yang termasuk dalam kelompok metode
formal yaitu Temporal Logic of Actions (TLA). Keunggulan dari TLA adalah spesifikasi dan properti
dapat dinyatakan dengan satu bentuk yang sama yaitu berupa formula-formula dari TLA. Proses
verifikasi sendiri dapat dilakukan dengan membuktikan bahwa properti merupakan implikasi dari
spesifikasi.
Penelitian ini bertujuan untuk menerapkan pembuatan spesifikasi dan verifikasi secara formal
dengan TLA. Studi kasus yang diambil adalah Bounded Retransmission Protocol (BRP).
Hasil dari penelitian ini adalah dapat dibuat spesifikasi BRP dengan menggunakan TLA + yang
merupakan bahasa pengembangan dari TLA. Selain itu berhasil dilakukan verifikasi bahwa spesifikasi
yang dibuat memenuhi properti yang diharapkan. Pembuktian dilakukan secara deduktif
dengan menggunakan aturan pembuktian yang disedikan oleh TLA.
