形式仕様記述 B-Method は仕様の無矛盾性を保証するが、要求仕様に対する妥当性の検証は困難である。仕様の不変条件が緩い場合、開発者が意図しない動作を許容する可能性がある。これに対し、開発者が作成した状態遷移図と形式仕様から導出した遷移図を比較する検証手法が提案されているが、状態遷移図の状態数が異なる場合の検証能力に課題があった。そこで本研究では、不変条件の緩みが状態数や遷移数の増加をもたらすことや操作の事前条件の厳しさによる遷移数の減少といった形式仕様から導出される状態遷移図の特性に着目し、複数の不変条件の誤りがある場合でも検証を行える誤り検出手法を提案する。