実行時検証

実行時検証は、実行中のシステムから情報を抽出し、それを使用して特定のプロパティを満たしている、または違反している観察された動作を検出し、場合によってはそれに反応することをベースにしたコンピューティングシステムの分析および実行アプローチです。^{[ 1 ]}データ競合やデッドロックの自由など、いくつかの非常に特殊なプロパティは、通常、すべてのシステムで満たすことが望ましく、アルゴリズム的に実装するのが最適かもしれません。他のプロパティは、形式仕様としてより便利に捉えることができます。実行時検証仕様は通常、有限状態マシン、正規表現、文脈自由パターン、線形時相論理などのトレース述語形式、またはこれらの拡張で表現されます。これにより、通常のテストよりもアドホックでないアプローチが可能になります。ただし、テストオラクルとリファレンス実装に対する検証を含め、実行中のシステムを監視するためのあらゆるメカニズムは、実行時検証と見なされます。正式な要件仕様が提供されると、そこからモニターが合成され、インストルメンテーションによってシステムに組み込まれます。実行時検証は、セキュリティまたは安全性ポリシーの監視、デバッグ、テスト、検証、妥当性確認、プロファイリング、障害保護、動作変更（回復など）など、多くの目的に使用できます。実行時検証では、1つまたは少数の実行トレースのみを分析し、実際のシステムで直接作業することにより、モデルチェックや定理証明などの従来の形式検証手法の複雑さを回避します。そのため、カバレッジは少なくなりますが、比較的スケールアップしやすく、分析結果の信頼性が高まります（システムを形式的にモデル化する面倒でエラーが発生しやすいステップを回避するため）。さらに、リフレクティブ機能により、実行時検証をターゲットシステムの不可欠な部分にして、展開中にその実行を監視およびガイドすることができます。

歴史と文脈

実行中のシステムやプログラムに対して形式的または非形式的に指定されたプロパティをチェックすることは古くからあるテーマであり (有名な例としてはソフトウェアの動的型付け、ハードウェアのフェイルセーフデバイスやウォッチドッグタイマーなど)、その正確な起源を特定するのは困難です。実行時検証という用語は、形式的検証とテストの境界にある問題に対処することを目的とした 2001 年のワークショップ^{[ 2 ]}の名前として正式に導入されました。大規模なコードベースでは、テストケースを手動で記述すると非常に時間がかかります。また、開発中にすべてのエラーを検出できるわけではありません。自動検証への初期の貢献は、NASAエイムズ研究センターでKlaus Havelund とGrigore Rosuによって、宇宙船、ローバー、航空電子工学技術に対する高い安全基準を達成するために行われました^{[ 3 ]} 。彼らは、時相論理の仕様を検証し、単一の実行パスを解析することでJavaプログラムの競合状態とデッドロックを検出するツールを提案しました。

現在、実行時検証技術は、実行時監視、実行時チェック、実行時リフレクション、実行時分析、動的分析、実行時/動的シンボリック分析、トレース分析、ログファイル分析など、様々な別名で呼ばれることがよくあります。これらはすべて、異なる分野、あるいは異なるコミュニティの研究者によって適用された、同じ高レベルの概念の事例を指しています。実行時検証は、デプロイメント前のテスト（特にモデルベーステスト）やデプロイメント中のフォールトトレラントシステムなど、他の確立された分野と密接に関連しています。

実行時検証の広範な領域では、次のようないくつかのカテゴリを区別することができます。

原子性など、主に並行性に関連する一連のプロパティを対象とする「仕様不要」な監視。この分野における先駆的な研究は、SavageらによるEraserアルゴリズム^{[ 4 ]である。}
時相論理仕様に関する監視。この方向への初期の貢献は、Lee、Kannan、および彼らの協力者^{[ 5 ]}^{[ 6 ]}とHavelundとRosuによってなされました。^{[ 7 ]}^{[ 8 ]}

基本的なアプローチ

実行時検証方法の広範な分野は、3つの次元で分類することができます。^{[ 9 ]}

システムは、実行中（オンライン）または実行後に（ログ分析などの形式で）監視できます（オフライン）。
検証コードはシステムに統合されるか (アスペクト指向プログラミングの場合と同様に)、外部エンティティとして提供されます。
モニターは、必要な仕様の違反または検証を報告できます。

