Bus Rapid Transit -yang lebih umum dikenal sebagai busway -merupakan sarana transportasi umum yang cukup banyak dipakai oleh warga ibukota. Tetapi jalur khusus bus sering disalahgunakan oleh pengendara kendaraan non-bus, oleh karena itu pengelola berencana membangun sistem jalur lawan arus (contraflow). Akan tetapi, sistem ini akan mempunyai masalah ketika diterapkan di persimpangan. Untuk mengatasi hal tersebut Dibutuhkan sebuah lampu lalu lintas untuk mengatur arus lalu lintas. Pada tugas akhir ini, penulis akan memodelkan sistem lampu lalu lintas di persimpangan menggunakan jalur lawan arus. Kemudian model akan diformalisasikan ke dalam model formal dengan logika temporal tertentu. Model selanjutnya akan diverifikasi dan hasil dari verifikasi akan dianalisis untuk memastikan bahwa model formal yang dibangun memenuhi spesifikasi yang telah dibuat.