Pour inclusion dans le noyau Linux 5.20 (peut-être que la branche sera numérotée 6.0), un ensemble de correctifs est proposé avec l'implémentation du mécanisme RV (Runtime Verification), qui fournit des outils pour vérifier le bon fonctionnement sur des systèmes hautement fiables qui garantissent le absence d'échecs. La vérification est effectuée au moment de l'exécution en attachant des gestionnaires à des points de trace qui vérifient la progression réelle de l'exécution par rapport à un modèle déterministe de référence prédéterminé de l'automate qui définit le comportement attendu du système.
Les informations provenant des points de trace déplacent le modèle d'un état à un autre, et si le nouvel état ne correspond pas aux paramètres du modèle, un avertissement est généré ou le noyau est placé dans un état de « panique » (les systèmes à haute fiabilité sont censés détecter et réagir à de telles situations). Le modèle d'automate, qui définit les transitions d'un état à un autre, est exporté au format « dot » (graphviz), après quoi il est traduit à l'aide de l'utilitaire dot2c en une représentation C, qui est chargée sous la forme d'un module noyau qui suit les écarts de la progression de l’exécution par rapport au modèle prédéfini.
La vérification de modèle d'exécution se positionne comme une méthode plus légère et plus facile à mettre en œuvre pour vérifier l'exécution correcte des systèmes critiques, complétant les méthodes classiques de vérification de la fiabilité telles que la vérification de modèle et les preuves mathématiques de la conformité du code aux spécifications données dans un document formel. langue. Parmi les avantages de RV figure la capacité de fournir une vérification stricte sans implémentation séparée de l'ensemble du système dans un langage de modélisation, ainsi qu'une réponse flexible aux événements imprévus, par exemple pour bloquer la propagation d'une défaillance dans les systèmes critiques.
Source: opennet.ru