ウォーターフォール型のオンプレシステム開発におけるのインフラ環境構築では、上流設計での検討漏れや担当者間の認識齟齬による設計ミス・設定誤りが原因で後工程で手戻りが発生し、工程遅延や人的リソースの追加によるコスト増が問題となる。本発表では、形式手法のモデル検査ツールであるAlloyを使用し、WEBサーバとファイアウォールを用いた通信についてモデル化を行い、設計時点での仕様の正当性を検証する方式を報告する。