УДК 004.052.42
В. А. К р и щ е н к о
ИССЛЕДОВАНИЕ ТАЙМЕРА УДЕРЖАНИЯ
ПРИ ДИНАМИЧЕСКОЙ МАРШРУТИЗАЦИИ
НА ОСНОВЕ АЛГОРИТМА БЕЛЛМАНА–ФОРДА
В протоколе обмена маршрутной информацией RIP существует
проблема образования ложных маршрутов и маршрутных петель.
Сформулирована задача нахождения интервалов значений тайме-
ров протокола, позволяющих предотвратить образование марш-
рутных петель для заданной топологии сети. Предложен способ
решения поставленной задачи, включающий формальное описание
стандарта протокола RIP, построение по данному описанию и за-
данной топологии сети конечной модели и ее последующую фор-
мальную верификацию.
E-mail:
Ключевые слова
:
IP-маршрутизация, RIP, верификация протокола, тай-
мер удержания.
Группа протоколов обмена маршрутной информацией под общим
названием RIP [1, 2], достаточно широко используется в IP-сетях. Для
расчета метрики маршрутов все версии протокола RIP используют рас-
пределенный вариант алгоритма Беллмана-Форда [3], который может
приводить к возникновению ложных маршрутов и циклов маршрути-
зации.
Для уменьшения числа случаев, которые ведут к появлению таких
циклов, стандарты протокола RIP содержат ряд механизмов, напри-
мер таких как правило расщепленного горизонта [1]. В некоторые
широко применяемые реализации протокола RIP включен также до-
полнительный таймер удержания [4], не входящий в текущий стандарт
протокола. Существуют рекомендуемые значения таймеров протокола,
призванные уменьшить вероятность возникновения ложных циклов
маршрутизации в сети.
Представляет интерес вопрос, как для заданной топологии сети
найти такие значения таймеров, которые исключат возможность обра-
зования ложных циклов маршрутизации. Для создания модели прото-
кола RIP и ее применения для поиска значений таймера удержания,
предотвращающих циклы, если таковые существуют в исследуемой
топологии сети необходима формализации протокола. В работе [5]
дано формальное доказательство корректности протокола RIP и опи-
сана его модель на языке Promela [6], но рассмотрен лишь случай
отсутствия ошибок в сети, а предлагаемая модель не включала в себя
таймеры протокола.
На основе формальной модели протокола обмена маршрутной ин-
формацией RIPv2 создана модель протокола на языке верификации
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
99
