Bundaran yang ada di jalan-jalan di Indonesia sebagai modal pengatur lalu lintas di persimpangan sudah tertera sejak lama dalam Peraturan Pemerintah RI No. 43 tahun 1993 tentang Prasarana dan Lalu Lintas Jalan sebagai salah satu bentuk pengaturan persimpangan yang diizinkan. Bundaran lalu lintas memiliki titik konflik (titik tempat kemungkinan kendaraan saling menabrak satu sama lain atau dengan pejalan kaki) yang lebih sedikit dibanding persimpangan jalan biasa yang membuat bundaran lebih aman dibanding persimpangan jalan tradisional. Mengerti jalanan adalah bagian penting dari keberlangsungan hidup hampir semua orang maka penting untuk sebuah modal pengatur lalu lintas jalan untuk ketat, presisi, dan tidak ambigu. Metode Formal dapat memodelkan sistem bundaran jalan atau lebih spesifiknya modern roundabout untuk menjamin sistem tersebut ketat, presisi, dan tidak ambigu dengan memverifikasi persyaratan yang ada pada sistem. Namun simulasi dalam bentuk model formal dari modern roundabout masih belum ada, maka pada tugas akhir ini penulis membangun model formal dari sistem modern roundabout. Sistem modern roundabout dimodelkan ke dalam model formal dengan struktur Kripke dan spesifikasi formalnya ke dalam logika temporal linear. Selanjutnya, model diverifikasi terhadap spesifikasi yang telah dibuat (dengan model checking, salah satu metode verifikasi dalam metode formal) menghasilkan model formal dari sistem modern roundabout yang valid.
Kata Kunci: modern roundabout, logika temporal linear, metode formal, pemodelan, model checking