Metode formal: sekadar praktik rekayasa yang baik? (2024)

• Pengantar

  • Marc Brooker adalah insinyur di AWS yang menangani database dan sistem serverless, serta menekankan pentingnya metode formal dalam rekayasa perangkat lunak.

• Pentingnya metode formal

  • Metode formal sangat penting untuk menghemat waktu dan biaya dalam sistem berskala besar, sistem terdistribusi, dan sistem tingkat rendah yang krusial.
  • Rekayasa perangkat lunak adalah latihan dalam mengoptimalkan waktu dan biaya.
  • Metode formal meningkatkan kecepatan dan efisiensi pengembangan perangkat lunak dengan mengurangi biaya pengerjaan ulang dan menangani perubahan antarmuka sejak dini.

• Cakupan penerapan metode formal

  • Pada perangkat lunak yang didorong oleh kebutuhan pengguna yang berubah cepat, nilai metode formal bisa terbatas.
  • Dalam sistem berskala besar, terdistribusi, dan tingkat rendah, metode formal secara signifikan mengurangi pengerjaan ulang dan kepadatan bug.

• Metode formal dan alat

  • Metode formal dan penalaran otomatis mencakup berbagai alat, dan digunakan secara bermanfaat dalam sistem cloud skala besar AWS.
  • Ada bahasa spesifikasi seperti TLA+, P, dan Alloy, serta model checker, alat simulasi deterministik, dan bahasa pemrograman yang sadar verifikasi.

• Kesimpulan

  • Alat yang membantu memikirkan desain sistem pada tahap perancangan mempercepat pengembangan perangkat lunak, mengurangi risiko, dan memungkinkan pengembangan sistem yang optimal.
  • Bagi insinyur yang menangani sistem berskala besar dan kompleks, metode formal adalah bagian dari praktik rekayasa yang baik.

[GN⁺]

Opini Hacker News

• Verifikasi formal pada perangkat lunak sangat bergantung pada jenis perangkat lunak dan proses pengembangannya. Sebagian besar proyek perangkat lunak tidak kompatibel dengan persyaratan formal

  • Pengembangan dan perancangan perangkat lunak sering berjalan bersamaan, tetapi ini tidak cocok untuk metode formal
  • Sistem yang kritis terhadap keselamatan seperti perangkat lunak kedirgantaraan bisa sangat diuntungkan dari verifikasi formal

• Klaim bahwa metode formal dapat mengatasi kompleksitas perangkat lunak sering muncul

  • Ini bisa terasa menarik bagi orang yang menyukai pendekatan akademis
  • Namun, masih kurang contoh yang meyakinkan tentang bagaimana metode formal benar-benar menyelesaikan masalah nyata
  • Ada kesan bahwa dengan mempelajari alat seperti TLA, orang dapat memahami kegunaannya

• Ada dua jenis utama metode formal: teknik ekstrinsik yang terpisah dari kode dan teknik intrinsik yang menyertai kode

  • Teknik intrinsik bekerja pada level fungsional kode, sedangkan teknik ekstrinsik menganalisis model kode secara formal
  • Saat ini kita berada di masa keemasan riset metode formal, dan teknik intrinsik mendapat lebih banyak perhatian

• Metode formal ringan dapat dipelihara bersama codebase dan memberi lebih banyak wawasan daripada unit test

  • Pendekatan ini cocok dengan praktik pengembangan perangkat lunak pada umumnya

• Verifikasi formal perangkat lunak masih merupakan pekerjaan yang sangat sulit dan hanya bernilai pada kasus-kasus ekstrem

  • Diperlukan pengetahuan tingkat ahli, dan untuk sebagian besar sistem hal ini sangat kompleks
  • Mempelajari alat seperti Lean memang sulit, tetapi dokumentasinya baik

• Banyak artikel tentang metode formal terasa seperti upaya menghasilkan prospek bagi konsultan

  • Sebaiknya menunggu sampai metode formal benar-benar menghasilkan kode berkualitas tinggi

• Salah satu metode formal ringan adalah verifikasi jejak menggunakan Linear Temporal Logic

  • Ini adalah cara yang sederhana dan kuat untuk mencatat event dan menjalankan kondisi pada jejak eksekusi

• Metode formal modern seperti TLA+ dan Alloy semudah dipelajari seperti Python

  • Banyak sistem cloud telah diverifikasi dengan alat-alat ini (misalnya Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB)