Pour l'inclusion dans le noyau Linux 5.20 (il est possible que la branche porte le numéro 6.0), un ensemble de patches a été proposé pour la mise en œuvre du mécanisme RV (Runtime Verification), représentant des moyens pour vérifier la précision du fonctionnement sur des systèmes très fiables, garantissant l'absence de défaillances. La vérification est effectuée lors de l'exécution par l'attachement de gestionnaires à des points de traçage, comparant le déroulement réel de l'exécution avec un modèle déterministe de référence préalablement défini, qui détermine le comportement attendu du système.
Les informations des points de traçage traduisent 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 mis dans un état de « panic » (il est sous-entendu que les systèmes très fiables détecteront de telles situations et y réagiront). Le modèle automate, qui détermine les transitions d'un état à un autre, est exporté au format « dot » (graphviz), puis traduit à l'aide de l'outil dot2c en une représentation en langage C, qui est chargée sous la forme d'un module noyau, surveillant les écarts d'exécution par rapport au modèle prédéfini.
La vérification avec le modèle lors de l'exécution est positionnée comme une méthode plus légère et plus facile à mettre en œuvre dans la pratique, permettant de confirmer la précision de l'exécution sur des systèmes critiques, complétant les méthodes classiques de validation de la fiabilité, telles que la vérification du modèle et les preuves mathématiques de conformité du code aux spécifications définies dans un langage formel. Parmi les avantages du RV, on mentionne la possibilité d'assurer une vérification rigoureuse sans avoir à implémenter entièrement le 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 des systèmes critiques.
Source : opennet.ru
