- TLA+ adalah bahasa untuk memodelkan perangkat lunak pada tingkat yang lebih tinggi dari level kode, dan memodelkan perangkat keras pada tingkat yang lebih tinggi dari level rangkaian
- Menyediakan lingkungan pengembangan terintegrasi (IDE) untuk menulis model dan memeriksanya
- Alat yang paling banyak digunakan oleh para engineer adalah model checker TLC, dan juga tersedia proof checker
- TLA+ berbasis matematika dan tidak mirip dengan bahasa pemrograman apa pun
- Bagi sebagian besar engineer, memulai lewat PlusCal lebih mudah daripada langsung dengan TLA+
- Model TLA+ umumnya disebut sebagai "spesifikasi (Specification)". Dalam pengantar di bawah ini, disebut
model
PlusCal
- PlusCal adalah bahasa untuk menulis algoritme, khususnya algoritme paralel dan terdistribusi
- Digunakan untuk menulis algoritme sebagai kode presisi yang dapat diuji, bukan sekadar pseudocode
- Tampak seperti bahasa pemrograman sederhana, dan menyediakan konstruksi untuk mengekspresikan konkurensi dan nondeterminisme
- Dapat menggunakan rumus matematika sebagai ekspresi sehingga sangat ekspresif
- Algoritme PlusCal dikonversi menjadi model TLA+, dan dapat diverifikasi dengan alat TLA+
- Karena terlihat seperti bahasa pemrograman, ia mudah dipelajari, tetapi untuk menyusun model yang kompleks, TLA+ lebih cocok
Apa itu model
- Komputer dan jaringan mengikuti hukum fisika yang kontinu, tetapi perilakunya secara alami lebih mudah dimodelkan sebagai himpunan kejadian diskret
- Tidak ada model yang menggambarkan sistem nyata secara sempurna; model menggambarkan sebagian aspek sistem untuk tujuan tertentu
- TLA+ adalah bahasa pemodelan berbasis keadaan, yang merepresentasikan eksekusi sistem sebagai urutan keadaan
- Kejadian direpresentasikan sebagai pasangan dua keadaan yang berurutan, yang disebut 'langkah (step)'
- Sistem dimodelkan sebagai himpunan aksi yang menjelaskan semua kemungkinan eksekusi
Pemodelan di atas level kode
- TLA+ digunakan untuk memodelkan sistem pada level di atas kode
- Misalnya, algoritme Euclid dapat dijelaskan sebagai prosedur untuk menghitung pembagi persekutuan terbesar (GCD), bukan sebagai kode
- Tetapkan variabel x ke M, dan y ke N
- Kurangi nilai yang lebih kecil dari nilai yang lebih besar secara berulang antara x dan y
- Ulangi sampai x dan y menjadi sama, dan nilai itu adalah GCD
- Penjelasan seperti ini mengabaikan detail seperti tipe variabel atau penanganan pengecualian, dan hanya mengekspresikan konsep algoritme yang esensial
- Jika hanya fokus pada coding, sulit menemukan algoritme yang baik → dibutuhkan pemikiran abstrak
- Sebagian besar programmer mulai menulis kode tanpa model tingkat tinggi, dan ini menimbulkan kesalahan desain
- TLA+ adalah bahasa model tingkat tinggi yang dapat mendeskripsikan perilaku dan cara kerja kode dengan jelas
- Semakin kompleks sistem, semakin penting penyederhanaan, dan itu dicapai bukan melalui teknik coding melainkan melalui pemikiran tingkat tinggi
- Dalam sebuah proyek industri, ada kasus di mana pemodelan dengan TLA+ mengurangi ukuran kode sistem operasi real-time menjadi sepersepuluh
- Pemodelan efektif untuk menemukan kesalahan desain lebih awal, dan lebih andal daripada pengujian atau perbaikan kode
Pemodelan sistem paralel
- Sistem paralel terdiri dari banyak komponen (proses) yang bekerja secara bersamaan
- Sistem terdistribusi adalah proses-proses yang terpisah secara fisik dan berkomunikasi melalui pesan
- TLA+ memodelkan seluruh keadaan sistem sebagai keadaan global
- Berdasarkan pengalaman lebih dari 40 tahun, memodelkan sistem terdistribusi berdasarkan keadaan global adalah yang paling umum berguna
Mesin keadaan (State Machine)
- TLA+ mendefinisikan himpunan aksi dengan dua elemen berikut:
- Kondisi awal: menentukan keadaan awal yang mungkin
- Relasi keadaan berikutnya: menentukan langkah yang mungkin terjadi (pasangan keadaan berurutan)
- Himpunan aksi yang memenuhi dua kondisi ini adalah model
- Model semacam ini disebut mesin keadaan (state machine)
- Mesin keadaan hingga (finite-state machine) adalah mesin keadaan dengan jumlah keadaan yang terbatas
- Mesin Turing adalah contoh mesin keadaan; pada mesin Turing deterministik, tiap keadaan memiliki paling banyak satu keadaan berikutnya
- Cara praktis untuk menjelaskan makna bahasa pemrograman secara tepat adalah semantik operasional yang mengubahnya menjadi mesin keadaan
- Aksi keadaan berikutnya hanya menentukan langkah yang dapat terjadi, bukan berarti langkah itu pasti terjadi
- Untuk menyatakan bahwa suatu langkah harus terjadi, perlu menambahkan kondisi fairness (fairness property)
- Bahkan tanpa fairness, itu cukup untuk menemukan kesalahan commission, tetapi kesalahan omission tidak akan terdeteksi
- Dalam kebanyakan kasus, kesalahan yang lebih umum adalah commission, dan pemula sebaiknya mulai dari menulis kondisi awal serta relasi keadaan berikutnya
Verifikasi properti
- Model ditulis untuk memastikan apakah sistem bekerja seperti yang diinginkan
- Dengan alat TLA+, dapat diverifikasi apakah model memenuhi properti tertentu untuk semua kemungkinan perilaku
- Contoh: meskipun pada 99% keadaan awal eksekusi berakhir normal, yang harus diverifikasi adalah bahwa semua perilaku berakhir normal
- Properti yang paling umum adalah properti invarian (invariance property), yang harus selalu benar di setiap keadaan
- Model dengan kondisi fairness juga harus memverifikasi properti liveness (liveness property) → misalnya: eksekusi pasti berakhir
- Properti yang lebih kompleks dapat dinyatakan sebagai mesin keadaan, dan dapat diverifikasi apakah mesin keadaan lain mengimplementasikannya
- Di TLA+, tidak ada pembedaan formal antara mesin keadaan dan properti; keduanya diekspresikan sama sebagai rumus matematika
- Bahwa suatu mesin keadaan mengimplementasikan mesin keadaan lain berarti rumus tersebut tercakup secara logis
- Dalam praktiknya, kebanyakan hanya memeriksa invarian dan properti liveness sederhana, tetapi memahami konsep yang lebih kompleks juga membantu mencegah bug pada kode
Bahasa TLA+ itu sendiri
- TLA+ adalah bahasa berbasis matematika dan tidak tampak seperti bahasa pemrograman
- Programmer lebih terbiasa dengan bahasa pemrograman daripada notasi matematika, sehingga pada awalnya bisa terasa sulit
- Namun sebenarnya, matematika jauh lebih ekspresif daripada bahasa pemrograman
- Contoh: GCD dapat didefinisikan sebagai bilangan bulat positif terbesar yang membagi dua bilangan (tanpa perlu menjelaskan cara menghitungnya)
- Definisi matematis dapat menyisakan hanya inti yang diperlukan untuk tujuan tertentu, dan mengabstraksikan detail implementasi yang tidak perlu
- Proseduralisasi tidak memberikan abstraksi; itu hanya menyembunyikan kode di tempat lain
- PlusCal cocok untuk memulai belajar TLA+, dan bahkan pengguna berpengalaman pun lebih menyukai PlusCal untuk model sederhana
- Namun, untuk berpikir secara matematis dan melakukan pemodelan tingkat tinggi, penting untuk mempelajari TLA+ itu sendiri
3 komentar
https://cacm.acm.org/research/… Sudah digunakan dengan baik di AWS.
Coding bukanlah pemrograman
Disebutkan di artikel itu, jadi saya mencarinya.
Saya juga baru pertama kali melihatnya dari tulisan ini, jadi saya sempat mencarinya.