Bagaimana Cara Membuat Perangkat Lunak Misi Penting?

Saya belajar sendiri metode formal. Saya mendengar bahwa metode formal digunakan (dan biasanya hanya digunakan) untuk membuat perangkat lunak misi kritis (seperti pengontrol reaktor nuklir, pengontrol penerbangan pesawat, pengontrol penyelidikan luar angkasa). Itu sebabnya saya tertarik untuk mempelajarinya: hlm

Namun, setelah mempelajari metode formal (terutama LTL, CTL dan saudara kandung mereka), saya merasa bahwa mereka hanya dapat digunakan untuk memverifikasi kebenaran spesifikasi (keamanan, liveness, keadilan, dll).

Tetapi bagaimana cara memverifikasi bahwa perangkat lunak (tidak hanya spesifikasinya) memang benar?

Penafian: Saya idiot 90% dalam hal ilmu komputer teoretis. Jadi tolong berbelas kasihan saat menjawab.

Pertanyaannya agak luas. Untuk menjawabnya di ruang yang masuk akal saya akan membuat banyak penyederhanaan yang berlebihan.

Mari kita sepakat tentang terminologi. Suatu program benar ketika menyiratkan spesifikasinya. Pernyataan tidak jelas ini dibuat tepat dalam banyak hal, dengan menjabarkan apa sebenarnya program dan apa sebenarnya spesifikasi. Misalnya, dalam pengecekan model program adalah struktur Kripke dan spesifikasinya sering berupa formula LTL . Atau, program ini dapat berupa daftar petunjuk PowerPC dan spesifikasinya dapat berupa serangkaian pernyataan Hoare-Floyd yang ditulis dalam, katakanlah, logika urutan pertama. Ada banyak variasi yang memungkinkan. Sangat menggoda untuk menyimpulkan bahwa dalam satu kasus (struktur Kripke) kami tidak memverifikasi program yang sebenarnya, sementara dalam kasus kedua (daftar instruksi PowerPC) kami lakukan. Namun, penting untuk menyadari bahwa kami benar-benar melihat model matematika dalam kedua kasus, dan ini sangat baik. (Situasinya sangat mirip dengan fisika di mana, misalnya, mekanika klasik adalah model realitas matematika.)

Kebanyakan formalisasi membedakan antara sintaks dan semantik program; yaitu, bagaimana itu diwakili dan apa artinya. Semantik suatu program adalah apa yang diperhitungkan dari sudut pandang verifikasi program. Tetapi, tentu saja penting untuk memiliki cara yang jelas dalam memberikan makna pada (representasi sintaksis) program. Dua cara populer adalah sebagai berikut:

