為了包含在Linux 核心5.20（也許該分支將編號為6.0）中，提出了一組補丁，其中實現了RV（運行時驗證）機制，該機制提供了用於檢查高可靠系統上正確操作的工具，以保證沒有失敗。 驗證是在運行時透過將處理程序附加到追蹤點來執行的，這些點根據定義系統預期行為的自動機的預定參考確定性模型檢查實際執行進度。
來自追蹤點的資訊將模型從一種狀態移動到另一種狀態，如果新狀態與模型的參數不匹配，則會產生警告或將核心置於「恐慌」狀態（高可靠性系統預計會檢測到）並應對此類情況）。 定義從一種狀態到另一種狀態的轉換的自動機模型被導出為「點」格式 (graphviz)，之後使用 dot2c 實用程式將其轉換為 C 表示形式，該表示形式以內核模組的形式加載，追蹤執行進度與預定義模型的偏差。
運行時模型檢查被定位為一種更輕量級且更易於實現的方法，用於驗證關鍵任務系統上的正確執行，補充了經典的可靠性驗證方法，例如模型檢查和代碼符合正式規範中給出的規範的數學證明。語言。 RV 的優點之一是能夠提供嚴格的驗證，而無需使用建模語言單獨實現整個系統，並且能夠靈活地回應不可預見的事件，例如阻止關鍵系統中故障的進一步傳播。
來源： opennet.ru