Linux 5.20 カーネル (おそらくブランチには 6.0 の番号が付けられるでしょう) に組み込まれるために、信頼性の高いシステムでの正しい動作をチェックする手段である RV (Runtime Verification) メカニズムの実装を伴う一連のパッチが提案されています。障害がないことを保証します。 検証は、システムの予期される動作を決定するオートマトンの所定の参照決定論的モデルに対して実際の実行の進行状況をチェックするトレースポイントにハンドラーをアタッチすることによって実行時に行われます。
トレースポイントからの情報によってモデルはある状態から別の状態に移動され、新しい状態がモデルのパラメーターと一致しない場合、警告が生成されるか、カーネルが「パニック」状態になります (信頼性の高いシステムでは、そのような状況を検出して対応します）。 ある状態から別の状態への遷移を定義するオートマトン モデルは、「ドット」 (graphviz) 形式にエクスポートされ、その後、dot2c ユーティリティを使用して C 表現に変換され、偏差を追跡するカーネル モジュールの形式でロードされます。事前定義されたモデルから実行の進行状況を確認します。
ランタイム モデル チェックは、モデル チェックやコードが指定された仕様に準拠していることの数学的証明など、信頼性検証の古典的な方法を補完する、ミッション クリティカルなシステムでの実行の正しさを検証する、より軽量で実装が簡単な方法として位置付けられています。形式的な言語で。 RV の利点には、システム全体をモデリング言語で個別に実装することなく厳密な検証を提供できることと、たとえば重要なシステムでの障害のさらなる伝播をブロックするなど、予期せぬイベントに柔軟に対応できることが挙げられます。
出所： オープンネット.ru