実行時検証

Java Iteratorインターフェイスでは、メソッドが呼び出されるhasNext()前に、メソッドが呼び出されて true を返す必要がありますnext()。これが起こらない場合、ユーザーがコレクションの「末尾を超えて」反復処理してしまう可能性が非常に高くなります。右の図は、実行時検証によってこのプロパティをチェックおよび強制するためのモニタを定義する有限状態機械を示しています。不明なnext()状態からメソッドを呼び出すことは、そのような操作が安全でない可能性があるため、常にエラーになります。hasNext()が呼び出されてtrue を返す場合、を呼び出すのは安全なnext()ので、モニタはmore状態に入ります。ただし、メソッドがfalse をhasNext()返す場合、要素はもうなく、モニタはnone状態に入ります。more 状態と none 状態では、メソッドを呼び出しても新しい情報は得られません。more 状態からメソッドを呼び出すのは安全ですが、要素がさらに存在するかどうかは不明になるため、モニタは最初のunknown状態に戻ります。最後に、 none状態からメソッドを呼び出すと、エラー状態に入ります。以下は、パラメトリック過去時間線形時相論理を使用したこのプロパティの表現です。hasNext()next()next()

${\displaystyle \forall ~{\text{Iterator}}~i\quad i.{\text{next}}()~\rightarrow ~\odot (i.{\text{hasNext}}()==true)}$

この式は、next()メソッドの呼び出しの直前に、hasNext()true を返すメソッドの呼び出しがなければならないことを示しています。ここでのプロパティは、イテレータでパラメトリックですi。概念的には、これはテスト プログラム内の可能なイテレータごとにモニターのコピーが 1 つ存在することを意味しますが、ランタイム検証システムはパラメトリック モニターをこのように実装する必要はありません。このプロパティのモニターは、式に違反したとき (つまり、有限状態機械がエラーnext()状態に入ったとき) にハンドラをトリガーするように設定されます。これは、を最初に呼び出さずにが呼び出された場合hasNext()、またhasNext()はがの前に呼び出されたがfalse がnext()返された場合に発生します。

Java のVectorクラスには、要素を反復処理するための 2 つの方法があります。前の例で示したように Iterator インターフェイスを使用する方法と、Enumerationインターフェイスを使用する方法です。Iterator インターフェイスには remove メソッドが追加されていますが、主な違いは、Iterator は「fail fast」であるのに対し、Enumeration はそうではない点です。つまり、Iterator を使用して Vector を反復処理しているときに、(Iterator の remove メソッドを使用する以外の方法で) Vector を変更すると、ConcurrentModificationExceptionがスローされます。しかし、前述のように、Enumeration を使用する場合はそうではありません。Enumeration の観点から Vector が矛盾した状態になるため、プログラムから非決定的な結果が生じる可能性があります。Enumeration インターフェイスをまだ使用しているレガシー プログラムでは、基となる Vector が変更されたときに Enumeration が使用されないように強制したい場合があります。この動作を強制するには、次のパラメトリック正規パターンを使用できます。

∀ Vector v , Enumeration e : ( e = v .elements()) ( e .nextElement()) ^* v .update() e .nextElement()

このパターンは、列挙型とベクトルの両方でパラメトリックです。直感的には、そして上記のように、ランタイム検証システムはパラメトリックモニタをこのように実装する必要はありませんが、このプロパティのパラメトリックモニタは、ベクトルと列挙型の可能なペアごとに非パラメトリックモニタインスタンスを作成して追跡すると考えることができます。一部のイベントは、複数のモニタに同時に関係する場合があります。たとえばv.update()、ランタイム検証システムは、（概念的に）それらをすべての関心のあるモニタにディスパッチする必要があります。ここでは、プロパティが指定されているため、プログラムの悪い動作を示します。したがって、このプロパティは、パターンに一致するかどうかを監視する必要があります。右の図は、このパターンに一致し、プロパティに違反するJavaコードを示しています。ベクトルvは、列挙型eが作成された後で更新され、その後eが使用されます。

