Għall-inklużjoni fil-kernel Linux 5.20 (forsi l-fergħa se tkun innumerata 6.0), sett ta 'garża huwa propost bl-implimentazzjoni tal-mekkaniżmu RV (Runtime Verification), li jipprovdi għodod għall-iċċekkjar tal-operat korrett fuq sistemi affidabbli ħafna li jiggarantixxu l- assenza ta' fallimenti. Il-verifika titwettaq waqt ir-runtime billi jitwaħħlu handlers ma 'punti ta' traċċa li jiċċekkjaw il-progress attwali tal-eżekuzzjoni kontra mudell deterministiku ta 'referenza predeterminat tal-awtomat li jiddefinixxi l-imġieba mistennija tas-sistema.
Informazzjoni minn punti ta’ traċċa tmexxi l-mudell minn stat għal ieħor, u jekk l-istat il-ġdid ma jaqbilx mal-parametri tal-mudell, tiġi ġġenerata twissija jew il-qalba titqiegħed fi stat ta’ "paniku" (sistemi ta’ affidabilità għolja huma mistennija li jiskopru u jirrispondu għal sitwazzjonijiet bħal dawn). Il-mudell tal-awtomat, li jiddefinixxi t-tranżizzjonijiet minn stat għall-ieħor, jiġi esportat fil-format "dot" (graphviz), u wara jiġi tradott bl-użu tal-utilità dot2c f'rappreżentazzjoni C, li titgħabba fil-forma ta' modulu tal-qalba li tracks devjazzjonijiet tal-progress ta 'eżekuzzjoni mill-mudell predefinit.
L-iċċekkjar tal-mudell run-time huwa pożizzjonat bħala metodu eħfef u eħfef biex jiġi implimentat ta' verifika ta' eżekuzzjoni korretta fuq sistemi kritiċi għall-missjoni, li jikkumplimenta metodi klassiċi ta' verifika ta' affidabbiltà bħall-iċċekkjar tal-mudelli u provi matematiċi ta' konformità tal-kodiċi ma' speċifikazzjonijiet mogħtija f'forma formali. lingwa. Fost il-vantaġġi ta 'RV hemm il-kapaċità li tipprovdi verifika stretta mingħajr implimentazzjoni separata tas-sistema kollha f'lingwa ta' mmudellar, kif ukoll rispons flessibbli għal avvenimenti mhux previsti, pereżempju, biex jimblokka t-tixrid ulterjuri ta 'falliment f'sistemi kritiċi.
Sors: opennet.ru