Perpustakaan Digital ITB

Pengembangan perangkat lunak menuntut tingkat pengujian yang lengkap. Hal ini menjadi masalah karena untuk melakukan pengujian yang lengkap diperlukan biaya yang cukup besar, selain itu memerlukan sumber daya manusia yang cukup handal. Dewasa ini, pengembangan perangkat lunak banyak yang menggunakan metode berorientasi objek, tetapi untuk sistem-sistem yang kritikal diperlukan pengujian yang lebih sulit, oleh karena itu dikembangkan suatu metode pengembangan perangkat lunak yang baru, yaitu metode formal. Metode formal adalah metode untuk membangun perangkat lunak dengan menggunakan bahasa matematika, sehingga untuk melakukan spesifikasi awal agak menyulitkan, tetapi akan menghasilkan spesifikasi yang lebih akurat. Oleh karena itu, diperlukan suatu metode analisis yang sudah umum digunakan untuk kemudian dipetakan menjadi spesifikasi formal. Metode formal yang digunakan adalah metodologi RAISE. RAISE membangun spesifikasi dengan dimulai dari pendekatan abstract-applicative, kemudian dilanjutkan dengan membuat spesifikasi tersebut menjadi konkret, kemudian untuk diterjemahkan menjadi bahasa yang lebih mendekati bahasa pemrograman yaitu concrete-imperative. Kemudian, jika ada masalah konkurensi, maka spesifikasi concrete-imperative dapat dijadikan sebagai dasar untuk membangun concrete-concurrent. Sebagai studi kasus, dipilih sebuah sistem pemesanan resources, dengan batasan yaitu sistem yang dibangun harus mempunyai basis data, dan menimbulkan masalah konkurensi. Berdasarkan hasil penelitian, maka dapat disimpulkan bahwa dengan membuat analisis dengan metode berorientasi objek, maka cukup memudahkan dalam membuat spesifikasi formal, dan metode formal sudah dapat memberikan spesifikasi untuk masalah konkurensi dengan menggunakan channel.