Tesis ini menyajikan hasil penelitian tentang pemodelan, pembuatan formal spesifikasi dan pemverifikasian beberapa studi kasus memanfaatkan penggunaan notasi Behavior Tree (BT) untuk memodelkan requirements dan SAL model-checker untuk memeriksa properties-nya. Penelitian ini merupakan langkah awal dalam mencapai otomatisasi dalam pengembangan perangkat lunak. Hal ini dicapai dengan terlebih dahulu mengotomatisasi proses untuk menghasilkan spesifikasi untuk input ke model-checker tool dari model yang telah tersedia. Notasi BT digunakan memodelkan requirements dan editor TextBE membantu dalam menghasilkan representasi grafisnya. Model BT yang terbentuk kemudian ditranslasi ke bahasa dari SAL sehingga kita dapat memverifikasinya menggunakan SAL Tool. Hasil translasi dari notasi BT ke kode SAL dilakukan secara otomatis. Hal ini terwujud dengan memetakan setiap node dari BT ke kode SAL menggunakan aturan translasi yang sudah ditetapkan.