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