NIM : 22064163
Grup : B
Metrics for Formal Methods:
The ATC (Air –Traffic Control Information System) case study
1. Intoduction
Karena kualitas dan keandalan menjadi faktor yang penting dalam pengembangan perangkat lunak untuk meningkatkan persaingan bisnis dan peraturan persyaratan yang berbeda, banyak organisasi yang mempertimbangkan penggunaan metode formal sebagai bagian dari proses pengembangan software mereka. Menggunakan metode formal,sebuah implementasi software dapat ditampilkan secara kukuh untuk memenuhi spesifikasi.
Sebuah awal spesifikasi dapat dikembangkan secara formal menggunakan ketepatan matematika dan notasi logis dan spesifikasi ini akan ditampilkan secara konsisten dengan menunjukkan bukti kebenaran. Dalam laporan ini, penulis mempelajari isu-isu yang terlibat dalam menerapkan metode formal untuk pengembangan Air –Traffic Control Information System (ATC). Penulis menganalisis proyek dari metrik dan pengukuran perspektif, untuk menyelidiki pertanyaan seperti apakah metode formal berpengaruh pada kualitas akhir dari produk, dan apakah metode ini sebenarnya bisa menyimpan biaya pengembangan dibandingkan dengan pengembangan tradisional. Penulis melihat apakah manfaat dan kegunaan metode formal dibuat dalam analisis asli dari proyek ATC adalah benar dalam konteks teori pengukuran(measurement).
2. Latar Belakang
Laporan studi kasus ATC pada Display Information System dikembangkan oleh Praxis untuk UK Civil Aviation Authority (CAA). Sistem yang mereka kembangkan adalah subsistem dari Central Control Function (CCF) - sebuah sistem yang otomatis menawarkan dukungan untuk mengontrol lalu lintas udara.
Salah satu fungsi utama CCF adalah untuk menangani pendekatan urutan,menghasilkan dan memanipulasi urutan masuk utama untuk penerbangan bandara kompleks. CCF terdiri dari beberapa sistem:
• National Airspace System
• a radar system
• Airport Data Information Systems
• closed-circuit televisions
• CCF Display Information System (CDIS) – (subjek dari studi kasus ini)
CDIS bertanggung jawab untuk menampilkan informasi untuk mengatur lalu lintas udara. Kontrol yang berinteraksi dengan sistem untuk memilih informasi yang inginmereka lihat. Informasi yang ditampilkan meliputi:
• waktu kedatangan dan penerbangan
• kondidi cuaca
• status peralatan di Bandar udara
• informasi ke dalam sistem secara manual .Selain itu, controller yang mengatur
urutan masuk penerbangan menggunakan layar sentuh untuk langsung memanipulasi urutan melalui CDIS.
Gambar 1: Arsitektur CDIS
Gambar 1 menunjukkan arsitektur CDIS. Pada pusat CDIS adalah CCPS (CDIS Pusat Pengolahan Sistem), yang menangani komunikasi dengan sistem eksternal, data repositori, dan sistem kontrol. Stasiun control tersambung ke server melalui LAN.
Keputusan untuk menggunakan metode formal merupakan akibat langsung dari onfunctional
Persyaratan sistem:
• informasi harus ditampilkan dalam 1-2 detik setelah menerima
• ketersediaan 99,97%
• tidak boleh ada satu titik kegagalan
metode formal digunakan dalam spesifikasi, desain dan verifikasi. Besaran batas waktu untuk ukuran dan kompleksitas sistem, digunakan berbagai metode formal.
3. Analisa pada kasus ATC
ATC merupakan proyek yang bagus untuk studi kasus - hal ini sesuai situasi kehidupan nyata, dan jangka waktu yang cukup panjang. Penulis ingin mempelajari efek dari metode formal pada akhir kualitas produk, juga jika sebagai metode praktis dan manfaatnya dapat diterapkan secara kehidupan nyata proyek-proyek berskala besar. Untuk menjawab pertanyaan tersebut, sesuai kesalahan dan kegagalan data, serta upaya dikeluarkan pada tahapan pembangunan yang berbeda, dikumpulkan sepanjang proyek. Data kemudian dianalisa sebagai upaya untuk membantu menjawab pertanyaan.
Untuk mendukung hal ini, penulis membandingkan metrik dari proyek dengan proyek-proyek serupa. Kesimpulan utama adalah:
1. Lebih efektif dibandingkan proyek serupa. Proyek menghasilkan
rata-rata 13 baris kode disampaikan per hari.
2. Produk yang telah disampaikan punya kesalahan lebih sedikit dibandingkan produk sejenis. Hanya ada 0,75 kesalahan per kloc dilaporkan selama 20 bulan penggunaan pertama.
Untuk point 1, perbandingan dibuat terhadap COCOMO, yang dapat dilihat
sebagai dasar umum. Namun, untuk proyek yang diberikan, tidak jelas hasil apa yang berbeda dari saran COCOMO. Perbedaan mungkin disebabkan oleh proses perangkat lunak, staf, organisasi, jenis proyek, atau bahkan penggunaan metode formal. Perbedaan mungkin juga karena faktor subjektif, seperti bagaimana berbagai aspek organisasi dan proyek dievaluasi dalam formula COCOMO.
Selain itu, dalam praktiknya ada sedikit bukti untuk menunjukkan bahwa eksponen dalam formula COCOMO berbeda dari CDIS. Misalnya, dianalisa tujuh
set data yang berbeda, dan menemukan bahwa hanya 1 perbedaan dari 1 atau lebih daripada 0.5. Sebaliknya, COCOMO menyatakan bahwa adalah suatu eksponen antara
1,12 dan 1,20 untuk sebuah proyek dari jenis ini. Konstan yang tepat digunakan untuk
COCOMO perbandingan tidak diberikan dalam laporan. Untuk point 2, merujuk kepada laporan, yang luar biasa, tingkat kesalahan dalam safetycritical sistem. Sekali lagi, tidak jelas jika hasil yang berbeda adalah karena penggunaan formal atau metode yang lain. Namun, dapat disimpulkan bahwa kesalahan harga sangat rendah. Ini mungkin, setidaknya di bagian, karena yang akan penggunaan metode formal, dan menjamin penelitian lebih lanjut.
Table 1: Effort pada tahap pengembangan proyek CDIS dibandingkan COCOMO
4. Kesimpulan
Hasil Praxis dari pengembangan system informasi ATC menunjukkan bahwa sistem metode formal dapat digunakan pada kehidupan nyata, proyek-proyek industri. Namun, tidak ada bukti kuantitatif yang yang bertanggung jawab untuk meningkatkan kualitas kode dan keandalan sistem. Kemungkinan besar, ini merupakan kombinasi dari metode formal dengan informal, serta persyaratan analisis, yang hasilnya lebih tinggi dalam kualitas kode.
sumber:Metrics for formal methods:The ATC case study
Tommy Staffans, Andreas Enbacka
Department of Computer Science
Abo Akademi University December 2004
1 komentar:
pertamax
Posting Komentar