技術要約：Lolaにおける実行時検証とモデルベース診断の統合フレームワーク

問題提起

安全クリティカルなシステムには、故障の検出だけでなく、効果的な緩和策を講じるための根本原因の特定も求められる。**実行時検証（Runtime Verification: RV）は、実行中の振る舞いから仕様からの逸脱を検出するのに有効であり、一方でモデルベース診断（Model-Based Diagnosis: MBD）**は、故障したコンポーネントを特定するための原理的なフレームワークである。しかし、これら二つの手法は歴史的に孤立して運用されてきた。従来のRVモニタは、仕様違反を検出するために、潜在的に無制限な状態シーケンスにわたるシステム挙動を分析するが、MBDは通常、故障が検出された後の、特定されない単一の時点において動作する。さらに、既存の統合手法は、検出された故障アクションをMBDの意味における異常なコンポーネントに直接マッピングできなかったり、統一されたストリームベースの推論フレームワーク内での不確実な入力や時間的な故障ダイナミクスを扱う能力を欠いていたりすることが多い。

手法

本論文では、ストリームベースの仕様記述言語であるLola内で、ストリームベースのRVとMBDを統合する統一フレームワークを提案する。コアとなる手法は、検証と診断の両方の情報を特殊なストリームとしてエンコードすることであり、これにより、不確実性下での継続的な観測と記号的推論が可能になる。

1. Lolaにおける統一エンコーディング

著者らは、診断対象のシステム $S = (sd, comps)$ をLolaシステム $(\phi, comps)$ へとマッピングする：

• **システム記述 ($sd$):** **仮定ストリーム** ($\alpha$) にエンコードされる。これは定義により真である。このストリームには、行動知識（例：$ \neg ab(c) \to beh_c $）およびシステムの一般的な知識が含まれる。
• コンポーネント ($comps$):** 各コンポーネント$c$は、そのコンポーネントが異常（$ab(c)$）であることを示す内部ブール・ストリーム**によって表される。
• 観測: 観測可能なシステム変数（入力/出力）は、確定的（決定論的）または不確実（非決定論的な区間または集合）な入力ストリームとしてモデル化される。
• 観測不可能な変数: 直接測定されない内部システム値は、内部ストリームとしてモデル化される。
• 診断問題インスタンス (DPI): タプル $(\phi, comps, \Psi)$ であり、ここで $\Psi$ は現在時刻までの入力制約の履歴を表す。

2. 記号的推論と診断計算

フレームワークは、時刻 $t$ までの観測と整合するすべての可能なシステム挙動を表す制約集合 $[\phi]_{\Psi}^{\leq t}$ を維持する記号的モニタを利用する。

• 制約解決: 制約の整合性をチェックし、含意を導出するために、SMTソルバ（例：Z3）が使用される。
• 診断の導出: 診断とは、システム記述を観測事項と整合させるコンポーネントの状態（正常/異常）に関する仮定である。フレームワークは、最小の衝突（すべてのコンポーネントが正常ではあり得ない集合）を特定し、それらの最小ヒット集合を計算することで、最小診断を算出する。
• プルーニング（枝刈り）: 監視を定数時間かつ定数空間で行うために、制約を書き換えて制約集合のサイズを制限し、必要な履歴情報のみを保持するプルーニング戦略を用いる。

3. 診断シナリオ

フレームワークは、コンポーネントの故障の性質に基づき、以下の3つの異なる診断モードをサポートする：

