Рассмотрена автоматизация поиска ошибок конфигурирования межсетевых экранов (брандмауэров) на основе принципов логического анализа. Как прави- ло, для описания поведения сетевых экранов использованы процессные модели, а для формулировки требований (свойств) некорректности — язык модальной логики. В настоящей статье детально изложена методика перехода от про- цессных моделей описания поведения сетевых экранов и условий их некоррект- ности, формулируемых на языке модальной логики, к конкретным логическим программам, реализующим проверку некорректности конфигурирования сете- вых экранов.