Model Formal Dan Verifikasi Sistem Layanan Presensi Rfid Dengan Logika Temporal: Studi Kasus Di Universitas Telkom, Indonesia

Abstract

Sistem presensi RFID (Radio Frequency Identification) di Universitas Telkom adalah suatu sistem layanan yang bertujuan untuk meningkatkan efisiensi dalam proses pencatatan kehadiran mahasiswa. Saat ini masalah masih banyak ditemukan sehingga keandalan sistem layanan presensi masih belum optimal. Salah satu masalahnya adalah presensi mahasiswa terkadang tidak terekam pada sistem tersebut. Dalam tugas akhir ini, penulis terlebih dulu membuat dokumen tertulis (diagram aktivitas) dan spesifikasi sistem secara rinci dan jelas berdasarkan hasil observasi di lapangan. Hasil tersebut akan diformalisasikan ke dalam model formal dengan logika temporal tertentu. Selanjutnya penulis menggunakan metode formal untuk melakukan verifikasi spesifikasi keamanan (safety) dan keterjangkauan (liveness) berdasarkan model yang dibentuk. Tugas akhir ini memberikan suatu contoh translasi dari diagram aktivitas ke dalam model formal untuk sistem layanan presensi RFID. Lebih jauh, penulis menunjukkan bahwa metode formal dapat mendukung verifikasi sistem layanan presensi RFID di Universitas Telkom. Kata Kunci: metode formal, RFID, diagram aktivitas, model formal