Исследование таймера удержания при динамической маршрутизации на основе алгоритма Беллмана-Форда
Опубликовано: 10.10.2012
Авторы: Крищенко В.А.
Опубликовано в выпуске: #1(1)/2012
DOI: 10.18698/2308-6033-2012-1-20
Раздел: Информационные технологии
В протоколе обмена маршрутной информацией RIP существует проблема образования ложных маршрутов и маршрутных петель. Сформулирована задача нахождения интервалов значений таймеров протокола, позволяющих предотвратить образование маршрутных петель для заданной топологии сети. Предложен способ решения поставленной задачи, включающий формальное описание стандарта протокола RIP, построение по данному описанию и заданной топологии сети конечной модели и ее последующую формальную верификацию.
Литература
[1] Malkin G. RFC 2453: RIP version 2. Internet Standard. 1998
[2] Malkin G., Minnear R. RFC 2080: RIPng for IPv6. Internet Standard. 1997
[3] Bellman R. On a Routing Problem // Quarterly of Applied Mathematics – 1958. – Vol. 16, No. 1. P. 87–90
[4] Bruno A., Kim J. CCDA Exam Certification Guide, 2nd Edition – Cisco Press, 2003. – 696 p.
[5] Bhargavan K., Gunter C.A., Obradovich D. RoutingInformation Protocol in HOL/SPIN // Proc. of the 13th Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs ’00). 2000. — P. 53–72
[6] Holzmann G. The SPIN Model Checker: Primer and Reference Manual. — Addison-Wesley, 2003. – 608 p.
[7] Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. – М.: МЦНМО, 2002. – 416 c.