Para ser incluído no kernel Linux 5.20 (talvez o branch seja numerado 6.0), foi proposto um conjunto de patches com a implementação do mecanismo RV (Runtime Verification), que é um meio de verificar o correto funcionamento em sistemas altamente confiáveis que garantem a ausência de falhas. A validação é feita em tempo de execução anexando manipuladores a pontos de rastreamento que verificam o progresso real da execução em relação a um modelo determinístico de referência predeterminado do autômato que determina o comportamento esperado do sistema.
As informações dos tracepoints movem o modelo de um estado para outro, e se o novo estado não corresponder aos parâmetros do modelo, um aviso é gerado ou o kernel é colocado em estado de "pânico" (entende-se que sistemas altamente confiáveis irão detectar tais situações e responder a elas). O modelo de autômato que define as transições de um estado para outro é exportado para o formato “ponto” (graphviz), após o qual é traduzido usando o utilitário dot2c em uma representação C, que é carregada na forma de um módulo de kernel que rastreia desvios do progresso da execução a partir de um modelo predefinido.
A verificação do modelo em tempo de execução é posicionada como um método mais leve e fácil de implementar para verificar a exatidão da execução em sistemas de missão crítica, complementando os métodos clássicos de verificação de confiabilidade, como verificação de modelo e provas matemáticas de conformidade do código com as especificações fornecidas. em uma linguagem formal. Entre as vantagens do RV está a capacidade de fornecer verificação rigorosa sem uma implementação separada de todo o sistema em uma linguagem de modelagem, bem como uma resposta flexível a eventos imprevistos, por exemplo, para bloquear a propagação de uma falha em sistemas críticos.
Fonte: opennet.ru