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