Spesifikasi dan verifikasi Bounded Retransmission Protocol (BRP) dengan Temporal Logic of Actions (TLA+)

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.