Sistem Kontrol Lalulintas kereta api di suatu stasiun harus memenuhi kriteria dapat diandalkan (reliable); dalam arti, untuk menjamin keamanan sistem, waktu respon dari sistem terhadap lingkungannya harus sesuai dengan yang disyaratkan. Kegagalan sistem dalam merespon lingkungannya dapat menyebabkan terjadinya situasi krisis yang dapat berakibat fatal bagi manusia atau lingkungannya. Dalam penelitian ini dilakukan percobaan untuk membuat aturan agar memenuhi persyaratan keamanan dan persyaratan fungsional di stasiun kereta api yang terhubung dengan dua stasiun yang lain melalui jalur ganda. Aturan-aturan ini menjamin tidak akan terjadi tabrakan kereta api atau kereta api keluar dari relnya. Aturan-aturan itu diwijudkan dalam bentuk pengaturan sinyal, pengaturan posisi wesel dan pengaturan ada tidaknya kereta api di suatu ruas jalur. Pengaturan yang ada memerlukan strategi-strategi kontrol yang perlu dikaji konsistensinya untuk menjamin bahwa pengaturan yang ada sudah berjalan sesuai dengan persyaratan keamanan dan persyaratan fungsional yang diinginkan. Untuk itu dilakukan pemodelan formal dari strategi kontrol tersebut dengan menggunakan Kalkulus Durasi dan uji konsistensi dilakukan dengan menggunakan Proff. Checker/Duration Calculus. Hasil verifikasi menunjukkan bahwa strategi kontrol yang dibuat sudah memenuhi konsistensi dengan aturan-aturan yang menjamin persyaratan keamanan dan persyaratan fungsional. Penggunaan Kalkulus Durasi dalam permodelan formal dari sistem pengendali lalulintas kereta api di stasiun dengan rel ganda mampu mengakomodasi: 1. Keadaan sistem kontrol dalam suatu interval waktu. 2.Urutan kejadian dan perubahan keadaan yang diakibatkan adanya interaksi dengan lingkungan. 3. Kebutuhan formula-formula yang lebih rinci dalam mekanisme sistem pengendali dan batasan waktu dalam setiap perubahan keadaan yang merupakan syarat fungisonal.