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