Linux ядросына 5.20 қосу үшін (бәлкім, тармақ 6.0 нөмірленетін болады) RV (Runtime Verification) механизмін енгізу арқылы патчтар жинағы ұсынылады, ол жоғары сенімді жүйелерде дұрыс жұмыс істеуді тексеру үшін құралдарды қамтамасыз етеді. сәтсіздіктердің болмауы. Жүйенің күтілетін әрекетін анықтайтын автоматтың алдын ала анықталған анықтамалық детерминирленген үлгісіне қарсы нақты орындалу барысын тексеретін бақылау нүктелеріне өңдеушілерді қосу арқылы тексеру орындалу уақытында орындалады.
Бақылау нүктелерінен алынған ақпарат модельді бір күйден екінші күйге ауыстырады, ал егер жаңа күй модель параметрлеріне сәйкес келмесе, ескерту жасалады немесе ядро «үрбелең» күйіне орналастырылады (сенімділігі жоғары жүйелер оны анықтайды деп күтілуде) және осындай жағдайларға жауап беру). Бір күйден екінші күйге өтуді анықтайтын автомат моделі «нүкте» пішіміне (graphviz) экспортталады, содан кейін ол dot2c утилитасының көмегімен ядро модулі түрінде жүктелетін C көрінісіне аударылады. алдын ала анықталған үлгіден орындалу барысының ауытқуларын бақылайды.
Орындалу уақытындағы модельді тексеру миссиясы маңызды жүйелерде дұрыс орындалуды тексерудің жеңілірек және оңай орындалатын әдісі ретінде орналастырылған, модельді тексеру және ресми құжатта берілген спецификацияларға код сәйкестігінің математикалық дәлелдері сияқты сенімділікті тексерудің классикалық әдістерін толықтырады. тіл. RV артықшылықтарының қатарында модельдеу тілінде бүкіл жүйені бөлек енгізусіз қатаң тексеруді қамтамасыз ету, сондай-ақ күтпеген оқиғаларға икемді жауап беру, мысалы, сыни жүйелердегі сәтсіздіктің одан әрі таралуын блоктау мүмкіндігі бар.
Ақпарат көзі: opennet.ru