それにもかかわらず、実行時検証の基本的なプロセスは同様である：^{[ 9 ]}

モニターは何らかの形式仕様から作成されます。このプロセスは、プロパティが規定されている形式言語の式と等価なオートマトンが存在する場合、通常は自動的に実行されます。正規表現を変換するには有限状態機械を使用できます。線形時相論理のプロパティはBüchiオートマトンに変換できます（線形時相論理からBüchiオートマトンへの変換も参照）。
システムは、実行状態に関するイベントをモニターに送信するようにインストルメントされています。
システムが実行され、モニターによって検証されます。
モニターは受信したイベントトレースを検証し、仕様が満たされているかどうかを判定します。さらに、モニターはシステムにフィードバックを送信し、誤った動作を修正できるようにします。オフライン監視を使用する場合、検証は後から行われるため、原因となったシステムはフィードバックを受け取ることができません。

例

以下の例では、本稿執筆時点（2011年4月）までに、複数の実行時検証グループによって、多少の差異はあるものの検討されてきたいくつかの単純なプロパティについて説明します。より興味深い点として、以下の各プロパティはそれぞれ異なる仕様形式を用いており、すべてパラメトリックです。パラメトリックプロパティとは、パラメトリックイベント（データをパラメータにバインドするイベント）によって形成されるトレースに関するプロパティです。ここで、パラメトリックプロパティはという形式を持ちます。ここで、は、汎用的な（インスタンス化されていない）パラメトリックイベントを参照する、適切な形式による仕様です。このようなパラメトリックプロパティの直感的な理解は、で表されるプロパティが、観測対象トレースにおいて（パラメトリックイベントを通じて）遭遇するすべてのパラメータインスタンスに対して成立しなければならないということです。以下の例はいずれも特定の実行時検証システムに固有のものではありませんが、パラメータのサポートは明らかに必要です。以下の例ではJava構文が前提とされているため、「==」は論理等価性、「==」は代入を表します。一部のメソッド（例えば、UnsafeEnumExample内）は、Java APIの一部ではないダミーメソッドであり、分かりやすさのために使用されています。 $\forall パラメータ:\varphi$ $\varphi$ $\varphi$ update()

次がある

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

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

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

安全でない列挙体

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

∀ ベクトルv、列挙体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 )

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

研究の課題と応用

ランタイム検証の研究のほとんどは、以下に挙げたトピックの 1 つ以上を扱っています。

実行時のオーバーヘッドの削減

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

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

プロパティの指定

あらゆる形式的アプローチにおける主要な実際的障害の一つは、ユーザーが仕様の読み方や書き方を知りたがらない、あるいは学びたくない、あるいは理解しようとしないことです。デッドロックやデータ競合など、仕様が暗黙的に規定されている場合もありますが、ほとんどの場合、仕様は作成する必要があります。特に実行時検証の文脈において、さらなる不便さとして、既存の仕様言語の多くは、意図された特性を捉えるのに十分な表現力を備えていないことが挙げられます。

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

実行モデルと予測分析

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

行動修正

テストや網羅的な検証とは異なり、ランタイム検証は、再構成、マイクロリセット、あるいはチューニングやステアリングと呼ばれるより微細な介入メカニズムを通じて、検出された違反からシステムを回復させることを可能とします。これらの手法をランタイム検証の厳格な枠組みの中で実装することは、新たな課題をもたらします。

アクションの仕様。 実行する変更は、ユーザーが無関係な実装の詳細を知る必要がない程度に抽象化された方法で指定する必要があります。さらに、システムの整合性を維持するために、そのような変更がいつ実行できるかを規定する必要があります。
介入効果についての推論。 介入によって状況が改善されるか、少なくとも悪化しないかを知ることが重要です。
アクションインターフェース。 監視のためのインストルメンテーションと同様に、システムがアクション呼び出しを受信できるようにする必要があります。呼び出しメカニズムは必然的にシステムの実装の詳細に依存します。しかし、仕様レベルでは、どのような状況でどのようなアクションをいつ適用すべきかを指定することにより、システムにフィードバックを提供するための宣言的な方法をユーザーに提供する必要があります。

参照

参考文献

