Ukuze kufakwe ku-Linux kernel 5.20 (mhlawumbe igatsha lizoba nenombolo 6.0), kuhlongozwa isethi yamapheshana ngokuqaliswa komshini we-RV (Runtime Verification), ohlinzeka ngamathuluzi okuhlola ukusebenza okulungile kumasistimu athembeke kakhulu aqinisekisa ukungabikho kokwehluleka. Ukuqinisekisa kwenziwa ngesikhathi sokusebenza ngokunamathisela izibambi ukuze ulandelele amaphoyinti ahlola ukuqhubeka kwangempela kokusetshenziswa ngokumelene nemodeli enqunywe kusengaphambili yereferensi ye-automaton echaza ukuziphatha okulindelekile kwesistimu.
Ulwazi olusuka kumaphuzu omkhondo lususa imodeli isuka kwesinye isifunda iye kwesinye, futhi uma isimo esisha singahambisani nemingcele yemodeli, kukhiqizwa isixwayiso noma i-kernel ibekwe esimweni "sokwethuka" (izinhlelo zokuthembeka okuphezulu kulindeleke ukuthi zihlonze. futhi uphendule ezimweni ezinjalo). Imodeli ye-automaton, echaza uguquko ukusuka kwesinye isimo ukuya kwesinye, ithunyelwa kufomethi βyechashaziβ (graphviz), ngemuva kwalokho ihunyushwe kusetshenziswa insiza ye-dot2c ibe isethulo esingu-C, esilayishwa ngesimo semojula ye-kernel ilandelela ukuchezuka kwenqubekelaphambili yokwenza kusukela kumodeli echazwe ngaphambilini.
Ukuhlola imodeli yesikhathi sokugijima kubekwe njengendlela enesisindo esilula futhi kulula ukuyisebenzisa yokuqinisekisa ukwenziwa okulungile ezinhlelweni ezibaluleke kakhulu zenjongo, okuhambisana nezindlela zokuqinisekisa ukwethembeka kwakudala njengokuhlola amamodeli kanye nobufakazi bezibalo bokuhambisana nekhodi nokucaciswa okunikezwe ngokusemthethweni. ulimi. Phakathi kwezinzuzo ze-RV yikhono lokuhlinzeka ngokuqinisekiswa okuqinile ngaphandle kokuqaliswa okuhlukile kwesistimu yonke ngolimi lokumodela, kanye nokuphendula okuguquguqukayo ezenzakalweni ezingalindelekile, isibonelo, ukuvimba ukusabalalisa okuqhubekayo kokwehluleka ezinhlelweni ezibucayi.
Source: opennet.ru