Tesis ini membahas tentang pengembangan perangkat lunak pengendali lalu lintas kereta api. Paradigma yang dipergunakan dalam pengembangan perangkat lunak tersebut adalah metodologi formal, yaitu metodologi RAISE (Rigorous Approach to Industrial Software Engineering). Lintasan rel kereta api yang dimodelkan pada tesis ini menggunakan dua jalur serah yang menghubungkan antar dua stasiun yang bertetangga. Pada setiap stasiun terdapat dua atau lebih jalur dua arah. Lintasan kereta api dimungkinkan untuk bertemu dengan jalur mobil. Pada titik-titik pertemuan ini, yang selanjutnya akan disebut perlintasan kereta api, prioritas tertinggi untuk lewat diberikan kepada kereta api. Untuk mengatur arus mobil yang akan melewati perlintasan tersebut, digunakan pintu-pintu perlintasan yang bisa membuka dan menutup. Pengendalian lalu lintas kereta api yang dirancang pada tesis ini meliputi pengendalian pintu-pintu perlintasan, lampu-lampu sinyal yang menentukan boleh tidaknya kereta api berjalan, dan switch penghubung antar jalur yang mengatur hubungan antar jalur.