воспользоваться перебором всех возможных значений таймеров
T
route
,
T
hold
и
T
flush
.
Для описания верифицируемой модели выбран язык Promela [6]
как достаточно распространенный язык описания конечных моделей,
состоящих из конкурирующих процессов. Рассмотренный выше упро-
щенный вариант формализации протокола выбран в качестве исход-
ного. В частности, в модели хранятся и передаются маршруты только
до единственной сети, поскольку при полном переборе состояний си-
стемы значительно эффективнее оценивать маршруты до каждой сети
в отдельных экспериментах в силу их независимости.
Поскольку в протоколе RIP используется групповая рассылка и
простой транспортный протокол UDP, то в случае возникновения про-
блем в сети рассылающая сторона не предпринимает никаких специ-
альных действий. При поиске условий для полного устранения воз-
никновения маршрутных петель в качестве модели ошибок можно
рассмотреть следующую:
•
сеть может быть исправна (сообщение передается корректно) или
неисправна (сообщение теряется);
•
сеть изменяет свое состояние случайным образом перед переда-
чей по ней сообщения протокола RIP.
При необходимости можно ограничить максимальное число смены
состояний для каждой сети.
Результаты экспериментов.
Созданная модель была использована
для проведения экспериментов с рассмотренной сетью, состоящей из
четырех маршрутизаторов (см. рис. 2). Эта сеть известна тем, что в
ней существует вероятность возникновение циклов маршрутизации в
случае использования протокола RIP без таймера удержания.
В ходе вычислительных экспериментов проверялись все ком-
бинации из следующих возможных значений таймеров с учетом
ограничения
T
hold
6
T
flush
:
h
T
route
,
T
flush
,
T
hold
i 2 {
60
,
90
,
120
,
150
}
×
×{
120
,
150
,
180
,
210
,
240
}
×{
120
,
150
,
180
,
210
,
240
}
.
Для исследуемой
сети были рассмотрены две модели ошибок: в первом случае сети
x
,
y
,
z
изменяли свое состояние сколь угодно раз, во втором — не более
двух раз.
В таблице приведены только те комбинации значений таймеров, ко-
торые успешно прошли проверку и которые имеют минимальное зна-
чение
T
hold
для данных
T
flush
и
T
route
.
В обоих вариантах модели оши-
бок сети были получены одинаковые допустимые значения таймеров.
Как следует из таблицы, для рассматриваемой сети в случае совпадаю-
щих значений таймеров у всех маршрутизаторов для предотвращения
образования циклов должно выполняться условие
T
route
6
T
hold
2
.
В ре-
зультате применения созданного метода могут быть найдены условия,
108
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
