抽象モデル検査

コンピュータサイエンスと数学において、抽象化モデル検査は、モデルを単独で開発するには実際の表現が複雑すぎるシステムのためのモデル検査の一形態です。そのため、設計は縮小された「抽象」バージョンへと一種の変換を経ます。

変数の集合は、値の変化に応じて可視変数と不可視変数に分割されます。実状態空間は、可視変数のより小さな集合に要約されます。

ガロア連結

実空間と抽象空間はガロア連結である。つまり、抽象空間から要素を取り、それを具体化し、その具体化されたバージョンを抽象化すると、結果は元の状態と同じになる。一方、実空間から要素を取り、それを抽象化し、その抽象化されたバージョンを具体化すると、最終的な結果は元の状態のスーパーセットになる。

つまり、

${\displaystyle \eta}$ ( (抽象)) = 抽象 ( (実在)) 実在 ${\displaystyle \theta}$
${\displaystyle \theta}$ ${\displaystyle \eta}$ ${\displaystyle \supseteq }$

参照

• 抽象的解釈
• 自動定理証明
• 計算ツリーロジック
• 形式検証
• モデル検査ツールのリスト
• プログラム分析（コンピュータサイエンス）
• 静的コード分析

参考文献

• Edmund M. Clarke、Orna Grumberg、David E. Long (1994). 「モデル検査と抽象化」. ACM Transactions on Programming Languages and Systems . 16 (5): 1512– 1542. CiteSeerX  10.1.1.79.3022 . doi :10.1145/186025.186051. S2CID  207884170.