Awal minggu ini, saya menjadi pembicara utama di Konferensi TLA+ 2024 (tonton videonya atau lihat slide). Pesan saya dalam keynote adalah sesuatu yang saya yakini kebenarannya sejak lama: metode formal adalah bagian penting dari praktik rekayasa perangkat lunak yang baik. Jika Anda seorang insinyur perangkat lunak, terutama yang bekerja pada sistem skala besar, sistem terdistribusi, atau sistem tingkat rendah yang kritis, dan tidak menggunakan metode formal sebagai bagian dari pendekatan Anda, Anda mungkin membuang-buang waktu dan uang.
Sebab, pada akhirnya, engineering adalah latihan mengoptimalkan waktu dan uang1.
“Akan lebih baik jika teknik tidak lagi dianggap secara umum, dan bahkan didefinisikan, sebagai seni membangun. Dalam arti penting tertentu, ini lebih merupakan seni untuk tidak membangun; atau, untuk mendefinisikannya secara kasar namun tidak secara tidak tepat, ini adalah seni melakukan hal tersebut dengan baik dengan satu dolar, yang dapat dilakukan oleh setiap orang yang ceroboh dengan dua dolar.” Arthur Wellington2
Pada awalnya, ini mungkin tampak berlawanan dengan intuisi. Metode formal tidaklah murah, tidak terlalu mudah, dan tidak cocok dengan setiap pendekatan rekayasa perangkat lunak. Masuk akal untuk memulai dengan keyakinan bahwa pendekatan formal akan meningkatkan biaya, terutama biaya teknik yang tidak berulang. Menurut pengalaman saya, hal ini tidak benar, karena dua alasan. Yang pertama adalah pengerjaan ulang. Rekayasa perangkat lunak agak unik dalam bidang teknik karena desain dan konstruksi cenderung terjadi pada waktu yang sama, dan banyak konstruksi dapat dimulai tanpa banyak kemajuan dalam desain. Hal ini tidak berlaku dalam teknik kelistrikan (merancang PCB atau memasang kabel tidak dapat dilakukan sampai desain selesai), atau teknik sipil (memulai pekerjaan tanah sebelum Anda tahu apa yang sedang Anda bangun adalah mungkin, tetapi cara yang dapat diandalkan untuk melakukannya membuang-buang uang), atau teknik mesin, dan sebagainya. Ini adalah kekuatan perangkat lunak yang sangat besar – sifat mutabilitasnya telah menjadi salah satu alasan mengapa perangkat lunak menguasai dunia – namun juga dapat meningkatkan biaya iterasi desain secara signifikan dengan mengubah iterasi desain menjadi iterasi implementasi. Yang kedua adalah biaya perubahan. Setelah API atau sistem memiliki pelanggan, mengubahnya menjadi jauh lebih mahal dan sulit. Hal ini pada dasarnya terkait dengan Hukum Hyrum:
Dengan jumlah pengguna API yang memadai, apa pun yang Anda janjikan dalam kontrak tidak menjadi masalah: semua perilaku sistem Anda yang dapat diamati akan bergantung pada seseorang.
Mengisolasi perilaku sistem dengan API adalah ide bagus. Faktanya, saya menganggapnya sebagai salah satu ide terpenting dalam semua rekayasa perangkat lunak. Hukum Hyrum mengingatkan kita akan keterbatasan pendekatan ini: pengguna akan bergantung pada setiap detail implementasi API. Ini tidak berarti perubahan tidak mungkin dilakukan. Saya telah terlibat dalam banyak proyek dalam karier saya yang telah sepenuhnya mengimplementasikan kembali sistem di balik API. Ini hanya berarti bahwa perubahan itu mahal, dan abstraksi seperti API tidak secara efektif mengubah kenyataan tersebut.
Dengan menghemat biaya pengerjaan ulang, dan dengan melakukan perubahan antarmuka lebih awal, pekerjaan desain formal dapat secara signifikan meningkatkan kecepatan dan efisiensi proses pembuatan perangkat lunak.
Sistem macam apa?
Hal ini tampaknya tidak berlaku untuk semua jenis perangkat lunak. Perangkat lunak yang sangat didorong oleh kebutuhan pengguna yang berkembang pesat atau sulit untuk diformalkan, mulai dari UI dan situs web hingga penerapan logika harga, mungkin memerlukan begitu banyak pengerjaan ulang sehingga nilai desain awal menjadi berkurang (atau biayanya secara signifikan ditingkatkan). Inilah ide mendasar di balik agile: dengan menjalankan implementasi dan pengumpulan persyaratan secara paralel, waktu yang dibutuhkan untuk memasarkan produk dapat dikurangi. Lebih penting lagi, ketika pengumpulan persyaratan merupakan proses yang berkelanjutan, hal ini memungkinkan implementasi untuk diselesaikan bahkan ketika persyaratan berkembang. Dalam banyak kasus, pendekatan paralel terhadap pembangunan ini merupakan pendekatan yang optimal, dan bahkan diperlukan untuk mencapai kemajuan.
Di sisi lain, sebagian besar perangkat lunak di balik sistem berskala besar, terdistribusi, dan tingkat rendah telah memahami persyaratan dengan baik. Atau, setidaknya, sebagian besar persyaratan statis yang dipahami dengan baik sehingga desain formal di awal mengurangi pengerjaan ulang dan kepadatan bug selama fase implementasi (dan setelahnya, ketika sistem sedang dalam produksi).
Sebagian besar perdebatan tentang desain di depan vs tangkas berasal dari orang-orang dari berbagai spektrum perangkat lunak yang saling berdiskusi. Kita tidak perlu heran bahwa perangkat lunak dengan model pengumpulan persyaratan yang sangat berbeda akan memiliki pendekatan rekayasa optimal yang berbeda. Sepertinya semakin dekat proses persyaratannya hukum fisika desain yang lebih berharga, dan desain formal, sedang dalam proses rekayasa. Semakin dekat persyaratan dengan pendapat pengguna, semakin kurang berharga persyaratan tersebut.
Hal ini tidak berarti bahwa tidak ada gunanya menuliskan secara jelas kebutuhan pengguna, dan mencari cara formal untuk menentukannya. Menuliskan persyaratan, secara formal atau informal, sangatlah berharga. Tidak menuliskannya dapat membuang banyak waktu, dan menyebabkan banyak perselisihan, karena orang-orang pada akhirnya akan beralih ke arah yang lain. Namun hal ini berarti bahwa seringkali sulit (dan mungkin tidak ekonomis) untuk secara formal menentukan segala bentuk kebutuhan manusia. Saya tidak tahu cara menentukan persyaratan estetika UI, keterbacaan dokumentasi, atau bahkan konsistensi penamaan API, misalnya.
Ketidaksepakatan lain dalam bidang ini juga tampaknya berasal dari gagasan berbeda tentang apa itu pendekatan formal, dan betapa berharganya pendekatan tersebut. Saya, misalnya, cenderung melihat banyak hal lingkaran dan panah sekolah desain perangkat lunak hanya membuang-buang waktu jika tidak terlibat langsung dengan pertanyaan-pertanyaan yang sangat sulit. Pendapat itu mungkin berasal dari ketidaktahuan, dan saya berpendapat dengan lemah. Namun saya yakin bahwa pengalaman kelas SE universitas saya yang mendeskripsikan 100 baris kode dalam 100 rim UML membuat saya memiliki opini yang sangat rendah tentang manfaat merancang perangkat lunak. Jika dilakukan dengan buruk, atau dengan alat yang buruk, bahkan hal yang paling berharga pun tidak ada gunanya.
Alat yang mana?
Metode formal dan penalaran otomatis adalah bidang yang luas, dengan sejumlah alat yang sangat banyak. Selama karir saya, di domain saya di sistem cloud besar, saya menemukan rangkaian berikut berguna (tetapi saya yakin ada alat yang menurut saya berguna jika saya mengetahuinya).
- Spesifikasi bahasa seperti P, TLA+Dan Paduanbersama dengan pemeriksa model terkait.
- Alat simulasi deterministik seperti kekacauan yang memungkinkan, bersama dengan fuzzing, pendekatan berprinsip untuk mencari ruang keadaan melalui pengujian.
- Bahasa pemrograman yang sadar verifikasi seperti Dafny dan pemverifikasi kode seperti Kani. Saya bukan ahli mendalam dalam alat-alat ini, dan jarang menggunakannya dibandingkan yang lain.
- Teknik simulasi numerik. Saya cenderung membuat sendiri (seperti yang telah saya tulis sebelumnya), tetapi ada banyak kerangka kerja dan alat di luar sana.
- Papan tulis metode formal-ish. Ini adalah metode seperti menggambar tabel keputusantabel kebenaran, mesin status eksplisit, dll di papan tulis atau dalam dokumen desain.
Saya suka survei metode di Menggunakan Metode Formal Ringan untuk Memvalidasi Node Penyimpanan Nilai Kunci di Amazon S3 juga. Itu adalah tempat yang bagus untuk memulai.
Namun, pada postingan ini, kami tidak ingin terlalu terikat pada gagasan bahwa memverifikasi implementasi adalah satu-satunya tujuan akhir yang layak di sini. Ini memang merupakan tujuan yang berharga, namun saya telah menemukan banyak manfaat dalam menggunakan alat seperti TLA+ dan P untuk memikirkan desain dengan lebih cepat dan konkrit sebelum membangun.
Perangkat lunak lebih cepat, lebih cepat
Kembali pada tahun 2015 ketika kami sedang menulis Bagaimana Amazon Web Services Menggunakan Metode Formal untuk CACM, fokus saya adalah pada kebenaran. Tentang memverifikasi properti keamanan dan keaktifan desain saya, dan mendapatkan desain yang benar dengan lebih cepat. Saat berbicara dengan salah satu tim yang menggunakan TLA+ pada sistem manajemen kunci internal, saya menemukan sesuatu yang lebih saya sukai. Kata-kata ini, dari Tabel 1:
memverifikasi optimasi agresif
Ini membuka mata. Alat seperti TLA+ tidak hanya membantu kita membangun sistem lebih cepat, tetapi juga membantu kita membangun sistem lebih cepat. Mereka memungkinkan kami dengan cepat mengeksplorasi kemungkinan pengoptimalan, menemukan batasan yang benar-benar penting, dan memeriksa apakah pengoptimalan yang kami usulkan sudah benar. Mereka, dalam banyak kasus, menghilangkan trade-off yang sulit antara kebenaran dan kinerja yang dapat membuat banyak sistem terjebak.
Kesimpulan
Menggunakan alat untuk membantu kita berpikir tentang desain sistem pada tahap desain dapat meningkatkan kecepatan pengembangan perangkat lunak secara signifikan, mengurangi risiko, dan memungkinkan kami mengembangkan sistem yang lebih optimal sejak awal. Bagi kita yang bekerja pada sistem berskala besar dan kompleks, hal tersebut hanyalah bagian dari praktik teknik yang baik.
Dalam Bentuk Video
Catatan kaki
