I'w cynnwys yn y cnewyllyn Linux 5.20 (efallai y bydd y gangen yn cael ei rhifo 6.0), cynigir set o glytiau gyda gweithrediad y mecanwaith RV (Runtime Verification), sy'n darparu offer ar gyfer gwirio gweithrediad cywir ar systemau hynod ddibynadwy sy'n gwarantu'r absenoldeb methiannau. Perfformir dilysu ar amser rhedeg trwy gysylltu'r trinwyr Γ’ phwyntiau olrhain sy'n gwirio'r cynnydd gwirioneddol wrth gyflawni yn erbyn model penderfynol cyfeiriadol a bennwyd ymlaen llaw o'r awtomaton sy'n diffinio ymddygiad disgwyliedig y system.
Mae gwybodaeth o bwyntiau hybrin yn symud y model o un cyflwr i'r llall, ac os nad yw'r cyflwr newydd yn cyd-fynd Γ’ pharamedrau'r model, cynhyrchir rhybudd neu rhoddir y cnewyllyn mewn cyflwr "panig" (disgwylir i systemau dibynadwyedd uchel ganfod). ac ymateb i sefyllfaoedd o'r fath). Mae'r model automaton, sy'n diffinio trawsnewidiadau o un cyflwr i'r llall, yn cael ei allforio i'r fformat "dot" (graphviz), ac ar Γ΄l hynny mae'n cael ei gyfieithu gan ddefnyddio'r cyfleustodau dot2c i gynrychioliad C, sy'n cael ei lwytho ar ffurf modiwl cnewyllyn sy'n olrhain gwyriadau yn y cynnydd gweithredu oddi wrth y model a ddiffiniwyd ymlaen llaw.
Mae gwirio model amser rhedeg wedi'i leoli fel dull ysgafnach a haws ei weithredu o wirio gweithrediad cywir ar systemau sy'n hanfodol i genhadaeth, gan ategu dulliau gwirio dibynadwyedd clasurol megis gwirio modelau a phrofion mathemategol o gydymffurfiaeth cod Γ’ manylebau a roddir mewn ffurflen ffurfiol. iaith. Ymhlith manteision RV mae'r gallu i ddarparu dilysiad llym heb weithrediad ar wahΓ’n o'r system gyfan mewn iaith fodelu, yn ogystal ag ymateb hyblyg i ddigwyddiadau annisgwyl, er enghraifft, i rwystro lledaeniad pellach methiant mewn systemau critigol.
Ffynhonnell: opennet.ru