8 / 11
один, пакеты могут не совпадать, пересекаться, быть подмножествами
один другого и т.п.
Язык временн´ой модальной логики не использует в явном виде со-
стояния и правила вывода. В рассматриваемом случае исходными для
анализа некорректностей сетевых экранов, во-первых, являются про-
цессные графы переходов, содержащие состояния в явном виде, во-
вторых, вывод осуществляется в языке логического программирования
с присущей ему стратегией вывода. При переходе от описания некор-
ректностей на язык логического программирования VISUAL PROLOG
состояния будут появляться в явном виде в качестве термов в фактах
и правилах.
На примере простейшего затенения рассмотрим формирование на
языке VISUAL PROLOG конкретной логической программы проверки
этой некорректности.
Процедура формирования логической программы проверки
некорректности.
Используем процессный граф переходов, приве-
денный на рис. 2,
а
. Предположим, что пакеты, именованные на этом
графе, являются следующими:
p
1
= udp 192.168.1.1,
p
2
= tcp 10.1.1.0,
p
3
= udp 192.168.1.1,
p
4
= tcp 10.1.1.26,
p
5
= tcp 10.1.1.64.
Пакет
p
1
затеняется пакетом
p
3
, поскольку они совпадают, но со-
гласно процессному графу (см. рис. 2,
а
) первый пакет должен быть
принят (
accept
), а второй — запрещен (
drop
).
В зависимости от структуры описания пакетов в разделе
domains
могут описываться различные типы функторов. В данном примере в
разделе
domains
объявим функтор
f
(
symbol, integer, integer, integer
,
integer
,
symbol
), элементами которого являются тип протокола, ip-
адрес, состоящий из четырех целых чисел, и действие, совершаемое
над ним. Здесь же введем список, содержащий описанные функторы.
В результате имеем
domains
f =f
(
symbol, integer, integer, integer
,
integer
,
symbol
)
list = f
∗
Раздел
predicates
включает в себя описание тех же предикатов, что
и логическая схема программы, приведенная ранее:
predicates
nondeterm transition
(
symbol, f , symbol
)
nondeterm accessible
(
symbol, list, symbol
)
В разделе
clauses
логической программы каждому переходу
(
b
i
,
?
a
.!
a,
b
j
) на процессном графе ?
a= udp 192.168.1.1
, !
a
= !
accept
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 1 107