Linux ядросуна 5.20 киргизүү үчүн (балким, бутак 6.0 номери болушу мүмкүн) RV (Runtime Verification) механизмин ишке ашыруу менен патчтардын топтому сунушталат, ал жогорку ишенимдүү системалардын туура иштешин текшерүү үчүн куралдарды камсыз кылат. кемчиликтердин жоктугу. Текшерүү системанын күтүлгөн жүрүм-турумун аныктаган автоматтын алдын ала аныкталган референттик детерминисттик моделине каршы аткаруунун иш жүзүндөгү жүрүшүн текшерген көзөмөлдөө пункттарына иштеткичтерди тиркөө аркылуу аткаруу убагында аткарылат.
Издөө чекиттеринен алынган маалымат моделди бир абалдан экинчи абалга жылдырат, ал эми жаңы абал моделдин параметрлерине дал келбесе, эскертүү түзүлөт же ядро "паника" абалына жайгаштырылат (ишенимдүүлүгү жогору системалар аны аныктоо үчүн күтүлөт) жана мындай кырдаалдарга жооп берүү). Бир абалдан экинчи абалга өтүүнү аныктаган автомат модели “чекит” форматына (graphviz) экспорттолот, андан кийин ал dot2c утилитасынын жардамы менен Си түрүнө которулат, ал ядро модулу түрүндө жүктөлөт. алдын ала аныкталган моделден аткаруу прогрессинин четтөөлөрүн көзөмөлдөйт.
Иштөө убактысынын моделин текшерүү миссиясы үчүн маанилүү системаларда туура аткарылышын текшерүүнүн жеңилирээк жана ишке ашырууга оңой ыкмасы катары жайгаштырылган, моделди текшерүү жана коддун расмий түрдө берилген спецификацияларга ылайык келүүсүнүн математикалык далилдери сыяктуу ишенимдүүлүктү текшерүүнүн классикалык ыкмаларын толуктайт. тил. RV артыкчылыктарынын арасында бүтүндөй системаны моделдөө тилинде өзүнчө ишке киргизбестен катуу текшерүүнү камсыз кылуу, ошондой эле күтүлбөгөн окуяларга ийкемдүү жооп берүү, мисалы, критикалык системалардагы бузулуунун андан ары жайылышын бөгөт коюу мүмкүнчүлүгү бар.
Source: opennet.ru