Se propone un mecanismo para la verificación de la corrección del núcleo en Linux
Se ha propuesto un conjunto de parches para incluir en el núcleo de Linux 5.20 (posiblemente, la rama recibirá el número 6.0) que implementa el mecanismo RV (Runtime Verification), que proporciona herramientas para verificar la corrección en sistemas de alta confiabilidad, garantizando la ausencia de fallos. La verificación se realiza en tiempo de ejecución mediante la unión de manejadores a puntos de seguimiento, comprobando el flujo real de ejecución con un modelo de autómata determinista previamente definido […]
