2 / 11
поведения сетевых экранов, а для описания типовых ошибок пове-
дения — язык модальной логики, на котором записываются наиболее
типичные требования (их выполнение позволяет исключить опреде-
ленные типы ошибок). Там же рассмотрены принципы создания логи-
ческих программ проверки правильности некорректностей, приведе-
ны примеры логических программ проверки правильности поведения
брандмауэров на языке VISUAL PROLOG.
Настоящая статья посвящена анализу корректности описания по-
ведения сетевых экранов по тем же принципам, которые изложены в
работе [1]. Однако в отличие от работы [1] здесь упор сделан на изло-
жение детальной методики перехода от процессных моделей описания
поведения сетевых экранов и условий их корректности, формулируе-
мых на языке модальной логики, к конкретным логическим програм-
мам, реализующим проверку корректности конфигурирования сетевых
экранов.
Сначала изложим принципы описания поведения сетевых экранов
процессными моделями в виде, который наиболее естественно позво-
лит перейти к представлению их в языке логического программирова-
ния VISUAL PROLOG.
Принципы анализа поведения процессных графов переходов на
языке логического программирования VISUAL PROLOG.
Тради-
ционное описание поведения сетевых экранов осуществляется списка-
ми управления доступом. Каждый список управления доступом состо-
ит из списка правил. Отдельное правило, также называемое условием
перехода, представляется парами ?
a
.!
a
или ?not
a
.!
e
, где ?
a
, ?not
a
—
восприятия, после получения которых сетевой экран совершает дей-
ствия (реакции) !
a
или !
e
. Правила обрабатываются в определенном
порядке, зависящем от вида списка управления доступом. Если имеем
восприятие ?
a
, то выполняется реакция !
a
и переход к реализации оче-
редного правила. Если имеем восприятие ?not
a
, то никакой реакции
нет (реакция является пустой и обозначается символом !
e
) и начина-
ется очередное правило.
В процессных графах переходов, описывающих поведение сетевых
экранов, каждое состояние процесса изображается кружком, внутрь
которого помещается символ этого состояния. Из каждого состояния
возможен переход только в два других состояния. Переходы из од-
ного состояния происходят в результате выполнения альтернативных
правил ?
a
.!
a
или ?not
a
.!
e
. Начальное состояние обозначается двойным
кружком, а финальное (если оно есть) — жирным кружком.
Переходы из состояния
b
i
в состояние
b
j
в результате выполнения
правила ?
a
.!
a
представляется тройкой (
b
i
,
?
a
.!
a,
b
j
), а из состояния
b
i
в состояние
b
j
в результате выполнения правила ?not
a
.!
e
– тройкой
(
b
i
,?not
a
.!
e
,
b
j
). Путем на графе, ведущем из состояния
b
i
в состояние
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 1 101