前述の2つの例は有限状態の特性を示していますが、実行時検証で使用される特性ははるかに複雑になる可能性があります。SafeLock特性は、特定のメソッド呼び出し内で、(再入可能な)Lockクラスの取得と解放の回数が一致するというポリシーを強制します。もちろん、これはロックを取得したメソッド以外でのロックの解放を禁止しますが、これはテスト対象システムが達成すべき望ましい目標である可能性が非常に高いです。以下に、パラメトリックなコンテキストフリーパターンを使用したこの特性の仕様を示します。

∀ スレッドt、ロックl : S →ε | S begin( t ) S end( t ) | S l .acquire( t ) S l .release( t )

このパターンは、各スレッドとロックに対して、入れ子になった開始/終了と取得/解放のペアのバランスの取れたシーケンスを指定します（${\displaystyle \epsilon }$は空のシーケンスです。ここで、begin と end は、プログラム内のすべてのメソッドの開始と終了 (acquire と release の呼び出しを除く) を指します。メソッドの開始と終了を関連付ける必要があるのは、それらが同じスレッドに属している場合のみであるため、これらはスレッドでパラメトリックです。acquire と release イベントも、同じ理由でスレッドでパラメトリックです。さらに、ある Lock のリリースを別の Lock の取得に関連付けたくないため、Lock でもパラメトリックです。極端な場合、Thread と Lock の可能な組み合わせごとに、プロパティのインスタンス、つまりコンテキストフリー解析メカニズムのコピーが存在する可能性があります。これも直感的に理解できます。実行時検証システムが同じ機能を異なる方法で実装する可能性があるためです。たとえば、システムに Threads がある場合、$t1$、$t2$、 そして$t3$ロック付き${\displaystyle l_{1}}$そして${\displaystyle l_{2}}$すると、ペアのプロパティ インスタンスを維持する必要が生じる可能性があります <$t1$、${\displaystyle l_{1}}$>, <$t1$、${\displaystyle l_{2}}$>, <$t2$、${\displaystyle l_{1}}$>, <$t2$、${\displaystyle l_{2}}$>, <$t3$、${\displaystyle l_{1}}$>、および <$t3$、${\displaystyle l_{2}}$このプロパティは、パターンが正しい動作を指定しているため、パターンに一致しない場合は監視する必要があります。右の図は、このプロパティに違反する2つのトレースを示しています。図の下方向のステップはメソッドの開始を表し、上方向のステップは終了を表します。図中の灰色の矢印は、同じロックの取得と解放の一致を示しています。簡略化のため、トレースには1つのスレッドと1つのロックのみが表示されています。

実行中のシステムを監視すると、通常は実行時にオーバーヘッドが発生します（ハードウェアモニタの場合は例外となる場合があります）。特に生成されたモニタがシステムとともに展開される場合は、実行時検証ツールのオーバーヘッドを可能な限り削減することが重要です。実行時オーバーヘッドを削減する手法には、以下のようなものがあります。

