ABSTRAKSI: Kereta api merupakan salah satu transportasi utama yang banyak digunakan di Indonesia. Karena banyak digunakan, maka faktor keamanan adalah sesuatu yang sangat penting dalam berjalannya kereta api. Untuk alasan itu, maka penting untuk dibuat model yang baik yang dapat menunjang faktor keamanan dari kereta api. Data sistem diperoleh dari hasil pengamatan di lapangan, yaitu di stasiun kereta api Bandung.
Metode formal dapat menghasilkan spesifikasi yang tidak ambigu, karena menggunakan notasi matematis sehingga tidak terjadi kesalahan penasfiran dari sistem yang dibuat. Salah satu pemodelan yang dapat menghasilkan spesifikasi yang baik dengan metode formal yaitu menggunakan Z. Z menggunakan kumpulan teori dan kalkulus predikat. Berbeda dengan metode informal, dengan menggunakan notasi matematis tersebut maka kesalahan pada sistem dapat ditemukan pada tahapan pengembangan sistem yang lebih awal.
Tugas akhir ini mengkhususkan diri pada pemodelan jalur kereta api yang berjalan otomatis. Hasil penelitian pada tugas akhir ini menunjukkan bahwa sistem kerja kerets api dapat dimodelkan kedalam model formal dengan menggunakan notasi Z. Untuk memenuhi persyaratan sistem, aman dan adil, maka diperlukan berbagai kondisi yang diterapkan pada model.
Kata Kunci : metode formal, Z, kereta api, otomatis, pemodelanABSTRACT: Train is one of the most frequent use main transportation in Indonesia. Because of the frequent use, security factor is an important part of the operation of trains. For that reason, it is important to make a model that can support the security factor of trains. The data for the system is gathered from a field observation in Bandung train station.
Formal method can made an unambiguous specification, because it use a mathematical notation so that won’t be any missinterpreter in the system. One of the modeling mothod that can made a good specification with formal method is Z. Z use a set of theory and predicate calculus. Different from an informal method, with those mathematical notation, mistake in the system can be found in earlier stage of the system development.
This final project specified itself in modeling an automatic train track system. The result of this final project shows that an automatic train system can be modeled into formal model with the use of Z notation. To statisfied the requirment of the system, which is safety and fairness, it is needed to amply some condition.
Keyword: formal method, Z, train, automatic, modelling