MODEL CHECKING PADA PROTOKOL BERMAN DAN GARAY - Sheila Nurul Huda (Seminar Nasional Aplikasi Teknologi Informasi (SNATI), 2011)
Distributed consensus merupakan permasalahan yang dikenal dalam sistem terdistribusi dimana terdapat beberapa proses yang berjalan secara konkuren, tiap proses memulai dengan nilai awalnya, dan pada akhirproses mereka harus mencapai nilai yang sama. Artinya, semua proses harus mencapai kesepakatan, sekalipun nilai awal mereka mungkin berbeda. Terdapat kondisi yang memungkinkan terjadinya kegagalan pada proses yang terlibat, kondisi ini disebut byzantine failure. Protokol Berman dan Garay dirancang untuk menyelesaikan distributed consensus dengan kehadiran byzantine failure. Untuk mendapatkan kepastian secara formal bahwa protokol tersebut mencapai distributed consensus dilakukan verifikasi dengan metode model checking menggunakan SPIN model checker.