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