Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

技術要約：LustreにおけるSTLを用いた実行時検証のための同期型オブザーバの再考

問題提起
信号時相論理（STL）は、サイバーフィジカルシステム（CPS）、特に実行時検証において、時間的な安全性プロパティを規定するための標準的な形式手法である。しかし、既存のSTLツールは、通常、事前に記録された信号や抽象的なオートマトンモデルに対して動作しており、実際にデプロイされている実行可能なコードに対して動作するものではない。その結果、入れ子構造を持つSTLプロパティに対して、監視対象のシステムと同期して動作する、実行時相当のセマンティクスを持つ実行可能な仕組みが欠如している。さらに、同期言語であるLustreは静的検証のために「同期型オブザーバ」を使用するが、これらのオブザーバを実行時検証に活用する可能性については、これまで十分に探求されてこなかった。具体的な課題は、「3値」の性質をどのように扱うかにある。有界な時間演算子は未来を展望するため、モニターは各ティック（時刻）において即座に判定を下すことができず、確定的な結論に達くまでに遅延が生じる。

手法
著者らは、同期型STL（SSTL）の断片を、データフロー言語であるLustre内の同期型オブザーバへと直接コンパイルする手法を提案している。この手法の核心は、入れ子になった数式を、固定された離散時間のウィンドウを監視する、入れ子のない有限の義務（obligations）の集合へと「展開（unrolling）」することにある。

1. 3値ストリーミング・セマンティクス： 本手法は、クレイニー（Kleene）の3値セマンティクス（def_true、def_false、unknown）を採用している。各ティックにおいて、オブザーバはこれまでに観測された接頭辞（prefix）に基づき、判定を出力する。Unknownは、数式のホライゾン（期間）がまだ経過していないことを示す。これは、確定的真理（pos）と確定的偽理（neg）を表す一対のブール信号を用いて実装される。
2. プリミティブ構成（until_leaf）： 著者らは、有界な「until」演算子（$U_{[a,b]}$）を実装する、再利用可能な単一のLustreノードであるuntil_leafを合成している。このプリミティブは、前提条件（「生存」信号）と後件条件（「発見」信号）を特定のウィンドウにわたって追跡する。これは、証拠が見つかった場合にdef_trueを、早期終了（前提条件の失敗）またはウィンドウの満了によってdef_falseを出力する。
3. 再帰的合成： 入れ子になった数式は、ボトムアップで合成される。システムは、外側の演算子によって必要とされるすべての開始オフセットに対して、until_leafプリミティブのコピーをインスタンス化する。これらのコピーは、論理積（AND）、論理和（OR）、および否定（NOT）に関するクレイニー論理の規則に従って結合される。
   • 有界演算子（$\square_{[a,b]}$、$\diamond_{[a,b]}$）の場合、合成プロセスは、区間内の各開始オフセットに対応するリーフ（葉）へと数式を展開する。
   • フリーランニング・システムで一般的な、無界のGlobally演算子（$\square$）については、シフトレジスタ構成を導入している。無限のオブザーバをインスタンス化する代わりに、$H+1$（$H$は内部ホライゾン）のサイズのレジスタが状態を再利用し、内側の数式の「生存」コピーを無期限に追跡することを可能にする。
4. 可視化： 編集可能なトレース上で入れ子になったオブザーバの3値判定をレンダリングする、インタラクティブなブラウザベースのツールが提供されている。これは、複雑な入れ子状の時間的挙動のデバッグや直感的な理解を助ける。

主な貢献

1. 実行可能なオンライン・モニタリング： 本手法は、実際の実行可能なコードと同じ同期言語（Lustre）内で共にコンパイルされ、システムとロックステップで動作するオブザーバを合成する。
2. 任意の入れ子構造を持つモジュール式コンパイル： 非入れ子演算子に限定されていた先行研究（Bellangerら）とは異なり、本手法は任意の入れ子構造を持つ有界SSTLプロパティをサポートする。
3. 無界の外側演算子： 本アプローチは、内側の構造を有界に保ちつつ、フリーランニング・システムに適したグローバルに無界な外側演算子（$\square$）を受け入れる。
4. 二重の有用性： 得られるオブザーバは二重の目的を果たす。これらは実行時モニターとして機能すると同時に、副産物として、別途モデルを用意することなくKind2モデルチェッカーに対する静的検証義務としても機能する。
5. 実行時のための3値セマンティクス： 実装は因果的なクレイニー判定を提供し、トレースが許容する限り、モニターが確定的な回答を早期に確定できるようにする。

結果と評価
著者らは、スプリング・マス・システムと、緊急ブレーキを伴う車間距離制御（ACC）シナリオの2つのケーススタディを用いて、本手法を評価した。

• 正確性： 合成されたすべてのオブザーバは、Kind2モデルチェッカーによって検証された。実行時と静的な判定は、相互排除不変量（$pos \land neg = \text{false}$）を含むすべてのプロパティにおいて一致した。
• パフォーマンス： オブザーバはC言語にコンパイルされ、lv6インタプリタを介して実行された。ティックあたりの実行コストはナノ秒単位（複雑さに応じて約6.7 nsから206.5 nsの範囲）で測定され、典型的なミリ秒スケールの制御周期を大幅に下回っており、オンライン展開への実現可能性が確認された。
• 早期終了： 3値セマンティクスは効果的であった。ケーススタディにおいて、有界プロパティは理論上のホライゾンよりも厳密に早く確定的な判定に達した。例えば、深く入れ子になったプロパティ（$P3$）は、15ティック早く確定した。
• 無界の挙動： 無界の$\square$演算子は、違反が発生した際に（例：ギャップが安全閾値を下回った場合）正しくdef_falseにラッチする反証メカニズムとして機能し、それ以外の場合はunknownのままとなった。

意義と主張
本論文は、形式的な仕様と、同期型CPSの実行可能な実行時モニタリングとの間の隔たりを埋めることを主張している。システムの言語で直接オブザーバを合成することにより、著者らは、展開されたコードに対して抽象モデルを検証する際に見られる「モデリングの乖離」を排除している。本研究は、複雑で入れ子になった時間的プロパティを、低レイテンシかつ高信頼性でオンライン監視できることを示している。著者らは、本研究を、入れ子の深さと静的検証への偏りに焦点を当てたBellangerら[5]の拡張として位置づけている。その貢献は、明示的な3値セマンティクスに対して健全かつ完全な、体系的な合成手法として提示されており、実行時実行と静的モデルチェックの両方を通じて検証されている。

限界
著者らは、主に3つの限界を認めている。

1. 状態爆発： リーフの数はウィンドウ幅の積となるため、大きな区間（例：$\diamond_{[0,100]}$）においてオブザーバのサイズが指数関数的に増大する可能性がある。
2. 閉じた系の仮定： ケーススタディでは、プラントをLustre内の閉じた系としてモデル化している。外部センサー入力を持つ真の開放系を監視することは、今後の課題である。
3. 離散ドメイン： 現在のアプローチは、厳密にサンプリングされた離散ドメイン内で動作しており、連続的なSTLロバストネス・セマンティクスはまだサポートしていない。