---

　モデル検査とは、システムが取り得る全ての状態と全てのパスを網羅的に検査（テスト）できる技術です。システムを有限個の状態から成るモデルで表現すると、システムが満たすべき性質がモデル上で成り立つかどうかを、モデルが取り得る全ての状態とパス上で全自動かつ網羅的に検査できます。しらみつぶしに検査するので、性質が成り立たない極めて特別な状態やパス、すなわち不具合が1つでも存在すると、必ず発見することができます。このモデル検査を計算機（PC）上で自動で実行するソフトウェアがモデル検査ツールです。

　　=> モデル検査の説明資料（PDF 512KB）

　　=> モデル検査ツールについて（PDF 260KB）

　　=> モデル検査をステートマシン図に適用した事例（外部サイト）

　　=> モデル検査のユースケース（外部サイト）