В.В. Девятков, Т.Н. Мьё
14
ending([put(end,enduac)]):-
preending([put(brps,byersp)]),thread([put(end,enduac)]).
3.2.
Построение по описанию на языке модальной логики раз-
дела GOAL.
В рамках настоящей работы не ставилось цели описания
на языке модальной логики всех свойств или требований, которым
должны удовлетворять процессные SIP-спецификации. Они могут
быть самыми различными, кроме того, они достаточно подробно пе-
речислены в литературных источниках [8]. Принципы использования
модальной логики для описания указанных свойств также хорошо
известны [9]. Например, если агент
UAC
,
начав
процесс
uac
имеет
хотя бы одну нить, при выполнении которой он обязательно перехо-
дит к процессу
inviting
, то это свойство можно выразить простой мо-
дальной формулой
◊
inviting
(
X
), где
inviting
(
X
) — предикат, который
становится истинным при выполнении процесса
inviting
в результате
выполнения нити
X.
Это означает, что должен существовать хотя бы
один путь на графе, показанном на рис. 2, ведущий из вершины
uac
в
вершину
inviting.
На языке ПРОЛОГ это можно выразить в виде сле-
дующего раздела
goal
(цели):
goal
uac([put(X1,Y1)]),thread([put(X2,Y2)]),inviting([put(X2,Y2)]).
3.3.
Проверка свойства.
Полученная по процессному описанию
логическая программа на языке ПРОЛОГ при заданной цели
uac([put(X1,Y1)]), thread([put(X2,Y2)]), inviting([put(X2,Y2)])
выдает следующий результат:
X1 = start, Y1 = startuac, X2 = reqc, Y2 = invite,
означающий, что существует нить
start
(
startuac
).
reqc
(
invite
), выпол-
нив которую процесс
UAC
переходит после завершения процесса
uac
к выполнению процесса
inviting.
Заключение.
В настоящей статье рассматривается проверка пра-
вильности и корректности (ошибок) SIP-спецификаций модели по-
следовательностных взаимодействующих агентов. В отличие от дру-
гих работ мы используем хорошо структурированный и более разви-
той вариант языка, основанный на моделях взаимодействующих
последовательностных процессов (π-исчислении), язык временнόй
модальной логики для описания требований к спецификациям и язык
логического программирования ПРОЛОГ для проверки правильности
спецификаций. В статье изложены принципы перехода от процесс-
ных моделей SIP-спецификаций к логической программе и от требо-
