Perpustakaan Digital ITB

Kereta api adalah sebuah moda transportasi darat yang termasuk dalam kategori safety critical system dan membutuhkan standar keselamatan safety integrity level (SIL) 4 yang merupakan standar keselamatan paling tinggi. Salah satu syarat utama sistem dengan SIL-4 adalah dilakukannya verifikasi formal pada sistem software dan hardware yang digunakan untuk menjamin keselamatan pengoperasian sistem tersebut. Sistem interlocking pada pengoperasian kereta api membentuk suatu sistem yang mengatur perjalanan dan arah pergerakan kereta api. Untuk memenuhi standar keselamatan SIL 4, penelitian tugas akhir ini mengajukan sistem interlocking kereta api yang dimodelkan secara modular dengan menggunakan petri net dan finite state automata (FSA). Spesifikasi keselamatan pengoperasian model sistem interlocking didefinisikan dengan menggunakan logika temporal jenis computational tree logic (CTL). Model checking untuk verifikasi model terhadap spesifikasi dieksekusi pada model checker TAPAAL dan UPPAAL. Jika model memenuhi spesifikasi, model checker akan memberikan hasil “satisfied” dan jika tidak maka model checker akan memberikan hasil “not satisfied” yang kemudian dapat menjadi dasar untuk perbaikan model (model correction). Hasil verifikasi dan penyempurnaan model dengan metode formal pada penelitian ini menunjukkan bahwa metode model checking berpotensi untuk diimplementasikan dalam perancangan dan verifikasi sistem interlocking kereta api. Model yang sudah memenuhi spesifikasi kemudian diimplementasikan ke dalam bentuk graphical user interface (GUI) pada Matlab.