За включване в ядрото на Linux 5.20 (възможно е версията да получи номер 6.0) е предложен набор от патчи с реализация на механизма RV (Runtime Verification), представляващ средства за проверка на коректността на работата на високо надеждни системи, гарантиращи отсъствието на сривове. Проверката се извършва по време на изпълнение чрез прикрепяне на обработчици към точки на проследяване, които сверяват действителния ход на изпълнението с предварително определен еталонен детерминиран модел на автомата, определящ очакваното поведение на системата.
Информацията от точките на проследяване превежда модела от едно състояние в друго и ако новото състояние не отговаря на параметрите на модела, се генерира предупреждение или ядрото преминава в състояние 'panic' (предполага се, че високо надеждните системи ще определят подобни ситуации и ще реагират на тях). Моделът на автомата, определящ преходите от едно състояние в друго, се експортира в формат 'dot' (graphviz), след което се транслира с помощта на утилита dot2c в представяне на C, което се зарежда под формата на модул на ядрото, следящ отклоненията на изпълнението от предварително определен модел.
Сверката с модела по време на изпълнение се позиционира като по-лек и лесен за реализация на практика метод за потвърждаване на коректността на изпълнението на критично важни системи, допълващ класическите методи за потвърждаване на надеждността, като проверка на модела и математически доказателства за съответствие на кода на спецификациите, зададени на формален език. Сред предимствата на RV е възможността да се осигури строга верификация без отделна реализация на цялата система на езика за моделиране, както и гъвкаво реагиране на непредвидени събития, например, за блокиране на по-нататъшното разпространение на неизправност в критично важни системи.
Източник: opennet.ru
