Kanggo dilebokake ing kernel Linux 5.20 (mbok menawa cabang kasebut bakal diwenehi nomer 6.0), sakumpulan patch diusulake kanthi implementasi mekanisme RV (Verifikasi Runtime), sing nyedhiyakake alat kanggo mriksa operasi sing bener ing sistem sing dipercaya banget sing njamin ora ana kegagalan. Verifikasi dileksanakake ing runtime dening Masang pawang kanggo nglacak titik sing mriksa kemajuan nyata saka eksekusi marang model deterministik referensi predetermined saka automaton sing nemtokake prilaku samesthine saka sistem.
Informasi saka titik jejak mindhah model saka siji negara menyang negara liyane, lan yen negara anyar ora cocog karo paramèter model, bebaya bakal digawe utawa kernel diselehake ing "gupuh" negara (sistem linuwih dhuwur samesthine kanggo ndeteksi. lan nanggapi kahanan kaya ngono). Model automaton, sing nemtokake transisi saka negara siji menyang negara liyane, diekspor menyang format "titik" (graphviz), sawise diterjemahake nggunakake sarana dot2c menyang perwakilan C, sing dimuat ing wangun modul kernel sing nglacak panyimpangan saka kemajuan eksekusi saka model sing wis ditemtokake.
Pemeriksa model run-time dipanggonke minangka cara sing luwih entheng lan luwih gampang diimplementasikake kanggo verifikasi eksekusi sing bener ing sistem kritis misi, nglengkapi metode verifikasi keandalan klasik kayata pamriksa model lan bukti matematika babagan kepatuhan kode karo spesifikasi sing diwenehake ing format resmi. basa. Antarane kaluwihan saka RV punika kemampuan kanggo nyedhiyani verifikasi ketat tanpa implementasine kapisah saka kabeh sistem ing basa modeling, uga respon fleksibel kanggo acara unforeseen, contone, kanggo mblokir panyebaran luwih saka Gagal ing sistem kritis.
Source: opennet.ru