Für den Kern von Linux 5.20 (möglicherweise wird dieser Zweig die Nummer 6.0 erhalten) wurde ein Satz von Patches vorgeschlagen, die einen Mechanismus zur Laufzeitüberprüfung (Runtime Verification, RV) implementieren. Dieser bietet Mittel zur Überprüfung der korrekten Funktionalität in hochverfügbaren Systemen, die Ausfälle ausschließen. Die Überprüfung erfolgt in Echtzeit durch das Anfügen von Handlern an Abtastpunkte, die den tatsächlichen Ablauf mit einem im Voraus definierten Referenzmodell des Automaten abgleichen, das das erwartete Verhalten des Systems festlegt.
Information von Tracepoints überträgt das Modell von einem Zustand in einen anderen. Wenn der neue Zustand nicht mit den Modellenparametern übereinstimmt, wird eine Warnung generiert oder der Kernel wechselt in den Zustand "panic" (es wird davon ausgegangen, dass hochverfügbare Systeme solche Situationen erkennen und darauf reagieren). Das Automatonmodell, das die Übergänge von einem Zustand in einen anderen definiert, wird im "dot"-Format (Graphviz) exportiert und anschließend mit dem Tool dot2c in eine C-Repräsentation übersetzt, die als Kernelmodul geladen wird, um Abweichungen von der vorgegebenen Modellausführung zu überwachen.
Die Überprüfung mit einem Modell während der Ausführung wird als leichter und praktischer Weg angesehen, um die Korrektheit von kritischen Systemen zu bestätigen. Dies ergänzt klassische Methoden der Zuverlässigkeitsbestätigung, wie die Modellüberprüfung und mathematische Nachweise zur Übereinstimmung des Codes mit den Spezifikationen in einer formalen Sprache. Zu den Vorteilen von RV gehört die Möglichkeit, eine strenge Verifizierung zu gewährleisten, ohne dass eine separate Implementierung des gesamten Systems in einer Modellierungssprache erforderlich ist. Außerdem ermöglicht sie eine flexible Reaktion auf unvorhergesehene Ereignisse, zum Beispiel zur Verhinderung einer weiteren Ausbreitung von Fehlern in kritischen Systemen.
Quelle: opennet.ru