• 計測機能の改善。実行中のシステムからイベントを抽出し、それをモニターに送信する処理は、単純に行うと実行時に大きなオーバーヘッドが発生する可能性があります。既存の実行ログを明示的に対象とするツールでない限り、適切なシステム計測はあらゆる実行時検証ツールにとって不可欠です。現在使用されている計測手法は数多くあり、それぞれに長所と短所があります。カスタム計測や手動計測から、専用ライブラリ、アスペクト指向言語へのコンパイル、仮想マシンの拡張、ハードウェアサポートの活用まで多岐にわたります。
• 静的解析との組み合わせ。コンパイラでよく見られる静的解析と動的解析の一般的な組み合わせは、静的に満たせないすべての要件を監視することです。実行時検証では、最終的には同等の二重のアプローチが標準になりつつあり、それは静的解析を使用して、そうでなければ網羅的な監視の量を減らすことです。静的解析は、監視対象のプロパティと監視対象のシステムの両方に対して実行できます。監視対象のプロパティの静的解析により、特定のイベントを監視する必要がないこと、特定のモニターの作成を遅延できること、および特定の既存のモニターがトリガーされないためガベージコレクションできることが明らかになります。監視対象のシステムの静的解析により、モニターに影響を与えないコードを検出できます。たとえば、上記のHasNextプロパティを監視する場合、各呼び出しの直前に、どのパスでもtrueを返す呼び出しがある（制御フロー グラフで確認できる）を計測する必要はありません。i.next()i.hasnext()
• 効率的なモニタの生成と管理。上記の例のようなパラメトリックなプロパティを監視する場合、監視システムは、各パラメータ インスタンスに関して監視対象プロパティの状態を追跡する必要があります。このようなインスタンスの数は理論的には無制限であり、実際には膨大になる傾向があります。重要な研究課題は、観測されたイベントを、それを必要とするインスタンスに効率的にディスパッチする方法です。関連する課題は、このようなインスタンスの数を小さく保つ方法 (ディスパッチが速くなるように)、言い換えれば、不要なインスタンスの作成をできるだけ長く回避する方法、および、不要になったインスタンスをすぐに削除する方法です。最後に、パラメトリック監視アルゴリズムは通常、非パラメトリックモニタを生成するための同様のアルゴリズムを一般化します。したがって、生成された非パラメトリックモニタの品質が、結果として得られるパラメトリックモニタの品質を決定します。ただし、他の検証アプローチ (モデル検査など) とは異なり、ランタイム検証では、状態の数や生成されたモニタのサイズはそれほど重要ではありません。実際、一部のモニターは、上記のSafeLockプロパティのように、無限に多くの状態を持つことができますが、どの時点においても発生している状態は有限個に限られます。重要なのは、実行システムからイベントを受信した際に、モニターがどれだけ効率的にある状態から次の状態へ遷移するかということです。

形式的なアプローチ全般における主要な実用上の障害の一つは、ユーザーが仕様書の読み書き方法を知りたがらない、あるいは学びたくないという点である。デッドロックやデータ競合などの仕様書は暗黙的に存在する場合もあるが、ほとんどの場合は作成する必要がある。さらに、特に実行時検証の文脈では、既存の仕様記述言語の多くが、意図した特性を十分に表現できないという問題もある。

• より優れた形式体系。ランタイム検証コミュニティでは、従来の仕様形式体系よりもランタイム検証に適したアプリケーションドメインに適合する仕様形式体系の設計に多大な労力が費やされてきました。これらの形式体系の中には、従来の形式体系に構文上の変更をほとんど、あるいは全く加えず、意味論（例えば、有限トレースと無限トレースの意味論など）と実装（ブッチオートマトンではなく最適化された有限状態機械など）のみを変更するものがあります。また、上記の例に見られるように、パラメータの追加など、ランタイム検証には適しているものの、他の検証手法には容易には適用できない機能で既存の形式体系を拡張するものもあります。最後に、ランタイム検証専用に設計された仕様形式体系もあり、このドメインで最大限の成果を上げようとし、他のアプリケーションドメインについてはほとんど考慮していません。ランタイム検証のための普遍的に優れた、あるいはドメイン固有の優れた仕様形式体系を設計することは、現在も、そして今後も主要な研究課題の一つであり続けるでしょう。
• 定量的特性。他の検証手法と比較して、ランタイム検証はシステム状態変数の具体的な値に基づいて動作できるため、プログラム実行に関する統計情報を収集し、この情報を用いて複雑な定量的特性を評価することが可能です。この機能を最大限に活用するためには、より表現力豊かな特性言語が必要です。
• より優れたインターフェース。プロパティ仕様の読み書きは、専門家以外にとっては容易ではありません。専門家でさえ、比較的小さな時相論理式（特にネストされた「until」演算子を含む場合）を何分も見つめてしまうことがよくあります。重要な研究分野は、さまざまな仕様形式に対応した強力なユーザーインターフェースを開発し、ユーザーがプロパティをより簡単に理解、記述、そして場合によっては視覚化できるようにすることです。
• 仕様のマイニング。ユーザーが仕様を作成するのに役立つツールサポートがどのようなものであっても、特に些細な仕様の場合は、そもそも仕様を書かなくて済む方が、ほとんどの場合、ユーザーにとってありがたいでしょう。幸いなことに、プロパティを取得したいアクション/イベントを正しく使用すると思われるプログラムは数多く存在します。そうであれば、それらの正しいプログラムから必要なプロパティを自動的に学習することで、それらのプログラムを活用したいと思うのは当然です。自動的にマイニングされた仕様の全体的な品質は、手動で作成された仕様よりも低いと予想される場合でも、それらは後者の出発点として、あるいはバグの発見を目的とした自動ランタイム検証ツールの基盤として使用できます（仕様が不十分だと、テスト中に許容されることが多い誤検出や誤否定につながります）。

