モデル検査 - mrsekut-p

モデル検査

Model Checking

検査対象とするクリプキ構造において、与えられた論理式が成り立つかどうかを判定する

ソフトウェアが持つすべての動作を網羅的かつ自動的に探索することで性質を検証する

仕様中の論理式を内部的に木構造に変換し、全ての組み合わせを実行する。力技

時相論理を使って仕様を書く

組合わせ爆発すると停止しない

その場合は、Model Slicingなどを行って状態数を削減するなどの工夫をする

その際に本質を削ってしまうと意味がなくなるので難易度が高い

広い意味でのモデル検査

Refinement Checker

ツール

大域的モデル検査

global model checking

CTL等を用いたモデル検査

局所的モデル検査

local model checking

LTL等を用いたモデル検査

主が計算であるソフトウェア向けの手法

リアクティブシステム向けの手法

/mrsekut-book-4007305803/135 ((e) モデル検査)

/mrsekut-book-4883732584/023

http://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf

https://codezine.jp/article/detail/10164

https://www.principia-m.com/slides/formal_methods.pdf

https://github.com/Kuniwak/reversi-ios#教訓テスト容易設計からモデル検査容易設計へ