^ Ezio BartocciとYliès Falcone編、『Lectures on Runtime Verification - Introductory and Advanced Topics』、Lecture Notes in Computer Scienceシリーズ（LNCS、第10457巻）の一部、またProgramming and Software Engineeringサブシリーズ（LNPSE、第10457巻）の一部、2018年。Lecture Notes in Computer Science. 第10457巻. 2018年. doi : 10.1007/978-3-319-75632-5 . ISBN 978-3-319-75631-8. S2CID 23246713 .
^ 「RV'01 - ランタイム検証に関する最初のワークショップ」 .ランタイム検証カンファレンス. 2001年7月23日. 2017年2月25日閲覧。
^ Klaus HavelundとGrigore Rosu. 2004. 「実行時検証ツールJava PathExplorerの概要」システム設計における形式手法、24(2)、2004年3月。
^ Stefan Savage、Michael Burrows、Greg Nelson、Patrick Sobalvarro、Thomas Anderson. 1997. Eraser: マルチスレッドプログラムのための動的データ競合検出器. ACM Trans. Comput. Syst. 15(4), 1997年11月, pp. 391-411.
^ Moonjoo Kim、Mahesh Viswanathan、Insup Lee、Hanêne Ben-Abdellah、Sampath Kannan、および Oleg Sokolsky、「時間的プロパティの正式に指定されたモニタリング」、ヨーロッパリアルタイムシステム会議の議事録、1999 年 6 月。
^ Insup Lee、Sampath Kannan、Moonjoo Kim、Oleg Sokolsky、Mahesh Viswanathan、「形式仕様に基づく実行時保証」、並列および分散処理技術およびアプリケーションに関する国際会議の議事録、1999 年 6 月。
^ Klaus Havelund、「実行時分析を使用した Java プログラムのモデルチェックのガイド」、第 7 回国際 SPIN ワークショップ、2000 年 8 月。
^ Klaus Havelund と Grigore Rosu、「書き換えを使用したプログラムの監視」、Automated Software Engineering (ASE'01)、2001 年 11 月。
^ ^a ^b Yliès Falcone、Klaus Havelund、Giles、「実行時検証に関するチュートリアル」、2013

[1] Ezio BartocciとYliès Falcone編、『Lectures on Runtime Verification - Introductory and Advanced Topics』、Lecture Notes in Computer Scienceシリーズ（LNCS、第10457巻）の一部、またProgramming and Software Engineeringサブシリーズ（LNPSE、第10457巻）の一部、2018年。Lecture Notes in Computer Science. 第10457巻. 2018年. doi : 10.1007/978-3-319-75632-5 . ISBN 978-3-319-75631-8. S2CID 23246713 .

[2] 「RV'01 - ランタイム検証に関する最初のワークショップ」 .ランタイム検証カンファレンス. 2001年7月23日. 2017年2月25日閲覧。

[Havelund2001Overview-3] Klaus HavelundとGrigore Rosu. 2004. 「実行時検証ツールJava PathExplorerの概要」システム設計における形式手法、24(2)、2004年3月。

[SavageTCS1997-4] Stefan Savage、Michael Burrows、Greg Nelson、Patrick Sobalvarro、Thomas Anderson. 1997. Eraser: マルチスレッドプログラムのための動的データ競合検出器. ACM Trans. Comput. Syst. 15(4), 1997年11月, pp. 391-411.

[5] Moonjoo Kim、Mahesh Viswanathan、Insup Lee、Hanêne Ben-Abdellah、Sampath Kannan、および Oleg Sokolsky、「時間的プロパティの正式に指定されたモニタリング」、ヨーロッパリアルタイムシステム会議の議事録、1999 年 6 月。

[6] Insup Lee、Sampath Kannan、Moonjoo Kim、Oleg Sokolsky、Mahesh Viswanathan、「形式仕様に基づく実行時保証」、並列および分散処理技術およびアプリケーションに関する国際会議の議事録、1999 年 6 月。

[HavelundSPIN2000-7] Klaus Havelund、「実行時分析を使用した Java プログラムのモデルチェックのガイド」、第 7 回国際 SPIN ワークショップ、2000 年 8 月。

[HavelundRosuASE2001-8] Klaus Havelund と Grigore Rosu、「書き換えを使用したプログラムの監視」、Automated Software Engineering (ASE'01)、2001 年 11 月。

[havelundRVTutorial2012-9] Yliès Falcone、Klaus Havelund、Giles、「実行時検証に関するチュートリアル」、2013

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]である。

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]