Protokol komunikasi melibatkan beberapa proses yang konkuren, sehingga verifikasi protokol komunikasi dengan metode informal sukar dilakukan. Untuk mengatasi masalah tersebut verifikasi protokol komunikasi dilakukan dengan metode formal. Tugas akhir ini melakukan formalisasi dan verifikasi suatu protokol komunikasi dengan menggunakan alat bantu Symbolic Model Verifier (SMV). Protokol komunikasi yang akan diformalisasi dan diverifikasi, menyediakan servis pengiriman data searah dari mesin pengiriman ke mesin penerima yang saling terhubung point-to point, dengan menggunakan mekanisme stop dan wait. Servis protokol ini dianggap kurang handal sehingga protokol menggunakan mekanisme time out dan pengiriman ulang data. Pata tugas akhir ini protokol tersebut akan diverifikasi bebas dari deadlock dan livelock serta mengalami progress.