Рис. 5. Отправка и получение сообщений протокола RIP
одном из двух состояний: данные либо передаются по сети корректно,
либо безвозвратно теряются. Сети из множества
N
\
N
error
работают
всегда корректно: таковыми, например, с целью уменьшения состоя-
ний системы могут считаться сети, подключенные только к одному
маршрутизатору. Каждая сеть
n
2
N
error
случайно изменяет или со-
храняет свое состояние каждый раз, когда какой-либо маршрутизатор
посылает сообщения, содержащие известные ему маршруты, своим
соседям или после отправки сообщения каждому соседу.
Реализация модели системы, использующей протокол RIP.
Сеть
из маршрутизаторов, использующих протокол RIP, можно рассматри-
вать как систему с конечным числом состояний, состоящую из не-
зависимых процессов. Поскольку в протоколе RIP отсутствует какая-
либо синхронизация между маршрутизаторами, то передачу сообще-
ний между ними можно моделировать с помощью асинхронных кана-
лов. Такая система является конечной, поскольку любая использую-
щая протокол RIP сеть не может иметь «диаметр», превышающий 15
маршрутизаторов. Таким образом, верифицируемая система является
распределенной системой с ограниченным числом процессов.
Метод верификации конечных моделей путем полного перебора со-
стояний [7] может быть применен для решения поставленной задачи
при зафиксированных значения таймеров
T
route
,
T
hold
и
T
flush
.
Для рас-
смотренного примера очевидным нарушения корректности системы
будет
α
b
(
v
)
=
h
c, l, x
i ∨
α
b
(
v
)
=
h
d, l, y
i
.
Интервалы всех таймеров протокола RIP выбираются с периодом,
равным значению таймера рассылки сообщение
T
send
= 30
с, при-
чем значения интервалов таймеров не превышают нескольких минут.
Поэтому, множество возможных значений любого таймера протоко-
ла содержит лишь несколько элементов, и при верификации можно
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
107
