Path: Top » Member » rina@tf.itb.ac.id

PEMODELAN DAN VERIFIKASI FORMAL PADA SISTEM INTERLOCKING KERETA API MENGGUNAKAN METODA MODEL CHECKING

MODELLING AND FORMAL VERIFICATION ON TRAIN INTERLOCKING SYSTEM USING MODEL CHECKING

Undergraduate Theses from JBPTITBTF / 2017-07-08 12:37:27
Oleh : Kevin Pradityo NIM 13313022 & Benedictus Aristyo N. NIM 13313096
Dibuat : 2017-07-05, dengan 10 file

Keyword : IL 4, verifikasi formal, petri net, FSA, model checker, koreksi model, GUI

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.

Deskripsi Alternatif :

Railway is a ground transportation modes that falls within the category of safety critical system and requires safety integrity level (SIL) 4. One of the main requirements of a system with SIL-4 is the formal verification of software and hardware systems used to ensure the safety of system operation. The interlocking system in the operation of the railroad forms a system that governs the journey and direction of rail movement. To fulfill SIL 4 safety standards, this paper proposes a modular modeled of rail interlocking system using petri net and finite state automata (FSA). The safety specification of the operation of the interlocking system model is defined by using the logic temporal type computational tree logic (CTL). The model checking for model verification of specifications is executed on the TAPAAL and UPPAAL model checker. If the model complies the specifications, the model checker will produce a "satisfied" result and if it does not then the model checker will give a "not satisfied" result which can then be the basis for model correction. The result of verification and model refinement with formal method in this research indicates that the model checking method has the potential to be implemented in the design and verification of rail interlocking system. Models that satisfy the specifications are then implemented into the graphical user interface (GUI) in Matlab.

Beri Komentar ?#(0) | Bookmark

PropertiNilai Properti
ID PublisherJBPTITBTF
Organisasi
Nama KontakRina
AlamatPerpustakaan Departemen Teknik Fisika
KotaBandung
DaerahJawa Barat
NegaraIndonesia
Telepon
Fax
E-mail Administratoradmin@tf.itb.ac.id
E-mail CKOckolib@tf.itb.ac.id