Para a súa inclusión no núcleo Linux 5.20 (quizais a rama estará numerada 6.0), proponse un conxunto de parches coa implementación do mecanismo RV (Runtime Verification), que proporciona ferramentas para comprobar o correcto funcionamento en sistemas altamente fiables que garanten o ausencia de fallos. A verificación realízase en tempo de execución unindo controladores a puntos de rastrexo que verifican o progreso real da execución fronte a un modelo determinista de referencia predeterminado do autómata que define o comportamento esperado do sistema.
A información dos puntos de traza move o modelo dun estado a outro, e se o novo estado non coincide cos parámetros do modelo, xérase un aviso ou o núcleo colócase nun estado de "pánico" (espérase que os sistemas de alta fiabilidade detecten e responder a tales situacións). O modelo de autómata, que define as transicións dun estado a outro, expórtase ao formato "punto" (graphviz), despois do cal se traduce mediante a utilidade dot2c nunha representación C, que se carga en forma de módulo do núcleo que rastrexa as desviacións do progreso da execución respecto ao modelo predefinido.
A verificación de modelos en tempo de execución sitúase como un método máis lixeiro e máis fácil de implementar para verificar a correcta execución en sistemas de misión crítica, complementando os métodos clásicos de verificación de fiabilidade, como a comprobación de modelos e as probas matemáticas do cumprimento do código coas especificacións dadas nun formulario formal. lingua. Entre as vantaxes de RV está a capacidade de proporcionar unha verificación estrita sen unha implementación separada de todo o sistema nunha linguaxe de modelado, así como unha resposta flexible a eventos imprevistos, por exemplo, para bloquear a propagación dun fallo en sistemas críticos.
Fonte: opennet.ru