第6章 リアルタイムカーネルのランタイム検証
ランタイム検証は、システムイベントとその正式な仕様における動作等価性をチェックするための軽量かつ厳密な方法です。ランタイム検証では、tracepoints に接続するカーネルに統合されたモニターを使用します。システムの状態が定義された仕様から逸脱した場合、ランタイム検証プログラムはリアクターをアクティブにして、ログファイルにイベントをキャプチャーしたり、極端なケースでは障害伝播を防止するためにシステムをシャットダウンしたりするなどの対応を、通知するか可能にします。
6.1. ランタイムモニターとリアクター
ランタイム検証 (RV) モニターは、RV モニター抽象概念にカプセル化され、定義された仕様とカーネルトレースの間で調整を行い、ランタイムイベントをトレースファイルにキャプチャーします。RV モニターには以下が含まれます。
- 参照モデル。これはシステムの参照モデルです。
- モニターインスタンス。これは、CPU ごとのモニターやタスクごとのモニターなどの、モニターのインスタンスのセットです。
- モニターをシステムに接続するヘルパー関数。
ランタイム時にシステムを検証および監視することに加えて、予期しないシステムイベントへの応答を有効にすることができます。反応の形式は、トレースファイルへのイベントのキャプチャーから、極端な反応 (安全性が重要なシステムでシステム障害を回避するためのシャットダウンなど) の開始まで、さまざまです。
リアクターは、必要に応じてシステムイベントへの反応を RV モニターが定義するために使用できる反応方法です。デフォルトでは、モニターはアクションのトレース出力を提供します。
