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

Question

シンボリック実行とモデル チェック (モデル変換など) の違いは何ですか? それらの違いがわかりません。彼らは同じですか？！

Answer 1

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

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

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