Para su inclusión en el kernel Linux 5.20 (quizás la rama lleve el número 6.0), se propone un conjunto de parches con la implementación del mecanismo RV (Runtime Verification), que proporciona herramientas para comprobar el correcto funcionamiento de sistemas altamente confiables que garantizan la ausencia de fallas. La verificación se realiza en tiempo de ejecución adjuntando controladores a puntos de seguimiento que verifican el progreso real de la ejecución con un modelo determinista de referencia predeterminado del autómata que define el comportamiento esperado del sistema.
La información de los puntos de seguimiento mueve el modelo de un estado a otro, y si el nuevo estado no coincide con los parámetros del modelo, se genera una advertencia o el núcleo entra en estado de "pánico" (se espera que los sistemas de alta confiabilidad detecten y responder a tales situaciones). El modelo de autómata, que define las transiciones de un estado a otro, se exporta al formato "punto" (graphviz), después de lo cual se traduce usando la utilidad dot2c a una representación C, que se carga en forma de un módulo del núcleo que rastrea las desviaciones del progreso de ejecución del modelo predefinido.
La verificación de modelos en tiempo de ejecución se posiciona como un método más liviano y más fácil de implementar para verificar la ejecución correcta en sistemas de misión crítica, complementando los métodos clásicos de verificación de confiabilidad, como la verificación de modelos y las pruebas matemáticas del cumplimiento del código con las especificaciones dadas en un formulario formal. idioma. Entre las ventajas de RV se encuentra la capacidad de proporcionar una verificación estricta sin una implementación separada de todo el sistema en un lenguaje de modelado, así como una respuesta flexible a eventos imprevistos, por ejemplo, para bloquear la propagación de una falla en sistemas críticos.
Fuente: opennet.ru