シンボリック実行とモデルチェック

Question

シンボリック実行と（モデル変換などの）モデル検査の違いは何ですか？私はそれらの違いを理解していない。彼らは同じですか？！

Answer 1

モデルチェックでは、システムを有限状態マシンとしてエンコードし、そのFSMをモデルチェッカーと仕様に提供する必要があります。モデルチェッカーは、仕様がそのシステムで常に保持されていることを確認します。

シンボリック実行では、プログラムのみを提供し、シンボリック実行エンジンは、実行可能なすべてのパスを調べて、テスト入力またはアサーションを生成します。

単純な違いの例：並行性。モデル検査は、入力として提供されたFSMで指定されているためマルチスレッドシステムを処理できますが、シンボリック実行では複数のスレッドを処理できません。

Answer 2

モデルチェック： プログラムが仕様を満たしていることを正式に検証する方法。この仕様は、通常、「入力がxならば、プログラムのすべての実行（全体的に）にはy - holdでなければならない」というような一時的な論理式で与えられる（例えばEdward A Lee参照）。

記号モデル検査と明示的な状態検査の比較： プログラムは有限状態マシン（FSM）にすることができます。ここでは明示的な状態チェックで十分です。しかし、幸いなことに、モデルチェッカーはFSMの同時、確率的、リアルタイムのアプリケーションにも存在します。非常に大きな（無限の）状態数を持つシステムでの状態の爆発を防ぐために、記号モデル検査が使用されています。 記号モデル検査では、状態や入力などはシンボルとして、命題の公式（または状態の集合、集合演算など）として扱われます。モデルチェックを実行するためには到達可能性分析が必要であり、これを行うにはプログラムの遷移が記号的に実行されます。これらのチェッカーは、インストルメントされたネイティブコードの通常の実行を利用することはできません。

シンボリック実行： シンボリック実行中には、さまざまなエンコーディング方法があります。シンボリック実行の発明者が定義したように、モデル検査に非常に特化したものもあれば、モジュール式でスタンドアロンのシンボリック実行フレームワークで使用されるものもあります。

JPF、Javaにパスファインダー：モデルチェッカ、明示的な状態検査記号的実行フレームワークは、多くの場合、等

最後に、いくつかの例をテストするために使用可能であることが確認もシンボリックモデルのいくつかの要素（探索、検索）を使用し、入力：Javaバイトコード

SPF、シンボリックパスファインダー：シンボリック実行、JPF

JCBMCの拡張子：有界モデル検査、JPFの延長、SPF

XRTS：探査とシンボルIC実行、入力：CILバイトコード

IntelliTest：パラメータ化されたユニットテストがXRTSを使用しています

仕様エクスプローラ：モデルベーステストは、あなたの種類の助けをXRTS