Разработка процессов синхронизации моделей и принципов проверки их корректности
3
Этому посвящена и наша работа. Для создания механизмов син-
хронизации предлагается использовать процессные модели [12], вы-
разительные возможности которых широки, а теория хорошо развита,
что позволяет описывать сложные механизмы синхронизации. Свой-
ства механизмов синхронизации предлагается описывать формально
как свойства процессных моделей синхронизации на языке времен-
ной модальной логики. Процессные модели в дальнейшем будем
называть просто процессами. Процессы позволяют более четко и
полно классифицировать и описывать синхронизацию. Анализ
свойств синхронизации предлагается осуществлять методами логиче-
ского программирования, т. е. путем доказательства или вывода
свойств процессов синхронизации. Такой подход к проверке кор-
ректности синхронизации является гораздо более изящным, полным
и не имеет ограничений.
Процессные модели.
Аппарат теории процессов хорошо подхо-
дит для формального описания и анализа поведения систем, которые
состоят из нескольких взаимодействующих компонентов. Эти ком-
поненты работают параллельно, их взаимодействие происходит пу-
тем пересылки сигналов или сообщений от одних компонентов дру-
гим [13]. Такой системой является и система синхронизации моделей.
Рассмотрим элементы аппарата теории процессов, которые будут
применены в дальнейшем для описания ее поведения.
Каждый процесс имеет алфавит восприятий и реакций
1 2
,
, ...,
m
A a a
a
. Каждый символ
a
этого алфавита обозначает
некоторый объект, получаемый (воспринимаемый) процессом из
внешней среды (восприятие процесса), выдаваемый процессом во
внешнюю среду (внешняя реакция процесса), или объект, используе-
мый процессом для внутренних нужд (внутренняя реакция процесса).
Процессы действуют, воспринимая, порождая для внутреннего упо-
требления или выдавая наружу объекты с соответствующими имена-
ми. Для того чтобы различать типы действий, будем использовать
следующие обозначения:
?a
— восприятия,
!a
— внешние реакции,
b
— внутренние реакции.
Нитью
a
*
будем называть кортеж (конечный или бесконечный) дей-
ствий
*
0 1 2
2 1
...
.
m m
a a a a a a
Последовательность выполнения действий
нити слева направо называется выполнением нити процессом
P
. Симво-
лом
е
обозначается пустое действие. Нить, состоящая из единственного
пустого действия, называется пустой нитью. Процессом
P
называется
множество нитей
S
, которые он может выполнять. Поведением процесса
P
называется порядок выполнения множества этих нитей.
Введем обозначения:
?A
— множество всех восприятий некото-
рого процесса
P
, включая пустое восприятие
?e
;
!A
— конечное мно-
