モデル検査

システムの状態遷移を網羅的に探索し、満たすべき性質が成り立つかを機械的に検証する手法。テストでは見つけにくい並行処理の不具合を検出できる。

システムの全ての状態を網羅的に探索し、仕様を満たすかどうかを自動的に検証する形式手法。時相論理（CTL、LTL）で記述された性質の成否を判定する。デッドロックの検出、安全性・活性の検証に有効だが、状態爆発が課題。

システムを有限の状態遷移モデルとして表し、到達しうるすべての状態を網羅的に調べて、満たすべき性質（デッドロックが起きないなど）が成り立つかを自動的に検証する手法。テストでは再現しにくい並行処理の不具合を見つけられ、性質が成り立たない場合はそこに至る手順を反例として示す。

概念実証。新しい技術やアイデアの実現可能性を検証するために、小規模な試作やテストを行うこと。本格的な開発に着手する前に、技術的な実現性やビジネス上の効果を確認する。

数学的な論理や集合論に基づく形式言語を使って、ソフトウェアの仕様を厳密に記述すること。自然言語で書いた仕様のあいまいさや矛盾をなくし、仕様の正しさを機械的に検証できる。VDMやZ記法などがある。

形式仕様記述の手法の一つ。仕様記述言語（VDM-SLなど）で、扱うデータの型や不変条件、操作の事前条件と事後条件を厳密に記述し、仕様の検証や段階的な詳細化を行う。IBMのウィーン研究所で開発された。

価値実証のこと。新しいサービスや製品が実際のビジネスにおいて価値を提供できるかを検証すること。PoCが技術的実現可能性を確認するのに対し、PoVはビジネス上の価値や効果を実証する。

集合論と述語論理に基づいて仕様を厳密に記述する形式仕様記述言語。曖昧さのない仕様を作れる。

形式仕様記述と段階的詳細化によってソフトウェアを開発する手法。VDMToolsなどの支援ツールがある。