Model Formal

Model metode formal mencakup sekumpulan aktivitas yang membawa kepada spesifikasi matematis perangkat lunak komputer. Metode formal memungkinkan perekayasa perangkat lunak untuk mengkhususkan, mengembangkan, dan memverifikasi system berbasis computer dengan menggunakan notasi matematis yang tepat. Variasi didalam pendekatan ini, disebut juga clean-room rekayasa perangkat lunak, sedang diaplikasikan oleh banyak organisasi pengembang perangkat lunak.

Bila metode formal dipakai selama masa pengembangan, metode itu memberika mekanisme untuk mengeliminasi banyak masalah yang sulit dipecahkan dengan menggunakan paradigma perangkat lunak yang lain. Ambiguitas, ketidaklengkapan, dan ketidak-konsistenan bisa ditemukan dan diperbaiki secara lebih mudah, tidak melalui kajian ad hoc tetapi melalui aplikasi analisis matematis. Jika metode formal dipakai selama masa perancangan, mereka berfungsi sebagai dasar verifikasi program sehingga memungkinkan perekayasa perangkat lunak untuk menemukan dan memperbaiki kesalahan yang mungkin saja tidak terdeteksi.

Meskipun belum menjadi pendekatan utama, model metode formal sudah menawarkan janji perangkat lunak yang bebas cacat/kesalahan, tetapi perhatian tentang kemampuan aplikasinya didalam lingkungan bisnis sudah mulai disuarakan:

1. Pengembangan model formal banyak memakan waktu dan mahal.
2. Karena beberapa pengembang perangkat lunak perlu mempunyai latar belakang yang diperlukan untuk mengaplikasikan metode formal, maka diperlukan pelatihan yang ekstensif.
3. Sulit untuk menggunakan model – model sebagai sebuah mekanisme komunikasi bagi pemakai yang secara teknik belum canggih.

Meskipun demikian, sepertinya metode formal ini akan memperoleh banyak penganut diantara pengembang perangkat lunak yang harus membangun perangkat lunak yang kritis untuk keselamatan (misalnya pengembang perangkat medis dan penerbangan pesawat), serta diantara pengembang yang harus menderita karena factor ekonomis yang harus dialami oeh perangkat lunak.