Für die Aufnahme in den Linux-Kernel 5.20 (möglicherweise wird der Zweig die Nummer 6.0 erhalten) wird eine Reihe von Patches mit der Implementierung des RV-Mechanismus (Runtime Verification) vorgeschlagen, der Tools zur Überprüfung des korrekten Betriebs auf hochzuverlässigen Systemen bereitstellt, die dies garantieren Abwesenheit von Fehlern. Die Überprüfung erfolgt zur Laufzeit, indem Handler an Trace-Punkte angehängt werden, die den tatsächlichen Ausführungsfortschritt anhand eines vorgegebenen deterministischen Referenzmodells des Automaten überprüfen, das das erwartete Verhalten des Systems definiert.
Informationen von Trace-Punkten verschieben das Modell von einem Zustand in einen anderen, und wenn der neue Zustand nicht mit den Parametern des Modells übereinstimmt, wird eine Warnung generiert oder der Kernel wird in einen „Panik“-Zustand versetzt (Systeme mit hoher Zuverlässigkeit sollten dies erkennen). und auf solche Situationen reagieren). Das Automatenmodell, das Übergänge von einem Zustand in einen anderen definiert, wird in das „Dot“-Format (graphviz) exportiert und anschließend mit dem Dienstprogramm dot2c in eine C-Darstellung übersetzt, die in Form eines Kernelmoduls geladen wird Verfolgt Abweichungen des Ausführungsfortschritts vom vordefinierten Modell.
Die Laufzeitmodellüberprüfung wird als leichtere und einfacher zu implementierende Methode zur Überprüfung der korrekten Ausführung auf geschäftskritischen Systemen positioniert und ergänzt klassische Methoden zur Zuverlässigkeitsüberprüfung wie Modellüberprüfung und mathematische Beweise für die Codekonformität mit formalen Spezifikationen Sprache. Zu den Vorteilen von RV gehört die Möglichkeit einer strengen Verifizierung ohne separate Implementierung des gesamten Systems in einer Modellierungssprache sowie die flexible Reaktion auf unvorhergesehene Ereignisse, um beispielsweise die weitere Ausbreitung eines Fehlers in kritischen Systemen zu verhindern.
Source: opennet.ru