■モデル検査と形式証明 モデル検査と形式証明は形式検証技術の主要な技術である。一般に、型式証明は「安全性証明」と言われているが、具体的に「安全性証明」というものは存在せず、「デッドロックがない」とか「ブレーキを踏むと必ずブレーキランプが点灯…

ペアワイズ法は多くのバグを検出できるが、バグがないことを示すものではない。一般的な方法でバグ検出率が高い方法。こうした技術はシステムが一定の品質基準（網羅基準、または社内の品質基準）を満たすことを示すために用いるのに都合が良い。品質基準を…