Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
5
Так, для графа переходов, приведенного на рис. 1, канонически-
ми процессными выражениями, адекватными этому графу, будут
следующие:
1
1 4 1
1 4 2
2 1 1
2 3 2
3 2 1
3 2 2
4 1 2
4 3 1
1 1
2 2
3 3 4
?
?
?
?
?
? ,
?
?
?
!
!
!
b e
b b a
b b a
b b a
b b a
b b a
P b b a
b b a
b b a
a b
a b
a b b
= ⎛
⎞
= ⎜
⎟
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟
=
⎜
⎟⎟
= ⎝
⎠
где каждое внутреннее процессное выражение вида
?
i
j
k
b b a
=
задает
один переход из состояния
j
b
в состояние
i
b
в результате восприятия
?
k
a
. Выражение
!
i
j
a b
=
задает реакцию
!
i
a
после перехода процесса
в состояние
j
b
.
Если исходным описанием процесса являются канонические про-
цессные выражения, то переход от этих выражений к графу перехо-
дов процесса и наоборот очевиден. Канонические процессные выра-
жения могут быть рекурсивными.
2. Принципы процессного описания спецификаций.
В настоя-
щей статье, как и в работе [2], модели могут содержать множество
пользовательских агентов на стороне клиентов
UAC
и множество
пользовательских агентов на стороне серверов
UAS
. Взаимодействие
агентов осуществляется с помощью обмена сообщениями. Каждый
агент является последовательностным процессом, параллельно функ-
ционирующим с другими.
Как уже говорилось во введении, главной задачей моделирования
является автоматизация разработки правильных и корректных при-
ложений на основе использования языков, обеспечивающих высокий
уровень абстрагирования описания поведения от ненужных деталей,
например от деталей на уровне стеков протоколов.
При этом модель считаем
правильной
, если взаимодействие
агентов удовлетворяет определенным условиям, а под
корректно-
стью
подразумеваем удовлетворение каждого агента некоторым
формальным спецификациям, описывающим его индивидуальное
поведение.
В терминах нитей модель будет
правильной
, если каждый агент
в процессе взаимодействия с другими агентами выполняет только те
