論理的に検証可能なモデルと特性を用いて、システムの仕様や設計を分析する手法。
Hillel Wayneが、システムを実装する前に設計上の欠陥を発見するための形式手法の原則を紹介する。特性の強さ、状態空間の探索、環境に関する仮定に焦点を当て、簡略化した並行性・障害・再試行の分析によって、高コストなエラーを早期に明らかにできることを例示する。