Zur Aufnahme in den Kernel Linux 5.20 (möglicherweise erhĂ€lt der Branch die Nummer 6.0) wurde ein Satz von Patches vorgeschlagen, der die Implementierung des Mechanismus RV (Runtime Verification) umfasst, der Mittel zur ĂberprĂŒfung der Korrektheit des Betriebs in hochzuverlĂ€ssigen Systemen bereitstellt, die eine Ausfallfreiheit garantieren. Die ĂberprĂŒfung erfolgt wĂ€hrend der AusfĂŒhrung durch das Anheften von Handlern an Tracepoints, die den tatsĂ€chlichen Ablauf der AusfĂŒhrung mit einem im Voraus definierten Referenzmodell eines Automaten abgleichen, das das erwartete Verhalten des Systems festlegt.
Die Informationen von den Tracepoints ĂŒbertragen das Modell von einem Zustand in einen anderen, und wenn der neue Zustand nicht den Parametern des Modells entspricht, wird eine Warnung generiert oder der Kernel wird in den Zustand âpanicâ versetzt (es wird davon ausgegangen, dass hochzuverlĂ€ssige Systeme solche Situationen erkennen und darauf reagieren). Das Automatmodell, das die ĂbergĂ€nge von einem Zustand in einen anderen definiert, wird im âdotâ-Format (graphviz) exportiert und anschlieĂend mithilfe des Tools dot2c in eine C-Darstellung ĂŒbersetzt, die als Kernel-Modul geladen wird, das Abweichungen vom bestimmten Modell ĂŒberwacht.
Der Abgleich mit dem Modell wĂ€hrend der AusfĂŒhrung wird als leichter und einfacher umsetzbarer Ansatz zur BestĂ€tigung der Korrektheit der AusfĂŒhrung in kritischen Systemen positioniert, ergĂ€nzt durch klassische Methoden zur BestĂ€tigung der ZuverlĂ€ssigkeit, wie ModellĂŒberprĂŒfung und mathematische Nachweise der Ăbereinstimmung von Code mit den auf formalem Sprach vorgesehenen Spezifikationen. Zu den Vorteilen von RV gehört die Möglichkeit, eine strenge Verifikation ohne separate Implementierung des gesamten Systems in einer Modellierungssprache zu gewĂ€hrleisten, sowie eine flexible Reaktion auf unvorhergesehene Ereignisse, um beispielsweise eine weitere Verbreitung von Fehlern in kritischen Systemen zu blockieren.
Quelle: opennet.ru
