Penelitian ini bertujuan untuk melakukan analisis dan pengembangan lebih lanjut terhadap penelitian-penelitian di Fasilkom UI mengenai formalisasi sistem pengendali lalu lintas kereta api. Bahan penelitian yang digunakan adalah skripsi dan tesis mahasiswa serta kode program hasil formalisasi yang telah dilakukan sebelumnya. Analisis dilakukan pada karakteristik pendeskripsian komponenkomponen sistem, pendefinisian spesifikasi, serta metode verifikasi yang digunakan pada tiap penelitian. Sedangkan pengembangan dilakukan dengan melakukan rekonstruksi model sistem pada penelitian terakhir dengan bahasa TLA+. Kemudian dilakukan verifikasi pada hasil rekonstruksi dengan menggunakan model checker TLC. Hasil verifikasi kemudian dianalisa untuk menentukan definisi spesifikasi yang paling sesuai untuk model sistem yang telah dibuat.