• マルチインスタント診断: コンポーネントの状態が過去 $k$ インスタント（$t-k$ から $t$ まで）のウィンドウ内で静的であると仮定する。$k$-インスタント診断は、このウィンドウ内のすべての観測を説明する。論文では、非時間的（atemporal）な仕様に対しては、$k$-インスタント診断は単一インスタント診断の集約と同等であるが、時間的（temporal）な仕様（非ゼロのオフセットを持つもの）に対しては、より焦点を絞った結果を提供することを証明している。
• 時間的診断: コンポーネントの状態が時間の経過とともに変化することを許容する。$k$-テンポラル診断は、コンポーネント $c$ が具体的に時刻 $t'$ において異常であることを示すペアの集合 $(c, t')$ である。これは、過熱などの一時的な故障や、伝播によって後に顕在化する故障を特定するために極めて重要である。
• 拡張設定: 背景知識（コンポーネントを強制的に正常とする）、強力な故障モデル（特定の故障挙動を指定する）、および抽象的なモデリングを自然に組み込むことができる。

主な貢献

1. 統一エンコーディング: システム記述と診断の仮定をLolaにおける特殊なストリームとして表現する方法。これは、観測された挙動に対するすべての有効な診断を暗黙的に表現する。
2. マルチインスタント診断理論: 観測の移動ウィンドウにおける時間不変な故障を診断するための一般化された理論であり、標準的なマルチ観測診断を特殊なケースとして包含する。
3. 時間的診断: 時間依存の異常性をサポートし、「どの」コンポーネントが故障しているかだけでなく、「いつ」故障が発生したかを特定することを可能にする。
4. 柔軟な診断シナリオ: 単一のストリームベースのフレームワーク内で、背景知識、抽象的モデリング、および様々な故障タイプ（持続的 vs 一時的）をエレガントに扱う能力。
5. 実装と評価: HS-Treeアルゴリズム、QuickXplain、およびZ3を統合したプロトタイプ実装を、ISCAS85およびISCAS89のベンチマークを用いて検証した。

結果

著者らは、2つのブール回路を用いてフレームワークを評価した：

• c17 (ISCAS85): 6つのコンポーネントを持つ純粋な組合せ回路。
• s27 (ISCAS89): 14個のコンポーネントを持つ順序回路。

知見:

• 実現可能性: フレームワークは、両方の回路において実際に注入された故障（stuck-at-false）を正常に特定した。
• 時間的精度: 順序回路（s27）において、フレームワークは、観測ウィンドウ（$k$）が故障の発生源と伝播時間をカバーするのに十分な大きさである場合にのみ、故障を正しく局所化した。
• パフォーマンス:
  • 実行時間は $k$ の値が大きくなるにつれて増加した。c17の場合、$k$-インスタント診断は1インスタントあたり最大246 ms（$k=0$）から775 ms（$k=31$）まで要した。
  • 時間的診断は、$(c, t')$ を個別のコンポーネントとして扱うことによる組合せ爆発のため、大幅にコストが高くなった。c17の場合、時間的診断は $k=5$ で1インスタントあたり最大8.7秒、$k=12$ で136秒を要した。
  • 計算コストにもかかわらず、著者らは、定数 $k$ を用いることで実行時間が全トレース長に依存しなくなることを指摘しており、プルーニング戦略の実行可能性を裏付けている。

重要性と主張

本論文は、実行時検証とモデルベース診断のコンパクトで根拠のある統合を提供すると主張している。その重要性は、自動化された故障検出（RV）と体系的な根本原因分析（MBD）の間の溝を、単一のストリームベースのフレームワーク内で埋めた点にある。

著者らは、このアプローチが以下の特性を持つことを強調している：

• 不確実な入力と環境の仮定をサポートし、専門知識に基づく精緻な推論を可能にする。
• 記号的推論を活用して各時点での判定を生成することにより、オンライン診断を可能にする。
• RV（効率的かつ継続的な監視）とMBD（原理的な根本原因分析）の強みを統合した相乗的な組み合わせを提供する。
• 制約によって定義されるすべての「可能世界」と導出された値が整合することを保証する、**健全な（sound）**フレームワークである。

本研究は、Lolaを複雑な診断タスクに使用することの実現可能性を示す概念実証として提示されており、安全クリティカルなシステムにおける将来的な実用的応用のための理論的基礎を提供するものである。