Perkembangan teknologi informasi yang semakin pesat membuat komputer semakin banyak digunakan sebagai alat bantu dalam menjalankan kegiatan industri dan bisnis. Piranti lunak yang digunakan oleh komputer memegang peranan yang sangat penting. Jika penggunaan piranti lunak tersebut menghasilkan galat (error), maka dunia industri atau bisnis tersebut dapat mengalami kerugian. Untuk menjamin bahwa piranti lunak tersebut bebas dari galat, maka pengembangan piranti lunak tersebut dapat dilakukan dengan menggunakan metode B. Metode B adalah suatu metodologi formal yang digunakan dalam pengembangan piranti lunak, mulai dari spesifikasi sampai dengan implementasi piranti lunak. Dari suatu spesifikasi awal yang bersifat abstrak dan modular, akan dilakukan beberapa tahap refinement sampai mencapai suatu model yang lebih konkrit, yang merupakan kode programnya. Spesifikasi awal tersebut dikembangkan secara matematik sesuai dengan spesifikasi awalnya, sehingga kebenaran piranti lunak tersebut dapat dijamin. Fokus pada tugas akhir ini adalah menelaah refinement dengan metode B dan menerapkannya terhadap suatu studi kasus aplikasi perbankan yang diajukan oleh Martin B¨uchi. Penerapan metode B ini menggunakan alat bantu Atelier B. Hasil penerapan refinement dengan metode B pada studi kasus aplikasi perbankan itu menguatkan bahwa penerapan metodologi formal pada suatu aplikasi dapat menjamin kebenaran aplikasi tersebut. Walaupun penerapan refinement dengan metode B membutuhkan lebih banyak biaya, aplikasi yang dihasilkan dapat dijamin bebas dari galat yang dapat mengakibatkan kerugian besar.