Bagaimana kita tahu bahwa metode formal berfungsi?

Tujuan penting dari metode formal adalah untuk membuktikan kebenaran sistem, baik dengan cara otomatis atau yang diarahkan manusia. Namun, tampaknya bahkan jika Anda dapat memberikan bukti kebenaran, Anda TIDAK mungkin dapat menjamin bahwa sistem tidak akan gagal. Sebagai contoh:

• Spesifikasi mungkin tidak memodelkan sistem dengan benar, atau sistem produksi mungkin terlalu rumit untuk dimodelkan, atau sistem mungkin cacat secara inheren karena persyaratan yang bertentangan. Teknik apa yang diketahui untuk menguji apakah suatu spesifikasi masuk akal sama sekali?
• Proses pembuktian mungkin juga cacat! Siapa yang tahu bahwa aturan inferensi itu benar dan sah? Selain itu, buktinya bisa sangat besar, dan bagaimana kita tahu mereka tidak mengandung kesalahan? Ini adalah jantung dari kritik di de Millo, Lipton, dan Perlis "Proses Sosial dan Bukti Teorema dan Program". Bagaimana para peneliti metode formal modern merespons kritik ini?
• Saat runtime, ada banyak kejadian dan faktor nondeterministik yang dapat secara serius mempengaruhi sistem. Sebagai contoh, sinar kosmik dapat mengubah RAM dengan cara yang tidak dapat diprediksi, dan lebih umum kami tidak memiliki jaminan bahwa perangkat keras tidak akan mengalami kesalahan Bizantium, yang telah terbukti Lamport sangat sulit untuk dikuatkan. Jadi kebenaran sistem statis tidak menjamin sistem tidak akan gagal! Apakah ada teknik yang diketahui bertanggung jawab atas kesalahan perangkat keras yang sebenarnya?
• Saat ini, pengujian adalah alat paling penting yang kami miliki untuk menetapkan bahwa perangkat lunak berfungsi. Sepertinya itu harus menjadi alat pelengkap dengan metode formal. Namun, saya kebanyakan melihat penelitian yang berfokus pada metode formal atau pengujian. Apa yang diketahui tentang menggabungkan keduanya?

Mengenai 4: Ada banyak pekerjaan yang menggabungkan metode formal dan pengujian. "Pengujian metode formal" Google mengungkapkan pekerjaan yang cukup besar. Meskipun ada banyak tujuan berbeda dari pekerjaan tersebut, salah satu tujuan utama adalah untuk menghasilkan ruang tes yang lebih efektif. Pembicaraan ini memberikan pengantar yang bagus, berdasarkan pengecekan model.

Juga mengenai masalah keamanan perangkat lunak , yang telah diedit dari pertanyaan: metode formal perlu bekerja lebih keras untuk disampaikan di ranah itu. Biasanya seseorang menulis spesifikasi untuk perangkat lunak dan memverifikasi bahwa spesifikasi terpenuhi, yaitu, ketika input memenuhi prasyarat bahwa output memenuhi postkondisi. Untuk memastikan perangkat lunak yang aman, orang juga perlu memeriksa juga bahwa perangkat lunak berperilaku bijaksana untuk input yang tidak memenuhi persyaratan. (Ini tentu saja setara dengan pengaturan prasyarat menjadi true untuk semua input.) Ruang semua input biasanya jauh lebih besar dari sekadar input yang dibentuk dengan baik, tetapi biasanya ini adalah satu tempat di mana bahkan perangkat lunak yang berfungsi secara fungsional dapat dilanggar, hanya dengan melanggar asumsinya.

Mengenai poin 3: Beberapa pekerjaan telah dilakukan untuk memverifikasi sistem dalam pengaturan di mana kesalahan dimodelkan secara eksplisit, termasuk Kesalahan Logika: Penalaran Tentang Program toleran-kesalahan. Matthew Meola dan David Walker. Simposium Eropa tentang Pemrograman, 2010. Bekerja pada pengecekan model probabilistik dan verifikasi probabilistik tentunya keduanya juga menangani masalah kesalahan sampai tingkat tertentu.