ランタイム検証ツールのエラー検出能力は、実行トレースの分析能力に大きく依存します。モニターがシステムとともに展開される場合、ランタイムオーバーヘッドを低く抑えるため、計測は通常最小限に抑えられ、実行トレースも可能な限り単純化されます。テストにランタイム検証を使用する場合は、より包括的な計測が可能となり、イベントに重要なシステム情報を付加することで、モニターが実行システムのより洗練されたモデルを構築し、分析できるようになります。例えば、イベントにベクトルクロック情報、データフロー情報、制御フロー情報を付加することで、モニターは実行システムの因果モデルを構築できます。このモデルでは、観測された実行はあくまでも可能なインスタンスの一つに過ぎません。モデルと整合性のあるイベントの他の組み合わせは、システムの実行可能なシナリオであり、異なるスレッドインターリーブで発生する可能性があります。このように推論された実行におけるプロパティ違反を（監視することで）検出​​することで、モニターは観測された実行では発生しなかったものの、同じシステムの別の実行で発生する可能性のあるエラーを予測できるようになります。重要な研究課題の一つは、可能な限り多くの他の実行トレースを含む実行トレースからモデルを抽出することである。

テストや徹底的な検証とは異なり、ランタイム検証は、再構成、マイクロリセット、あるいはチューニングやステアリングと呼ばれるよりきめ細かな介入メカニズムを通じて、検出された違反からシステムが回復することを可能にするという利点があります。これらの技術をランタイム検証の厳格なフレームワーク内で実装すると、新たな課題が生じます。

• アクションの仕様。 ユーザーが実装の詳細を知る必要がないように、実行すべき変更内容を抽象的に指定する必要があります。さらに、システムの整合性を維持するために、そのような変更がいつ実行できるかを指定する必要があります。
• 介入効果についての考察。 介入が状況を改善する、あるいは少なくとも状況を悪化させないことを確認することが重要です。
• アクションインターフェース。 監視のための計測と同様に、システムがアクション呼び出しを受け取れるようにする必要があります。呼び出しメカニズムは必然的にシステムの実装の詳細に依存します。しかし、仕様レベルでは、どのようなアクションをいつ、どのような条件下で適用すべきかを指定することで、ユーザーにシステムへのフィードバックを宣言的に提供する必要があります。

