Teknik formal method adalah teknik yang mengandalkan perhitungan matematika dalam setiap prosesnya. Hanya digunakan pada sistem yang sangat memperhatikan keamanan atau keselamatan dari pengguna keamanan atau keselamatan dari pengguna. Contoh penggunaan teknik ini adalah aerospace engineering.Dalam ilmu komputer, rekayasa perangkat lunak khusus, metode formal adalah jenis tertentu dari teknik matematis berdasarkan untuk spesifikasi, pengembangan dan verifikasi sistem perangkat lunak dan perangkat keras. Penggunaan metode formal untuk perangkat lunak dan desain hardware dimotivasi oleh harapan bahwa , seperti dalam disiplin ilmu teknik lainnya, melakukan analisis matematis yang tepat dapat berkontribusi untuk keandalan dan ketahanan dari desain.
Metode formal digambarkan sebagai penerapan berbagai cukup luas fundamental ilmu komputer teoritis, dalam kalkuli logika tertentu, bahasa formal, teori automata, dan semantik program, tetapi juga sistem jenis dan tipe data aljabar untuk masalah dalam spesifikasi perangkat lunak dan perangkat keras dan verifikasi.
Metode formal dapat digunakan di sejumlah tingkatan:
Tingkat 0: spesifikasi formal dapat dilakukan dan kemudian program yang dikembangkan dari ini informal. Hal ini telah dijuluki metode formal lite. Ini mungkin menjadi pilihan biaya yang paling efektif dalam banyak kasus.
Tingkat 1: Pengembangan Formal dan verifikasi formal dapat digunakan untuk menghasilkan sebuah program dengan cara yang lebih formal. Misalnya, bukti dari sifat atau penyempurnaan dari spesifikasi untuk program dapat dilakukan. Ini mungkin yang paling tepat dalam sistem integritas tinggi yang melibatkan keselamatan atau keamanan.
Level 2: provers Teorema dapat digunakan untuk melakukan sepenuhnya resmi mesin-diperiksa bukti. Hal ini bisa sangat mahal dan hanya praktis berharga jika biaya kesalahan sangat tinggi (misalnya, dalam bagian-bagian penting dari desain mikroprosesor).
Informasi lebih lanjut mengenai hal ini diperluas di bawah ini.
Seperti dengan semantik bahasa pemrograman, gaya metode formal dapat secara kasar diklasifikasikan sebagai berikut:
Denotational semantik, di mana makna dari suatu sistem dinyatakan dalam teori matematika dari domain. Pendukung metode tersebut bergantung pada sifat dipahami dengan baik domain untuk memberi arti bagi sistem, kritikus menunjukkan bahwa tidak setiap sistem mungkin secara intuitif atau alami dipandang sebagai fungsi.
Operasional semantik, di mana makna dari suatu sistem dinyatakan sebagai urutan tindakan model (mungkin) komputasi sederhana. Pendukung metode tersebut menunjukkan kesederhanaan model mereka sebagai alat untuk kejelasan ekspresif, kritikus kontra bahwa masalah semantik baru saja tertunda (yang mendefinisikan semantik dari model sederhana?).
Aksiomatis semantik, dimana arti dari sistem dinyatakan dalam prasyarat dan postconditions yang benar sebelum dan setelah sistem melakukan tugas masing-masing. Para pendukung perhatikan koneksi ke logika klasik, kritik mencatat bahwa semantik seperti itu tidak pernah benar-benar menggambarkan apa yang sistem tidak (hanya apa yang benar sebelum dan sesudahnya).
Lightweight Formal Methods
Beberapa praktisi percaya bahwa masyarakat metode formal telah ditekankan formalisasi penuh spesifikasi atau desain. Mereka berpendapat bahwa ekspresi dari bahasa yang terlibat, serta kompleksitas sistem yang dimodelkan, membuat formalisasi penuh sulit dan tugas mahal. Sebagai alternatif, berbagai metode formal yang ringan, yang menekankan spesifikasi parsial dan aplikasi terfokus, telah diusulkan. Contoh dari pendekatan ringan untuk metode formal termasuk objek Alloy notasi pemodelan, sintesis Denney tentang beberapa aspek dari notasi Z dengan kasus pengembangan penggunaan didorong, dan CSK VDM Alat.
* Keuntungan menggunakan teknik formal method adalah :
(a) Meminimalkan resiko dengan adanya perhitungan komputasi.
* Sedangkan kerugiannya adalah :
(a) biaya tinggi
(b) kompleks
(c) Tidak Umum untuk Ptoyek software pada umumnya
Lightweight Formal Methods
Beberapa praktisi percaya bahwa masyarakat metode formal telah ditekankan formalisasi penuh spesifikasi atau desain. Mereka berpendapat bahwa ekspresi dari bahasa yang terlibat, serta kompleksitas sistem yang dimodelkan, membuat formalisasi penuh sulit dan tugas mahal. Sebagai alternatif, berbagai metode formal yang ringan, yang menekankan spesifikasi parsial dan aplikasi terfokus, telah diusulkan. Contoh dari pendekatan ringan untuk metode formal termasuk objek Alloy notasi pemodelan, sintesis Denney tentang beberapa aspek dari notasi Z dengan kasus pengembangan penggunaan didorong, dan CSK VDM Alat.
* Keuntungan menggunakan teknik formal method adalah :
(a) Meminimalkan resiko dengan adanya perhitungan komputasi.
* Sedangkan kerugiannya adalah :
(a) biaya tinggi
(b) kompleks
(c) Tidak Umum untuk Ptoyek software pada umumnya
0 komentar:
Posting Komentar