Разработка процессов синхронизации моделей и принципов проверки их корректности
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
.
Очевидно, что если исходным описанием процесса являются ка-
нонические процессные выражения, то переход от этих выражений к
графу переходов процесса и наоборот очевиден. Канонические про-
цессные выражения могут быть рекурсивными.
При помощи обозначенного теоретического аппарата можно
условно представить систему синхронизации моделей в виде про-
цесса, воспринимающего пару моделей
?s
и
?t
, результатом работы
которого является преобразованная определенным образом пара
моделей
!s
и
!t
(рис. 2). Внутренние состояния
b
процесса синхрони-
зации могут быть связаны с состоянием моделей или же с этапами
их обработки.
Наиболее важный класс задач, для решения которых предназна-
чена теория процессов, связан с проблемой верификации процессов.
Она заключается в построении формального доказательства того, что
анализируемый процесс обладает заданными свойствами.
