Terjadinya kasus penyebaran vaksin palsu di Indonesia pada pertengahan tahun 2016 merupakan kejadian buruk yang membuat keamanan alur distribusi vaksin dipertanyakan. Alur distribusi diatur oleh PT. Bio Farma. Pada tugas akhir ini penulis melakukan verifikasi alur distribusi vaksin di Indonesia menggunakan pendekatan metode formal, yaitu Logika Temporal Linear.
Alur distribusi vaksin terlebih dahulu dimodelkan dalam diagram aktivitas. Kemudian diagram aktivitas diverifikasi terhadap persyaratan yang diatur oleh BPOM (Badan Pengawas Obat dan Makanan) dan WHO (World Health Organization). Verifikasi dilakukan dengan model checker NuSMV. Dari tugas akhir ini, penulis menyimpulkan alur distribusi vaksin di Indonesia terbukti aman secara formal terhadap beberapa persyaratan keamanan yang diatur oleh BPOM dan WHO. Namun, alur distribusi tersebut tidak dapat secara spesifik menjamin beberapa persyaratan keamanan yang ditentukan dan beberapa persyaratan fungsional tambahan.