REKAYASA PERANGKAT LUNAK
Spesifikasi Formal
MUHLIS TAHIR 092904033 PTIK A 2009
TUJUAN :
Untuk menjelaskan mengapa teknik spesifikasi formal membantu menemukan masalah dalam persyaratan sistem
Untuk
menggambarkan
penggunaan
teknik
aljabar
untuk
spesifikasi antarmuka
Untuk menggambarkan penggunaan teknik berbasis model untuk spesifikasi perilaku
TOPIK YANG DIBAHAS : •
Spesifikasi formal dalam proses perangkat lunak
•
Sub-sistem spesifikasi interface
•
Perilaku spesifikasi
METODE FORMAL
Spesifikasi formal merupakan bagian dari koleksi yang lebih umum
teknik yang dikenal sebagai 'metode formal'.
Ini semua didasarkan pada representasi matematis dan analisis perangkat lunak.
Metode formal termasuk
Spesifikasi formal;
Spesifikasi analisis dan bukti;
Transformasional pembangunan;
Program verifikasi.
PENERIMAAN METODE FORMAL
Metode formal belum menjadi mainstream teknik pengembangan perangkat
lunak seperti yang pernah diperkirakan
Perangkat lunak lain rekayasa teknik telah berhasil meningkatkan kualitas sistem. Karena itu membutuhkan metode formal telah berkurang;
Perubahan pasar telah membuat waktu-ke-pasar bukan perangkat lunak dengan kesalahan rendah menghitung faktor kunci. Metode formal tidak mengurangi waktu ke pasar;
Ruang lingkup metode formal terbatas. Mereka tidak cocok untuk menentukan dan menganalisis user interface dan interaksi pengguna;
Metode formal masih sulit untuk skala sampai dengan sistem yang besar.
PENGGUNAAN METODE FORMAL
Manfaat utama dari metode formal dalam mengurangi jumlah kesalahan
pada sistem.
Akibatnya, daerah utama mereka diterapkan dalam rekayasa sistem kritis. Ada beberapa proyek yang berhasil di mana metode formal telah
digunakan di daerah ini.
Di daerah ini, penggunaan metode formal yang paling mungkin untuk biaya-biaya sistem efektif karena kegagalan yang tinggi harus dihindari.
SPESIFIKASI DALAM PROSES PERANGKAT LUNAK •
Spesifikasi dan desain erat bercampur.
•
Desain arsitektur sangat penting untuk struktur spesifikasi dan proses spesifikasi.
•
Spesifikasi formal dinyatakan dalam notasi matematika
dengan tepat didefinisikan, sintaks dan semantik kosakata.
SPESIFIKASI DAN DESAIN
PESIFIKASI DALAM PROSES PERANGKAT LUNAK
PENGGUNAAN SPESIFIKASI FORMAL
Spesifikasi formal melibatkan investasi lebih banyak upaya dalam fase awal pengembangan perangkat lunak.
Hal ini mengurangi kesalahan persyaratan sebagai memaksa analisis rinci tentang persyaratan.
Ketidaklengkapan
dan
inkonsistensi
dapat
ditemukan
dan
diselesaikan.
Oleh karena itu, tabungan yang dibuat sebagai jumlah pengerjaan ulang karena masalah persyaratan berkurang.
BIAYA PROFIL
Penggunaan spesifikasi formal berarti bahwa profil biaya sebuah perubahan proyek
Ada biaya depan lebih besar sebagai lebih banyak waktu dan usaha yang dihabiskan mengembangkan spesifikasi;
Namun, pelaksanaan dan validasi biaya harus dikurangi sebagai proses spesifikasi mengurangi kesalahan dan ambiguitas dalam persyaratan.
BIAYA PENGEMBANGAN DENGAN SPESIFIKASI FORMAL
SPESIFIKASI TEKNIK
Spesifikasi aljabar
Sistem ini ditetapkan dalam hal operasi dan hubungan mereka.
Model berbasis spesifikasi
Sistem ini ditetapkan dalam hal model negara yang dibangun menggunakan konstruksi matematika seperti set dan urutan. Operasi didefinisikan oleh modifikasi negara sistem.
FORMAL SPESIFIKASI BAHASA
SPESIFIKASI INTERFACE o
Sistem yang besar dipecah menjadi subsistem dengan antarmuka yang terdefinisi dengan baik antara subsistem.
o
Spesifikasi antarmuka subsistem memungkinkan pengembangan independen dari subsistem yang berbeda.
o
Interface dapat didefinisikan sebagai tipe data abstrak atau kelas objek.
o
Pendekatan aljabar untuk spesifikasi formal sangat cocok untuk antarmuka spesifikasi seperti yang difokuskan pada operasi didefinisikan dalam suatu objek.
SUB-SISTEM ANTARMUKA
STRUKTUR SPESIFIKASI ALJABAR
SPESIFIKASI KOMPONEN
Pengantar
Mendefinisikan jenis (nama jenis) dan menyatakan spesifikasi lainnya yang digunakan.
Deskripsi
Informal menjelaskan operasi pada jenis.
Tanda tangan
Mendefinisikan sintaks dari operasi dalam antarmuka dan parameter mereka.
Aksioma
Mendefinisikan semantik operasi dengan mendefinisikan aksioma yang mencirikan perilaku.
SISTEMATIS ALJABAR SPESIFIKASI
Spesifikasi aljabar suatu sistem dapat dikembangkan secara sistematis
Spesifikasi penataan;
Spesifikasi penamaan;
Operasi seleksi;
Informal operasi spesifikasi;
Sintaks definisi;
Definisi aksioma.
SPESIFIKASI OPERASI
Pembuat operasi. Operasi yang menciptakan entitas dari jenis yang ditentukan.
Inspeksi operasi. Operasi yang mengevaluasi entitas dari jenis yang ditentukan.
Untuk menetapkan perilaku, menentukan inspektur operasi untuk setiap operasi konstruktor.
OPERASI PADA DAFTAR ADT
Pembuat operasi yang mengevaluasi untuk mengurutkan Daftar
Membuat, Kontra dan Tail.
Pemeriksaan operasi yang mengambil daftar semacam sebagai parameter dan pengembalian semacam lainnya
Kepala dan Panjang.
Ekor dapat didefinisikan dengan menggunakan konstruktor yang sederhana? Membuat dan Cons. Tidak perlu mendefinisikan Kepala dan Panjang dengan Tail.
DAFTAR SPESIFIKASI
REKURSI DALAM SPESIFIKASI
Operasi sering ditentukan secara rekursif.
Ekor (Cons (L, v)) = jika L = Buat kemudian Buat? lain Cons (Tail (L), v).
Kontra ([5, 7], 9) = [5, 7, 9]
Ekor ([5, 7, 9]) = Tail (Cons ([5, 7], 9)) =
Kontra (Tail ([5, 7]), 9) = Cons (Tail (Kekurangan ([5], 7)), 9) =
Kontra (Cons (Ekor ([5]), 7), 9) =
Kontra (Cons (Ekor (Kekurangan ([], 5)), 7), 9) =
Kontra (Cons ([Buat], 7), 9) = Cons ([7], 9) = [7, 9]
INTERFACE SPESIFIKASI SISTEM KRITIS
Pertimbangkan sebuah sistem kontrol lalu lintas udara di mana
pesawat terbang melalui sektor dikelola wilayah udara.
Setiap sektor dapat mencakup sejumlah pesawat tetapi, untuk alasan keamanan, ini harus dipisahkan.
Dalam contoh ini, pemisahan vertikal sederhana 300m diusulkan.
Sistem tersebut harus memperingatkan controller jika pesawat diinstruksikan untuk bergerak sehingga pemisahan aturan dilanggar.
SEBUAH OBJEK SEKTOR
operasi Kritis pada objek yang mewakili sektor yang dikendalikan
Enter. Tambahkan pesawat udara ke wilayah udara yang
dikendalikan;
Tinggalkan. Hapus pesawat terbang dari wilayah udara yang dikendalikan;
Pindah. Memindahkan pesawat dari satu ketinggian ke yang lain;
Lookup. Mengingat pesawat identifier, kembali tinggi saat ini;
PRIMITIF OPERASI
Hal ini kadang diperlukan untuk memperkenalkan operasi tambahan untuk menyederhanakan spesifikasi.
Operasi lain maka dapat didefinisikan menggunakan operasi yang lebih primitif.
Primitif operasi
Buat. Bawa sebuah instance dari suatu sektor menjadi ada;
Put. Tambahkan pesawat tanpa pemeriksaan keamanan;
Dalam-ruang. Menentukan apakah sebuah pesawat yang diberikan dalam sektor ini;
Pendudukan. Mengingat ketinggian, menentukan apakah ada pesawat dalam ketinggian 300m itu.
SEKTOR SPESIFIKASI (1)
SEKTOR SPESIFIKASI (2)
SPESIFIKASI KOMENTAR
Gunakan konstruktor dasar Buat dan Pasang untuk menentukan operasi lainnya.
Tentukan Pendudukan dan In-ruang angkasa yang menggunakan Membuat dan Pasang dan gunakan mereka untuk membuat cek dalam definisi operasi lain.
Semua operasi yang mengakibatkan perubahan sektor ini harus memeriksa bahwa kriteria keselamatan berlaku.
PERILAKU SPESIFIKASI
Aljabar spesifikasi bisa rumit ketika operasi objek tidak independen dari negara objek.
Spesifikasi Model berbasis memperlihatkan keadaan sistem dan
mendefinisikan operasi dalam hal perubahan ke negara itu.
Notasi Z adalah teknik matang untuk spesifikasi model yang berbasis. Ini menggabungkan deskripsi formal dan informal dan
menggunakan grafis menyoroti saat menyajikan spesifikasi.
STRUKTUR DARI SEBUAH SKEMA Z
PEMODELAN POMPA INSULIN
Skema Z untuk pompa insulin menyatakan sejumlah variabel negara termasuk:
Input
variabel
seperti
switch?
(saklar
perangkat),
InsulinReservoir? (jumlah saat ini insulin dalam reservoir) dan Membaca? (pembacaan dari sensor);
Output variabel seperti alarm! (alarm system), display1, display2! (menampilkan pada pompa) dan dosis! (dosis insulin
akan dikirimkan).
SKEMA INVARIAN •
Setiap skema Z memiliki bagian invarian yang mendefinisikan kondisi yang selalu benar.
•
Untuk skema pompa insulin itu selalu benar bahwa
Dosis harus kurang dari atau sama dengan kapasitas reservoir insulin;
Tidak ada dosis tunggal bisa lebih dari 4 unit insulin dan total dosis disampaikan dalam jangka waktu tidak boleh melebihi 25 unit insulin. Ini adalah kendala keamanan;
Display2! menunjukkan jumlah insulin akan dikirimkan.
POMPA INSULIN SKEMA
NEGARA INVARIANTS
PERHITUNGAN DOSIS
Pompa insulin menghitung jumlah insulin yang diperlukan dengan membandingkan saat ini dengan membaca dua bacaan sebelumnya.
Jika ini menunjukkan bahwa glukosa darah meningkat maka insulin disampaikan.
Informasi tentang dosis total dikirimkan dipertahankan untuk memungkinkan
invariant
pengecekan
keamanan
yang
akan
diterapkan.
Perhatikan bahwa invarian ini selalu berlaku - tidak perlu mengulang dalam perhitungan dosis.
LARI SKEMA (1)
LARI SKEMA (2)
GULA OK SKEMA
HAL-HAL PENTING
Spesifikasi sistem formal melengkapi spesifikasi teknik informal.
Spesifikasi formal tepat dan jelas. Mereka menghapus bidang keraguan dalam spesifikasi.
Spesifikasi formal kekuatan analisis kebutuhan sistem pada tahap awal. Mengoreksi kesalahan pada tahap ini lebih murah daripada memodifikasi sistem disampaikan.
Spesifikasi
teknik
formal
yang
paling
pengembangan sistem kritis dan standar.
diterapkan
dalam
HAL-HAL PENTING
Teknik aljabar cocok untuk antarmuka spesifikasi antarmuka mana didefinisikan sebagai satu set kelas objek.
Model-model teknik berdasarkan sistem dengan menggunakan set dan fungsi. Ini menyederhanakan beberapa jenis spesifikasi perilaku.
Operasi
didefinisikan
dalam
model
berbasis
spec.
dengan
mendefinisikan kondisi sebelum dan sesudah pada keadaan sistem.
SEKIAN DAN TERIMA KASIH
