конечных моделей Promela. С помощью разработанной модели рассма-
тривается использование таймера удержания для минимальной топо-
логии, подверженной образованию маршрутных петель в случае при-
менения правила расщепленного горизонта.
Формальное описание протокола RIP.
На основании стандар-
тов [1, 2] и описания работы таймера удержания [4] можно пред-
ставить более формально подмножество протокола RIP с таймером
удержания. Следует отметить, что протоколы RIP2 [1] и RIPng [2]
различаются главным образом форматами передаваемых сообщений
и используемым сетевым протоколом, поэтому дальнейшее описание
применимо к ним обоим.
В протоколе RIP маршрутизатор не хранит никакой информации о
сетевой топологии, кроме таблицы маршрутизации и сведений о не-
посредственно подключенных к нему сетях. Пусть
L
=
{
0
,
1
, . . . ,
μ
}
—
множество всех возможных значений метрик маршрутов. Протокол
RIP использует метрику, равную числу маршрутизаторов до сети на-
значения. Значение метрики
μ
= 16
выбрано в качестве «бесконечно-
сти» и означает недоступность сети.
Введем обозначения:
R
—
множество всех маршрутизаторов ис-
пользующей RIP системы;
N
—
множество всех сетей системы;
E
r
N
—
множество сетей, подключенных к маршрутизатору
r
;
A
k
r
N
—
множество сетей, известных маршрутизатору
r
в момент
времени
t
k
.
Таблица маршрутизации маршрутизатора
r
2
R
в момент време-
ни
t
k
является отображением:
α
k
r
:
A
k
r
→
R
×
L
×
N.
В таблице маршрутизации запись о маршруте является упорядо-
ченной тройкой
α
k
r
(
n
)
=
h
h, l, s
i
:
n
2
A
k
r
cеть назначения данного маршрута;
h
2
R
cледующий маршрутизатор в маршруте;
l
2
L
pассчитанная метрика маршрута;
s
2
E
r
—
сеть, из которой была получена информация о данном
маршруте, eсли маршрутизатор не подключен к сети
n
непосредствен-
но (
n /
2
E
r
).
Метрика маршрута до сети не изменяется:
8
k
:
α
k
r
(
n
)
=
h
r,
1
,
n
i
,
если маршрутизатор подключен к сети непосредственно (
n
2
E
r
).
Для краткости условимся в дальнейшем опускать индекс
k
,
когда
он очевиден или неважен. В начальный момент времени маршрутиза-
тор располагает информацией только о подключенных к нему сетях
(
A
0
r
=
E
r
),
и начальная таблица маршрутизации содержит информа-
цию только о них:
8
n
2
E
r
:
α
0
r
(
n
)
=
h
r,
1
,
n
i
.
100
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
