Pembangkitan kasus uji program java berdasarkan model checking

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.