Untuk dimasukkan dalam kernel Linux 5.20 (mungkin cabangnya akan diberi nomor 6.0), serangkaian tambalan diusulkan dengan penerapan mekanisme RV (Runtime Verification), yang menyediakan alat untuk memeriksa operasi yang benar pada sistem yang sangat andal yang menjamin tidak adanya kegagalan. Verifikasi dilakukan saat runtime dengan melampirkan penangan ke titik jejak yang memeriksa kemajuan aktual eksekusi terhadap model deterministik referensi yang telah ditentukan dari automaton yang menentukan perilaku sistem yang diharapkan.
Informasi dari titik jejak memindahkan model dari satu keadaan ke keadaan lain, dan jika keadaan baru tidak sesuai dengan parameter model, peringatan akan dihasilkan atau kernel ditempatkan dalam keadaan "panik" (sistem dengan keandalan tinggi diharapkan dapat mendeteksi dan merespons situasi seperti itu). Model automaton, yang mendefinisikan transisi dari satu keadaan ke keadaan lain, diekspor ke format βtitikβ (graphviz), setelah itu diterjemahkan menggunakan utilitas dot2c ke dalam representasi C, yang dimuat dalam bentuk modul kernel yang melacak penyimpangan kemajuan eksekusi dari model yang telah ditentukan.
Pemeriksaan model run-time diposisikan sebagai metode yang lebih ringan dan lebih mudah diterapkan untuk memverifikasi eksekusi yang benar pada sistem yang kritis, melengkapi metode verifikasi keandalan klasik seperti pemeriksaan model dan bukti matematis dari kepatuhan kode dengan spesifikasi yang diberikan secara formal. bahasa. Di antara kelebihan RV adalah kemampuannya untuk memberikan verifikasi yang ketat tanpa implementasi terpisah dari seluruh sistem dalam bahasa pemodelan, serta respons yang fleksibel terhadap kejadian yang tidak terduga, misalnya, untuk memblokir penyebaran kegagalan lebih lanjut dalam sistem kritis.
Sumber: opennet.ru