Dewasa ini proses pembuatan spesifikasi dan verifikasi perangkat lunak kurang begitu diperhatikan. Para pengembang sekarang ini lebih fokus kepada hasil akhir tanpa memperhatikan segala kemungkinan-kemungkinan yang tidak baik di kemudian hari. Proses pembuatan spesifikasi dan verifikasi-lah yang dapat menghindarkan pengguna perangkat lunak akibat kerugian yang akan ditanggungnya saat perangkat lunak tersebut mengalami kerusakan. Kerugian akibat kerusakan ini dibedakan menjadi dua yaitu kerugian langsung akibat rusaknya perangkat lunak tersebut dan kerugian biaya perbaikan perangkat lunak tersebut.
Lingu dan LinguSQL adalah suatu jawaban atas kebutuhan dukungan terhadap proses pembuatan spesifikasi dan verifikasi. Lingu yang merupakan bahasa spesifikasi, dapat digunakan untuk spesifikasi perangkat lunak yang dikhususkan pada aplikasi transaksi basis data. Sementara itu, LinguSQL adalah suatu alat verifikasi bahasa Lingu dengan berbantukan theorem prover HOL. Selain melakukan verifikasi LinguSQL juga dapat mentransformasikan bahasa Lingu menjadi bahasa Java.
Dalam tugas akhir ini akan digunakan studi kasus aplikasi perbankan dalam melakukan pembuatan spesifikasi dan pelaksanaan verifikasi terhadap perangkat lunak tersebut. Proses pembuatan spesifikasi dan verifikasi ini dijalankan dengan menggunakan Lingu dan LinguSQL. Setelah kegiatan tersebut dilakukan, selanjutnya proses pembuatan spesifikasi dan verifikasi yang dijalankan dengan menggunakan Lingu akan dibandingkan dengan Metode-B. Metode-B adalah bahasa spesifikasi yang sudah umum digunakan dalam melaksanakan proses pembuatan spesifikasi dan verifikasi terhadap perangkat lunak.
Hasil dari tugas akhir ini adalah kesimpulan tentang perbandingan antara Lingu dan LinguSQL dengan Metode-B dan Atelier-B. Dalam penelitian ini disimpulkan bahwa Lingu mempunyai fasilitas dukungan terhadap aplikasi basis data. Selain itu, Metode-B didapatkan juga terjamin handal untuk melakukan refinement terhadap suatu perangkat lunak.
Nowadays, software specification and verification process is still lacking. Recent developers turn focus more to result without emphasizing any negative possibilities that could be occured next time. However, specification and verification process is able to minimize software failure so that a financial loss caused by either missing functionality or software alteration cost can be reduced.
Lingu and Lingu SQL provide support for specification and verification process. Lingu is specification language for database transaction aplication purpose, while LinguSQL is Lingu's verification tool assisted by HOL theorem prover. In addition, LinguSQL transforms Lingu into Java programming language.
Research reported here used banking case study. Specification and verification process was run by using Lingu and LinguSQL. Then, result of this process was compared with similar one that had been executed by B-Metode, a previous research by Theresia (2005).
This final assignment produces a conclusion of the comparison between Lingu and B-method. Through this research, we conclude that Lingu has a supporting facility for an application that use database. Beside that, we also found that B-method is absolutely reliable for doing refinement on software.
