Pemodelan lampu lalu lintas pada persimpangan yang menggunakan jalur lawan arus untuk Bus Rapid Transit sudah dilakukan sebelumnya. Namun, sistem tersebut kurang sesuai bila diterapkan pada dunia nyata. Untuk itu, pada penelitian ini dilakukan perbaikan terhadap sistem lampu lalu lintas serta ditentukan pula waktu yang sesuai bagi setiap lampu lalu lintas untuk menyala. Sistem yang diperbaiki direpresentasikan dalam model LTL dan timed automata dengan bahasa spesifikasi dalam TCTL yang sesuai dengan model-checker UPPAAL. Hasil pemodelan tersebut diverifikasi berdasarkan spesifikasi keselamatan, ketercapaian, dan keadilan untuk model LTL. Sedangkan TCTL hanya digunakan untuk verifikasi timed automata terkait keselamatan dan ketercapaian.