Для Linux предложен механизм верификации корректности работы ядра
Для включения в состав ядра Linux 5.20 (возможно, ветка получит номер 6.0) предложен набор патчей с реализацией механизма RV (Runtime Verification), представляющего средства для проверки корректности работы на высоконадежных системах, гарантирующих отсутствие сбоев. Проверка производится во время выполнения через прикрепление обработчиков к точкам трассировки, сверяющих фактический ход выполнения с заранее определённой эталонной детерминированной моделью автомата, определяющего ожидаемое поведение системы. Информация от точек трассировки переводит модель из одного состояния в другое, и если новое состояние не соответствует параметрам модели, генерируется предупреждение или ядро переводится в состояние «panic» (подразумевается, что высоконадёжные системы будут определять подобные ситуации и реагировать на них). Модель автомата, … Читать далее Для Linux предложен механизм верификации корректности работы ядра
