За Linux е предложен механизъм за проверка на правилната работа на ядрото

За включване в ядрото на Linux 5.20 (може би клонът ще бъде номериран 6.0) се предлага набор от корекции с внедряването на механизма RV (Runtime Verification), който предоставя инструменти за проверка на правилната работа на високонадеждни системи, които гарантират липса на неуспехи. Проверката се извършва по време на изпълнение чрез прикачване на манипулатори към точки за проследяване, които проверяват действителния напредък на изпълнение спрямо предварително определен референтен детерминистичен модел на автомата, който дефинира очакваното поведение на системата.

Информацията от точките за проследяване премества модела от едно състояние в друго и ако новото състояние не съответства на параметрите на модела, се генерира предупреждение или ядрото се поставя в състояние на "паника" (очаква се системите с висока надеждност да открият и реагирайте на такива ситуации). Моделът на автомата, който дефинира преходи от едно състояние към друго, се експортира във формат „точка“ (graphviz), след което се превежда с помощта на помощната програма dot2c в C представяне, което се зарежда под формата на модул на ядрото, който проследява отклоненията на напредъка на изпълнение от предварително дефинирания модел.

Проверката на модела по време на изпълнение се позиционира като по-лек и по-лесен за прилагане метод за проверка на правилното изпълнение на критични за мисията системи, допълвайки класическите методи за проверка на надеждността като проверка на модела и математически доказателства за съответствие на кода със спецификациите, дадени във формални език. Сред предимствата на RV е способността да се осигури стриктна проверка без отделна реализация на цялата система на език за моделиране, както и гъвкав отговор на непредвидени събития, например, за блокиране на по-нататъшното разпространение на повреда в критични системи.

Източник: opennet.ru