Sistem kontrol yang safety critical harus memenuhi kriteria terperecaya (reliable): dalam arti, utnutuk menjamin keamanan sistem, waktu respon dari sistem terhadap lingkungannya harus sesuai dengan yang diisyaratkan. Kegagalan sistem dalam merespon lingkungannya dapat menyebabkan terjadinya situasi kritis yang dapat berakibat fatal bagi manusia atau lingkungannya. Sistem seperti di atas harus dirancang dengan presisi yang cukup tinggi. Penggunaan bahasa alami dalam proses perancangannya dapat menimbulkan pernyataan-pernyataan yang ambigu sehingga persyaratan-persyaratan maupun spesifikasi sistem kurang terekspresikan secara akurat. Untuk menjamin akurasi rancangan sistem digunakan metoda formal, yang menggambarkan deskripsi umum dari sistem dengan menggunakan konsep matematika sehingga rancangan sistem dan ide-ide yang ada dapat diformulasikan dengan lebih tepat. Penelitian ini merupakan studi kasus yang mencoba membuat rancangan sistem dan ide-ide yang ada dapat diformulasikan dengan lebih tepat. Penelitian ini merupakan studi kasus yang mencoba membuat rancangan sistem pada top level dari sistem kontrol persimpangan rel kereta api satu jalur dengan menggunakan pendekatan metode formal, dalam hal ini DC (Duration Calculus). Studi kasus yang diajukan, mempertimgngkan kondisi stuck pada jalan raya: suatu kasus yang ada di Indonesia. Selanjutnya untuk menjamin bahwa formalisasi rancangan sistem yang telah dibuat memenuhi persyaratan-persyaratan yang diajukan, dilakukan verifikasi dengan menggunakan alat bantu PC/DC (Proff Checker for Duration Calculus).