Abstract:
Pengujian merupakan hal yang sangat penting dalam membangun suatu perangkat lunak. Pengujian
berfungsi untuk mencari kesalahan pada program dengan cara mengidentifikasi ketepatan,
kelengkapan, dan mutu dari suatu perangkat lunak. Hal ini membutuhkan biaya yang tidak
sedikit. Pengotomatisan pengujian diharapkan dapat menurunkan biaya produksi dan juga
meningkatkan keandalan suatu perangkat lunak. Test case merupakan masukan spesifik yang
akan dicoba ketika sebuah perangkat lunak diuji. Pengujian adalah mencoba beberapa test
case yang dibuat oleh penguji. Pada umumnya test case yang diuji hanya mewakili beberapa
contoh kasus saja dan tidak mencoba seluruh kemungkinan state pada program. Untuk bisa
menentukan test case yang tepat, efisien, dan menelusuri seluruh kemungkinan state, maka
digunakan model checking sebagai pembangkit test case. Pada skripsi ini digunakan kakas
Java Path Finder (JPF) untuk melakukan model checking. JPF adalah sebuah sistem untuk
memverifikasi Java bytecode yang bertujuan untuk mencari cacat atau kesalahan pada program.
JPF dapat melakukan symbolic execution. Symbolic execution adalah cara menganalisis program
untuk menentukan masukan seperti apa yang menyebabkan setiap bagian dari program dieksekusi.
Perangkat lunak yang berhasil dibangun menerima masukan berupa sebuah file java lalu
melakukan otomatisasi dalam konfigurasi kakas JPF untuk melakukan symbolic execution .
Perangkat lunak akan menampilkan hasil pembangkitan test case dengan memproses output
dari hasil eksekusi program JPF sehingga mudah dibaca oleh pengguna. Perangkat lunak yang
dibangun masih terbatas dalam menangani kasus-kasus tertentu pada file Java, misalnya hanya
dapat membangkitkan test case dengan tipe data primitif dan kondisi-kondisi tertentu saja.
