В.В. Девятков, Т.Н. Мьё
6
нити, которые разработчик считает допустимыми, и
корректной
, ес-
ли все эти нити одного агента удовлетворяют некоторым формаль-
ным спецификациям. В рамках настоящей статьи будем полагать, что
как свойства правильности, так и свойства корректности удастся
формально специфицировать и, следовательно, формально прове-
рить.
Пример простой процессной модели.
Для иллюстрации описа-
ния поведения простой процессной модели воспользуемся парой аген-
тов
UAC
и
UAS
, взятой из работы [2], и сначала опишем их поведение
на языке графов, а затем на языке процессных выражений. Агенты яв-
ляются параллельно выполняющимися последовательностными про-
цессами
UAC
и
UAS
, образующими в совокупности процесс
P UAC UAS
. Процессы
UAC
и
UAS
взаимодействуют по 10 каналам,
имена которых
ackc, brpc, irpc, reqc, sakc, acks, brps, irps, reqs, saks
.
Каналы
ackc, brpc, irpc, reqc, sakc
являются входными для процесса
UAС
и выходными для процесса
UAS
, а каналы
acks, brps, irps, reqs,
saks,
наоборот, — выходными для процесса
UAC
и входными для про-
цесса
UAS
. Полагаем, что каждый из процессов может выполнять
только шесть типов действий:
invite
,
invSucc
(любой из 2
nn
ответов на
действие
invite
),
invFail
(любой из 3
nn
—6
nn
ответов на действие
invite
),
ack
,
bye
,
byeRsp
(любой из 200 OK ответов на действие
buy
).
Если какое-либо действие
a
берется из канала с именем
c
, то
оно является
восприятием
и записывается как
c
?
a
, если же оно вы-
дается в канал
c
, то оно является
внешней реакцией
и записывается как
c
!
a
. Если действие
a
является внутренней реакцией, то оно записывает-
ся просто как
!
a
. Имена процессов начинаются с прописной буквы.
Граф переходов процесса
UAC
представлен на рис. 2, а процесса
UAS
— на рис. 3. Процессные выражения
UAC
и
UAS
приведены со-
ответственно на рис. 4 и 5.
Рассмотрим сначала принцип работы последовательностного
процесса
UAC
(см. рис. 2 и 4). Вследствие большей компактности
принцип работы процесса будем пояснять, используя процессные
выражения рис. 4. Граф переходов, изображенный на рис. 2, позволя-
ет наглядно следить за работой процесса.
До начала работы процесса
UAC
ни один из его последовательност-
ных подпроцессов не выполняется. Только один из подпроцессов может
выполняться в дальнейшем в любой текущий момент времени. Поэтому
будем говорить, что когда выполняется какой-либо подпроцесс, напри-
мер
Inviting
, то процесс
UAC
находится в состоянии
Inviting
.
После запуска на выполнение процесса
UAC
начинает выпол-
няться нить
UAC.reqc!invite
подпроцесса
Inviting
, в результате чего
в канал
reqc
выдается действие (внешняя реакция)
!invite
, нить
UAC.reqc!invite
закончит свое выполнение и начинает выполняться
