Verifikasi sistem elevator dengan coloured petri nets

Abstract

Multiple elevators system adalah sebuah sistem elevator yang mengatur 2 atau lebih elevator di dalamnya. Sistem elevator ini mampu mengerjakan proses-proses yang masuk secara bersamaan dengan memanfaatkan sifat concurrency. Dengan adanya concurrency ini car elevator pada multiple elevators system dapat bekerja secara bersamaan, dengan kata lain car satu dengan car yang lain dapat bekerja secara independent tanpa perlu memperhatikan kondisi dari car lain dalam sistem yang sama. Pada skripsi ini, telah dibangun sebuah perangkat lunak simulasi yang mampu melakukan simulasi pergerakan dari multiple elevators system. Kemudian telah dilakukan verifikasi menggunakan coloured petri nets. Coloured petri nets adalah sebuah bahasa grafis yang dapat digunakan untuk memodelkan sistem yang konkuren. Verifikasi dilakukan dengan tujuan untuk memastikan perangkat lunak simulasi multiple elevators system teruji kebenarannya.

Setelah dilakukan pengujian terhadap perangkat lunak simulasi multiple elevators system, dapat disimpulkan bahwa perangkat lunak simulasi yang dibangun sudah mampu menyimulasikan objek-objek yang terdapat dalam sistem elevator di dunia nyata, serta menyimulasikan pergerakan dari masing-masing objek meskipun tidak disimulasikan interaksi antara objek penumpang dengan elevator seperti pada dunia nyata. Untuk model CPN, telah berhasil memodelkan seluruh bagian sistem elevator kedalam bentuk komponen CPN sesuai dengan definisi formal dari CPN. Komponen-komponen dimodelkan berdasarkan definisi formal CPN yaitu 9-tuple (P,T,A,P,V,C,G,E,I ). Dilakukan verifikasi terhadap kondisi-kondisi yang terjadi dalam model CPN, sehingga dapat diketahui apakah dengan properti yang sama dengan sistem elevator, model CPN mampu mencapai kondisi-kondisi yang sama terjadi pada sistem elevator. Verifikasi dilakukan dengan teknik model checking dan menggunakan fitur ASK-CTL dari CPNTools. Model CPN juga mampu mengobservasi seluruh kondisi yang mungkin terjadi dalam sistem elevator yang mungkin akan sulit ditemukan jika hanya menggunakan simulasi saja.

Hasil dari skripsi ini adalah sebuah perangkat lunak yaitu, perangkat lunak simulasi yang dibangun dengan menggunakan bahasa pemrograman Java pada kakas Greenfoot dan sebuah model CPN yang dibangun dengan bahasa grafis coloured petri net dengan kakas CPN Tools.