Urutan poin Anda:

• Kebenaran semua spesifikasi pada akhirnya bersifat subyektif: mereka dianggap mampu memecahkan masalah dengan benar menurut penggunanya atau tidak. Tidak ada jalan keluar dari ini pengembangan perangkat lunak, dan tidak ada metode yang memiliki peluru perak untuk yang satu ini.
• Banyak pekerjaan membuktikan bahwa prosesnya benar sehubungan dengan asumsinya. Biasanya ada informasi yang tersedia bagi para ahli untuk memvalidasi aturan-aturan ini. Setiap aktivitas manusia dapat mengalami kesalahan tetapi sistem yang sangat formal yang menggunakan pendekatan yang dipelajari dengan baik jauh lebih sedikit mengalami kesalahan daripada hampir semua proses manusia lainnya.
• Pada titik tertentu, sistem apa pun memiliki mode kegagalan di luar ruang lingkup sistem itu. Anda masih lebih baik menghilangkan semua sumber kesalahan yang dapat diprediksi , bahkan jika Anda membiarkan beberapa sumber yang tidak dapat diprediksi tidak ditemukan.
• Menguji dan membuktikan dapat dengan mudah hidup berdampingan. Pengujian adalah proses yang kurang spesifik, lebih ad hoc , sehingga Anda mungkin menemukan lebih sedikit pekerjaan formal yang dilakukan. Tetapi Anda mungkin tertarik pada alat seperti QuickCheck yang melengkapi dengan menguji bukti yang ditawarkan oleh sistem jenis Haskell.

Metode formal telah terbukti berhasil dengan sangat baik. Tanpa mereka, kita tidak akan mampu mengatasi kompleksitas merancang sistem digital modern (mikroprosesor).

Tidak ada kapal mikro tanpa logikanya yang tunduk pada verifikasi kesetaraan fungsional; tanpa FPU yang menjadi subjek FV; tanpa protokol koherensi cache yang menjadi sasaran FV (ini telah terjadi sejak 1995).

Kecuali perbedaan yang jelas antara perangkat lunak dan sistem fisik yang direkayasa (misalnya jembatan, tempat seseorang dapat menambahkan faktor keamanan), mereka memainkan peran matematika teknik dalam CS. Namun, penggunaan FM selalu tergantung pada manfaat / biaya. Pengujian fuzz memberi hasil besar di perusahaan-perusahaan seperti Microsoft (Google SAGE dalam satu slide).

