Software-Defined Networking (SDN)における経路変更手順の設計次第では、パケットロスやセキュリティ上の脆弱性といった問題が発生する可能性がある。本研究では、これらのリスクを軽減し、信頼性を向上させるために、モデル検査を利用した経路変更手順生成手法を提案する。本手法では、一般的なモデル検査ツールであるNuSMVを利用し、生成される反例をもとに適切な経路変更手順を構築する。また、モデルの状態数の増加を抑制するために、モデルを「ブロック」と呼ばれる単位に事前に抽象化する手法を採用した。提案手法の有効性について確認するために、計算量及び実行時間の観点から評価を行った。