ランタイム検証の研究者たちは、プログラム計測をモジュール的に定義する手法として、アスペクト指向プログラミング（AOP ）の可能性に着目しました。アスペクト指向プログラミング（AOP）は一般的に、横断的な関心のモジュール化を促進します。ランタイム検証はまさにそのような関心の一つであり、AOPの特定の特性から恩恵を受けることができます。アスペクト指向のモニタ定義は大部分が宣言的であるため、命令型プログラミング言語で記述されたプログラム変換によって表現される計測よりも、推論が容易になる傾向があります。さらに、すべての計測が単一のアスペクト内に含まれているため、静的解析では、他の形式のプログラム計測よりも、監視アスペクトについて推論しやすくなります。そのため、現在の多くのランタイム検証ツールは、表現力豊かな高レベル仕様を入力として受け取り、何らかのアスペクト指向プログラミング言語（AspectJなど）で記述されたコードを出力として生成する仕様コンパイラの形で構築されています。

実行時検証は、証明可能な正しいリカバリコードと組み合わせて使用​​すれば、プログラム検証のための非常に貴重なインフラストラクチャを提供し、後者の複雑さを大幅に軽減できます。たとえば、ヒープソートアルゴリズムを形式的に検証することは非常に困難です。これを検証するためのより簡単な手法は、ソート対象の出力を監視し（線形複雑度モニタ）、ソートされていない場合は、挿入ソートなどの簡単に検証できる手順を使用してソートすることです。結果として得られるソートプログラムは、より簡単に検証できます。ヒープソートに求められるのは、マルチセットと見なされる元の要素を破壊しないことだけであり、これははるかに簡単に証明できます。反対の方向から見ると、形式検証を使用して実行時検証のオーバーヘッドを削減できます。これは、形式検証の代わりに静的解析を使用する場合にすでに述べたとおりです。実際、完全に実行時検証された、おそらく低速なプログラムから始めることができます。次に、コンパイラが静的解析を使用して型の正しさやメモリの安全性の実行時チェックを解除するのと同様に、形式検証（または静的解析）を使用してモニタを解除できます。

従来型の検証手法と比較すると、ランタイム検証の大きな欠点は、カバレッジが低いことです。ランタイムモニタがシステムとともに（プロパティ違反時に実行される適切なリカバリコードとともに）展開されている場合は問題ありませんが、システムのエラー検出にランタイム検証を使用する場合は、その有効性が制限される可能性があります。エラー検出目的でランタイム検証のカバレッジを高めるための手法には、以下のようなものがあります。

• 入力生成。適切な入力セット（プログラム入力変数値、システムコール値、スレッドスケジュールなど）を生成することで、テストの有効性を大幅に向上させることができることはよく知られています。これは、エラー検出に使用されるランタイム検証にも当てはまりますが、入力生成プロセスを駆動するためにプログラムコードを使用することに加えて、ランタイム検証では、利用可能な場合はプロパティ仕様を使用したり、監視技術を使用して望ましい動作を誘発したりすることもできます。このランタイム検証の使用方法により、ランタイム検証はモデルベーステストと密接に関連していますが、ランタイム検証仕様は通常、テスト目的で作成されるとは限らず、汎用的なものです。たとえば、上記の汎用的なUnsafeEnumプロパティをテストしたいとします。システム実行をパッシブに監視するために前述のモニターを生成する代わりに、2 番目のe.nextElement()イベントを生成しようとしているスレッドを（生成する直前に）フリーズさせ、他のスレッドを実行させて、そのうちの 1 つがv.update()イベントを生成することを期待し、その場合はエラーが見つかったという、よりスマートなモニターを生成できます。
• 動的シンボリック実行。シンボリック実行では、プログラムは具体的な入力なしに、つまりシンボリックに実行および監視されます。システムの1回のシンボリック実行で、多数の具体的な入力を処理できます。既製の制約解決または充足可能性チェックの手法は、シンボリック実行を駆動したり、その空間を体系的に探索したりするためによく使用されます。基盤となる充足可能性チェックが選択点を処理できない場合、その点を通過するために具体的な入力を生成できます。この具体的な実行とシンボリック実行の組み合わせは、コンコリック実行とも呼ばれます。