Studi yang dilakukan adalah untuk meneliti dan membuat model format dari sebuah perempatan di Jakarta. Diharapkan berbagai spesifikasi dapat diformalissikan untuk perempatan seperti itu. Spesifikasi yang dihasilkan seharusnya cukup untuk menjelaskan sifat-sifat dari perempatan tersebut. Penggunaan Temporal Logic sangat dibutuhkan karena sifat waktu nyata dari masalah ini. Setelah perempatan tersebut dimodelkan secara formal, perlu dilakukan verifikasi. Proses verifikasi dilakukan dengan bantuan alat verifikasi, dalam kasus ini dipakai STeP (Stanford Temporal Prover)