Notasi Z telah diakui kehandalannya sebagai alat bantu pembuatan dokumen spesifikasi formal dalam proses pengembangan suatu program aplikasi. Tulisan ini memberikan uraian ringkas pembuatan dokumen spesifikasi formal dengan notasi Z dalam studi kasus SIM BAAK Politeknik Elektronika Negeri Surabaya untuk keperluan belajar mahasiswa, beserta analisanya. Dimulai dengan spesifikasi dalam bahasa alamiah (bahasa Indonesia), yang kemudian dijabarkan secara formal dalam notasi Z yang berbasis pada model matematika. Selanjutnya, dilakukan pengujian terhadap model tersebut dengan menggunakan ZTC: A Type Checker for Z Notation, yaitu suatu program aplikasi yang dapat menguji tingkat akurasi, konsistensi dan kelengkapan dari model matematika dalam notasi Z. Didiskusikan pula beberapa faktor yang menjadi kendala saat digunakannya bentuk spesifikasi formal dalam proses pengembangan program aplikasi tersebut.
Kata kunci: Notasi Z, spesifikasi formal, skema Z, ZTC: A Type Checker for Z Notation
