Для Linux предложен механизм верификации корректности работы ядра
Для включения в состав ядра Linux 5.20 (возможно, ветка получит номер 6.0) предложен набор патчей с реализацией механизма RV (Runtime Verification), представляющего средства для проверки корректности работы на высоконадежных системах, гарантирующих отсутствие сбоев. Проверка производится во время выполнения через прикрепление обработчиков к точкам трассировки, сверяющих фактический ход выполнения с заранее определённой эталонной детерминированной моделью автомата, определяющего ожидаемое поведение системы.
Информация от точек трассировки переводит модель из одного состояния в другое, и если новое состояние не соответствует параметрам модели, генерируется предупреждение или ядро переводится в состояние «panic» (подразумевается, что высоконадёжные системы будут определять подобные ситуации и реагировать на них). Модель автомата, определяющая переходы из одного состояния в другое, экспортируется в формат «dot» (graphviz), после чего транслируется при помощи утилиты dot2c в представление на языке Си, которое загружается в форме модуля ядра, отслеживающего отклонения хода выполнения от предопределённой модели.
Сверка с моделью во время выполнения позиционируется как более легковесный и простой для реализации на практике способ подтверждения корректности выполнения на критически важных системах, дополняющий классические методы подтверждения надёжности, такие как проверка модели и математические доказательства соответствия кода спецификациям, заданным на формальном языке. Из достоинств RV называется возможность обеспечить строгую верификацию без отдельной реализации всей системы на языке моделирования, а также гибкое реагирование на непредвиденные события, например, для блокирования дальнейшего распространения сбоя в критически важных системах.
Источник: http://www.opennet.ru/opennews/art.shtml? num=57605
© OpenNet
