モデル検査

モデル検査(モデルけんさ、Model Checking)

対象システムを状態遷移系によりモデル化

状態遷移系の状態を網羅的に探索し、時相論理式が満たされるか検査

↓

複雑な状態遷移に絞って検証する

人手やテストでは検証しにくいものに対して検証する

ハードウェア設計

分散処理

並列処理

ありえる状態を全探索

下記はモデル検査に関連するもの

確認テスト

Q. モデル検査とは

Q. 時相論理

参考

関連