Bahkan di dalam mikro, terdapat subsistem (mis. Pipeline mikroprosesor), di mana FV tidak memiliki dampak yang sama seperti di tempat lain (misalnya FPU, di mana pengujian konvensional tidak dilakukan sama sekali dalam banyak kasus ketika evaluasi lintasan simbolik formal membuktikan tidak adanya bug. : Kaivola et al CAV'09).

Metode formal juga digunakan dalam sintesis artefak (kode, tes berkualitas tinggi, jadwal untuk menguras bank baterai secara optimal, ...). Tentu saja, semua masalah yang diangkat dalam pertanyaan cukup valid, dan seperti dalam penggunaan teknologi lainnya, iklan palsu harus dikenali dan dihindari.

Mengenai 2: jika sistem diformalkan dalam asisten bukti (misalnya, Twelf atau Agda atau Coq) dan sifat kesehatan dan kelengkapan diverifikasi, dan bukti dilakukan dalam pengkodean ini, ini bukan masalah. Anda mungkin telah memformalkan suatu sistem yang tidak menggambarkan apa yang Anda maksudkan, tetapi setidaknya Anda tidak akan memiliki bukti yang salah atau sistem yang rusak di mana Anda beralasan.

Namun, tampaknya bahkan jika Anda dapat memberikan bukti kebenaran, Anda TIDAK mungkin dapat menjamin bahwa sistem tidak akan gagal.

Ya, mungkin tidak ada jaminan . Metode formal dimaksudkan untuk menemukan dan menghilangkan kesalahan dan untuk meyakinkan manusia.

Teknik apa yang diketahui untuk menguji apakah suatu spesifikasi masuk akal sama sekali?

Anda mungkin tertarik pada alat pengecekan model untuk spesifikasi sistem formal .

Proses pembuktian mungkin juga cacat! Siapa yang tahu bahwa aturan inferensi itu benar dan sah?

Saya pikir (karena teorema ketidaklengkapan Goedel) menunjukkan sistem aturan inferensi secara konsisten tentu menarik bagi seperangkat aturan inferensi yang bahkan lebih kuat.

Selain itu, buktinya bisa sangat besar, dan bagaimana kita tahu bahwa mereka tidak mengandung kesalahan?

Mudah-mudahan, bukti besar diperiksa oleh pemeriksa bukti kecil yang dapat dibaca dan dipahami oleh manusia dalam jumlah waktu yang wajar. Ini kadang-kadang disebut "kriteria de Bruijn". Jika Anda percaya bahwa pemeriksa bukti tidak akan mengesahkan bukti yang salah, Anda hanya perlu memeriksa pemeriksa.

Apakah ada teknik yang diketahui bertanggung jawab atas kesalahan perangkat keras yang sebenarnya?

Bagaimana dengan bahasa assembly yang diketik dari kesalahan toleransi ?

Namun, saya kebanyakan melihat penelitian yang berfokus pada metode formal atau pengujian. Apa yang diketahui tentang menggabungkan keduanya?

"Konferensi TAP dikhususkan untuk konvergensi bukti dan tes" .

Hanya googling untuk "bukti dan tes" memiliki beberapa hit yang baik di atas flip.

Teknik apa yang diketahui untuk menguji apakah suatu spesifikasi masuk akal sama sekali?

Ini jelas merupakan panggilan penilaian. Dalam rekayasa perangkat lunak, orang telah merancang metodologi yang sangat ketat untuk menemukan / menulis / mengkonfirmasi spesifikasi. Ini dilakukan oleh manusia nyata dan menggunakan non formal (dalam arti non matematis proses), sehingga masih tunduk pada inkonsistensi, tetapi pada akhirnya, itu sesuai dengan apa yang orang ingin verifikasi, tidak lebih tidak kurang.

Apakah ada teknik yang diketahui bertanggung jawab atas kesalahan perangkat keras yang sebenarnya?

Tentu, ada bidang verifikasi yang dikenal sebagai verifikasi runtime , Anda juga dapat menggunakan model pengecekan berbasis eksekusi pada sistem nyata yang berjalan pada lingkungan yang benar-benar virtual yang tunduk pada skenario tertentu (saya berkontribusi sendiri untuk ini dengan V-DS + APMC ). Namun, ini jelas merupakan masalah besar untuk menambahkan interaksi antara sistem dan lingkungan ke dalam proses verifikasi.

Namun, saya kebanyakan melihat penelitian yang berfokus pada metode formal atau pengujian. Apa yang diketahui tentang menggabungkan keduanya?

Wow, hari ini aku akan benar-benar tak tahu malu dan mengutip diriku lagi. Dengan penulis bersama kami berupaya menggabungkan pemeriksaan dan pengujian model, Anda dapat melihat daftar publikasi mantan mahasiswa PhD grup kami atau mencari "perkiraan model probabilistik" atau "pengecekan model statistik" di mesin pencari yang baik (pekerjaan yang dilakukan oleh Younes dkk., Sen dkk. Atau saya sendiri dkk. Dan banyak lainnya).

Anda mungkin sangat tertarik dengan karya-karya John Rushby , salah satu perancang pepatah teorema PVS, yang secara umum tertarik pada persis poin yang Anda sebutkan. Anda dapat menikmati membaca laporan klasik ini kepada FAA tentang penggunaan Metode Formal dan Sertifikasi Sistem Kritis (1993) , dan tulisan - tulisannya yang lebih baru tentang menyusun kasus keselamatan formal probabilistik dari berbagai cara bukti yang disediakan (pengujian, bukti, analisis, dll).