Perpustakaan Digital ITB

Algoritma terdistribusi umum diimplementasikan dalam berbagai sistem terdistribusi, namun dalam implementasinya seringkali algoritma perlu dimodifikasi sehingga spesifikasi kebenaran algoritma belum tentu terjamin dan spesifikasi yang spesifik implementasi muncul. Bug dapat muncul jika spesifikasi tidak terpenuhi. Deteksi bug perlu dilakukan secepat mungkin dan deteksi perlu mencakup kasus-kasus ujung yang sulit dicapai. Salah satu solusi untuk melakukan deteksi bug adalah dengan mengintegrasikan model checker ke dalam alur pengujian sistem. Pada tugas akhir ini, sistem yang menjadi bahan uji adalah protokol Paxos pada Cassandra dan model checker diintegrasikan dengan alur pengujian dtest. Pendeteksian dilakukan terhadap implementasi. Pertama, implementasi Paxos di Cassandra dimodelkan sebagai sebuah sistem transisi. Kemudian, pencegatan dilakukan beberapa titik sehingga implementasi dapat bekerja sebagai sebuah sistem transisi yang dapat mengkomunikasikan event dan state. Selanjutnya, model implementasi diintegrasikan dengan model checker dan juga dengan dtest, dengan melakukan rancangan komunikasi tiga arah antara sistem Cassandra, dtest, dan model checker , dan masing-masing elemen mengimplementasikan komponen-komponen tertentu agar dapat saling berkomunikasi. Pengujian menunjukkan bahwa model checker yang diintegrasikan dengan dtest mampu mereproduksi bug yang hidup pada implementasi Paxos di Cassandra dengan tingkat keberhasilan 86,7 % untuk kasus pengujian dengan skenario bug dan keberhasilan 84,6 % untuk kasus eksplorasi dengan model checker. Model checker yang terintegrasi juga mampu mendeteksi kesalahan jika implementasi protokol Paxos Cassandra faulty.