Tesis ini memberikan model formal sistem pengendali lalulintas kereta api di suatu setasiun yang mempunyai dua jalur pemberhentian serta terhubung dengan dua setasiun lainnya melalui jalur tunggal. Model dibangun menggunakan bahasa Spesifikasi Kalkulus Durasi (Duration Calculus) dan diverifikasi menggunakan perngkat lunak PC/DC (Proof Checker for Duration Calculus). Hasil verifikasi menunjukkan bahwa semua persyaratan keselamatan (safety requirements) sistem pengendali dipenuhi oleh strategi kontrol yang diusulkan.