モデル検査

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

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

集合論や論理学などの数学的な表記法を使い、システムの仕様を曖昧さなく記述すること。自然言語の仕様に比べて解釈の違いが生じず、矛盾や漏れを機械的に検査できる。代表的な言語にVDMやZ記法がある。

形式手法の一つで、IBMウィーン研究所で生まれた仕様記述の方法とその言語（VDM-SL、VDM++）。データの型と不変条件、操作の事前条件・事後条件で仕様を厳密に書き、ツールによる構文・型の検査や、仕様を実行して確かめることができる。

集合論と一階述語論理に基づく形式仕様記述言語。システムの状態と操作を、宣言部と述語部からなるスキーマという単位で記述する。オックスフォード大学を中心に開発され、ISO/IEC 13568として標準化されている。

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

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

複数のプロセスやスレッドが互いに相手のリソース解放を待ち続け、すべての処理が停止する状態。相互排他、保持と待機、非横取り、循環待ちの4条件が同時に成立すると発生する。タイムアウトや資源の順序付けで回避する。