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