• (langkah kecil) semantik operasional : Ini sangat mirip dengan mendefinisikan bahasa pemrograman dengan menulis penerjemah untuk itu. Untuk ini, Anda perlu mengatakan apa statusnya , dan itu dipengaruhi oleh setiap pernyataan dalam bahasa tersebut. (Anda mungkin bertanya-tanya dalam bahasa apa Anda menulis penerjemah, tetapi saya akan berpura-pura tidak.)
• semantik aksiomatik : Di sini setiap tipe pernyataan dilengkapi dengan skema aksioma. Jadi, kira-kira, setiap kali pernyataan tertentu dari jenis itu digunakan, itu diterjemahkan untuk dapat menggunakan aksioma tertentu. Misalnya, tugas datang dengan skema { P [ x / e ] ${\bf x}:={\bf e}$ ; penugasan khusus x : = x + 1 dilengkapi dengan aksioma { x + 1 = 1 $\{P[{\bf x}/{\bf e}]\}\,{\bf x}:={\bf e}\,\{P\}$$x:=x+1$ jika kita instantiate skema dengan P = ( x = 1 ) .$\{x+1=1\}\,x:=x+1\,\{x=1\}$$P=(x=1)$

(Ada yang lain. Saya merasa sangat buruk karena menghilangkan semantik denotasional, tetapi jawaban ini sudah lama.) Kode mesin ditambah semantik operasional cukup dekat dengan apa yang oleh kebanyakan orang disebut 'program nyata'. Berikut ini adalah makalah seminal, yang kebetulan menggunakan semantik operasional untuk subset kode mesin DEC Alpha:

• Necula, Lee, Proof-Carrying Code , 1996

Mengapa Anda pernah menggunakan semantik tingkat tinggi, seperti yang aksiomatik? Ketika Anda tidak ingin bukti kebenaran bergantung pada perangkat keras tempat Anda menjalankannya. Pendekatannya kemudian adalah untuk membuktikan kebenaran suatu algoritma sehubungan dengan beberapa semantik tingkat tinggi yang nyaman, dan kemudian membuktikan bahwa semantik terdengar sehubungan dengan semantik tingkat rendah yang lebih dekat dengan mesin yang sebenarnya.

Singkatnya, saya bisa memikirkan tiga alasan yang mengarah pada pertanyaan Anda:

1. Anda hanya melihat semantik tingkat tinggi yang tidak terlihat seperti apa yang biasa Anda sebut program, dan Anda bertanya-tanya apakah ada yang tingkat rendah. Jawabannya iya.
2. Anda bertanya-tanya bagaimana Anda membuktikan bahwa model sesuai dengan kenyataan. Seperti dalam fisika, Anda tidak. Anda cukup membuat model yang lebih baik dan memeriksanya dengan kenyataan.
3. Anda belum melihat perbedaan antara sintaks dan semantik, dan berbagai cara untuk memberi makna pada program. Dua pertanyaan sebelumnya berisi beberapa buku.

Jawaban ini hanya mencoba mengidentifikasi tiga cara berbeda di mana saya memahami pertanyaan itu. Masuk jauh ke salah satu poin ini akan membutuhkan banyak ruang.

Salah satu pendekatan untuk mengurangi kesenjangan antara suatu program dan spesifikasinya adalah menggunakan bahasa dengan semantik formal. Contoh yang menarik di sini adalah Esterel . Lihatlah halaman web Gérard Berry untuk beberapa pembicaraan menarik tentang karyanya yang membawa metode formal ke dunia nyata. http://www-sop.inria.fr/members/Gerard.Berry/

ps Sudah di Airbus? Anda telah terbang dengan metode formal!

Ilmu membangun perangkat lunak yang dapat diandalkan di "dunia nyata" masih sedang dikembangkan dan sedikit banyak mendekati studi budaya atau antropologis yang inheren, karena komputer dan perangkat lunak tidak "menyebabkan" bug — manusia memang! jawaban ini akan fokus pada pendekatan T / J umum yang verifikasi perangkat lunak formal dapat dilihat sebagai satu elemen.

pengamatan yang luar biasa adalah bahwa seringkali perangkat lunak yang "cukup baik" namun "kereta" sering kali dapat menjual lebih baik perangkat lunak yang lebih baik diuji tetapi fungsionalitasnya lebih rendah di pasar. dengan kata lain, pasar tidak selalu mengutamakan kualitas perangkat lunak dan teknik rekayasa perangkat lunak modern, yang tidak selalu menekankan kualitas, agak mencerminkan hal itu. apalagi kualitas sering dapat menambah biaya yang signifikan untuk produk akhir. dengan peringatan itu, berikut adalah beberapa dasar-dasarnya:

• sistem redundan / toleran kesalahan. ini adalah bidang studi yang luas. toleransi kesalahan & redundansi dapat dirancang ke dalam banyak lapisan sistem. misalnya router, server, disk drive, dan sebagainya.

• pengujian . semua jenis— pengujian unit, pengujian integrasi, pengujian penerimaan pengguna, pengujian regresi, dll.

• sekarang pengujian otomatis melalui test suites yang dapat dijalankan tanpa pengawasan lebih berkembang / penting. suite tes yang sedang berjalan sering digabungkan dengan alat bangun.

• konsep penting dalam pengujian adalah cakupan kode . yaitu kode apa dijalankan oleh tes. tes tidak dapat menemukan bug dalam kode yang tidak "disentuh" ​​oleh tes.

• konsep kunci lain dalam pengujian adalah test harnessess yang kode latihan yang tidak mudah diakses secara langsung.

• tes harus melatih semua level perangkat lunak. jika perangkat lunak dimodulasi dengan baik, ini tidak sulit. tes tingkat yang lebih tinggi harus menembus jauh ke dalam kode. tes yang menggunakan sejumlah besar kode dengan pengaturan tes kecil meningkatkan "leverage uji" .

• membuat kode seminimal mungkin mungkin penting untuk pengujian. pengujian harus menjadi pertimbangan dalam desain arsitektur. seringkali ada beberapa cara untuk mengimplementasikan fitur yang sama namun beberapa memiliki implikasi yang jauh berbeda untuk cakupan uji / leverage. untuk setiap cabang dalam kode, ini seringkali merupakan test case lain. cabang dalam cabang meningkat ke peningkatan jalur kode yang eksponensial. Oleh karena itu menghindari logika bersarang / bersyarat meningkatkan kemampuan untuk menguji.

• sedang belajar kegagalan perangkat lunak (masif) yang terkenal dimana terdapat banyak contoh & studi kasus sangat membantu untuk memahami sejarah dan mengembangkan pola pikir yang berorientasi pada pertimbangan kualitas.

• seseorang bisa terbawa dengan pengujian! ada masalah dengan keduanya terlalu sedikit atau terlalu banyak pengujian. ada "sweet spot". perangkat lunak tidak dapat berhasil dibangun di kedua ekstrim.

• gunakan semua alat dasar dengan cara yang paling efektif. debugger, profiler kode, alat jangkauan kode uji, sistem pelacakan cacat, dll! tidak harus berkomitmen untuk memperbaiki, tetapi melacak bahkan cacat terkecil dalam perangkat lunak pelacakan.

• penggunaan SCM, manajemen kode sumber, dan teknik percabangan dengan hati-hati adalah penting dalam menghindari regresi, mengisolasi dan memajukan perbaikan, dll.

• Pemrograman N-versi : praktik yang sering digunakan untuk mengembangkan Perangkat Lunak Misi Kritis. Premis dari praktik ini adalah bahwa N program yang dikembangkan secara independen tidak mungkin memiliki bug / kesalahan yang sama. Ini telah dikritik dalam beberapa makalah . NVP , bagaimanapun, praktik bukan konsep teoritis.

Saya percaya fisikawan Feynman memiliki beberapa akun tentang metode yang digunakan NASA untuk menjamin keandalan sistem pesawat ulang-alik dalam bukunya "Apa yang Anda pedulikan apa yang dipikirkan orang lain?" - katanya mereka memiliki dua tim, katakanlah Tim A dan Tim B. tim A membangun perangkat lunak. tim B mengambil pendekatan permusuhan dengan Tim A dan mencoba memecahkan perangkat lunak.

akan membantu jika Tim B memiliki latar belakang rekayasa perangkat lunak yang baik, yaitu mereka sendiri dapat menulis kode harness / tes terprogram dan sebagainya. dalam hal ini Tim B memiliki tingkat sumber daya yang hampir sama dengan Tim A. di sisi lain, pendekatan ini mahal karena hampir dapat menggandakan biaya pembuatan perangkat lunak. lebih khusus, ada tim QA yang lebih kecil dibandingkan dengan tim pengembangan.

Pendekatan lama (tetapi masih digunakan dalam beberapa aplikasi) adalah pemrograman versi-N

Dari Wikipedia:

Pemrograman N-versi ( NVP ), juga dikenal sebagai pemrograman multiversion , adalah metode atau proses dalam rekayasa perangkat lunak di mana banyak program yang secara fungsional setara dihasilkan secara independen dari spesifikasi awal yang sama. Konsep pemrograman versi-N diperkenalkan pada tahun 1977 oleh Liming Chen dan Algirdas Avizienis dengan dugaan sentral bahwa "independensi upaya pemrograman akan sangat mengurangi kemungkinan kesalahan perangkat lunak identik yang terjadi dalam dua atau lebih versi program" .Tujuannya NVP adalah untuk meningkatkan keandalan operasi perangkat lunak dengan membangun toleransi kesalahan atau redundansi.
....

Lihat misalnya: " Tantangan dalam Membangun Kesalahan - Sistem Kontrol Penerbangan Toleransi untuk Pesawat Sipil "

Pada dasarnya, pertanyaan yang Anda lakukan mencakup dua masalah terbesar dalam penelitian insinyur perangkat lunak: kesesuaian antara spesifikasi dan model serta antara model dan kode. Model di sini representasi dari apa yang akan dilakukan sistem, atau bagaimana hal itu akan dilakukan, ada banyak tingkatan untuk memodelkan sistem.

Jadi, ada beberapa orang yang mencoba menemukan jawaban terbaik untuk pertanyaan Anda. Karena itu sangat sulit untuk memeriksa kebenaran suatu perangkat lunak berdasarkan pada suatu model, misalnya, menggunakan metode formal. Saya tahu JML adalah cara untuk melakukannya, tetapi saya tidak tahu batas penggunaannya.

Untuk menyelesaikannya, bagaimana mengecek kebenaran kode sulit dilakukan, orang mencoba mencampur metode formal dan pengujian, membuat pengujian secara otomatis dari spesifikasi misalnya. Salah satu contoh untuk sistem waktu nyata adalah TIOSTS yang didasarkan pada peristiwa waktu input / output.

Pengujian saja bukan pendekatan metode formal, melakukannya meningkatkan keandalan tetapi tidak memeriksa kebenaran.

Dua atau tiga tahun yang lalu saya mulai melihat metode formal yang diterapkan pada perangkat lunak. Ini adalah pencarian yang didorong oleh rasa ingin tahu, dan oleh perasaan bahwa saya harus belajar alat pemrograman dan metode dengan rentang waktu yang lebih lama. Meskipun saya bermimpi tentang Silver Bullet , saya benar-benar berpikir bahwa tidak ada jawaban untuk pertanyaan: "Bagaimana saya bisa menulis program yang benar?".

Pada titik pencarian setelah mencoba beberapa alat (Z, B, VHDL, dan Estelle), saya menggunakan TLA + . Ini adalah varian dari logika temporal dengan perangkat lunak untuk pengecekan model dan bukti mekanis. Saya pikir saya memilih pendekatan ini karena L. Lamport ada di belakangnya, sintaksinya sederhana, ada banyak contoh, ada komunitas yang merawatnya, dan bahasa serta alat-alatnya didokumentasikan dengan cukup baik.

Mengenai pertanyaan awal saya, saya pikir tidak ada jawaban yang lengkap. Namun, perlu dipelajari bahwa membayar untuk menentukan secara formal beberapa bagian dari suatu sistem. Ini juga sangat berguna untuk merekayasa balik beberapa yang kompleks. Artinya, Sangat efektif untuk membuat cetak biru untuk bagian yang sulit dan kritis. Namun, saya tidak berpikir ada metode yang efektif untuk menerjemahkan spesifikasi secara otomatis ke bahasa pemrograman atau kerangka kerja (kecuali jika Anda membatasi proyek ke lingkungan yang sangat spesifik). Saya juga tidak berpikir bahwa memiliki spesifikasi formal harus mencegah Anda menguji perangkat lunak.

Singkatnya, saya berpikir bahwa metafora berikut (dari Lamport) sangat kuat: "Apakah Anda mengharapkan sebuah rumah secara otomatis dibangun dari cetak biru? Apakah Anda akan membeli rumah yang belum dibangun dan tidak memiliki cetak biru?" .

Selama pencarian ini, saya menemukan sumber-sumber berikut berguna:

• Metode Spesifikasi Perangkat Lunak . Buku ini memberikan tinjauan luas tentang metode dan alat yang ada. Di sana Anda dapat menemukan penjelasan dasar dan contoh Z, SDL, TLA +, Petri Nets, Coq, dll.
• Jika Anda berpikir bahwa TLA + sesuai dengan kebutuhan Anda, saya sangat merekomendasikan buku Specifying Systems . Anda dapat memperoleh buku secara gratis, dan disertai dengan contoh-contoh untuk dimainkan :).
• Baru-baru ini, saya membaca beberapa artikel terkait yang memberikan dua perspektif yang berbeda untuk seni metode formal: Kasus untuk Metode Formal , dan Matematika yang Diverifikasi Secara Resmi .

Semoga berhasil!

Jawaban sejauh ini sudah mencakup sebagian besar dari apa yang harus dikatakan tentang dasar-dasar bagaimana menghubungkan spesifikasi dan kode satu sama lain. Saya hanya ingin menambahkan poin yang lebih praktis yang mendekati pertanyaan di header utas ini:

Bagaimana cara membuat perangkat lunak mission mission?

Ada alat yang secara otomatis menganalisis kode Anda untuk kesalahan (pelanggaran spesifikasi, atau "bug khas"). Sepengetahuan saya, sebagian besar metode ini didasarkan pada analisis statis dan tidak langsung berhubungan dengan teori yang Anda sebutkan (LTL / CTL / ...), tetapi mereka menemukan kesalahan dalam kode nyata dan sudah layak, dari sudut pandang praktis. lihat, untuk menggunakan alat tersebut dalam proyek industri. Saya pribadi belum menggunakan banyak dari mereka, tetapi tampaknya alat ini mulai diterima oleh para praktisi. Untuk bacaan lebih lanjut, saya dapat merekomendasikan artikel blog berikut:

http://www.altdevblogaday.com/2011/12/24/static-code-analysis/

Algoritma sertifikasi dapat berguna ketika membangun perangkat lunak misi penting.

Algoritma sertifikasi adalah algoritma yang menghasilkan, dengan setiap output, sertifikat atau saksi (bukti yang mudah diverifikasi) bahwa output tertentu belum dikompromikan oleh bug.

Baca lebih lanjut dalam makalah survei ini. Sertifikasi algoritma oleh McConnell, RM dan Mehlhorn, K. dan Naher, S. and Schweitzer, P.

Tetapi bagaimana cara memverifikasi bahwa perangkat lunak (tidak hanya spesifikasinya) memang benar?

Pengujian unit? Tulis tes untuk setiap persyaratan tunggal dalam spesifikasi, dan kemudian uji setiap metode tunggal dalam implementasi Anda untuk melihat bahwa output / inputnya sesuai dengan spesifikasi tersebut. Ini dapat diotomatisasi sehingga pengujian ini dijalankan terus menerus untuk memastikan tidak ada perubahan yang pernah merusak fitur yang sebelumnya berfungsi.

Secara teoritis, jika pengujian unit Anda memiliki cakupan kode 100% (yaitu setiap metode tunggal dalam kode Anda diuji) perangkat lunak Anda harus benar, asalkan tes itu sendiri akurat dan realistis.