ABSTRAK Nama : Ardi Program Studi : Ilmu Komputer Judul : Perbaikan BT2SAL Translator untuk Integrasi Model Checker dengan Trace Animator pada Paradigma Behavior Engineering Penelitian ini menggunakan behavior engineering sebagai suatu disiplin ilmu terintegrasi yang mendukung sistem dan rekayasa perangkat lunak skala besar. Behavior engineering juga mendukung pemodelan requirement perangkat lunak yang formal. Dalam behavior engineering, requirement dimodelkan ke dalam suatu diagram bernama behavior tree. Behavior tree memiliki spesifikasi formal yang dapat digunakan untuk keperluan verifikasi dan analisis desain pemodelan. Beberapa tool pengembangan untuk behavior tree telah dibuat dalam penelitian sebelumnya seperti BT2SAL Translator untuk melakukan translasi dari spesifikasi behavior tree ke spesifikasi masukan SAL, SAL Model-Checker untuk melakukan pengecekan model, Saltrace to Bttrace Program, dan Trace Animator untuk melakukan animasi alur proses dalam behavior tree. Penelitian ini merupakan penelitian lanjutan untuk mengintegrasikan SAL Model-Checker dengan Trace Animator sekaligus memperbaiki translasi dari BT2SAL Translator. Perbaikan translasi dicapai melalui perbaikan aturan-aturan translasi dan implementasinya pada BT2SAL Translator. Kata Kunci: Behavior tree, TextBE, SAL, Integrasi Tool, Model Checker, Trace Animator