Verifikasi formal sistem elevator dengan alloy

Abstract

Multiple Elevators System adalah sebuah sistem elevator yang mengatur beberapa elevator di dalamnya. Sistem ini mengerjakan proses-proses yang ada secara bersamaan sebagai proses yang konkuren, sehingga dapat melayani pengguna dengan lebih cepat dan adil. Pada skripsi ini, akan dibangun sebuah perangkat lunak yang mampu melakukan simulasi Multiple Elevators System, kemudian akan dilakukan verifikasi menggunakan Alloy. Alloy adalah sebuah bahasa spesifikasi untuk menggambarkan batasan struktur kompleks dan perilaku dari sebuah perangkat lunak. Verifikasi ini perlu dilakukan agar perangkat lunak simulasi Multiple Elevators System teruji secara formal.

Berdasarkan hasil pengujian yang dilakukan, dapat disimpulkan bahwa perangkat lunak simulasi Multiple Elevators System dan perangkat lunak Alloy dapat berjalan dengan baik. Perangkat lunak simulasi dapat menampilkan dengan baik bagaimana sistem elevator bekerja, sehingga dapat dengan mudah diamati dan dipahami. Semua fitur yang ada di dalam perangkat lunak juga sudah diuji dan seluruhnya berjalan dengan baik. Pada Alloy, seluruh properti-properti yang ada sudah berhasil dimodelkan. Kemudian dilakukan verifikasi atas instance dari properti-properti tersebut dan terbukti benar. Alloy juga mampu menampilkan skenario-skenario yang mungkin terjadi, sehingga memberikan gambaran yang lebih lengkap pada model yang sedang diuji.

Hasil dari skripsi ini adalah dua buah perangkat lunak, yang satu dituliskan dalam bahasa Java dan yang satu lagi dituliskan dalam bahasa Alloy. Perangkat lunak dalam bahasa Java berfungsi untuk melakukan simulasi bagaimana sebuah Multiple Elevators System bekerja, sedangkan perangkat lunak dalam bahasa Alloy berfungsi melakukan verifikasi secara formal pada model Multiple Elevators System yang digunakan.